theory ArchUntyped_AI

lemma store_pde_weaken:
  "\<lbrace>\<lambda>s. page_directory_at (p && ~~ mask pd_bits) s \<longrightarrow> P s\<rbrace> store_pde p e \<lbrace>Q\<rbrace> =
   \<lbrace>P\<rbrace> store_pde p e \<lbrace>Q\<rbrace>" apply (rule iffI) apply (simp add: valid_def) apply (erule allEI) apply clarsimp apply (simp add: valid_def) apply (erule allEI) apply clarsimp apply (rule use_valid, assumption) apply (simp add: store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def a_type_simps) apply (drule bspec, assumption) apply (simp add: simpler_store_pde_def obj_at_def fun_upd_def
            split: Structures_A.kernel_object.splits arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s\<rbrace> store_pde p e \<lbrace>Q\<rbrace> = \<lbrace>P\<rbrace> store_pde p e \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s\<rbrace> store_pde p e \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> store_pde p e \<lbrace>Q\<rbrace>
 2. \<lbrace>P\<rbrace> store_pde p e \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s\<rbrace> store_pde p e \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>s. (typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s) \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa) \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa)
 2. \<lbrace>P\<rbrace> store_pde p e \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s\<rbrace> store_pde p e \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s) \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa) \<Longrightarrow> P s \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa)
 2. \<lbrace>P\<rbrace> store_pde p e \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s\<rbrace> store_pde p e \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> store_pde p e \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s\<rbrace> store_pde p e \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa) \<Longrightarrow> \<forall>s. (typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s) \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa) \<Longrightarrow> (typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s) \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>P s \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa); typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s; ((), b) \<in> fst (store_pde p e s)\<rbrakk> \<Longrightarrow> Q () b proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>P s \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa); typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s; ((), b) \<in> fst (store_pde p e s)\<rbrakk> \<Longrightarrow> \<lbrace>?P14 s b\<rbrace> store_pde p e \<lbrace>Q\<rbrace>
 2. \<And>s b. \<lbrakk>P s \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa); typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s; ((), b) \<in> fst (store_pde p e s)\<rbrakk> \<Longrightarrow> ?P14 s b s proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>P s \<longrightarrow> (\<forall>x\<in>fst ((do pd <- get_pd (p && ~~ mask pd_bits);
kobj <- get_object (p && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := e)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := e))))\<rparr>)
od) s). case x of (x, xa) \<Rightarrow> Q x xa); typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s; ((), b) \<in> fst ((do pd <- get_pd (p && ~~ mask pd_bits);
kobj <- get_object (p && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := e)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := e))))\<rparr>)
od) s)\<rbrakk> \<Longrightarrow> \<lbrace>?P14 s b\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
kobj <- get_object (p && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := e)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := e))))\<rparr>)
od \<lbrace>Q\<rbrace>
 2. \<And>s b. \<lbrakk>P s \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa); typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s; ((), b) \<in> fst (store_pde p e s)\<rbrakk> \<Longrightarrow> ?P14 s b s proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>P s \<longrightarrow> (\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa); typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<longrightarrow> P s; ((), b) \<in> fst (store_pde p e s)\<rbrakk> \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := e)))) \<longrightarrow> Q () (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := e))))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s b pd. \<lbrakk>\<forall>x\<in>fst (store_pde p e s). case x of (x, xa) \<Rightarrow> Q x xa; P s; ((), b) \<in> fst (store_pde p e s); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> Q () (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then e else pd a))) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b pd. \<lbrakk>P s; ((), b) \<in> fst (store_pde p e s); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); case ((), b) of (x, xa) \<Rightarrow> Q x xa\<rbrakk> \<Longrightarrow> Q () (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then e else pd a))) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!