kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_AI

lemma set_aobject_cur_tcb [wp]:
  "set_object ptr (ArchObj obj)  \<lbrace>\<lambda>s. cur_tcb s\<rbrace>" unfolding cur_tcb_def by (rule hoare_lift_Pf [where f=cur_thread]) wp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (cur_thread s) s\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. tcb_at (cur_thread s) s\<rbrace>
theory KHeap_AI

lemma set_aobject_valid_idle[wp]:
  "set_object ptr (ArchObj obj) \<lbrace>\<lambda>s. valid_idle s\<rbrace>" by (wpsimp wp: valid_idle_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_. valid_idle\<rbrace>
theory KHeap_AI

lemma set_aobject_reply_caps[wp]:
  "set_object ptr (ArchObj obj) \<lbrace>\<lambda>s. valid_reply_caps s\<rbrace>" by (wp valid_reply_caps_st_cte_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>
theory KHeap_AI

lemma set_aobject_reply_masters[wp]:
  "set_object ptr (ArchObj obj) \<lbrace>valid_reply_masters\<rbrace>" by (wp valid_reply_masters_cte_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>
theory SubMonad_AI

lemma submonad_do_machine_op:
  "submonad machine_state (machine_state_update \<circ> K) \<top> do_machine_op" apply unfold_locales apply (clarsimp simp: ext stateAssert_def do_machine_op_def o_def gets_def
                             get_def bind_def return_def submonad_fn_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. submonad machine_state (machine_state_update \<circ> K) (\<lambda>_. True) do_machine_op proof (prove)
goal (5 subgoals):
 1. \<forall>x s. True \<longrightarrow> machine_state ((machine_state_update \<circ> K) x s) = x
 2. \<forall>x y s. (machine_state_update \<circ> K) x ((machine_state_update \<circ> K) y s) = (machine_state_update \<circ> K) x s
 3. \<forall>s. (machine_state_update \<circ> K) (machine_state s) s = s
 4. \<And>s x. True = True
 5. do_machine_op = submonad_fn machine_state (machine_state_update \<circ> K) (\<lambda>_. True) proof (prove)
goal:
No subgoals!
theory SubMonad_AI

lemma submonad_args_pspace:
  "submonad_args kheap (kheap_update o (\<lambda>x _. x)) \<top>" by (simp add: submonad_args_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. submonad_args kheap (kheap_update \<circ> (\<lambda>x _. x)) (\<lambda>_. True)
theory SubMonad_AI

lemma assert_get_thread_do_machine_op_comm:
  "empty_fail m' \<Longrightarrow>
   do x \<leftarrow> gets_the (get_tcb t); y \<leftarrow> do_machine_op m'; n x y od =
   do y \<leftarrow> do_machine_op m'; x \<leftarrow> gets_the (get_tcb t); n x y od" apply (rule submonad_comm2 [OF _ _ submonad_do_machine_op]) apply (rule submonad_args_pspace) apply (rule assert_get_tcb_pspace) apply (simp add: empty_fail_cond)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m' \<Longrightarrow> do x <- gets_the (get_tcb t);
do_machine_op m' >>= n x
od = do y <- do_machine_op m';
x <- gets_the (get_tcb t);
n x y
od proof (prove)
goal (7 subgoals):
 1. empty_fail m' \<Longrightarrow> submonad_args ?f ?r ?g
 2. empty_fail m' \<Longrightarrow> gets_the (get_tcb t) = submonad_fn ?f ?r ?g ?im
 3. \<And>s x x'. empty_fail m' \<Longrightarrow> ?r x ((machine_state_update \<circ> K) x' s) = (machine_state_update \<circ> K) x' (?r x s)
 4. \<And>s x. empty_fail m' \<Longrightarrow> ?g ((machine_state_update \<circ> K) x s) = ?g s
 5. \<And>s x. empty_fail m' \<Longrightarrow> True = True
 6. empty_fail m' \<Longrightarrow> empty_fail ?im
 7. empty_fail m' \<Longrightarrow> empty_fail m' proof (prove)
goal (6 subgoals):
 1. empty_fail m' \<Longrightarrow> gets_the (get_tcb t) = submonad_fn kheap (kheap_update \<circ> (\<lambda>x _. x)) (\<lambda>_. True) ?im
 2. \<And>s x x'. empty_fail m' \<Longrightarrow> (kheap_update \<circ> (\<lambda>x _. x)) x ((machine_state_update \<circ> K) x' s) = (machine_state_update \<circ> K) x' ((kheap_update \<circ> (\<lambda>x _. x)) x s)
 3. \<And>s x. empty_fail m' \<Longrightarrow> True = True
 4. \<And>s x. empty_fail m' \<Longrightarrow> True = True
 5. empty_fail m' \<Longrightarrow> empty_fail ?im
 6. empty_fail m' \<Longrightarrow> empty_fail m' proof (prove)
goal (5 subgoals):
 1. \<And>s x x'. empty_fail m' \<Longrightarrow> (kheap_update \<circ> (\<lambda>x _. x)) x ((machine_state_update \<circ> K) x' s) = (machine_state_update \<circ> K) x' ((kheap_update \<circ> (\<lambda>x _. x)) x s)
 2. \<And>s x. empty_fail m' \<Longrightarrow> True = True
 3. \<And>s x. empty_fail m' \<Longrightarrow> True = True
 4. empty_fail m' \<Longrightarrow> empty_fail (gets (\<lambda>a. case a t of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | Some _ \<Rightarrow> None) >>= assert_opt)
 5. empty_fail m' \<Longrightarrow> empty_fail m' proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma get_asid_pool_wp [wp]:
  "\<lbrace>\<lambda>s. \<forall>pool. ko_at (ArchObj (ASIDPool pool)) p s \<longrightarrow> Q pool s\<rbrace>
  get_asid_pool p
  \<lbrace>Q\<rbrace>" apply (simp add: get_asid_pool_def get_object_def) apply (wp|wpc)+ apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pool. ako_at (ASIDPool pool) p s \<longrightarrow> Q pool s\<rbrace> get_asid_pool p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pool. ako_at (ASIDPool pool) p s \<longrightarrow> Q pool s\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
case kobj of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>pool. ako_at (ASIDPool pool) p s \<longrightarrow> Q pool s \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> (\<forall>x xa. the (kheap s p) = CNode x xa \<longrightarrow> True) \<and> (\<forall>x. the (kheap s p) = TCB x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s p) = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s p) = Notification x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s p) = ArchObj x \<longrightarrow> (\<forall>xa. x = ASIDPool xa \<longrightarrow> Q xa s) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> True) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> True) \<and> (\<forall>xa xb. x = DataPage xa xb \<longrightarrow> True)) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_asid_pool_typ_at [wp]:
  "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace>" apply (simp add: set_asid_pool_def set_object_def get_object_def) apply wp including unfold_objects by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh ptr = Some y);
return (the (kh ptr))
od;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool pool)));
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (ASIDPool pool))\<rparr>)
od \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (typ_at T p s) \<Longrightarrow> (\<exists>y. kheap s ptr = Some y) \<longrightarrow> a_type (the (kheap s ptr)) = a_type (ArchObj (ASIDPool pool)) \<longrightarrow> P (typ_at T p (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (ASIDPool pool))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. P (typ_at T p s) \<Longrightarrow> (\<exists>y. kheap s ptr = Some y) \<longrightarrow> a_type (the (kheap s ptr)) = a_type (ArchObj (ASIDPool pool)) \<longrightarrow> P (typ_at T p (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (ASIDPool pool))\<rparr>))
theory ArchAcc_AI

