kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAcc_AI

lemma arch_derive_cap_valid_cap:
  "\<lbrace>valid_cap (cap.ArchObjectCap arch_cap)\<rbrace>
  arch_derive_cap arch_cap
  \<lbrace>valid_cap\<rbrace>, -" apply(simp add: arch_derive_cap_def) apply(cases arch_cap, simp_all add: arch_derive_cap_def o_def) apply(rule hoare_pre, wpc?, wp+;
            clarsimp simp add: cap_aligned_def valid_cap_def split: option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap (ArchObjectCap arch_cap)\<rbrace> arch_derive_cap arch_cap \<lbrace>valid_cap\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap (ArchObjectCap arch_cap)\<rbrace> case arch_cap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap arch_cap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap arch_cap) | _ \<Rightarrow> returnOk (ArchObjectCap arch_cap) \<lbrace>valid_cap\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. arch_cap = ASIDPoolCap x11 x12 \<Longrightarrow> \<lbrace>valid_cap (ArchObjectCap (ASIDPoolCap x11 x12))\<rbrace> returnOk (ArchObjectCap (ASIDPoolCap x11 x12)) \<lbrace>valid_cap\<rbrace>, -
 2. arch_cap = ASIDControlCap \<Longrightarrow> \<lbrace>valid_cap (ArchObjectCap ASIDControlCap)\<rbrace> returnOk (ArchObjectCap ASIDControlCap) \<lbrace>valid_cap\<rbrace>, -
 3. \<And>x31 x32 x33 x34 x35. arch_cap = PageCap x31 x32 x33 x34 x35 \<Longrightarrow> \<lbrace>valid_cap (ArchObjectCap (PageCap x31 x32 x33 x34 x35))\<rbrace> returnOk (ArchObjectCap (PageCap x31 x32 x33 x34 None)) \<lbrace>valid_cap\<rbrace>, -
 4. \<And>x41 x42. arch_cap = PageTableCap x41 x42 \<Longrightarrow> \<lbrace>valid_cap (ArchObjectCap (PageTableCap x41 x42))\<rbrace> case x42 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (PageTableCap x41 x42)) \<lbrace>valid_cap\<rbrace>, -
 5. \<And>x51 x52. arch_cap = PageDirectoryCap x51 x52 \<Longrightarrow> \<lbrace>valid_cap (ArchObjectCap (PageDirectoryCap x51 x52))\<rbrace> case x52 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (PageDirectoryCap x51 x52)) \<lbrace>valid_cap\<rbrace>, - proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma arch_derive_cap_inv:
  "arch_derive_cap arch_cap \<lbrace>P\<rbrace>" apply(simp add: arch_derive_cap_def, cases arch_cap, simp_all) apply(rule hoare_pre, wpc?, wp+; simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> arch_derive_cap arch_cap \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. arch_cap = ASIDPoolCap x11 x12 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (ArchObjectCap (ASIDPoolCap x11 x12)) \<lbrace>\<lambda>_. P\<rbrace>
 2. arch_cap = ASIDControlCap \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (ArchObjectCap ASIDControlCap) \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>x31 x32 x33 x34 x35. arch_cap = PageCap x31 x32 x33 x34 x35 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (ArchObjectCap (PageCap x31 x32 x33 x34 None)) \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>x41 x42. arch_cap = PageTableCap x41 x42 \<Longrightarrow> \<lbrace>P\<rbrace> case x42 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (PageTableCap x41 x42)) \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>x51 x52. arch_cap = PageDirectoryCap x51 x52 \<Longrightarrow> \<lbrace>P\<rbrace> case x52 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (PageDirectoryCap x51 x52)) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma ucast_mask_asid_low_bits [simp]:
  "ucast ((asid::word32) && mask asid_low_bits) = (ucast asid :: 10 word)" by (word_eqI_solve simp: asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits) = UCAST(32 \<rightarrow> 10) asid
theory ArchAcc_AI

lemma ucast_ucast_asid_high_bits [simp]:
  "ucast (ucast (asid_high_bits_of asid)::word32) = asid_high_bits_of asid" by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 7) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = asid_high_bits_of asid
theory ArchAcc_AI

lemma mask_asid_low_bits_ucast_ucast:
  "((asid::word32) && mask asid_low_bits) = ucast (ucast asid :: 10 word)" by (word_eqI_solve simp: asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)
theory ArchAcc_AI

lemma set_asid_pool_cur [wp]:
  "set_asid_pool p a \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace>" unfolding set_asid_pool_def by (wpsimp wp: get_object_wp)

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

lemma set_asid_pool_cur_tcb [wp]:
  "set_asid_pool p a \<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_asid_pool p a \<lbrace>\<lambda>_. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (cur_thread s) s\<rbrace> set_asid_pool p a \<lbrace>\<lambda>_ s. tcb_at (cur_thread s) s\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_valid_arch [wp]:
  "set_asid_pool p a \<lbrace>valid_arch_state\<rbrace>" by (rule valid_arch_state_lift) (wp set_asid_pool_typ_at)+

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

