kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchArch_IF

lemma modify_arm_next_asid_reads_respects:
  "reads_respects aag l \<top> (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := param\<rparr>\<rparr>))" apply (simp add: equiv_valid_def2) apply (rule modify_ev2) 
  (* slow 5s *)
   by (auto simp: reads_equiv_def affects_equiv_def states_equiv_for_def equiv_for_def
          intro: equiv_asids_triv' split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := param\<rparr>\<rparr>)) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := param\<rparr>\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv aag (s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_next_asid := param\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_next_asid := param\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv aag (s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_next_asid := param\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_next_asid := param\<rparr>\<rparr>)
theory ArchArch_IF

lemma states_equiv_for_arm_hwasid_table_update1:
  "states_equiv_for P Q R S (s\<lparr>arch_state := (arch_state s)\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) t =
   states_equiv_for P Q R S s t" by (clarsimp simp: states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) t = states_equiv_for P Q R S s t
theory ArchArch_IF

lemma states_equiv_for_arm_hwasid_table_update2:
  "states_equiv_for P Q R S t (s\<lparr>arch_state := (arch_state s)\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) =
   states_equiv_for P Q R S t s" apply (rule iffI) apply (drule states_equiv_for_sym) apply (rule states_equiv_for_sym) apply (simp add: states_equiv_for_arm_hwasid_table_update1) apply (drule states_equiv_for_sym) apply (rule states_equiv_for_sym) apply (simp add: states_equiv_for_arm_hwasid_table_update1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) = states_equiv_for P Q R S t s proof (prove)
goal (2 subgoals):
 1. states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) \<Longrightarrow> states_equiv_for P Q R S t s
 2. states_equiv_for P Q R S t s \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. states_equiv_for P Q R S (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) t \<Longrightarrow> states_equiv_for P Q R S t s
 2. states_equiv_for P Q R S t s \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. states_equiv_for P Q R S (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) t \<Longrightarrow> states_equiv_for P Q R S s t
 2. states_equiv_for P Q R S t s \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S t s \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S s t \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S s t \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) t proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma states_equiv_for_arm_hwasid_table_update':
  "states_equiv_for P Q R S t (s\<lparr>arch_state := (arch_state s)\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) =
   states_equiv_for P Q R S t s" by (rule states_equiv_for_arm_hwasid_table_update2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := Y\<rparr>\<rparr>) = states_equiv_for P Q R S t s
theory ArchArch_IF

lemma states_equiv_for_arm_next_asid_update1:
  "states_equiv_for P Q R S (s\<lparr>arch_state := (arch_state s)\<lparr>arm_next_asid := Y\<rparr>\<rparr>) t =
   states_equiv_for P Q R S s t" by (clarsimp simp: states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S (s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := Y\<rparr>\<rparr>) t = states_equiv_for P Q R S s t
theory ArchArch_IF

lemma states_equiv_for_arm_next_asid_update2:
  "states_equiv_for P Q R S t (s\<lparr>arch_state := (arch_state s)\<lparr>arm_next_asid := X\<rparr>\<rparr>)
     = states_equiv_for P Q R S t s" by (clarsimp simp: states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := X\<rparr>\<rparr>) = states_equiv_for P Q R S t s
theory ArchArch_IF

lemma states_equiv_for_arm_asid_map_update1:
  "states_equiv_for P Q R S (s\<lparr>arch_state := (arch_state s)\<lparr>arm_asid_map := X\<rparr>\<rparr>) t
     = states_equiv_for P Q R S s t" by (clarsimp simp: states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := X\<rparr>\<rparr>) t = states_equiv_for P Q R S s t
theory ArchArch_IF

lemma states_equiv_for_arm_asid_map_update2:
  "states_equiv_for P Q R S t (s\<lparr>arch_state := (arch_state s)\<lparr>arm_asid_map := X\<rparr>\<rparr>)
     = states_equiv_for P Q R S t s" by (clarsimp simp: states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S t (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := X\<rparr>\<rparr>) = states_equiv_for P Q R S t s
theory ArchArch_IF

lemma load_hw_asid_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag \<top>\<top> \<top> (load_hw_asid asid)" by (rule equiv_valid_2_unobservable; wpsimp simp: load_hw_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>_. True) (load_hw_asid asid)
theory ArchArch_IF

lemma states_equiv_for_arch_update1:
  "arm_asid_table A = arm_asid_table (arch_state s)
   \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>arch_state := A\<rparr>) t =
       states_equiv_for P Q R S s t" by (clarsimp simp: states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_asid_table A = asid_table s \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>arch_state := A\<rparr>) t = states_equiv_for P Q R S s t
theory ArchArch_IF

