kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchArch_IF

lemma check_mapping_pptr_reads_respects:
  "reads_respects aag l (K (\<forall>x. (tablePtr = Inl x \<longrightarrow> is_subject aag (x && ~~ mask pt_bits)) \<and>
                                (tablePtr = Inr x \<longrightarrow> is_subject aag (x && ~~ mask pd_bits))))
                  (check_mapping_pptr pptr pgsz tablePtr)" unfolding check_mapping_pptr_def fun_app_def apply (rule equiv_valid_guard_imp) apply (wpsimp wp: get_pte_reads_respects get_pde_rev) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (\<forall>x. (tablePtr = Inl x \<longrightarrow> is_subject aag (x && ~~ mask pt_bits)) \<and> (tablePtr = Inr x \<longrightarrow> is_subject aag (x && ~~ mask pd_bits)))) (check_mapping_pptr pptr pgsz tablePtr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (\<forall>x. (tablePtr = Inl x \<longrightarrow> is_subject aag (x && ~~ mask pt_bits)) \<and> (tablePtr = Inr x \<longrightarrow> is_subject aag (x && ~~ mask pd_bits)))) (case tablePtr of Inl ptePtr \<Rightarrow> do pte <- get_pte ptePtr;
return (case pte of InvalidPTE \<Rightarrow> False | LargePagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMLargePage | SmallPagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMSmallPage)
od | Inr pdePtr \<Rightarrow> do pde <- get_pde pdePtr;
return (case pde of SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMSection | SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMSuperSection | _ \<Rightarrow> False)
od) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (case tablePtr of Inl ptePtr \<Rightarrow> do pte <- get_pte ptePtr;
return (case pte of InvalidPTE \<Rightarrow> False | LargePagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMLargePage | SmallPagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMSmallPage)
od | Inr pdePtr \<Rightarrow> do pde <- get_pde pdePtr;
return (case pde of SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMSection | SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMSuperSection | _ \<Rightarrow> False)
od)
 2. \<And>s. K (\<forall>x. (tablePtr = Inl x \<longrightarrow> is_subject aag (x && ~~ mask pt_bits)) \<and> (tablePtr = Inr x \<longrightarrow> is_subject aag (x && ~~ mask pd_bits))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. K (\<forall>x. (tablePtr = Inl x \<longrightarrow> is_subject aag (x && ~~ mask pt_bits)) \<and> (tablePtr = Inr x \<longrightarrow> is_subject aag (x && ~~ mask pd_bits))) s \<Longrightarrow> (\<forall>x. tablePtr = Inl x \<longrightarrow> K (is_subject aag (x && ~~ mask pt_bits)) s \<and> True) \<and> (\<forall>x. tablePtr = Inr x \<longrightarrow> K (is_subject aag (x && ~~ mask pd_bits)) s \<and> True) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma lookup_pt_slot_reads_respects:
  "reads_respects aag l (K (is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits)))
                  (lookup_pt_slot pd vptr)" unfolding lookup_pt_slot_def fun_app_def by (wpsimp wp: get_pde_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits))) (lookup_pt_slot pd vptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits))) (doE pd_slot <- returnOk (lookup_pd_slot pd vptr);
pde <- liftE (get_pde pd_slot);
case pde of PageTablePDE ptab x xa \<Rightarrow> doE pt <- returnOk (ptrFromPAddr ptab);
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt + (pt_index << 2)) >>=E returnOk
odE | _ \<Rightarrow> throwError (MissingCapability 20)
odE)
theory ArchArch_IF

