kings-crown/FVELER_Isabelle huggingface dataset:
theory Arch_IF

lemma store_word_offs_globals_equiv:
  "store_word_offs ptr offs v \<lbrace>globals_equiv s\<rbrace>" unfolding store_word_offs_def fun_app_def apply (wp do_machine_op_globals_equiv) apply clarsimp apply (erule use_valid[OF _ storeWord_globals_equiv]) apply (wp | simp | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> store_word_offs ptr offs v \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do s <- get;
assert (in_user_frame (ptr + word_of_nat (offs * word_size)) s);
do_machine_op (storeWord (ptr + word_of_nat (offs * word_size)) v)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s x sa saa. \<lbrakk>?P4 s x saa; globals_equiv sa saa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (storeWord (ptr + word_of_nat (offs * word_size)) v (machine_state saa)). globals_equiv sa (saa\<lparr>machine_state := snd x\<rparr>)
 2. \<And>sa. \<lbrace>?B1 sa\<rbrace> assert (in_user_frame (ptr + word_of_nat (offs * word_size)) sa) \<lbrace>\<lambda>x. globals_equiv s and ?P4 sa x\<rbrace>
 3. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 4. \<And>sa. globals_equiv s sa \<Longrightarrow> ?Q sa proof (prove)
goal (4 subgoals):
 1. \<And>s sa saa b. \<lbrakk>?P4 s () saa; globals_equiv sa saa; ((), b) \<in> fst (storeWord (ptr + word_of_nat offs * word_of_nat word_size) v (machine_state saa))\<rbrakk> \<Longrightarrow> globals_equiv sa (saa\<lparr>machine_state := b\<rparr>)
 2. \<And>sa. \<lbrace>?B1 sa\<rbrace> assert (in_user_frame (ptr + word_of_nat (offs * word_size)) sa) \<lbrace>\<lambda>x. globals_equiv s and ?P4 sa x\<rbrace>
 3. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 4. \<And>sa. globals_equiv s sa \<Longrightarrow> ?Q sa proof (prove)
goal (4 subgoals):
 1. \<And>s sa saa b. \<lbrakk>?P4 s () saa; globals_equiv sa saa\<rbrakk> \<Longrightarrow> globals_equiv sa (saa\<lparr>machine_state := machine_state saa\<rparr>)
 2. \<And>sa. \<lbrace>?B1 sa\<rbrace> assert (in_user_frame (ptr + word_of_nat (offs * word_size)) sa) \<lbrace>\<lambda>x. globals_equiv s and ?P4 sa x\<rbrace>
 3. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 4. \<And>sa. globals_equiv s sa \<Longrightarrow> ?Q sa proof (prove)
goal:
No subgoals!
theory Arch_IF

lemma restrict_eq_asn_none: "f(N := None) = f |` {s. s \<noteq> N}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f(N := None) = f |` {s. s \<noteq> N}
theory Arch_IF

lemma thread_set_fault_valid_global_refs[wp]:
  "thread_set (tcb_fault_update A) thread \<lbrace>valid_global_refs\<rbrace>" apply (wp thread_set_global_refs_triv thread_set_refs_trivial thread_set_obj_at_impossible | simp)+ apply (rule ball_tcb_cap_casesI, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> thread_set (tcb_fault_update A) thread \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, v) \<Rightarrow> getF (tcb_fault_update A tcb) = getF tcb
 2. \<And>s. valid_global_refs s \<Longrightarrow> valid_global_refs s proof (prove)
goal:
No subgoals!
theory Arch_IF

lemma cap_swap_for_delete_valid_arch_caps[wp]:
  "cap_swap_for_delete a b \<lbrace>valid_arch_caps\<rbrace>" unfolding cap_swap_for_delete_def apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps\<rbrace> when (a \<noteq> b) $ do cap1 <- get_cap a;
cap2 <- get_cap b;
cap_swap cap1 a cap2 b
od \<lbrace>\<lambda>_. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_arch_caps s \<Longrightarrow> (if a \<noteq> b then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) a s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) b s \<longrightarrow> (valid_arch_caps and cte_wp_at (weak_derived cap) a and cte_wp_at (weak_derived capa) b) s) else valid_arch_caps) s proof (prove)
goal:
No subgoals!
theory Arch_IF

