theory Detype_R

lemma placeNewObject_copyGlobalMapping_commute:
  "monad_commute
     (valid_arch_state' and pspace_distinct' and pspace_aligned' and
      page_directory_at' r and
      pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and
      K (objBitsKO (injectKOS val) + us < word_bits \<and>
         is_aligned ptr (objBitsKO (injectKOS val) + us)) )
     (placeNewObject ptr val us) (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_placeNewObject_commute]) apply (rule storePDE_placeNewObject_commute) apply wp apply (wp pspace_no_overlap'_lift | clarsimp)+ apply (rule placeNewObject_gets_globalPD_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 pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) (placeNewObject ptr val us) (copyGlobalMappings r) proof (prove)
goal (1 subgoal):
 1. monad_commute (valid_arch_state' and pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) (placeNewObject ptr val us) (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 (placeNewObject ptr val us) (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 pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) s \<Longrightarrow> ?P s proof (prove)
goal (4 subgoals):
 1. \<And>ra. monad_commute (?Q3 ra) (placeNewObject ptr val us) (mapM_x (\<lambda>index. getObject (ra + (index << pdeBits)) >>= storePDE (r + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1])
 2. monad_commute ?P3 (placeNewObject ptr val us) (gets (armKSGlobalPD \<circ> ksArchState))
 3. \<lbrace>?P'3\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?Q3\<rbrace>
 4. \<And>s. (valid_arch_state' and pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (5 subgoals):
 1. \<And>ra raa. monad_commute (?P7 ra raa) (placeNewObject ptr val us) (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 (placeNewObject ptr val us) (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 pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (6 subgoals):
 1. \<And>ra raa rb. monad_commute (?Q10 ra raa rb) (placeNewObject ptr val us) (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 pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and ?P'10 ra raa and K (id raa \<noteq> id x) and (pde_at' (ra + (x << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and ?P'10 ra x)\<rbrace> getObject (ra + (x << pdeBits)) >>= storePDE (r + (x << pdeBits)) \<lbrace>\<lambda>v. pde_at' (ra + (raa << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and ?P'10 ra raa\<rbrace>
 4. monad_commute ?P3 (placeNewObject ptr val us) (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 pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and ?P'10 r ra) s)\<rbrace>
 6. \<And>s. (valid_arch_state' and pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) 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)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits)\<rbrace>
 2. \<And>ra raa x. \<lbrace>pde_at' (ra + (raa << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and ?P'10 ra raa and K (id raa \<noteq> id x) and (pde_at' (ra + (x << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and ?P'10 ra x)\<rbrace> getObject (ra + (x << pdeBits)) >>= storePDE (r + (x << pdeBits)) \<lbrace>\<lambda>v. pde_at' (ra + (raa << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and ?P'10 ra raa\<rbrace>
 3. monad_commute ?P3 (placeNewObject ptr val us) (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 pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and ?P'10 r ra) s)\<rbrace>
 5. \<And>s. (valid_arch_state' and pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (4 subgoals):
 1. \<And>ra raa x. \<lbrace>pde_at' (ra + (raa << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (pde_at' (r + (raa << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits)) and K (id raa \<noteq> id x) and (pde_at' (ra + (x << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (pde_at' (r + (x << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits)))\<rbrace> getObject (ra + (x << pdeBits)) >>= storePDE (r + (x << pdeBits)) \<lbrace>\<lambda>v. pde_at' (ra + (raa << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (pde_at' (r + (raa << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits))\<rbrace>
 2. monad_commute ?P3 (placeNewObject ptr val us) (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 pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (pde_at' (r + (rb << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits))) s)\<rbrace>
 4. \<And>s. (valid_arch_state' and pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) s \<Longrightarrow> (?P3 and ?P'3) s proof (prove)
goal (3 subgoals):
 1. monad_commute ?P3 (placeNewObject ptr val us) (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 pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (pde_at' (r + (rb << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits))) s)\<rbrace>
 3. \<And>s. (valid_arch_state' and pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) 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 pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (pde_at' (r + (rb << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits))) s)\<rbrace>
 2. \<And>s. (valid_arch_state' and pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) s \<Longrightarrow> (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and ?P'3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_state' and pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us))) s \<Longrightarrow> (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) 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 pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (pde_at' (r + (ra << pdeBits)) and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits))) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ra. \<lbrakk>valid_arch_state' s; pspace_distinct' s; pspace_aligned' s; page_directory_at' r s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); 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>pspace_distinct' s; pspace_aligned' s; pspace_no_overlap' ptr ((case injectKOS val of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us) s; (case injectKOS val of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < word_bits; is_aligned ptr ((case injectKOS val of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); 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>pspace_distinct' s; pspace_aligned' s; pspace_no_overlap' ptr ((case injectKOS val of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us) s; (case injectKOS val of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < word_bits; is_aligned ptr ((case injectKOS val of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); 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!