kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchRetype_AC

lemma copy_global_mappings_index_subset:
  "set [kernel_base >> 20.e.2 ^ (pd_bits - 2) - 1] \<subseteq> {x. \<exists>y. x = y >> 20}" apply clarsimp apply (rule_tac x="x << 20" in exI) apply (subst shiftl_shiftr1, simp) apply (simp add: word_size) apply (rule sym, rule less_mask_eq) apply (simp add: word_leq_minus_one_le pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. \<exists>y. x = y >> 20} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kernel_base >> 20 \<le> x; x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> \<exists>y. x = y >> 20 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kernel_base >> 20 \<le> x; x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> x = x << 20 >> 20 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kernel_base >> 20 \<le> x; x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> x = x && mask (size x - 20) << 20 - 20 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kernel_base >> 20 \<le> x; x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> x = x && mask 12 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kernel_base >> 20 \<le> x; x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ 12 proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma copy_global_mappings_integrity:
  "is_aligned x pd_bits
   \<Longrightarrow> \<lbrace>integrity aag X st and K (is_subject aag x)\<rbrace>
       copy_global_mappings x
       \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: copy_global_mappings_def) apply (wp mapM_x_wp[OF _ subset_refl] store_pde_respects) apply (drule subsetD[OF copy_global_mappings_index_subset]) apply (fastforce simp: pd_shifting') apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x pd_bits \<Longrightarrow> \<lbrace>integrity aag X st and K (is_subject aag x)\<rbrace> copy_global_mappings x \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x pd_bits; is_subject aag x\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st\<rbrace> copy_global_mappings x \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x pd_bits; is_subject aag x\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (x + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>global_pd xa s. \<lbrakk>is_aligned x pd_bits; is_subject aag x; xa \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; integrity aag X st s\<rbrakk> \<Longrightarrow> (integrity aag X st and K (is_subject aag (x + (xa << 2) && ~~ mask pd_bits))) s
 2. \<lbrakk>is_aligned x pd_bits; is_subject aag x\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. integrity aag X st\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x; integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>global_pd xa s. \<lbrakk>is_aligned x pd_bits; is_subject aag x; integrity aag X st s; xa \<in> {x. \<exists>y. x = y >> 20}\<rbrakk> \<Longrightarrow> (integrity aag X st and K (is_subject aag (x + (xa << 2) && ~~ mask pd_bits))) s
 2. \<lbrakk>is_aligned x pd_bits; is_subject aag x\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. integrity aag X st\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x; integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x pd_bits; is_subject aag x\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x; integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma state_vrefs_detype[Retype_AC_assms, dest]:
  "x \<in> state_vrefs (detype R s) p \<Longrightarrow> x \<in> state_vrefs s p" unfolding state_vrefs_def by (clarsimp simp: detype_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> state_vrefs (detype R s) p \<Longrightarrow> x \<in> state_vrefs s p proof (prove)
goal (1 subgoal):
 1. x \<in> (case_option {} vs_refs_no_global_pts \<circ> kheap (detype R s)) p \<Longrightarrow> x \<in> (case_option {} vs_refs_no_global_pts \<circ> kheap s) p
theory ArchRetype_AC

lemma sata_detype[Retype_AC_assms]:
  "state_asids_to_policy aag (detype R s) \<subseteq> state_asids_to_policy aag s" apply (clarsimp) apply (erule state_asids_to_policy_aux.induct) apply (auto intro: state_asids_to_policy_aux.intros split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy aag (detype R s) \<subseteq> state_asids_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_asids_to_policy_aux aag (\<lambda>p. if fst p \<in> R then None else caps_of_state s p) (asid_table s) (state_vrefs (detype R s)) \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ptr acap asid. \<lbrakk>(if fst ptr \<in> R then None else caps_of_state s ptr) = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs (detype R s) poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, ab, pasObjectAbs aag pdptr) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 3. \<And>a aa b asid poolptr. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma word_size_bits_untyped_min_bits[Retype_AC_assms]: "word_size_bits \<le> untyped_min_bits" by (simp add: word_size_bits_def untyped_min_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_size_bits \<le> untyped_min_bits
theory ArchRetype_AC

lemma word_size_bits_resetChunkBits[Retype_AC_assms]: "word_size_bits \<le> resetChunkBits" by (simp add: word_size_bits_def Kernel_Config.resetChunkBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_size_bits \<le> resetChunkBits
theory ArchRetype_AC

lemma cli_default_cap[Retype_AC_assms]:
  "tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> cap_links_irq aag p (default_cap tp p' sz dev)" unfolding cap_links_irq_def apply (cases tp, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> cap_links_irq aag p (default_cap tp p' sz dev) proof (prove)
goal (1 subgoal):
 1. tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> \<forall>irq\<in>cap_irqs_controlled (default_cap tp p' sz dev). (p, Control, pasIRQAbs aag irq) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma pd_shifting_dual':
  "is_aligned (pd::word32) pd_bits
   \<Longrightarrow> pd + (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2" apply (subst (asm) pd_bits_def) apply (subst (asm) pageBits_def) apply (simp add: pd_shifting_dual) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> pd + (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2 proof (prove)
goal (1 subgoal):
 1. is_aligned pd (pageBits + 2) \<Longrightarrow> pd + (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2 proof (prove)
goal (1 subgoal):
 1. is_aligned pd (12 + 2) \<Longrightarrow> pd + (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2 proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma region_in_kernel_window_preserved:
  assumes "\<And>P. f \<lbrace>\<lambda>s. P (arch_state s)\<rbrace>"
  shows "\<And>S. f \<lbrace>region_in_kernel_window S\<rbrace>" apply (clarsimp simp: valid_def region_in_kernel_window_def) apply (erule use_valid) apply (rule assms) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>S. \<lbrace>region_in_kernel_window S\<rbrace> f \<lbrace>\<lambda>_. region_in_kernel_window S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>S s a b x. \<lbrakk>\<forall>x\<in>S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow; (a, b) \<in> fst (f s); x \<in> S\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state b) x = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<And>S s a b x. \<lbrakk>\<forall>x\<in>S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow; x \<in> S\<rbrakk> \<Longrightarrow> \<lbrace>?P10 S s a b x\<rbrace> f \<lbrace>\<lambda>a b. arm_kernel_vspace (arch_state b) x = ArmVSpaceKernelWindow\<rbrace>
 2. \<And>S s a b x. \<lbrakk>\<forall>x\<in>S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow; x \<in> S\<rbrakk> \<Longrightarrow> ?P10 S s a b x s proof (prove)
goal (1 subgoal):
 1. \<And>S s a b x. \<lbrakk>\<forall>x\<in>S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow; x \<in> S\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma dmo_freeMemory_vms:
  "do_machine_op (freeMemory ptr bits) \<lbrace>valid_machine_state\<rbrace>" apply (unfold do_machine_op_def) apply (wp modify_wp freeMemory_vms | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (freeMemory ptr bits ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma freeMemory_valid_irq_states:
  "freeMemory ptr bits \<lbrace>\<lambda>ms. valid_irq_states (s\<lparr>machine_state := ms\<rparr>)\<rbrace>" unfolding freeMemory_def by (wp mapM_x_wp[OF _ subset_refl] storeWord_valid_irq_states)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. valid_irq_states (s\<lparr>machine_state := ms\<rparr>)\<rbrace> freeMemory ptr bits \<lbrace>\<lambda>_ ms. valid_irq_states (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. valid_irq_states (s\<lparr>machine_state := ms\<rparr>)\<rbrace> mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] \<lbrace>\<lambda>_ ms. valid_irq_states (s\<lparr>machine_state := ms\<rparr>)\<rbrace>
theory ArchRetype_AC

lemma init_arch_objects_pas_cur_domain[Retype_AC_assms, wp]:
  "init_arch_objects tp ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_cur_domain aag\<rbrace> init_arch_objects tp ptr n us refs \<lbrace>\<lambda>_. pas_cur_domain aag\<rbrace>
theory ArchRetype_AC

lemma retype_region_pas_cur_domain[Retype_AC_assms, wp]:
  "retype_region ptr n us tp dev \<lbrace>pas_cur_domain aag\<rbrace>" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_cur_domain aag\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>_. pas_cur_domain aag\<rbrace>
theory ArchRetype_AC

lemma reset_untyped_cap_pas_cur_domain[Retype_AC_assms, wp]:
  "reset_untyped_cap src_slot \<lbrace>pas_cur_domain aag\<rbrace>" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_cur_domain aag\<rbrace> reset_untyped_cap src_slot \<lbrace>\<lambda>_. pas_cur_domain aag\<rbrace>
theory ArchRetype_AC

lemma arch_data_to_obj_type_not_ASIDPoolObj[Retype_AC_assms, simp]:
  "arch_data_to_obj_type v \<noteq> Some ASIDPoolObj" by (clarsimp simp: arch_data_to_obj_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_data_to_obj_type v \<noteq> Some ASIDPoolObj
theory ArchRetype_AC

lemma data_to_nat_of_nat[Retype_AC_assms, simp]:
  "of_nat (data_to_nat x) = x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_nat (data_to_nat x) = x
theory ArchRetype_AC

lemma nonzero_data_to_nat_simp[Retype_AC_assms]:
  "0 < data_to_nat x \<Longrightarrow> 0 < x" by (auto dest: word_of_nat_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < data_to_nat x \<Longrightarrow> 0 < x
theory ArchRetype_AC

lemma storeWord_integrity_autarch:
  "\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and>
         (is_aligned p 2 \<longrightarrow> (\<forall>p' \<in> ptr_range p 2. is_subject aag p'))\<rbrace>
   storeWord p v
   \<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>" unfolding storeWord_def apply wp apply (auto simp: integrity_def is_aligned_mask [symmetric]
            intro!: trm_lrefl ptr_range_memI ptr_range_add_memI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and> (is_aligned p 2 \<longrightarrow> (\<forall>p'\<in>ptr_range p 2. is_subject aag p'))\<rbrace> storeWord p v \<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and> (is_aligned p 2 \<longrightarrow> (\<forall>p'\<in>ptr_range p 2. is_subject aag p'))\<rbrace> do assert (p && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(p := word_rsplit v ! 3, p + 1 := word_rsplit v ! 2, p + 2 := word_rsplit v ! 1, p + 3 := word_rsplit v ! 0)))
od \<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. integrity aag X st (s\<lparr>machine_state := sa\<rparr>) \<and> (is_aligned p 2 \<longrightarrow> (\<forall>p'\<in>ptr_range p 2. is_subject aag p')) \<Longrightarrow> p && mask 2 = 0 \<longrightarrow> integrity aag X st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(p := word_rsplit v ! 3, p + 1 := word_rsplit v ! 2, p + 2 := word_rsplit v ! 1, p + 3 := word_rsplit v ! 0)) sa\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma storeWord_respects:
  "\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and>
         (\<forall>p' \<in> ptr_range p word_size_bits. aag_has_auth_to aag Write p')\<rbrace>
   storeWord p v
   \<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>" unfolding storeWord_def word_size_bits_def apply wp apply (auto simp: integrity_def is_aligned_mask [symmetric]
            intro!: trm_write ptr_range_memI ptr_range_add_memI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and> (\<forall>p'\<in>ptr_range p word_size_bits. (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag)\<rbrace> storeWord p v \<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and> (\<forall>p'\<in>ptr_range p 2. (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag)\<rbrace> do assert (p && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(p := word_rsplit v ! 3, p + 1 := word_rsplit v ! 2, p + 2 := word_rsplit v ! 1, p + 3 := word_rsplit v ! 0)))
od \<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. integrity aag X st (s\<lparr>machine_state := sa\<rparr>) \<and> (\<forall>p'\<in>ptr_range p 2. (pasSubject aag, Write, pasObjectAbs aag p') \<in> pasPolicy aag) \<Longrightarrow> p && mask 2 = 0 \<longrightarrow> integrity aag X st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(p := word_rsplit v ! 3, p + 1 := word_rsplit v ! 2, p + 2 := word_rsplit v ! 1, p + 3 := word_rsplit v ! 0)) sa\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma dmo_cacheRangeOp_lift:
  "(\<And>a b. do_machine_op (oper a b) \<lbrace>P\<rbrace>)
   \<Longrightarrow> do_machine_op (cacheRangeOp oper x y z) \<lbrace>P\<rbrace>" by (wpsimp wp: dmo_mapM_x_wp_inv simp: cacheRangeOp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. \<lbrace>P\<rbrace> do_machine_op (oper a b) \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (cacheRangeOp oper x y z) \<lbrace>\<lambda>_. P\<rbrace>
theory ArchRetype_AC

lemma dmo_cleanCacheRange_PoU_respects [wp]:
  "do_machine_op (cleanCacheRange_PoU vstart vend pstart) \<lbrace>integrity aag X st\<rbrace>" by (wpsimp wp: dmo_cacheRangeOp_lift simp: cleanCacheRange_PoU_def cleanByVA_PoU_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do_machine_op (cleanCacheRange_PoU vstart vend pstart) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchRetype_AC

lemma dmo_mapM_x_cleanCacheRange_PoU_integrity:
  "do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU (f x) (g x) (h x)) refs) \<lbrace>integrity aag X st\<rbrace>" by (wp dmo_mapM_x_wp_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU (f x) (g x) (h x)) refs) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchRetype_AC

lemma init_arch_objects_integrity[Retype_AC_assms]:
  "\<lbrace>integrity aag X st and K (\<forall>x\<in>set refs. is_subject aag x)
                       and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace>
   init_arch_objects new_type ptr num_objects obj_sz refs
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm)+ apply (cases new_type; simp add: init_arch_objects_def split del: if_split) apply (wpsimp wp: mapM_x_wp[OF _ subset_refl] copy_global_mappings_integrity
                    dmo_mapM_x_cleanCacheRange_PoU_integrity
              simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (\<forall>x\<in>set refs. is_subject aag x) and K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace> init_arch_objects new_type ptr num_objects obj_sz refs \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api new_type obj_sz); \<forall>x\<in>set refs. is_subject aag x\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st\<rbrace> init_arch_objects new_type ptr num_objects obj_sz refs \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x6. \<lbrakk>\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api (ArchObject x6) obj_sz); \<forall>x\<in>set refs. is_subject aag x; new_type = ArchObject x6\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st\<rbrace> if x6 = PageDirectoryObj then do y <- mapM_x copy_global_mappings refs;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs)
od else return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchRetype_AC

lemma integrity_asids_detype[Retype_AC_assms]:
  assumes refs: "\<forall>r\<in>refs. pasObjectAbs aag r \<in> subjects"
  shows
    "integrity_asids aag subjects x a (detype refs s) s' =
     integrity_asids aag subjects x a s s'"
    "integrity_asids aag subjects x a s (detype refs s') =
     integrity_asids aag subjects x a s s'" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_asids aag subjects x a (detype refs s) s' = integrity_asids aag subjects x a s s' &&& integrity_asids aag subjects x a s (detype refs s') = integrity_asids aag subjects x a s s'
theory ArchRetype_AC

lemma retype_region_integrity_asids[Retype_AC_assms]:
  "\<lbrakk> range_cover ptr sz (obj_bits_api typ o_bits) n; typ \<noteq> Untyped;
     \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; integrity_asids aag {pasSubject aag} x a s st \<rbrakk>
     \<Longrightarrow> integrity_asids aag {pasSubject aag} x a s
           (st\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api typ o_bits)) ` {0 ..< n}
                            then Some (default_object typ dev o_bits)
                            else kheap s a\<rparr>)" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api typ o_bits) n; typ \<noteq> Untyped; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; integrity_asids aag {pasSubject aag} x a s st\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} x a s (st\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api typ o_bits)) ` {0..<n} then Some (default_object typ dev o_bits) else kheap s a\<rparr>)
theory Arch_AC

lemma ipc_buffer_has_auth_wordE:
  "\<lbrakk> ipc_buffer_has_auth aag thread (Some buf); p \<in> ptr_range (buf + off) sz;
     is_aligned off sz; sz \<le> msg_align_bits; off < 2 ^ msg_align_bits \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag Write thread p" unfolding ipc_buffer_has_auth_def by (fastforce elim: bspec set_mp[OF ptr_range_subset])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ipc_buffer_has_auth aag thread (Some buf); p \<in> ptr_range (buf + off) sz; is_aligned off sz; sz \<le> msg_align_bits; off < 2 ^ msg_align_bits\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case Some buf of None \<Rightarrow> True | Some p \<Rightarrow> is_aligned p msg_align_bits \<and> (\<forall>x\<in>ptr_range p msg_align_bits. (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag); p \<in> ptr_range (buf + off) sz; is_aligned off sz; sz \<le> msg_align_bits; off < 2 ^ msg_align_bits\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag p) \<in> pasPolicy aag
theory Arch_AC

lemma is_transferable_ArchCap[simp]:
  "\<not> is_transferable (Some (ArchObjectCap cap))" using is_transferable.simps by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_transferable_cap (ArchObjectCap cap) proof (prove)
using this:
is_transferable ?opt_cap = (?opt_cap = None \<or> ?opt_cap = Some NullCap \<or> (\<exists>t R. ?opt_cap = Some (ReplyCap t False R)))

goal (1 subgoal):
 1. \<not> is_transferable_cap (ArchObjectCap cap)