lemma get_pd_wp [wp]:
  "\<lbrace>\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) p s \<longrightarrow> Q pd s\<rbrace> get_pd p \<lbrace>Q\<rbrace>" unfolding get_pd_def including unfold_objects by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q pd s\<rbrace> get_pd p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q pd s\<rbrace> do kobj <- get_object p;
case kobj of ArchObj (PageDirectory pd) \<Rightarrow> return pd | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q pd s\<rbrace> do kobj <- get_object p;
case kobj of ArchObj (PageDirectory pd) \<Rightarrow> return pd | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>Q\<rbrace>
theory ArchAcc_AI

lemma get_pde_wp:
  "\<lbrace>\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s \<longrightarrow>
        Q (pd (ucast (p && mask pd_bits >> 2))) s\<rbrace>
  get_pde p
  \<lbrace>Q\<rbrace>" by (simp add: get_pde_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> Q (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) s\<rbrace> get_pde p \<lbrace>Q\<rbrace>
theory ArchAcc_AI

lemma get_pde_inv [wp]: "get_pde p \<lbrace>P\<rbrace>" by (wpsimp wp: get_pde_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_pde p \<lbrace>\<lambda>_. P\<rbrace>
theory ArchAcc_AI

lemma store_pde_typ_at [wp]:
  "store_pde ptr pde \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def get_object_def) apply (wpsimp simp: obj_at_def a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do pd <- get_pd (ptr && ~~ mask pd_bits);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh (ptr && ~~ mask pd_bits) = Some y);
return (the (kh (ptr && ~~ mask pd_bits)))
od;
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))\<rparr>)
od \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma get_pt_wp [wp]:
  "\<lbrace>\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) p s \<longrightarrow> Q pt s\<rbrace> get_pt p \<lbrace>Q\<rbrace>" apply (simp add: get_pt_def get_object_def) apply (wpsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q pt s\<rbrace> get_pt p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> Q pt s\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
case kobj of ArchObj (PageTable pt) \<Rightarrow> return pt | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma get_pte_wp:
  "\<lbrace>\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~mask pt_bits) s \<longrightarrow>
        Q (pt (ucast (p && mask pt_bits >> 2))) s\<rbrace>
  get_pte p
  \<lbrace>Q\<rbrace>" by (simp add: get_pte_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) s\<rbrace> get_pte p \<lbrace>Q\<rbrace>
theory ArchAcc_AI

lemma get_pte_inv [wp]:
  "\<lbrace>P\<rbrace> get_pte p \<lbrace>\<lambda>_. P\<rbrace>" by (wpsimp wp: get_pte_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_pte p \<lbrace>\<lambda>_. P\<rbrace>
theory ArchAcc_AI

lemma lookup_pt_slot_inv:
  "lookup_pt_slot pd vptr \<lbrace>P\<rbrace>" apply (simp add: lookup_pt_slot_def) apply (wp get_pde_wp|wpc)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> P s \<and> True) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb \<longrightarrow> P s) \<and> (\<forall>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> P s \<and> True) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> P s \<and> True) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma lookup_pt_slot_inv_any:
  "\<lbrace>\<lambda>s. \<forall>x. Q x s\<rbrace> lookup_pt_slot pd vptr \<lbrace>Q\<rbrace>,-"
  "\<lbrace>E\<rbrace> lookup_pt_slot pd vptr -, \<lbrace>\<lambda>ft. E\<rbrace>" apply (simp_all add: lookup_pt_slot_def) apply (wpsimp wp: get_pde_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. Q x s\<rbrace> lookup_pt_slot pd vptr \<lbrace>Q\<rbrace>, - &&& \<lbrace>E\<rbrace> lookup_pt_slot pd vptr -, \<lbrace>\<lambda>ft. E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>x. Q x s\<rbrace> liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)) \<lbrace>Q\<rbrace>, -
 2. \<lbrace>E\<rbrace> liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)) -, \<lbrace>\<lambda>ft. E\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_cte_wp_at:
  "set_pt ptr val \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace>" apply (simp add: set_pt_def) apply (wpsimp wp: set_object_wp_strong) apply (subst cte_wp_at_after_update') apply (clarsimp simp: a_type_def obj_at_def split: if_splits kernel_object.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> set_pt ptr val \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> set_object ptr (ArchObj (PageTable val)) \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (cte_wp_at P' p s); ko_at ko ptr s; a_type (ArchObj (PageTable val)) = a_type ko\<rbrakk> \<Longrightarrow> P (cte_wp_at P' p (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageTable val))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>P (cte_wp_at P' p s); ko_at ko ptr s; a_type (ArchObj (PageTable val)) = a_type ko\<rbrakk> \<Longrightarrow> obj_at (same_caps (ArchObj (PageTable val))) ptr s
 2. \<And>s ko. \<lbrakk>P (cte_wp_at P' p s); ko_at ko ptr s; a_type (ArchObj (PageTable val)) = a_type ko\<rbrakk> \<Longrightarrow> P (cte_wp_at P' p s) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_cte_wp_at:
  "set_pd ptr val \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace>" apply (simp add: set_pd_def) apply (wpsimp wp: set_object_wp_strong) apply (subst cte_wp_at_after_update') including unfold_objects apply (clarsimp simp: a_type_def split: if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> set_pd ptr val \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> set_object ptr (ArchObj (PageDirectory val)) \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (cte_wp_at P' p s); ko_at ko ptr s; a_type (ArchObj (PageDirectory val)) = a_type ko\<rbrakk> \<Longrightarrow> P (cte_wp_at P' p (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageDirectory val))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>P (cte_wp_at P' p s); ko_at ko ptr s; a_type (ArchObj (PageDirectory val)) = a_type ko\<rbrakk> \<Longrightarrow> obj_at (same_caps (ArchObj (PageDirectory val))) ptr s
 2. \<And>s ko. \<lbrakk>P (cte_wp_at P' p s); ko_at ko ptr s; a_type (ArchObj (PageDirectory val)) = a_type ko\<rbrakk> \<Longrightarrow> P (cte_wp_at P' p s) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>P (cte_wp_at P' p s); ko_at ko ptr s; a_type (ArchObj (PageDirectory val)) = a_type ko\<rbrakk> \<Longrightarrow> obj_at (same_caps (ArchObj (PageDirectory val))) ptr s
 2. \<And>s ko. \<lbrakk>P (cte_wp_at P' p s); ko_at ko ptr s; a_type (ArchObj (PageDirectory val)) = a_type ko\<rbrakk> \<Longrightarrow> P (cte_wp_at P' p s) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_asid_pool_cte_wp_at:
  "set_asid_pool ptr val \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace>" apply (simp add: set_asid_pool_def) including unfold_objects_asm by (wpsimp wp: set_object_wp_strong
           simp: a_type_def cte_wp_at_after_update'
          split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> set_asid_pool ptr val \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> set_object ptr (ArchObj (ASIDPool val)) \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> set_object ptr (ArchObj (ASIDPool val)) \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace>
theory ArchAcc_AI

lemma set_pt_pred_tcb_at[wp]:
  "set_pt ptr val \<lbrace>pred_tcb_at proj P t\<rbrace>" apply (simp add: set_pt_def) apply (wpsimp wp: set_object_wp_strong) apply (clarsimp simp: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> set_pt ptr val \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> set_object ptr (ArchObj (PageTable val)) \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>pred_tcb_at proj P t s; ko_at ko ptr s; a_type (ArchObj (PageTable val)) = a_type ko\<rbrakk> \<Longrightarrow> pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageTable val))\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_pred_tcb_at[wp]:
  "set_pd ptr val \<lbrace>pred_tcb_at proj P t\<rbrace>" apply (simp add: set_pd_def) apply (wpsimp wp: set_object_wp_strong) apply (clarsimp simp: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> set_pd ptr val \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> set_object ptr (ArchObj (PageDirectory val)) \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>pred_tcb_at proj P t s; ko_at ko ptr s; a_type (ArchObj (PageDirectory val)) = a_type ko\<rbrakk> \<Longrightarrow> pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageDirectory val))\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_asid_pool_pred_tcb_at[wp]:
  "set_asid_pool ptr val \<lbrace>pred_tcb_at proj P t\<rbrace>" apply (subst set_asid_pool_def) by (wpsimp wp: set_object_wp_strong
           simp: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> set_asid_pool ptr val \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> set_object ptr (ArchObj (ASIDPool val)) \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>
theory ArchAcc_AI

lemma mask_pd_bits_inner_beauty:
  "is_aligned p 2 \<Longrightarrow>
  (p && ~~ mask pd_bits) + (ucast ((ucast (p && mask pd_bits >> 2))::12 word) << 2) = (p::word32)" by (rule mask_split_aligned; simp add: pd_bits_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 2 \<Longrightarrow> (p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) << 2) = p
theory ArchAcc_AI

lemma more_pd_inner_beauty:
  fixes x :: "12 word"
  fixes p :: word32
  assumes x: "x \<noteq> ucast (p && mask pd_bits >> 2)"
  shows "(p && ~~ mask pd_bits) + (ucast x << 2) = p \<Longrightarrow> False" by (rule mask_split_aligned_neg[OF _ _ x]; simp add: pd_bits_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2) = p \<Longrightarrow> False
theory ArchAcc_AI

lemma mask_pt_bits_inner_beauty:
  "is_aligned p 2 \<Longrightarrow>
  (p && ~~ mask pt_bits) + (ucast ((ucast (p && mask pt_bits >> 2))::word8) << 2) = (p::word32)" by (rule mask_split_aligned; simp add: pt_bits_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 2 \<Longrightarrow> (p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) << 2) = p
theory ArchAcc_AI

lemma more_pt_inner_beauty:
  fixes x :: "word8"
  fixes p :: word32
  assumes x: "x \<noteq> ucast (p && mask pt_bits >> 2)"
  shows "(p && ~~ mask pt_bits) + (ucast x << 2) = p \<Longrightarrow> False" by (rule mask_split_aligned_neg[OF _ _ x]; simp add: pt_bits_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) x << 2) = p \<Longrightarrow> False
theory ArchAcc_AI

lemma set_pd_aligned [wp]:
  "set_pd base pd \<lbrace>pspace_aligned\<rbrace>" by (wpsimp simp: set_pd_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_pd base pd \<lbrace>\<lambda>_. pspace_aligned\<rbrace>