lemma p_le_0xF_helper:
  "((p::word32) \<le> 0xF) = (\<forall>n'\<ge>4. n'< word_bits \<longrightarrow> \<not> p !! n')" apply (subst upper_bits_unset_is_l2p_32) apply (simp add: word_bits_def) apply (auto intro: plus_one_helper dest: plus_one_helper2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p \<le> 0xF) = (\<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> p !! n') proof (prove)
goal (2 subgoals):
 1. 4 < word_bits
 2. (p \<le> 0xF) = (p < 2 ^ 4) proof (prove)
goal (1 subgoal):
 1. (p \<le> 0xF) = (p < 2 ^ 4) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma pd_shifting_at:
  "\<lbrakk> page_directory_at pd s; pspace_aligned s \<rbrakk> \<Longrightarrow>
  pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd" apply (rule pd_shifting) apply (clarsimp simp: pspace_aligned_def obj_at_def) apply (drule bspec, blast) including unfold_objects by (clarsimp simp: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageDirectory) pd s; pspace_aligned s\<rbrakk> \<Longrightarrow> pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageDirectory) pd s; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned pd 14 proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> is_aligned pd 14 proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd (obj_bits (the (kheap s pd)))\<rbrakk> \<Longrightarrow> is_aligned pd 14 proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd (obj_bits (the (kheap s pd)))\<rbrakk> \<Longrightarrow> is_aligned pd 14
theory ArchAcc_AI

lemma is_aligned_pt:
  "page_table_at pt s \<Longrightarrow> pspace_aligned s
    \<Longrightarrow> is_aligned pt pt_bits" apply (clarsimp simp: obj_at_def) apply (drule(1) pspace_alignedD) apply (simp add: pt_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) pt s; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned pt pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>pta. \<lbrakk>pspace_aligned s; kheap s pt = Some (ArchObj (PageTable pta))\<rbrakk> \<Longrightarrow> is_aligned pt pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>pta. \<lbrakk>pspace_aligned s; is_aligned pt (obj_bits (ArchObj (PageTable pta)))\<rbrakk> \<Longrightarrow> is_aligned pt pt_bits proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma is_aligned_global_pt:
  "\<lbrakk>x \<in> set (arm_global_pts (arch_state s)); pspace_aligned s; valid_arch_state s\<rbrakk>
   \<Longrightarrow> is_aligned x pt_bits" by (metis valid_arch_state_def valid_global_pts_def
            is_aligned_pt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set (arm_global_pts (arch_state s)); pspace_aligned s; valid_arch_state s\<rbrakk> \<Longrightarrow> is_aligned x pt_bits
theory ArchAcc_AI

lemma data_at_aligned:
  "\<lbrakk> data_at sz p s; pspace_aligned s \<rbrakk> \<Longrightarrow> is_aligned p (pageBitsForSize sz)" by (erule pspace_alignedE[where x=p]; fastforce simp: data_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>data_at sz p s; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned p (pageBitsForSize sz)
theory ArchAcc_AI

lemma page_table_pte_at_diffE:
  "\<lbrakk> page_table_at p s; q - p = x << 2;
    x < 2^(pt_bits - 2); pspace_aligned s \<rbrakk> \<Longrightarrow> pte_at q s" apply (clarsimp simp: diff_eq_eq add.commute) apply (erule(2) page_table_pte_atI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) p s; q - p = x << 2; x < 2 ^ (pt_bits - 2); pspace_aligned s\<rbrakk> \<Longrightarrow> pte_at q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) p s; q = p + (x << 2); x < 2 ^ (pt_bits - 2); pspace_aligned s\<rbrakk> \<Longrightarrow> pte_at (p + (x << 2)) s proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma p_0x3C_shift:
  "is_aligned (p :: word32) 6 \<Longrightarrow>
  (\<forall>p\<in>set [p , p + 4 .e. p + 0x3C]. f p) = (\<forall>x\<in>set [0, 4 .e. 0x3C]. f (x + p))" apply (clarsimp simp: upto_enum_step_def add.commute) apply (frule is_aligned_no_overflow, simp add: word_bits_def) apply (simp add: linorder_not_le [symmetric]) apply (erule notE) apply (simp add: add.commute) apply (erule word_random) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 6 \<Longrightarrow> (\<forall>p\<in>set [p , p + 4 .e. p + 0x3C]. f p) = (\<forall>x\<in>set [0 , 4 .e. 0x3C]. f (x + p)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 6; p + 0x3C < p; x \<le> 0xF\<rbrakk> \<Longrightarrow> f (p + x * 4) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 6; p + 0x3C < p; x \<le> 0xF; p \<le> 0x3F + p\<rbrakk> \<Longrightarrow> f (p + x * 4) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 6; \<not> p \<le> p + 0x3C; x \<le> 0xF; p \<le> 0x3F + p\<rbrakk> \<Longrightarrow> f (p + x * 4) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 6; x \<le> 0xF; p \<le> 0x3F + p\<rbrakk> \<Longrightarrow> p \<le> p + 0x3C proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 6; x \<le> 0xF; p \<le> p + 0x3F\<rbrakk> \<Longrightarrow> p \<le> p + 0x3C proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 6; x \<le> 0xF\<rbrakk> \<Longrightarrow> 0x3C \<le> 0x3F proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma shiftr_w2p:
  "x < len_of TYPE('a) \<Longrightarrow>
  2 ^ x = (2^(len_of TYPE('a) - 1) >> (len_of TYPE('a) - 1 - x) :: 'a :: len word)" apply simp apply (rule word_eqI) apply (auto simp: word_size nth_shiftr nth_w2p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < LENGTH('a) \<Longrightarrow> 2 ^ x = 2 ^ (LENGTH('a) - 1) >> LENGTH('a) - 1 - x proof (prove)
goal (1 subgoal):
 1. x < LENGTH('a) \<Longrightarrow> 2 ^ x = 2 ^ (LENGTH('a) - Suc 0) >> LENGTH('a) - Suc x proof (prove)
goal (1 subgoal):
 1. \<And>n. x < LENGTH('a) \<Longrightarrow> n < size (2 ^ x) \<longrightarrow> (2 ^ x) !! n = (2 ^ (LENGTH('a) - Suc 0) >> LENGTH('a) - Suc x) !! n proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma vptr_shiftr_le_2p:
  "(vptr :: word32)  >> 20 < 2 ^ pageBits" apply (rule le_less_trans[rotated]) apply (rule and_mask_less' [where w=max_word]) apply (simp add: pageBits_def) apply (rule word_leI) apply (simp add: word_size nth_shiftr) apply (drule test_bit_size) apply (simp add: pageBits_def word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vptr >> 20 < 2 ^ pageBits proof (prove)
goal (2 subgoals):
 1. ?y < 2 ^ pageBits
 2. vptr >> 20 \<le> ?y proof (prove)
goal (2 subgoals):
 1. pageBits < LENGTH(32)
 2. vptr >> 20 \<le> - 1 && mask pageBits proof (prove)
goal (1 subgoal):
 1. vptr >> 20 \<le> - 1 && mask pageBits proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < size (vptr >> 20); (vptr >> 20) !! n\<rbrakk> \<Longrightarrow> (- 1 && mask pageBits) !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 32; vptr !! (20 + n)\<rbrakk> \<Longrightarrow> n < pageBits proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 32; 20 + n < size vptr\<rbrakk> \<Longrightarrow> n < pageBits proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma page_directory_pde_at_lookupI:
  "\<lbrakk>page_directory_at pd s; pspace_aligned s\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s" apply (simp add: lookup_pd_slot_def Let_def) apply (erule (1) page_directory_pde_atI[rotated 2]) apply (rule vptr_shiftr_le_2p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageDirectory) pd s; pspace_aligned s\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageDirectory) pd s; pspace_aligned s\<rbrakk> \<Longrightarrow> pde_at (pd + (vptr >> 20 << 2)) s proof (prove)
goal (1 subgoal):
 1. typ_at (AArch APageDirectory) pd s \<Longrightarrow> vptr >> 20 < 2 ^ pageBits proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma vptr_shiftr_le_2pt:
  "((vptr :: word32) >> 12) && 0xFF < 2 ^ (pt_bits - 2)" apply (clarsimp simp: word_FF_is_mask pt_bits_def pageBits_def) apply (rule and_mask_less_size[where n=8, simplified]) apply (clarsimp simp: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vptr >> 12) && 0xFF < 2 ^ (pt_bits - 2) proof (prove)
goal (1 subgoal):
 1. (vptr >> 12) && mask 8 < 0x100 proof (prove)
goal (1 subgoal):
 1. 8 < size (vptr >> 12) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma page_table_pte_at_lookupI:
  "\<lbrakk>page_table_at pt s; pspace_aligned s\<rbrakk> \<Longrightarrow> pte_at (lookup_pt_slot_no_fail pt vptr) s" apply (simp add: lookup_pt_slot_no_fail_def) apply (erule (1) page_table_pte_atI[rotated 2]) apply (rule vptr_shiftr_le_2pt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) pt s; pspace_aligned s\<rbrakk> \<Longrightarrow> pte_at (lookup_pt_slot_no_fail pt vptr) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) pt s; pspace_aligned s\<rbrakk> \<Longrightarrow> pte_at (pt + ((vptr >> 12) && 0xFF << 2)) s proof (prove)
goal (1 subgoal):
 1. typ_at (AArch APageTable) pt s \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (pt_bits - 2) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_distinct [wp]:
  "set_pt p pt \<lbrace>pspace_distinct\<rbrace>" apply (simp add: set_pt_def) apply (wpsimp wp: set_object_wp_strong) apply (clarsimp simp: obj_at_def a_type_def pspace_distinct_same_type
                 split: kernel_object.splits arch_kernel_obj.splits if_splits) done

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

lemma set_pd_distinct [wp]:
  "set_pd p pd \<lbrace>pspace_distinct\<rbrace>" apply (simp add: set_pd_def) apply (wp set_object_distinct[THEN hoare_set_object_weaken_pre] get_object_wp) apply (clarsimp simp: obj_at_def a_type_def
                  split: kernel_object.splits arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> set_pd p pd \<lbrace>\<lambda>_. pspace_distinct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_. pspace_distinct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_distinct s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (PageDirectory pd)) = a_type ko \<longrightarrow> pspace_distinct s proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_caps_of_state [wp]:
  "set_pt p pt \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>" apply (simp add: set_pt_def) apply (wpsimp wp: set_object_wp_strong simp: obj_at_def a_type_simps) apply (subst cte_wp_caps_of_lift) prefer 2 apply assumption apply (auto simp: cte_wp_at_cases a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_pt p pt \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; AArch APageTable = a_type ko\<rbrakk> \<Longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko pa Pa. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; AArch APageTable = a_type ko\<rbrakk> \<Longrightarrow> cte_wp_at Pa pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = cte_wp_at Pa pa (?s'9 s ko)
 2. \<And>s ko. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; AArch APageTable = a_type ko\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'9 s ko)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; AArch APageTable = a_type ko\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'9 s ko))
 2. \<And>s ko pa Pa. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; AArch APageTable = a_type ko\<rbrakk> \<Longrightarrow> cte_wp_at Pa pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = cte_wp_at Pa pa (?s'9 s ko) proof (prove)
goal (1 subgoal):
 1. \<And>s ko pa Pa. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; AArch APageTable = a_type ko\<rbrakk> \<Longrightarrow> cte_wp_at Pa pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) = cte_wp_at Pa pa s proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_caps_of_state [wp]:
  "set_pd p pd \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>" apply (simp add: set_pd_def bind_assoc) apply (wpsimp wp: set_object_wp_strong simp: obj_at_def) apply (subst cte_wp_caps_of_lift) prefer 2 apply assumption by (case_tac ko; simp add: cte_wp_at_cases a_type_simps split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko\<rbrakk> \<Longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko pa Pa. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko\<rbrakk> \<Longrightarrow> cte_wp_at Pa pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) = cte_wp_at Pa pa (?s'7 s ko)
 2. \<And>s ko. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'7 s ko)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'7 s ko))
 2. \<And>s ko pa Pa. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko\<rbrakk> \<Longrightarrow> cte_wp_at Pa pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) = cte_wp_at Pa pa (?s'7 s ko) proof (prove)
goal (1 subgoal):
 1. \<And>s ko pa Pa. \<lbrakk>P (caps_of_state s); kheap s p = Some ko; a_type (ArchObj (PageDirectory pd)) = a_type ko\<rbrakk> \<Longrightarrow> cte_wp_at Pa pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) = cte_wp_at Pa pa s
