theory Retype_R

lemma copyGlobalMappings_pde_mappings':
  "\<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
        and K (is_aligned pd pdBits)\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (simp add: copyGlobalMappings_def objBits_simps archObjSize_def) apply wp apply (rule_tac P="is_aligned globalPD pdBits \<and> is_aligned pd pdBits"
                in hoare_gen_asm) apply (rule mapM_x_wp[where S="{x. x < 2 ^ (pdBits - 2)}"]) apply (wp getObject_valid_pde_mapping' | simp)+ apply clarsimp apply (drule(1) is_aligned_add_helper[OF _ shiftl_less_t2n]) apply (simp add: pdBits_def pageBits_def pdeBits_def) apply (drule(1) is_aligned_add_helper[OF _ shiftl_less_t2n]) apply (simp add: pdBits_def pageBits_def pdeBits_def) apply (simp add: pdeBits_def) apply simp apply (clarsimp simp: pdBits_def pdeBits_def le_less_trans) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (is_aligned pd pdBits)\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)\<rbrace> do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>globalPD. \<lbrace>?B1 globalPD\<rbrace> mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?B1\<rbrace>
 3. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> \<lbrace>?P'2 globalPD\<rbrace> mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. ?P'2 globalPD and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 3. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>globalPD x. \<lbrakk>is_aligned globalPD pdBits \<and> is_aligned pd pdBits; x \<in> {x. x < 2 ^ (pdBits - 2)}\<rbrakk> \<Longrightarrow> \<lbrace>valid_pde_mappings'\<rbrace> getObject (globalPD + (x << pdeBits)) >>= storePDE (pd + (x << pdeBits)) \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>
 2. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<subseteq> {x. x < 2 ^ (pdBits - 2)}
 3. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 4. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>globalPD x s. \<lbrakk>is_aligned globalPD pdBits \<and> is_aligned pd pdBits; x < 2 ^ (pdBits - 2); valid_pde_mappings' s\<rbrakk> \<Longrightarrow> globalPD + (x << pdeBits) && mask pdBits = pd + (x << pdeBits) && mask pdBits
 2. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<subseteq> {x. x < 2 ^ (pdBits - 2)}
 3. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 4. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>globalPD x s. \<lbrakk>x < 2 ^ (pdBits - 2); valid_pde_mappings' s; is_aligned globalPD pdBits; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> globalPD + (x << pdeBits) && mask pdBits = pd + (x << pdeBits) && mask pdBits
 2. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<subseteq> {x. x < 2 ^ (pdBits - 2)}
 3. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 4. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>globalPD x s. \<lbrakk>x < 2 ^ (pdBits - 2); valid_pde_mappings' s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pdBits < LENGTH(32)
 2. \<And>globalPD x s. \<lbrakk>x < 2 ^ (pdBits - 2); valid_pde_mappings' s; is_aligned pd pdBits; globalPD + (x << 2) && mask pdBits = x << 2 \<and> globalPD + (x << 2) && ~~ mask pdBits = globalPD\<rbrakk> \<Longrightarrow> globalPD + (x << pdeBits) && mask pdBits = pd + (x << pdeBits) && mask pdBits
 3. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<subseteq> {x. x < 2 ^ (pdBits - 2)}
 4. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 5. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>globalPD x s. \<lbrakk>x < 2 ^ (pdBits - 2); valid_pde_mappings' s; is_aligned pd pdBits; globalPD + (x << 2) && mask pdBits = x << 2 \<and> globalPD + (x << 2) && ~~ mask pdBits = globalPD\<rbrakk> \<Longrightarrow> globalPD + (x << pdeBits) && mask pdBits = pd + (x << pdeBits) && mask pdBits
 2. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<subseteq> {x. x < 2 ^ (pdBits - 2)}
 3. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 4. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>globalPD x s. \<lbrakk>x < 2 ^ (pdBits - 2); valid_pde_mappings' s; globalPD + (x << 2) && mask pdBits = x << 2 \<and> globalPD + (x << 2) && ~~ mask pdBits = globalPD\<rbrakk> \<Longrightarrow> pdBits < LENGTH(32)
 2. \<And>globalPD x s. \<lbrakk>x < 2 ^ (pdBits - 2); valid_pde_mappings' s; globalPD + (x << 2) && mask pdBits = x << 2 \<and> globalPD + (x << 2) && ~~ mask pdBits = globalPD; pd + (x << 2) && mask pdBits = x << 2 \<and> pd + (x << 2) && ~~ mask pdBits = pd\<rbrakk> \<Longrightarrow> globalPD + (x << pdeBits) && mask pdBits = pd + (x << pdeBits) && mask pdBits
 3. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<subseteq> {x. x < 2 ^ (pdBits - 2)}
 4. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 5. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>globalPD x s. \<lbrakk>x < 2 ^ (pdBits - 2); valid_pde_mappings' s; globalPD + (x << 2) && mask pdBits = x << 2 \<and> globalPD + (x << 2) && ~~ mask pdBits = globalPD; pd + (x << 2) && mask pdBits = x << 2 \<and> pd + (x << 2) && ~~ mask pdBits = pd\<rbrakk> \<Longrightarrow> globalPD + (x << pdeBits) && mask pdBits = pd + (x << pdeBits) && mask pdBits
 2. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<subseteq> {x. x < 2 ^ (pdBits - 2)}
 3. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 4. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<subseteq> {x. x < 2 ^ (pdBits - 2)}
 2. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 3. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>globalPD. is_aligned globalPD pdBits \<and> is_aligned pd pdBits \<Longrightarrow> {x. pptrBase >> 20 \<le> x \<and> x \<le> 2 ^ (pdBits - pdeBits) - 1} \<subseteq> {x. x < 2 ^ (pdBits - 2)}
 2. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 3. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD. valid_pde_mappings' and K (is_aligned globalPD pdBits \<and> is_aligned pd pdBits)\<rbrace>
 2. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and (\<lambda>y. is_aligned pd pdBits)) s \<Longrightarrow> (valid_pde_mappings' and K (is_aligned ((armKSGlobalPD \<circ> ksArchState) s) pdBits \<and> is_aligned pd pdBits)) s proof (prove)
goal:
No subgoals!