lemma flush_page_reads_respects:
  "reads_respects aag l \<top> (flush_page page_size pd asid vptr)" by (blast intro: reads_respects_unobservable_unit_return flush_page_states_equiv_for
                   flush_page_cur_thread flush_page_cur_domain flush_page_sched_act
                   flush_page_wuc flush_page_irq_state_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (flush_page page_size pd asid vptr)
theory ArchArch_IF

lemma invalidate_tlb_by_asid_reads_respects:
  "reads_respects aag l (\<lambda>_. True) (invalidate_tlb_by_asid asid)" apply (rule reads_respects_unobservable_unit_return) apply (rule invalidate_tlb_by_asid_states_equiv_for) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (invalidate_tlb_by_asid asid) proof (prove)
goal (6 subgoals):
 1. \<And>P Q R S st. \<lbrace>states_equiv_for P Q R S st\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 6. \<And>P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (irq_state_of_state s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv s. P (irq_state_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma get_master_pte_reads_respects:
  "reads_respects aag l (K (is_subject aag (p && ~~ mask pt_bits))) (get_master_pte p)" unfolding get_master_pte_def apply (wpsimp wp: get_pte_reads_respects hoare_drop_imps) apply (fastforce simp: pt_bits_def pageBits_def mask_lower_twice) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (p && ~~ mask pt_bits))) (get_master_pte p) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (p && ~~ mask pt_bits))) (do pte <- get_pte (p && ~~ mask 6);
case pte of LargePagePTE x xa xb \<Rightarrow> return pte | _ \<Rightarrow> get_pte p
od) proof (prove)
goal (1 subgoal):
 1. is_subject aag (p && ~~ mask pt_bits) \<Longrightarrow> is_subject aag ((p && ~~ mask 6) && ~~ mask pt_bits) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma get_master_pde_reads_respects:
  "reads_respects aag l (K (is_subject aag (x && ~~ mask pd_bits))) (get_master_pde x)" unfolding get_master_pde_def apply (wpsimp wp: get_pde_rev hoare_drop_imps) apply (fastforce simp: pd_bits_def pageBits_def mask_lower_twice) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (x && ~~ mask pd_bits))) (get_master_pde x) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (x && ~~ mask pd_bits))) (do pde <- get_pde (x && ~~ mask 6);
case pde of SuperSectionPDE x xa xb \<Rightarrow> return pde | _ \<Rightarrow> get_pde x
od) proof (prove)
goal (1 subgoal):
 1. is_subject aag (x && ~~ mask pd_bits) \<Longrightarrow> is_subject aag ((x && ~~ mask 6) && ~~ mask pd_bits) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma equiv_asids_arm_asid_table_update:
  "\<lbrakk> equiv_asids R s t; kheap s pool_ptr = kheap t pool_ptr \<rbrakk>
     \<Longrightarrow> equiv_asids R
           (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)
                                                            (asid_high_bits_of asid \<mapsto> pool_ptr)\<rparr>\<rparr>)
           (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := (asid_table t)
                                                            (asid_high_bits_of asid \<mapsto> pool_ptr)\<rparr>\<rparr>)" by (clarsimp simp: equiv_asids_def equiv_asid_def asid_pool_at_kheap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_asids R s t; kheap s pool_ptr = kheap t pool_ptr\<rbrakk> \<Longrightarrow> equiv_asids R (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> pool_ptr)\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := (asid_table t)(asid_high_bits_of asid \<mapsto> pool_ptr)\<rparr>\<rparr>)
theory ArchArch_IF

lemma set_asid_pool_reads_respects:
  "reads_respects aag l \<top> (set_asid_pool ptr pool)" unfolding set_asid_pool_def by (rule set_object_reads_respects)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_asid_pool ptr pool) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_object ptr (ArchObj (ASIDPool pool)))
theory ArchArch_IF

lemma equiv_asids_arm_asid_table_delete:
  "equiv_asids R s t
   \<Longrightarrow> equiv_asids R
         (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None
                                                             else arm_asid_table (arch_state s) a\<rparr>\<rparr>)
         (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None
                                                             else arm_asid_table (arch_state t) a\<rparr>\<rparr>)" by (clarsimp simp: equiv_asids_def equiv_asid_def asid_pool_at_kheap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_asids R s t \<Longrightarrow> equiv_asids R (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table s a\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table t a\<rparr>\<rparr>)
theory ArchArch_IF

