theory Detype_R

lemma doMachineOp_copyGlobalMapping_commute:
  "monad_commute (valid_arch_state' and page_directory_at' r)
                 (doMachineOp f) (copyGlobalMappings r)" apply (clarsimp simp:copyGlobalMappings_def) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split) apply (rule mapM_x_commute[where f = id]) apply (rule monad_commute_split[OF _ getPDE_doMachineOp_commute]) apply (rule doMachineOp_storePDE_commute) apply wp+ apply clarsimp apply (rule doMachineOp_ksArchState_commute) apply wp apply clarsimp apply (clarsimp simp: valid_arch_state'_def page_directory_at'_def objBits_simps archObjSize_def
                        pdBits_def pageBits_def) apply (drule le_m1_iff_lt[where x = "(0x1000::word32)",simplified,THEN iffD1]) apply (clarsimp simp: pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (valid_arch_state' and page_directory_at' r) (doMachineOp f) (copyGlobalMappings r) proof (prove)
goal (1 subgoal):
 1. monad_commute (valid_arch_state' and page_directory_at' r) (doMachineOp f) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (r + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P (doMachineOp f) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (r + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od)
 2. \<And>s. (valid_arch_state' and page_directory_at' r) s \<Longrightarrow> ?P s proof (prove)
goal (4 subgoals):
 1. \<And>ra. monad_commute (?Q3 ra) (doMachineOp f) (mapM_x (\<lambda>index. getObject (ra + (index << pdeBits)) >>= storePDE (r + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1])
 2. monad_commute ?P3 (doMachineOp f) (gets (armKSGlobalPD \<circ> ksArchState))
 3. \<lbrace>?P'3\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?Q3\<rbrace>
 4. \<And>s. (valid_arch_state' and page_directory_at' r) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (5 subgoals):
 1. \<And>ra raa. monad_commute (?P7 ra raa) (doMachineOp f) (getObject (ra + (raa << pdeBits)) >>= storePDE (r + (raa << pdeBits)))
 2. \<And>ra raa x. \<lbrace>?P7 ra raa and K (id raa \<noteq> id x) and ?P7 ra x\<rbrace> getObject (ra + (x << pdeBits)) >>= storePDE (r + (x << pdeBits)) \<lbrace>\<lambda>v. ?P7 ra raa\<rbrace>
 3. monad_commute ?P3 (doMachineOp f) (gets (armKSGlobalPD \<circ> ksArchState))
 4. \<lbrace>?P'3\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>r s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>ra\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. ?P7 r ra s)\<rbrace>
 5. \<And>s. (valid_arch_state' and page_directory_at' r) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (6 subgoals):
 1. \<And>ra raa rb. monad_commute (?Q10 ra raa rb) (doMachineOp f) (storePDE (r + (raa << pdeBits)) rb)
 2. \<And>r ra. \<lbrace>?P'10 r ra\<rbrace> getObject (r + (ra << pdeBits)) \<lbrace>?Q10 r ra\<rbrace>
 3. \<And>ra raa x. \<lbrace>pde_at' (ra + (raa << pdeBits)) and ?P'10 ra raa and K (id raa \<noteq> id x) and (pde_at' (ra + (x << pdeBits)) and ?P'10 ra x)\<rbrace> getObject (ra + (x << pdeBits)) >>= storePDE (r + (x << pdeBits)) \<lbrace>\<lambda>v. pde_at' (ra + (raa << pdeBits)) and ?P'10 ra raa\<rbrace>
 4. monad_commute ?P3 (doMachineOp f) (gets (armKSGlobalPD \<circ> ksArchState))
 5. \<lbrace>?P'3\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>r s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>ra\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. (pde_at' (r + (ra << pdeBits)) and ?P'10 r ra) s)\<rbrace>
 6. \<And>s. (valid_arch_state' and page_directory_at' r) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (5 subgoals):
 1. \<And>ra raa. \<lbrace>?P'10 ra raa\<rbrace> getObject (ra + (raa << pdeBits)) \<lbrace>\<lambda>ra. pde_at' (r + (raa << pdeBits))\<rbrace>
 2. \<And>ra raa x. \<lbrace>pde_at' (ra + (raa << pdeBits)) and ?P'10 ra raa and K (id raa \<noteq> id x) and (pde_at' (ra + (x << pdeBits)) and ?P'10 ra x)\<rbrace> getObject (ra + (x << pdeBits)) >>= storePDE (r + (x << pdeBits)) \<lbrace>\<lambda>v. pde_at' (ra + (raa << pdeBits)) and ?P'10 ra raa\<rbrace>
 3. monad_commute ?P3 (doMachineOp f) (gets (armKSGlobalPD \<circ> ksArchState))
 4. \<lbrace>?P'3\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>r s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>ra\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. (pde_at' (r + (ra << pdeBits)) and ?P'10 r ra) s)\<rbrace>
 5. \<And>s. (valid_arch_state' and page_directory_at' r) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (4 subgoals):
 1. \<And>ra raa x s. (pde_at' (ra + (raa << pdeBits)) and pde_at' (r + (raa << pdeBits)) and K (id raa \<noteq> id x) and (pde_at' (ra + (x << pdeBits)) and pde_at' (r + (x << pdeBits)))) s \<Longrightarrow> pde_at' (ra + (raa << pdeBits)) s \<and> pde_at' (r + (raa << pdeBits)) s
 2. monad_commute ?P3 (doMachineOp f) (gets (armKSGlobalPD \<circ> ksArchState))
 3. \<lbrace>?P'3\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>ra s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>rb\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. (pde_at' (ra + (rb << pdeBits)) and pde_at' (r + (rb << pdeBits))) s)\<rbrace>
 4. \<And>s. (valid_arch_state' and page_directory_at' r) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (3 subgoals):
 1. monad_commute ?P3 (doMachineOp f) (gets (armKSGlobalPD \<circ> ksArchState))
 2. \<lbrace>?P'3\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>ra s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>rb\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. (pde_at' (ra + (rb << pdeBits)) and pde_at' (r + (rb << pdeBits))) s)\<rbrace>
 3. \<And>s. (valid_arch_state' and page_directory_at' r) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'3\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>ra s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>rb\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. (pde_at' (ra + (rb << pdeBits)) and pde_at' (r + (rb << pdeBits))) s)\<rbrace>
 2. \<And>s. (valid_arch_state' and page_directory_at' r) s \<Longrightarrow> ((\<lambda>_. True) and ?P'3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_state' and page_directory_at' r) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>ra\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. (pde_at' ((armKSGlobalPD \<circ> ksArchState) s + (ra << pdeBits)) and pde_at' (r + (ra << pdeBits))) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ra. \<lbrakk>valid_arch_state' s; page_directory_at' r s; pptrBase >> 20 \<le> ra; ra \<le> 2 ^ (pdBits - pdeBits) - 1\<rbrakk> \<Longrightarrow> pde_at' (armKSGlobalPD (ksArchState s) + (ra << pdeBits)) s \<and> pde_at' (r + (ra << pdeBits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s ra. \<lbrakk>pptrBase >> 20 \<le> ra; ra \<le> 0xFFF; valid_asid_table' (armKSASIDTable (ksArchState s)) s; is_aligned r (12 + pdeBits); \<forall>y<0x1000. pde_at' (r + (y << 2)) s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); \<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s))\<rbrakk> \<Longrightarrow> pde_at' (armKSGlobalPD (ksArchState s) + (ra << pdeBits)) s \<and> pde_at' (r + (ra << pdeBits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s ra. \<lbrakk>pptrBase >> 20 \<le> ra; valid_asid_table' (armKSASIDTable (ksArchState s)) s; is_aligned r (12 + pdeBits); \<forall>y<0x1000. pde_at' (r + (y << 2)) s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); \<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); ra < 0x1000\<rbrakk> \<Longrightarrow> pde_at' (armKSGlobalPD (ksArchState s) + (ra << pdeBits)) s \<and> pde_at' (r + (ra << pdeBits)) s proof (prove)
goal:
No subgoals!