lemma states_equiv_for_arch_update2:
  "arm_asid_table A = arm_asid_table (arch_state s)
   \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := A\<rparr>) =
       states_equiv_for P Q R S t s" apply (rule iffI) apply (drule states_equiv_for_sym) apply (rule states_equiv_for_sym) apply (simp add: states_equiv_for_arch_update1) apply (drule states_equiv_for_sym) apply (rule states_equiv_for_sym) apply (simp add: states_equiv_for_arch_update1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_asid_table A = asid_table s \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := A\<rparr>) = states_equiv_for P Q R S t s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>arm_asid_table A = asid_table s; states_equiv_for P Q R S t (s\<lparr>arch_state := A\<rparr>)\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S t s
 2. \<lbrakk>arm_asid_table A = asid_table s; states_equiv_for P Q R S t s\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := A\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>arm_asid_table A = asid_table s; states_equiv_for P Q R S (s\<lparr>arch_state := A\<rparr>) t\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S t s
 2. \<lbrakk>arm_asid_table A = asid_table s; states_equiv_for P Q R S t s\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := A\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>arm_asid_table A = asid_table s; states_equiv_for P Q R S (s\<lparr>arch_state := A\<rparr>) t\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S s t
 2. \<lbrakk>arm_asid_table A = asid_table s; states_equiv_for P Q R S t s\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := A\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arm_asid_table A = asid_table s; states_equiv_for P Q R S t s\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := A\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arm_asid_table A = asid_table s; states_equiv_for P Q R S s t\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S t (s\<lparr>arch_state := A\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arm_asid_table A = asid_table s; states_equiv_for P Q R S s t\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>arch_state := A\<rparr>) t proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma find_free_hw_asid_states_equiv_for:
  "find_free_hw_asid \<lbrace>states_equiv_for P Q R S st\<rbrace>" unfolding find_free_hw_asid_def by (wpsimp wp: invalidate_hw_asid_entry_states_equiv_for
                 do_machine_op_mol_states_equiv_for invalidate_asid_states_equiv_for
           simp: states_equiv_for_arm_next_asid_update invalidateLocalTLB_ASID_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>states_equiv_for P Q R S st\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>states_equiv_for P Q R S st\<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>_. states_equiv_for P Q R S st\<rbrace>
theory ArchArch_IF

lemma arm_context_switch_reads_respects:
  "reads_respects aag l \<top> (arm_context_switch pd asid)" unfolding arm_context_switch_def apply (rule equiv_valid_guard_imp) apply (rule reads_respects_unobservable_unit_return) apply (wp do_machine_op_mol_states_equiv_for get_hw_asid_states_equiv_for
               | simp add: set_current_pd_def setHardwareASID_def
                           writeTTBR0_def dsb_def isb_def dmo_bind_valid)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (arm_context_switch pd asid) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do hwasid <- get_hw_asid asid;
do_machine_op $ do set_current_pd $ addrFromPPtr pd;
setHardwareASID hwasid
od
od) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (do hwasid <- get_hw_asid asid;
do_machine_op $ do set_current_pd $ addrFromPPtr pd;
setHardwareASID hwasid
od
od)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>P Q R S st. \<lbrace>states_equiv_for P Q R S st\<rbrace> do hwasid <- get_hw_asid asid;
do_machine_op $ do set_current_pd $ addrFromPPtr pd;
setHardwareASID hwasid
od
od \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do hwasid <- get_hw_asid asid;
do_machine_op $ do set_current_pd $ addrFromPPtr pd;
setHardwareASID hwasid
od
od \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> do hwasid <- get_hw_asid asid;
do_machine_op $ do set_current_pd $ addrFromPPtr pd;
setHardwareASID hwasid
od
od \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do hwasid <- get_hw_asid asid;
do_machine_op $ do set_current_pd $ addrFromPPtr pd;
setHardwareASID hwasid
od
od \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do hwasid <- get_hw_asid asid;
do_machine_op $ do set_current_pd $ addrFromPPtr pd;
setHardwareASID hwasid
od
od \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 6. \<And>P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do hwasid <- get_hw_asid asid;
do_machine_op $ do set_current_pd $ addrFromPPtr pd;
setHardwareASID hwasid
od
od \<lbrace>\<lambda>rv s. P (irq_state_of_state s)\<rbrace>
 7. \<And>s. True \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma arm_context_switch_states_equiv_for:
  "arm_context_switch pd asid \<lbrace>states_equiv_for P Q R S st\<rbrace>" unfolding arm_context_switch_def by (wp do_machine_op_mol_states_equiv_for get_hw_asid_states_equiv_for
      | simp add: set_current_pd_def setHardwareASID_def
                  dmo_bind_valid dsb_def isb_def writeTTBR0_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>states_equiv_for P Q R S st\<rbrace> arm_context_switch pd asid \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>states_equiv_for P Q R S st\<rbrace> do hwasid <- get_hw_asid asid;
do_machine_op $ do set_current_pd $ addrFromPPtr pd;
setHardwareASID hwasid
od
od \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
theory ArchArch_IF

lemma set_vm_root_states_equiv_for[wp]:
  "set_vm_root thread \<lbrace>states_equiv_for P Q R S st\<rbrace>" unfolding set_vm_root_def catch_def fun_app_def set_current_pd_def isb_def dsb_def writeTTBR0_def by (wpsimp wp: arm_context_switch_states_equiv_for do_machine_op_mol_states_equiv_for
                 hoare_vcg_all_lift whenE_wp hoare_drop_imps
           simp: dmo_bind_valid if_apply_def2)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>states_equiv_for P Q R S st\<rbrace> set_vm_root thread \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>states_equiv_for P Q R S st\<rbrace> do thread_root_slot <- return (thread, tcb_cnode_index 1);
thread_root <- get_cap thread_root_slot;
x <- case thread_root of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') (throwError InvalidRoot);
liftE (arm_context_switch pd asid)
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot;
case x of Inl e \<Rightarrow> do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (do machine_op_lift dsb_impl;
machine_op_lift (writeTTBR0_impl (addrFromKPPtr global_pd && 0xFFFFE000 || 0x18));
machine_op_lift isb_impl
od)
od | Inr b \<Rightarrow> return b
od \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
theory ArchArch_IF

lemma set_vm_root_reads_respects:
  "reads_respects aag l \<top> (set_vm_root tcb)" by (rule reads_respects_unobservable_unit_return) wp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_vm_root tcb)
