theory ArchRetype_AI

lemma mapM_x_store_pde_eq_kernel_mappings_restr:
  "pd \<in> S \<and> is_aligned pd pd_bits \<and> is_aligned pd' pd_bits
        \<and> set xs \<subseteq> {..< 2 ^ (pd_bits - 2)}
     \<Longrightarrow>
   \<lbrace>\<lambda>s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- S) \<rparr>)\<rbrace>
     mapM_x (\<lambda>idx. get_pde (pd' + (idx << 2)) >>=
                   store_pde (pd + (idx << 2))) xs
   \<lbrace>\<lambda>rv s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- S) \<rparr>)
               \<and> (\<forall>x \<in> set xs.
                    (\<exists>pdv pdv'. ko_at (ArchObj (PageDirectory pdv)) pd s
                      \<and> ko_at (ArchObj (PageDirectory pdv')) pd' s
                      \<and> pdv (ucast x) = pdv' (ucast x)))\<rbrace>" apply (induct xs rule: rev_induct, simp_all add: mapM_x_Nil mapM_x_append mapM_x_singleton) apply (erule hoare_seq_ext[rotated]) apply (simp add: store_pde_def set_pd_def set_object_def cong: bind_cong) apply (wp get_object_wp get_pde_wp) apply (clarsimp simp: obj_at_def split del: if_split) apply (frule shiftl_less_t2n) apply (simp add: pd_bits_def pageBits_def) apply (simp add: is_aligned_add_helper split del: if_split) apply (cut_tac x=x and n=2 in shiftl_shiftr_id) apply (simp add: word_bits_def) apply (simp add: word_bits_def pd_bits_def pageBits_def) apply (erule order_less_le_trans, simp) apply (clarsimp simp: fun_upd_def[symmetric] is_aligned_add_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pd \<in> S \<and> is_aligned pd pd_bits \<and> is_aligned pd' pd_bits \<and> set xs \<subseteq> {..<2 ^ (pd_bits - 2)} \<Longrightarrow> \<lbrace>\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)\<rbrace> mapM_x (\<lambda>idx. get_pde (pd' + (idx << 2)) >>= store_pde (pd + (idx << 2))) xs \<lbrace>\<lambda>rv s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<and> (\<forall>x\<in>set xs. \<exists>pdv pdv'. ako_at (PageDirectory pdv) pd s \<and> ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrace>\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)\<rbrace> mapM_x (\<lambda>idx. get_pde (pd' + (idx << 2)) >>= store_pde (pd + (idx << 2))) xs \<lbrace>\<lambda>rv s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<and> (\<forall>x\<in>set xs. \<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)))\<rbrace>; pd \<in> S \<and> is_aligned pd pd_bits \<and> is_aligned pd' pd_bits \<and> x < 2 ^ (pd_bits - 2) \<and> set xs \<subseteq> {..<2 ^ (pd_bits - 2)}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)\<rbrace> do xa <- mapM_x (\<lambda>idx. get_pde (pd' + (idx << 2)) >>= store_pde (pd + (idx << 2))) xs;
get_pde (pd' + (x << 2)) >>= store_pde (pd + (x << 2))
od \<lbrace>\<lambda>rv s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<and> (\<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))) \<and> (\<forall>x\<in>set xs. \<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. pd \<in> S \<and> is_aligned pd pd_bits \<and> is_aligned pd' pd_bits \<and> x < 2 ^ (pd_bits - 2) \<and> set xs \<subseteq> {..<2 ^ (pd_bits - 2)} \<Longrightarrow> \<lbrace>\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<and> (\<forall>x\<in>set xs. \<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)))\<rbrace> get_pde (pd' + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>rv s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<and> (\<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))) \<and> (\<forall>x\<in>set xs. \<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. pd \<in> S \<and> is_aligned pd pd_bits \<and> is_aligned pd' pd_bits \<and> x < 2 ^ (pd_bits - 2) \<and> set xs \<subseteq> {..<2 ^ (pd_bits - 2)} \<Longrightarrow> \<lbrace>\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<and> (\<forall>x\<in>set xs. \<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)))\<rbrace> do v <- get_pde (pd' + (x << 2));
va <- get_pd (pd + (x << 2) && ~~ mask pd_bits);
vb <- get_object (pd + (x << 2) && ~~ mask pd_bits);
a <- assert (a_type vb = a_type (ArchObj (PageDirectory (va(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := v)))));
vb <- get;
put (vb\<lparr>kheap := (kheap vb)(pd + (x << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (va(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := v))))\<rparr>)
od \<lbrace>\<lambda>rv s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<and> (\<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))) \<and> (\<forall>x\<in>set xs. \<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>pd \<in> S \<and> is_aligned pd pd_bits \<and> is_aligned pd' pd_bits \<and> x < 2 ^ (pd_bits - 2) \<and> set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<and> (\<forall>x\<in>set xs. \<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)))\<rbrakk> \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (pd' + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> (\<forall>pdb. ako_at (PageDirectory pdb) (pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)))))) \<longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (kheap s)(pd + (x << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)))))), kheap := kheap (s\<lparr>kheap := (kheap s)(pd + (x << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2))))))\<rparr>) |` (- S)\<rparr>) \<and> (\<exists>pdv. ako_at (PageDirectory pdv) pd (s\<lparr>kheap := (kheap s)(pd + (x << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2))))))\<rparr>) \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' (s\<lparr>kheap := (kheap s)(pd + (x << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2))))))\<rparr>) \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))) \<and> (\<forall>xa\<in>set xs. \<exists>pdv. ako_at (PageDirectory pdv) pd (s\<lparr>kheap := (kheap s)(pd + (x << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2))))))\<rparr>) \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') pd' (s\<lparr>kheap := (kheap s)(pd + (x << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2))))))\<rparr>) \<and> pdv (UCAST(32 \<rightarrow> 12) xa) = pdv' (UCAST(32 \<rightarrow> 12) xa))))) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. \<exists>pdv. kheap s pd = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. kheap s pd' = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s (pd' + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2))))))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (\<lambda>a. if a = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s a) |` (- S)\<rparr>) \<and> (\<exists>pdv. (if pd = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd) = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. (if pd' = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))) \<and> (\<forall>xa\<in>set xs. \<exists>pdv. (if pd = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd) = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. (if pd' = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) xa) = pdv' (UCAST(32 \<rightarrow> 12) xa))) proof (prove)
goal (2 subgoals):
 1. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. \<exists>pdv. kheap s pd = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. kheap s pd' = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s (pd' + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2))))))\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 2. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. \<exists>pdv. kheap s pd = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. kheap s pd' = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s (pd' + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)))))); x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (\<lambda>a. if a = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s a) |` (- S)\<rparr>) \<and> (\<exists>pdv. (if pd = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd) = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. (if pd' = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))) \<and> (\<forall>xa\<in>set xs. \<exists>pdv. (if pd = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd) = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. (if pd' = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) xa) = pdv' (UCAST(32 \<rightarrow> 12) xa))) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. \<exists>pdv. kheap s pd = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. kheap s pd' = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s (pd' + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); kheap s (pd + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)))))); x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (\<lambda>a. if a = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s a) |` (- S)\<rparr>) \<and> (\<exists>pdv. (if pd = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd) = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. (if pd' = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))) \<and> (\<forall>xa\<in>set xs. \<exists>pdv. (if pd = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd) = Some (ArchObj (PageDirectory pdv)) \<and> (\<exists>pdv'. (if pd' = pd + (x << 2) && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> pdv (UCAST(32 \<rightarrow> 12) xa) = pdv' (UCAST(32 \<rightarrow> 12) xa))) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. pdaa (UCAST(32 \<rightarrow> 12) x) = pda (UCAST(32 \<rightarrow> 12) x); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s pd' = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))))); x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (\<lambda>a. if a = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s a) |` (- S)\<rparr>) \<and> (\<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) x = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) x)) = pdv' (UCAST(32 \<rightarrow> 12) x)) \<and> (\<forall>xa\<in>set xs. \<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) xa = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) xa)) = pdv' (UCAST(32 \<rightarrow> 12) xa)) proof (prove)
