kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchArch_AC

lemma find_pd_for_asid_pd_slot_authorised [wp]:
  "\<lbrace>pas_refined aag and K (is_subject_asid aag asid) and pspace_aligned and valid_vspace_objs\<rbrace>
   find_pd_for_asid asid
   \<lbrace>\<lambda>rv _. is_subject aag (lookup_pd_slot rv vptr && ~~ mask pd_bits)\<rbrace>, -" apply (wp find_pd_for_asid_authority2) apply (clarsimp simp: lookup_pd_slot_pd) apply (fastforce dest: pas_refined_Control) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject_asid aag asid) and pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv _. is_subject aag (lookup_pd_slot rv vptr && ~~ mask pd_bits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_subject_asid aag asid) and pspace_aligned and valid_vspace_objs) s \<Longrightarrow> \<forall>pd. (\<forall>aag. pas_refined aag s \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag) \<and> (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s pd ref. \<lbrakk>pas_refined aag s; is_subject_asid aag asid; pspace_aligned s; valid_vspace_objs s; \<forall>aag. pas_refined aag s \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag; is_aligned pd pd_bits; (ref \<rhd> pd) s\<rbrakk> \<Longrightarrow> is_subject aag pd proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma unmap_page_table_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and invs
                       and K (is_subject_asid aag asid \<and> vaddr < kernel_base)\<rbrace>
   unmap_page_table asid vaddr pt
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: unmap_page_table_def page_table_mapped_def ) apply (rule hoare_pre) apply (wpsimp wp: store_pde_respects page_table_mapped_wp_weak get_pde_wp hoare_vcg_all_lift_R
               simp: cleanByVA_PoU_def
          | wp (once) hoare_drop_imps)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and invs and K (is_subject_asid aag asid \<and> vaddr < kernel_base)\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject_asid aag asid \<and> vaddr < kernel_base \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and invs\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject_asid aag asid \<and> vaddr < kernel_base \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and invs\<rbrace> do pdOpt <- doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE <catch> (\<lambda>y. return None);
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (lookup_pd_slot pd vaddr) InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot pd vaddr) (addrFromPPtr (lookup_pd_slot pd vaddr)));
flush_table pd asid vaddr pt
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_subject_asid aag asid \<and> vaddr < kernel_base \<Longrightarrow> \<lbrace>?Q4\<rbrace> do pdOpt <- doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE <catch> (\<lambda>y. return None);
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (lookup_pd_slot pd vaddr) InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot pd vaddr) (addrFromPPtr (lookup_pd_slot pd vaddr)));
flush_table pd asid vaddr pt
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>is_subject_asid aag asid \<and> vaddr < kernel_base; (integrity aag X st and pas_refined aag and invs) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_subject_asid aag asid; vaddr < kernel_base; integrity aag X st x; pas_refined aag x; invs x\<rbrakk> \<Longrightarrow> pspace_aligned x \<and> valid_vspace_objs x proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma clas_update_map_data_strg:
  "(is_pg_cap cap \<or> is_pt_cap cap)
   \<longrightarrow> cap_links_asid_slot aag p (ArchObjectCap (update_map_data (the_arch_cap cap) None))" unfolding cap_links_asid_slot_def by (fastforce simp: is_cap_simps update_map_data_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_pg_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_links_asid_slot aag p (ArchObjectCap (update_map_data (the_arch_cap cap) None)) proof (prove)