lemma transfer_caps_loop_irq_state[wp]:
  "transfer_caps_loop a b c d e f \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>" by (wp transfer_caps_loop_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> transfer_caps_loop a b c d e f \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
theory Arch_IF

lemma do_machine_op_mol_states_equiv_for:
  "do_machine_op (machine_op_lift f) \<lbrace>states_equiv_for P Q R S st\<rbrace>" apply (simp add: do_machine_op_def) apply (wp modify_wp | simp add: split_def)+ apply (clarify) apply (erule use_valid) apply simp apply (rule mol_states_equiv_for) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>states_equiv_for P Q R S st\<rbrace> do_machine_op (machine_op_lift f) \<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 ms <- gets machine_state;
(r, ms') <- select_f (machine_op_lift f ms);
modify (machine_state_update (\<lambda>_. ms'))
od \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. states_equiv_for P Q R S st s \<Longrightarrow> \<forall>x\<in>fst (machine_op_lift f (machine_state s)). states_equiv_for P Q R S st (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>states_equiv_for P Q R S st s; ((), b) \<in> fst (machine_op_lift f (machine_state s))\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S st (s\<lparr>machine_state := snd ((), b)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s b. states_equiv_for P Q R S st s \<Longrightarrow> \<lbrace>?P13 s b\<rbrace> machine_op_lift f \<lbrace>\<lambda>a b. states_equiv_for P Q R S st (s\<lparr>machine_state := snd (a, b)\<rparr>)\<rbrace>
 2. \<And>s b. states_equiv_for P Q R S st s \<Longrightarrow> ?P13 s b (machine_state s) proof (prove)
goal (2 subgoals):
 1. \<And>s b. states_equiv_for P Q R S st s \<Longrightarrow> \<lbrace>?P13 s b\<rbrace> machine_op_lift f \<lbrace>\<lambda>a b. states_equiv_for P Q R S st (s\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>s b. states_equiv_for P Q R S st s \<Longrightarrow> ?P13 s b (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s b. states_equiv_for P Q R S st s \<Longrightarrow> states_equiv_for P Q R S st (s\<lparr>machine_state := machine_state s\<rparr>)
theory Arch_IF

lemma set_message_info_reads_respects:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects aag l \<top> (set_message_info thread info)" unfolding set_message_info_def fun_app_def by (rule as_user_set_register_reads_respects'[OF domains_distinct])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_message_info thread info) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (as_user thread (setRegister msg_info_register (message_info_to_data info)))
theory Arch_IF

lemma set_mrs_reads_respects:
  "reads_respects aag l (K (aag_can_read aag t \<or> aag_can_affect aag l t)) (set_mrs t buf msgs)" apply (simp add: set_mrs_def cong: option.case_cong_weak) apply (wp mapM_x_ev' store_word_offs_reads_respects set_object_reads_respects
         | wpc | simp add: split_def split del: if_split add: zipWithM_x_mapM_x)+ apply (auto intro: reads_affects_equiv_get_tcb_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag t \<or> aag_can_affect aag l t)) (set_mrs t buf msgs) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. aag_can_read aag t \<or> aag_can_affect aag l t) (do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>));
case buf of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length msgs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) msgs);
return $ nat_to_len $ min (length msgs) msg_max_length
od
od) proof (prove)
goal (1 subgoal):
 1. aag_can_read aag t \<or> aag_can_affect aag l t \<Longrightarrow> \<forall>s ta. reads_equiv aag s ta \<and> affects_equiv aag l s ta \<longrightarrow> get_tcb t s = get_tcb t ta proof (prove)
goal:
No subgoals!
theory Arch_IF

lemma set_message_info_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
   set_message_info thread info
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding set_message_info_def by (wp as_user_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> set_message_info thread info \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> as_user thread $ setRegister msg_info_register $ message_info_to_data info \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory Arch_IF

lemma cancel_badged_sends_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
   cancel_badged_sends epptr badge
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace> " unfolding cancel_badged_sends_def by (wpsimp wp: set_endpoint_globals_equiv set_thread_state_globals_equiv
                 filterM_preserved dxo_wp_weak hoare_drop_imps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> cancel_badged_sends epptr badge \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> do ep <- get_endpoint epptr;
case ep of SendEP queue \<Rightarrow> do set_endpoint epptr IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue');
set_endpoint epptr ep';
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchArch_IF

lemma irq_state_clearExMonitor[wp]:
  "clearExMonitor \<lbrace>\<lambda>s. P (irq_state s)\<rbrace>" by (simp add: clearExMonitor_def | wp modify_wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_state s)\<rbrace> clearExMonitor \<lbrace>\<lambda>_ s. P (irq_state s)\<rbrace>
theory ArchArch_IF

lemma get_tcb_not_asid_pool_at:
  "get_tcb ref s = Some y \<Longrightarrow> \<not> asid_pool_at ref s" by (fastforce simp: get_tcb_def asid_pool_at_kheap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb ref s = Some y \<Longrightarrow> \<not> typ_at (AArch AASIDPool) ref s
theory ArchArch_IF

lemma equiv_asid_machine_state_update[Arch_IF_assms, simp]:
  "equiv_asid asid (machine_state_update f s) s' = equiv_asid asid s s'"
  "equiv_asid asid s (machine_state_update f s') = equiv_asid asid s s'" by (auto simp: equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_asid asid (machine_state_update f s) s' = equiv_asid asid s s' &&& equiv_asid asid s (machine_state_update f s') = equiv_asid asid s s'
theory ArchArch_IF

lemma set_simple_ko_globals_equiv[Arch_IF_assms]:
  "\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
   set_simple_ko f ptr ep
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding set_simple_ko_def apply (wpsimp wp: set_object_globals_equiv[THEN hoare_set_object_weaken_pre] get_object_wp
              simp: partial_inv_def)+ apply (fastforce simp: obj_at_def valid_arch_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa y. \<lbrakk>globals_equiv s sa; valid_arch_state sa; \<forall>ya y'. f ya = f y \<and> f y' = f y \<longrightarrow> ya = y'; ko_at (f y) ptr sa\<rbrakk> \<Longrightarrow> (a_type (f y) = AEndpoint \<longrightarrow> (\<forall>ko. ko_at ko ptr sa \<longrightarrow> a_type (f ep) = a_type ko \<longrightarrow> ptr \<noteq> arm_global_pd (arch_state sa) \<and> (ptr = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. f ep = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> ((\<exists>tcb'. f ep = TCB tcb') \<longrightarrow> tcb_at (idle_thread sa) sa)))) \<and> (a_type (f y) = ANTFN \<longrightarrow> (\<forall>ko. ko_at ko ptr sa \<longrightarrow> a_type (f ep) = a_type ko \<longrightarrow> ptr \<noteq> arm_global_pd (arch_state sa) \<and> (ptr = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. f ep = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> ((\<exists>tcb'. f ep = TCB tcb') \<longrightarrow> tcb_at (idle_thread sa) sa)))) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma set_thread_state_globals_equiv[Arch_IF_assms]:
  "\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
   set_thread_state ref ts
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding set_thread_state_def apply (wp set_object_globals_equiv dxo_wp_weak |simp)+ apply (intro impI conjI allI) apply (clarsimp simp: valid_arch_state_def obj_at_def tcb_at_def2 get_tcb_def is_tcb_def
                    dest: get_tcb_SomeD
                   split: option.splits kernel_object.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> do tcb <- gets_the $ get_tcb ref;
set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
do_extended_op (set_thread_state_ext ref)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv s sa \<and> valid_arch_state sa \<Longrightarrow> (\<exists>y. get_tcb ref sa = Some y) \<longrightarrow> ref \<noteq> arm_global_pd (arch_state sa) \<and> (ref = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch (the (get_tcb (idle_thread sa) sa)))) \<and> tcb_at (idle_thread sa) sa) proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb ref sa = Some y\<rbrakk> \<Longrightarrow> ref \<noteq> arm_global_pd (arch_state sa)
 2. \<And>sa tcb. \<lbrakk>globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb ref sa = Some y; ref = idle_thread sa; kheap sa (idle_thread sa) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch (the (get_tcb (idle_thread sa) sa)))
 3. \<And>sa. \<lbrakk>globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb ref sa = Some y; ref = idle_thread sa\<rbrakk> \<Longrightarrow> tcb_at (idle_thread sa) sa proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma as_user_globals_equiv[Arch_IF_assms]:
  "\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
   as_user tptr f
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding as_user_def apply (wpsimp wp: set_object_globals_equiv simp: split_def) apply (clarsimp simp: valid_arch_state_def get_tcb_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace> as_user tptr f \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace> do tcb <- gets_the $ get_tcb tptr;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object tptr (TCB new_tcb);
return a
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b. \<lbrakk>globals_equiv s sa; valid_arch_state sa; arm_global_pd (arch_state sa) \<noteq> idle_thread sa; get_tcb (arm_global_pd (arch_state sa)) sa = Some y; (a, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); tptr = arm_global_pd (arch_state sa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma not_in_global_not_arm:
  "A \<notin> global_refs s \<Longrightarrow> A \<noteq> arm_global_pd (arch_state s)" by (simp add: global_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<notin> global_refs s \<Longrightarrow> A \<noteq> arm_global_pd (arch_state s)
theory ArchArch_IF

lemma set_pt_reads_respects:
  "reads_respects aag l \<top> (set_pt ptr pt)" unfolding set_pt_def by (rule set_object_reads_respects)

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

lemma get_pt_reads_respects:
  "reads_respects aag l (K (is_subject aag ptr)) (get_pt ptr)" unfolding get_pt_def by (wpsimp wp: get_object_rev hoare_vcg_all_lift hoare_drop_imps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag ptr)) (get_pt ptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag ptr)) (do kobj <- get_object ptr;
case kobj of ArchObj (PageTable pt) \<Rightarrow> return pt | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od)
theory ArchArch_IF

lemma store_pte_reads_respects:
  "reads_respects aag l (K (is_subject aag (p && ~~ mask pt_bits)))
    (store_pte p pte)" unfolding store_pte_def fun_app_def by (wpsimp wp: set_pt_reads_respects get_pt_reads_respects)

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

lemma get_asid_pool_rev:
  "reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (get_asid_pool ptr)" unfolding get_asid_pool_def by (wpsimp wp: get_object_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (get_asid_pool ptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (do kobj <- get_object ptr;
case kobj of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od)
theory ArchArch_IF

lemma asid_high_bits_0_eq_1:
  "asid_high_bits_of 0 = asid_high_bits_of 1" by (auto simp: asid_high_bits_of_def asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_high_bits_of 0 = asid_high_bits_of 1
theory ArchArch_IF

lemma modify_arm_hwasid_table_reads_respects:
  "reads_respects aag l \<top> (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := 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_hwasid_table := 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_hwasid_table := 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_hwasid_table := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_hwasid_table := param\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_hwasid_table := 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_hwasid_table := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_hwasid_table := param\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_hwasid_table := param\<rparr>\<rparr>)
theory ArchArch_IF

lemma modify_arm_asid_map_reads_respects:
  "reads_respects aag l \<top> (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := 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_asid_map := 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_asid_map := 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_asid_map := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_map := param\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_map := 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_asid_map := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_map := param\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := param\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_map := param\<rparr>\<rparr>)