goal (3 subgoals):
 1. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. pdaa (UCAST(32 \<rightarrow> 12) x) = pda (UCAST(32 \<rightarrow> 12) x); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s pd' = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))))); x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. pdaa (UCAST(32 \<rightarrow> 12) x) = pda (UCAST(32 \<rightarrow> 12) x); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s pd' = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))))); x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - 2)
 3. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. pdaa (UCAST(32 \<rightarrow> 12) x) = pda (UCAST(32 \<rightarrow> 12) x); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s pd' = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))))); x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (\<lambda>a. if a = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s a) |` (- S)\<rparr>) \<and> (\<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) x = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) x)) = pdv' (UCAST(32 \<rightarrow> 12) x)) \<and> (\<forall>xa\<in>set xs. \<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) xa = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) xa)) = pdv' (UCAST(32 \<rightarrow> 12) xa)) proof (prove)
goal (2 subgoals):
 1. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. pdaa (UCAST(32 \<rightarrow> 12) x) = pda (UCAST(32 \<rightarrow> 12) x); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s pd' = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))))); x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - 2)
 2. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. pdaa (UCAST(32 \<rightarrow> 12) x) = pda (UCAST(32 \<rightarrow> 12) x); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s pd' = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))))); x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (\<lambda>a. if a = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s a) |` (- S)\<rparr>) \<and> (\<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) x = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) x)) = pdv' (UCAST(32 \<rightarrow> 12) x)) \<and> (\<forall>xa\<in>set xs. \<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) xa = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) xa)) = pdv' (UCAST(32 \<rightarrow> 12) xa)) proof (prove)