goal (1 subgoal):
 1. is_pg_cap cap \<or> is_pt_cap cap \<longrightarrow> (\<forall>asid\<in>cap_asid' (ArchObjectCap (update_map_data (the_arch_cap cap) None)). label_owns_asid_slot aag p asid)
theory ArchArch_AC

lemma pde_ref_pde_ref2:
  "\<lbrakk> pde_ref x = Some v; pde_ref2 x = Some v' \<rbrakk>
     \<Longrightarrow> v' = (v, 0, {Control})" unfolding pde_ref_def pde_ref2_def by (cases x, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref x = Some v; pde_ref2 x = Some v'\<rbrakk> \<Longrightarrow> v' = (v, 0, {Control}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case x of PageTablePDE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr) | _ \<Rightarrow> None) = Some v; (case x of InvalidPDE \<Rightarrow> None | PageTablePDE addr atts domain \<Rightarrow> Some (ptrFromPAddr addr, 0, {Control}) | SectionPDE addr atts domain rights \<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMSection, vspace_cap_rights_to_auth rights) | SuperSectionPDE addr atts rights \<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMSuperSection, vspace_cap_rights_to_auth rights)) = Some v'\<rbrakk> \<Longrightarrow> v' = (v, 0, {Control})
theory ArchArch_AC

lemma mask_PTCap_eq:
  "(ArchObjectCap (PageTableCap a b) = mask_cap R cap) = (cap = ArchObjectCap (PageTableCap a b))" by (auto simp: mask_cap_def cap_rights_update_def acap_rights_update_def
          split: arch_cap.splits cap.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ArchObjectCap (PageTableCap a b) = mask_cap R cap) = (cap = ArchObjectCap (PageTableCap a b))
theory ArchArch_AC

lemma is_transferable_is_arch_update:
  "is_arch_update cap cap' \<Longrightarrow> is_transferable (Some cap) = is_transferable (Some cap')" using is_transferable.simps is_arch_cap_def is_arch_update_def cap_master_cap_def by (simp split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_arch_update cap cap' \<Longrightarrow> is_transferable_cap cap = is_transferable_cap 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)))
is_arch_cap ?cap \<equiv> case ?cap of ArchObjectCap x \<Rightarrow> True | _ \<Rightarrow> False
is_arch_update ?cap ?cap' \<equiv> is_arch_cap ?cap \<and> cap_master_cap ?cap = cap_master_cap ?cap'
cap_master_cap ?cap \<equiv> case ?cap of UntypedCap dev ref n f \<Rightarrow> UntypedCap dev ref n 0 | EndpointCap ref bdg rghts \<Rightarrow> EndpointCap ref 0 UNIV | NotificationCap ref bdg rghts \<Rightarrow> NotificationCap ref 0 UNIV | ReplyCap ref master rghts \<Rightarrow> ReplyCap ref True UNIV | CNodeCap ref bits gd \<Rightarrow> CNodeCap ref bits [] | ThreadCap ref \<Rightarrow> ThreadCap ref | DomainCap \<Rightarrow> DomainCap | ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) | _ \<Rightarrow> ?cap

goal (1 subgoal):
 1. is_arch_update cap cap' \<Longrightarrow> is_transferable_cap cap = is_transferable_cap cap'
theory ArchArch_AC

lemma find_pd_for_asid_pd_owned[wp]:
  "\<lbrace>pas_refined aag and K (is_subject_asid aag asid)\<rbrace>
   find_pd_for_asid asid
   \<lbrace>\<lambda>rv _. is_subject aag rv\<rbrace>,-" apply (wp find_pd_for_asid_authority2) apply (auto simp: aag_has_Control_iff_owns) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject_asid aag asid)\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv _. is_subject aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_subject_asid aag asid)) s \<Longrightarrow> \<forall>pd. (\<forall>aag. pas_refined aag s \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag) \<and> (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> is_subject aag pd proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma do_flush_respects[wp]:
  "do_machine_op (do_flush typ start end pstart) \<lbrace>integrity aag X st\<rbrace>" by (cases "typ"; wpsimp wp: dmo_no_mem_respects simp: do_flush_def cache_machine_op_defs do_flush_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do_machine_op (do_flush typ start end pstart) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchArch_AC

lemma invalidate_tlb_by_asid_respects[wp]:
  "invalidate_tlb_by_asid asid \<lbrace>integrity aag X st\<rbrace>" unfolding invalidate_tlb_by_asid_def by (wpsimp wp: dmo_no_mem_respects simp: invalidateLocalTLB_ASID_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op $ invalidateLocalTLB_ASID hw_asid
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchArch_AC

lemma invalidate_tlb_by_asid_pas_refined[wp]:
  "invalidate_tlb_by_asid asid \<lbrace>pas_refined aag\<rbrace>" by (wpsimp wp: dmo_no_mem_respects simp: invalidate_tlb_by_asid_def invalidateLocalTLB_ASID_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory ArchArch_AC

lemma integrity_arm_asid_table_entry_update':
  "\<lbrakk> integrity aag X st s; atable = arm_asid_table (arch_state s);
     (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid
             \<longrightarrow> is_subject_asid aag asid') \<rbrakk>
     \<Longrightarrow> integrity aag X st (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
                                                          \<lambda>a. if a = asid_high_bits_of asid
                                                              then v
                                                              else atable a\<rparr>\<rparr>)" by (clarsimp simp: integrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity aag X st s; atable = asid_table s; \<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow> is_subject_asid aag asid'\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then v else atable a\<rparr>\<rparr>)
theory ArchArch_AC

lemma arm_asid_table_entry_update_integrity[wp]:
 "\<lbrace>integrity aag X st and (\<lambda> s. atable = arm_asid_table (arch_state s)) and
   K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid
              \<longrightarrow> is_subject_asid aag asid')\<rbrace>
  modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := atable(asid_high_bits_of asid := v)\<rparr>\<rparr>)
  \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (wp | simp)+ apply (blast intro: integrity_arm_asid_table_entry_update') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. atable = asid_table s) and K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow> is_subject_asid aag asid')\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := atable(asid_high_bits_of asid := v)\<rparr>\<rparr>) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st s \<and> atable = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow> is_subject_asid aag asid') \<Longrightarrow> integrity aag X st (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then v else asid_table s a\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma perform_asid_pool_invocation_respects:
  "\<lbrace>integrity aag X st and K (authorised_asid_pool_inv aag api)\<rbrace>
   perform_asid_pool_invocation api
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: perform_asid_pool_invocation_def) apply (wpsimp wp: set_asid_pool_integrity_autarch get_cap_wp set_cap_integrity_autarch) apply (auto iff: authorised_asid_pool_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (authorised_asid_pool_inv aag api)\<rbrace> perform_asid_pool_invocation api \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. authorised_asid_pool_inv aag api)\<rbrace> case api of Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of ArchObjectCap (PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xc xd pool. \<lbrakk>integrity aag X st s; authorised_asid_pool_inv aag (Assign x xa (a, b)); api = Assign x xa (a, b); cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap xc xd))) (a, b) s; ako_at (ASIDPool pool) xa s\<rbrakk> \<Longrightarrow> is_subject aag a \<and> is_subject aag xa proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma asid_pool_into_aag:
  "\<lbrakk> kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag Control p p'" apply (rule pas_refined_mem [rotated], assumption) apply (rule sta_vref) apply (fastforce simp: state_vrefs_def vs_refs_no_global_pts_def intro!: graph_ofI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, Control, pasObjectAbs aag p') \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s\<rbrakk> \<Longrightarrow> (p, Control, p') \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s\<rbrakk> \<Longrightarrow> (p', ?uu3, ?uv3, Control) \<in> state_vrefs s p proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma invoke_arch_respects:
  "\<lbrace>integrity aag X st and authorised_arch_inv aag ai and
    pas_refined aag and invs and valid_arch_inv ai and is_subject aag \<circ> cur_thread\<rbrace>
   arch_perform_invocation ai
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: arch_perform_invocation_def) apply (wpsimp wp: perform_page_table_invocation_respects perform_page_invocation_respects
                    perform_asid_control_invocation_respects perform_asid_pool_invocation_respects) apply (auto simp: authorised_arch_inv_def valid_arch_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and authorised_arch_inv aag ai and pas_refined aag and invs and valid_arch_inv ai and is_subject aag \<circ> cur_thread\<rbrace> arch_perform_invocation ai \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and authorised_arch_inv aag ai and pas_refined aag and invs and valid_arch_inv ai and is_subject aag \<circ> cur_thread\<rbrace> liftE (case ai of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; authorised_arch_inv aag ai s; pas_refined aag s; invs s; valid_arch_inv ai s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>x. ai = InvokePageTable x \<longrightarrow> valid_pti x s \<and> authorised_page_table_inv aag x) \<and> (\<forall>x. ai = InvokePage x \<longrightarrow> authorised_page_inv aag x \<and> valid_page_inv x s \<and> valid_vspace_objs s \<and> pspace_aligned s) \<and> (\<forall>x. ai = InvokeASIDControl x \<longrightarrow> authorised_asid_control_inv aag x) \<and> (\<forall>x. ai = InvokeASIDPool x \<longrightarrow> authorised_asid_pool_inv aag x) proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma pageBitsForSize_le_t29:
  "pageBitsForSize sz \<le> 29" by (cases sz, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBitsForSize sz \<le> 29
theory ArchArch_AC

lemma x_t2n_sub_1_neg_mask:
  "\<lbrakk> is_aligned x n; n \<le> m \<rbrakk>
     \<Longrightarrow> x + 2 ^ n - 1 && ~~ mask m = x && ~~ mask m" apply (erule is_aligned_get_word_bits) apply (rule trans, rule mask_lower_twice[symmetric], assumption) apply (subst add_diff_eq[symmetric], subst is_aligned_add_helper, assumption) apply simp+ apply (simp add: mask_def power_overflow) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n \<le> m\<rbrakk> \<Longrightarrow> x + 2 ^ n - 1 && ~~ mask m = x && ~~ mask m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> m; is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x + 2 ^ n - 1 && ~~ mask m = x && ~~ mask m
 2. \<lbrakk>n \<le> m; x = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x + 2 ^ n - 1 && ~~ mask m = x && ~~ mask m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> m; is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x + 2 ^ n - 1 && ~~ mask n) && ~~ mask m = x && ~~ mask m
 2. \<lbrakk>n \<le> m; x = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x + 2 ^ n - 1 && ~~ mask m = x && ~~ mask m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<le> m; is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n - 1 < 2 ^ n
 2. \<lbrakk>n \<le> m; is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x && ~~ mask m = x && ~~ mask m
 3. \<lbrakk>n \<le> m; x = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x + 2 ^ n - 1 && ~~ mask m = x && ~~ mask m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> m; x = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> 2 ^ n - 1 && ~~ mask m = 0 proof (prove)
goal:
No subgoals!
theory ArchArch_AC

lemma delete_asid_pool_respects[wp]:
  "\<lbrace>integrity aag X st and
    K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of x
               \<longrightarrow> is_subject_asid aag asid')\<rbrace>
   delete_asid_pool x y
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding delete_asid_pool_def apply simp apply (wp mapM_wp[OF _ subset_refl] | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of x \<longrightarrow> is_subject_asid aag asid')\<rbrace> delete_asid_pool x y \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of x \<longrightarrow> is_subject_asid aag asid')\<rbrace> do assert (x && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of x) = Some y) $ do pool <- get_asid_pool y;
mapM (\<lambda>offset. when (pool (UCAST(32 \<rightarrow> 10) offset) \<noteq> None) $ do flush_space $ x + offset;
invalidate_asid_entry $ x + offset
od) [0 .e. (1 << local.asid_low_bits) - 1];
asid_table' <- return (asid_table(asid_high_bits_of x := None));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. \<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of x \<longrightarrow> is_subject_asid aag asid')\<rbrace> do ya <- assert (x && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of x) = Some y) (do pool <- get_asid_pool y;
y <- mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (x + offset);
invalidate_asid_entry (x + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of x := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!