theory ArchAcc_AI

lemma store_pte_aligned [wp]:
  "store_pte pt p \<lbrace>pspace_aligned\<rbrace>" apply (simp add: store_pte_def set_pt_def) apply (wp set_object_aligned) including unfold_objects by (clarsimp simp: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> store_pte pt p \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> do pta <- get_pt (pt && ~~ mask pt_bits);
set_object (pt && ~~ mask pt_bits) (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt && mask pt_bits >> 2) := p))))
od \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned s \<Longrightarrow> \<forall>pta. ako_at (PageTable pta) (pt && ~~ mask pt_bits) s \<longrightarrow> pspace_aligned s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned s \<Longrightarrow> \<forall>pta. ako_at (PageTable pta) (pt && ~~ mask pt_bits) s \<longrightarrow> pspace_aligned s
theory ArchAcc_AI

lemma set_asid_pool_aligned [wp]:
  "set_asid_pool p ptr \<lbrace>pspace_aligned\<rbrace>" apply (simp add: set_asid_pool_def) including unfold_objects apply (wpsimp wp: set_object_wp_strong pspace_aligned_obj_update[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_asid_pool p ptr \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_object p (ArchObj (ASIDPool ptr)) \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_object p (ArchObj (ASIDPool ptr)) \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal:
No subgoals!