goal (2 subgoals):
 1. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. pdaa (UCAST(32 \<rightarrow> 12) x) = pda (UCAST(32 \<rightarrow> 12) x); is_aligned pd 14; is_aligned pd' 14; x < 0x1000; set xs \<subseteq> {..<0x1000}; kheap s pd' = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))))); x << 2 < 0x4000\<rbrakk> \<Longrightarrow> x < 0x40000000
 2. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. pdaa (UCAST(32 \<rightarrow> 12) x) = pda (UCAST(32 \<rightarrow> 12) x); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s pd' = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))))); x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (\<lambda>a. if a = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s a) |` (- S)\<rparr>) \<and> (\<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) x = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) x)) = pdv' (UCAST(32 \<rightarrow> 12) x)) \<and> (\<forall>xa\<in>set xs. \<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) xa = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) xa)) = pdv' (UCAST(32 \<rightarrow> 12) xa)) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s pda pdaa. \<lbrakk>pd \<in> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>); \<forall>x\<in>set xs. pdaa (UCAST(32 \<rightarrow> 12) x) = pda (UCAST(32 \<rightarrow> 12) x); is_aligned pd pd_bits; is_aligned pd' pd_bits; x < 2 ^ (pd_bits - 2); set xs \<subseteq> {..<2 ^ (pd_bits - 2)}; kheap s pd' = Some (ArchObj (PageDirectory pda)); kheap s pd = Some (ArchObj (PageDirectory pdaa)); a_type (ArchObj (PageDirectory pdaa)) = a_type (ArchObj (PageDirectory (pdaa(UCAST(32 \<rightarrow> 12) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))))); x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (\<lambda>a. if a = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s a) |` (- S)\<rparr>) \<and> (\<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) x = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) x)) = pdv' (UCAST(32 \<rightarrow> 12) x)) \<and> (\<forall>xa\<in>set xs. \<exists>pdv'. (if pd' = pd then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa a))) else kheap s pd') = Some (ArchObj (PageDirectory pdv')) \<and> (if UCAST(32 \<rightarrow> 12) xa = UCAST(32 \<rightarrow> 12) (x << 2 >> 2) then pda (UCAST(32 \<rightarrow> 12) (pd' + (x << 2) && mask pd_bits >> 2)) else pdaa (UCAST(32 \<rightarrow> 12) xa)) = pdv' (UCAST(32 \<rightarrow> 12) xa)) proof (prove)
goal:
No subgoals!