lemma set_asid_pool_state_equal_except_kheap:
  "((), s') \<in> fst (set_asid_pool ptr pool s)
   \<Longrightarrow> states_equal_except_kheap_asid s s' \<and>
       (\<forall>p. p \<noteq> ptr \<longrightarrow> kheap s p = kheap s' p) \<and>
       kheap s' ptr = Some (ArchObj (ASIDPool pool)) \<and>
       (\<forall>asid. asid \<noteq> 0
               \<longrightarrow> arm_asid_table (arch_state s) (asid_high_bits_of asid) =
                   arm_asid_table (arch_state s') (asid_high_bits_of asid) \<and>
                   (\<forall>pool_ptr. arm_asid_table (arch_state s) (asid_high_bits_of asid) =
                               Some pool_ptr
                               \<longrightarrow> asid_pool_at pool_ptr s = asid_pool_at pool_ptr s' \<and>
                                   (\<forall>asid_pool asid_pool'. pool_ptr \<noteq> ptr
                                                           \<longrightarrow> kheap s pool_ptr =
                                                               Some (ArchObj (ASIDPool asid_pool)) \<and>
                                                               kheap s' pool_ptr =
                                                               Some (ArchObj (ASIDPool asid_pool'))
                                                               \<longrightarrow> asid_pool (ucast asid) =
                                                                   asid_pool' (ucast asid))))" by (clarsimp simp: set_asid_pool_def put_def bind_def set_object_def get_object_def gets_def
                     get_def return_def assert_def fail_def states_equal_except_kheap_asid_def
                     equiv_for_def obj_at_def
              split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (set_asid_pool ptr pool s) \<Longrightarrow> states_equal_except_kheap_asid s s' \<and> (\<forall>p. p \<noteq> ptr \<longrightarrow> kheap s p = kheap s' p) \<and> kheap s' ptr = Some (ArchObj (ASIDPool pool)) \<and> (\<forall>asid. asid \<noteq> 0 \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr s = typ_at (AArch AASIDPool) pool_ptr s' \<and> (\<forall>asid_pool asid_pool'. pool_ptr \<noteq> ptr \<longrightarrow> kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))))
theory ArchArch_IF

lemma globals_equiv_arm_next_asid_update[simp]:
  "globals_equiv s (t\<lparr>arch_state := arch_state t\<lparr>arm_next_asid := x\<rparr>\<rparr>) = globals_equiv s t" by (simp add: globals_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv s (t\<lparr>arch_state := arch_state t\<lparr>arm_next_asid := x\<rparr>\<rparr>) = globals_equiv s t
theory ArchArch_IF

lemma globals_equiv_arm_asid_table_update[simp]:
  "globals_equiv s (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := x\<rparr>\<rparr>) = globals_equiv s t" by (simp add: globals_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv s (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := x\<rparr>\<rparr>) = globals_equiv s t
theory ArchArch_IF

lemma find_free_hw_asid_globals_equiv[wp]:
  "\<lbrace>globals_equiv s\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding find_free_hw_asid_def by (wp modify_wp invalidate_hw_asid_entry_globals_equiv
         dmo_mol_globals_equiv invalidate_asid_globals_equiv
      | wpc | simp add: invalidateLocalTLB_ASID_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
maybe_asid <- return (find (\<lambda>a. hw_asid_table a = None) (take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid])));
case maybe_asid of None \<Rightarrow> do invalidate_asid $ the $ hw_asid_table next_asid;
do_machine_op $ invalidateLocalTLB_ASID next_asid;
invalidate_hw_asid_entry next_asid;
new_next_asid <- return (next_asid + 1);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := new_next_asid\<rparr>\<rparr>);
return next_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchArch_IF

lemma store_hw_asid_globals_equiv[wp]:
  "store_hw_asid asid hw_asid \<lbrace>globals_equiv s\<rbrace>" unfolding store_hw_asid_def apply (wp find_pd_for_asid_assert_wp | rule modify_wp, simp)+ apply (fastforce simp: globals_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> store_hw_asid asid hw_asid \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do pd <- find_pd_for_asid_assert asid;
asid_map <- gets (arm_asid_map \<circ> arch_state);
asid_map' <- return (asid_map(asid \<mapsto> (hw_asid, pd)));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map'\<rparr>\<rparr>);
hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
hw_asid_map' <- return (hw_asid_map(hw_asid \<mapsto> asid));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv s sa \<Longrightarrow> \<forall>pd. vspace_at_asid asid pd sa \<and> asid \<noteq> 0 \<longrightarrow> globals_equiv s (sa\<lparr>arch_state := arch_state sa\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) sa)(asid \<mapsto> (hw_asid, pd))\<rparr>, arch_state := arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) sa)(asid \<mapsto> (hw_asid, pd))\<rparr>\<rparr>)\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) (sa\<lparr>arch_state := arch_state sa\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) sa)(asid \<mapsto> (hw_asid, pd))\<rparr>\<rparr>))(hw_asid \<mapsto> asid)\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma get_hw_asid_globals_equiv[wp]:
  "get_hw_asid asid \<lbrace>globals_equiv s\<rbrace>" unfolding get_hw_asid_def by (wp store_hw_asid_globals_equiv find_free_hw_asid_globals_equiv load_hw_asid_wp | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> get_hw_asid asid \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- find_free_hw_asid;
store_hw_asid asid new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchArch_IF

lemma invalidate_asid_entry_globals_equiv[wp]:
  "invalidate_asid_entry asid \<lbrace>globals_equiv s\<rbrace>" unfolding invalidate_asid_entry_def by (wpsimp wp: invalidate_hw_asid_entry_globals_equiv
                 invalidate_asid_globals_equiv load_hw_asid_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
when (maybe_hw_asid \<noteq> None) $ invalidate_hw_asid_entry (the maybe_hw_asid);
invalidate_asid asid
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchArch_IF

lemma flush_space_globals_equiv[wp]:
  "flush_space asid \<lbrace>globals_equiv s\<rbrace>" unfolding flush_space_def by (wp dmo_mol_globals_equiv load_hw_asid_wp
      | wpc
      | simp add: invalidateLocalTLB_ASID_def cleanCaches_PoU_def dsb_def
                  invalidate_I_PoU_def clean_D_PoU_def dmo_bind_valid)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> flush_space asid \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op $ invalidateLocalTLB_ASID hw_asid
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchArch_IF

lemma delete_asid_pool_globals_equiv[wp]:
  "delete_asid_pool base ptr \<lbrace>globals_equiv s\<rbrace>" unfolding delete_asid_pool_def by (wpsimp wp: set_vm_root_globals_equiv mapM_wp[OF _ subset_refl] modify_wp
                 invalidate_asid_entry_globals_equiv flush_space_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> delete_asid_pool base ptr \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of base) = Some ptr) $ do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. when (pool (UCAST(32 \<rightarrow> 10) offset) \<noteq> None) $ do flush_space $ base + offset;
invalidate_asid_entry $ base + offset
od) [0 .e. (1 << local.asid_low_bits) - 1];
asid_table' <- return (asid_table(asid_high_bits_of base := 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>_. globals_equiv s\<rbrace>
theory ArchArch_IF

lemma set_pt_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
   set_pt ptr pt
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding set_pt_def apply (wpsimp wp: set_object_globals_equiv[THEN hoare_set_object_weaken_pre]
              simp: a_type_def) apply (fastforce simp: valid_arch_state_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> set_pt ptr pt \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> set_object ptr (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa ko. \<lbrakk>globals_equiv s sa; valid_arch_state sa; ko_at ko ptr sa; AArch APageTable = (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz))\<rbrakk> \<Longrightarrow> ptr \<noteq> arm_global_pd (arch_state sa) \<and> (ptr = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) \<noteq> Some (TCB tcb))) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma set_vm_root_for_flush_globals_equiv[wp]:
  "set_vm_root_for_flush pd asid \<lbrace>globals_equiv s\<rbrace>" unfolding set_vm_root_for_flush_def set_current_pd_def fun_app_def by (wpsimp wp: dmo_mol_globals_equiv hoare_drop_imps hoare_vcg_all_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do tcb <- gets cur_thread;
thread_root_slot <- return (tcb, tcb_cnode_index 1);
thread_root <- get_cap thread_root_slot;
not_is_pd <- case thread_root of ArchObjectCap (PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> pd) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchArch_IF

lemma flush_table_globals_equiv[wp]:
  "flush_table pd asid cptr pt \<lbrace>globals_equiv s\<rbrace>" unfolding flush_table_def invalidateLocalTLB_ASID_def fun_app_def by (wp mapM_wp' dmo_mol_globals_equiv
      | wpc | simp add: do_machine_op_bind split del: if_split cong: if_cong)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> flush_table pd asid cptr pt \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do assert (cptr && mask (pageBitsForSize ARMSection) = 0);
root_switched <- set_vm_root_for_flush pd asid;
maybe_hw_asid <- load_hw_asid asid;
when (maybe_hw_asid \<noteq> None) (do hw_asid <- return (the maybe_hw_asid);
do_machine_op (machine_op_lift (invalidateLocalTLB_ASID_impl hw_asid));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>