theory ArchVSpaceEntries_AI

lemma mapM_x_store_pte_updates:
  "\<forall>x \<in> set xs. f x && ~~ mask pt_bits = p \<Longrightarrow>
   \<lbrace>\<lambda>s. (\<not> page_table_at p s \<longrightarrow> Q s) \<and>
        (\<forall>pt. ko_at (ArchObj (PageTable pt)) p s
           \<longrightarrow> Q (s \<lparr> kheap := (kheap s) (p := Some (ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x.
         ucast (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))) \<rparr>))\<rbrace>
     mapM_x (\<lambda>x. store_pte (f x) pte) xs
   \<lbrace>\<lambda>_. Q\<rbrace>" apply (induct xs) apply (simp add: mapM_x_Nil) apply wp apply (clarsimp simp: obj_at_def fun_upd_idem) apply (simp add: mapM_x_Cons) apply (rule hoare_seq_ext, assumption) apply (thin_tac "valid P f Q" for P f Q) apply (simp add: store_pte_def set_pt_def set_object_def) apply (wp get_pt_wp get_object_wp) apply (clarsimp simp: obj_at_def a_type_simps) apply (erule rsubst[where P=Q]) apply (rule abstract_state.fold_congs[OF refl refl]) apply (rule ext, clarsimp) apply (rule ext, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. f x && ~~ mask pt_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) xs \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set []. f x && ~~ mask pt_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set [] then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) [] \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pt_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pt_bits = p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set (a # xs) then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<rbrace> return () \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pt_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pt_bits = p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set (a # xs) then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) \<Longrightarrow> Q s
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pt_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pt_bits = p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set (a # xs) then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pt_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pt_bits = p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set (a # xs) then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pt_bits = p)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> do y <- store_pte (f a) pte;
mapM_x (\<lambda>x. store_pte (f x) pte) xs
od \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pte (f x) pte) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pt_bits = p)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> store_pte (f a) pte \<lbrace>\<lambda>y s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. f a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pt_bits = p) \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> store_pte (f a) pte \<lbrace>\<lambda>y s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. f a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pt_bits = p) \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> do pt <- get_pt p;
kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) := pte)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) := pte))))\<rparr>)
od \<lbrace>\<lambda>y s. (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>f a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pt_bits = p); (\<not> typ_at (AArch APageTable) p s \<longrightarrow> Q s) \<and> (\<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>))\<rbrakk> \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> (\<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) := pte)))) \<longrightarrow> (\<not> typ_at (AArch APageTable) p (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) := pte))))\<rparr>) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) := pte))))\<rparr>)) \<and> (\<forall>pta. ako_at (PageTable pta) p (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) := pte))))\<rparr>) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) := pte)))), kheap := (kheap (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) := pte))))\<rparr>))(p \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pta y)))\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pt. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pt_bits = f a && ~~ mask pt_bits; p = f a && ~~ mask pt_bits; Q (s\<lparr>kheap := (kheap s)(f a && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (\<lambda>y. if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr>); kheap s (f a && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> Q (s\<lparr>kheap := (\<lambda>b. if b = f a && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>b. if b = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) then pte else pt b))) else kheap s b)(f a && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) then pte else pt y)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pt. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pt_bits = f a && ~~ mask pt_bits; p = f a && ~~ mask pt_bits; kheap s (f a && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(f a && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (\<lambda>y. if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))\<rparr> = s\<lparr>kheap := (\<lambda>b. if b = f a && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>b. if b = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) then pte else pt b))) else kheap s b)(f a && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) then pte else pt y)))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pt v. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pt_bits = f a && ~~ mask pt_bits; p = f a && ~~ mask pt_bits; kheap s (f a && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); kheap s = v\<rbrakk> \<Longrightarrow> (kheap s)(f a && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (\<lambda>y. if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y))) = (\<lambda>b. if b = f a && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>b. if b = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) then pte else pt b))) else kheap s b)(f a && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) then pte else pt y))) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pt. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pt_bits = f a && ~~ mask pt_bits; p = f a && ~~ mask pt_bits; kheap s (f a && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (\<lambda>y. if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else pt y) = (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (f x && mask pt_bits >> 2)) ` set xs then pte else if y = UCAST(32 \<rightarrow> 8) (f a && mask pt_bits >> 2) then pte else pt y) proof (prove)
goal:
No subgoals!