theory ArchArch_IF

lemma get_pte_reads_respects:
  "reads_respects aag l (K (is_subject aag (ptr && ~~ mask pt_bits))) (get_pte ptr)" unfolding get_pte_def fun_app_def by (wpsimp wp: get_pt_reads_respects)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (ptr && ~~ mask pt_bits))) (get_pte ptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (ptr && ~~ mask pt_bits))) (do base <- return (ptr && ~~ mask pt_bits);
offset <- return (ptr && mask pt_bits >> 2);
pt <- get_pt base;
return (pt (UCAST(32 \<rightarrow> 8) offset))
od)
theory ArchArch_IF

lemma page_table_mapped_reads_respects:
  "reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs
                                         and K (is_subject_asid aag asid))
                  (page_table_mapped asid vaddr pt)" unfolding page_table_mapped_def catch_def fun_app_def by (wpsimp wp: get_pde_rev find_pd_for_asid_reads_respects)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (is_subject_asid aag asid)) (page_table_mapped asid vaddr pt) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (is_subject_asid aag asid)) (do x <- doE pd <- find_pd_for_asid asid;
pd_slot <- returnOk (lookup_pd_slot pd vaddr);
liftE (get_pde pd_slot) >>=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;
case x of Inl e \<Rightarrow> K (return None) e | Inr b \<Rightarrow> return b
od)
theory ArchArch_IF

lemma unmap_page_table_reads_respects:
  "reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs
                                         and K (is_subject_asid aag asid))
                  (unmap_page_table asid vaddr pt)" unfolding unmap_page_table_def fun_app_def page_table_mapped_def by (wp dmo_mol_reads_respects store_pde_reads_respects get_pde_rev
         flush_table_reads_respects find_pd_for_asid_reads_respects hoare_vcg_all_lift_R
      | wpc | simp add: cleanByVA_PoU_def | wp (once) hoare_drop_imps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (is_subject_asid aag asid)) (unmap_page_table asid vaddr pt) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (is_subject_asid aag asid)) (do pdOpt <- doE pd <- find_pd_for_asid asid;
pd_slot <- returnOk (lookup_pd_slot pd vaddr);
pde <- liftE (get_pde pd_slot);
case pde of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr pt = addr then Some pd else None) | _ \<Rightarrow> returnOk None
odE <catch> K (return None);
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do pd_slot <- return (lookup_pd_slot pd vaddr);
store_pde pd_slot InvalidPDE;
do_machine_op (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot));
flush_table pd asid vaddr pt
od
od)
theory ArchArch_IF

lemma do_flush_reads_respects:
  "reads_respects aag l \<top> (do_machine_op (do_flush typ start end pstart))" apply (cases "typ") by (wp dmo_mol_reads_respects dmo_cacheRangeOp_reads_respects
      | simp add: do_flush_def cache_machine_op_defs do_flush_defs dmo_bind_ev when_def
      | rule conjI | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (do_flush typ start end pstart)) proof (prove)
goal (4 subgoals):
 1. typ = Clean \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (do_flush typ start end pstart))
 2. typ = Invalidate \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (do_flush typ start end pstart))
 3. typ = CleanInvalidate \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (do_flush typ start end pstart))
 4. typ = Unify \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (do_flush typ start end pstart))
theory ArchArch_IF

lemma perform_page_directory_invocation_reads_respects:
  "reads_respects aag l (is_subject aag \<circ> cur_thread) (perform_page_directory_invocation pdi)" unfolding perform_page_directory_invocation_def apply (cases pdi) by (wp do_flush_reads_respects set_vm_root_reads_respects set_vm_root_for_flush_reads_respects
      | simp add: when_def requiv_cur_thread_eq split del: if_split
      | wp (once) hoare_drop_imps | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (is_subject aag \<circ> cur_thread) (perform_page_directory_invocation pdi) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (is_subject aag \<circ> cur_thread) (case pdi of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return ()) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. pdi = PageDirectoryFlush x11 x12 x13 x14 x15 x16 \<Longrightarrow> reads_respects aag l (is_subject aag \<circ> cur_thread) (case pdi of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return ())
 2. pdi = PageDirectoryNothing \<Longrightarrow> reads_respects aag l (is_subject aag \<circ> cur_thread) (case pdi of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return ())