kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_IF

lemma states_equiv_for_detype:
  "states_equiv_for P Q R S s s' \<Longrightarrow> states_equiv_for P Q R S (detype N s) (detype N s')" apply (simp add: states_equiv_for_def equiv_for_def equiv_asids_def obj_at_def equiv_asid_detype) apply (simp add: detype_def detype_ext_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S s s' \<Longrightarrow> states_equiv_for P Q R S (detype N s) (detype N s') proof (prove)
goal (1 subgoal):
 1. (\<forall>x. P x \<longrightarrow> kheap s x = kheap s' x) \<and> (\<forall>x. P x \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x) \<and> (\<forall>x. P x \<longrightarrow> device_state (machine_state s) x = device_state (machine_state s') x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt s' (a, b))) \<and> (\<forall>x. P x \<longrightarrow> ekheap s x = ekheap s' x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list s' (a, b))) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap s' (a, b))) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_states s x = interrupt_states s' x) \<and> (\<forall>x. Q x \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node s' x) \<and> (\<forall>x. S x \<longrightarrow> ready_queues s x = ready_queues s' x) \<and> (\<forall>asid. asid \<noteq> 0 \<and> R asid \<longrightarrow> equiv_asid asid s s') \<Longrightarrow> (\<forall>x. P x \<longrightarrow> kheap (detype N s) x = kheap (detype N s') x) \<and> (\<forall>x. P x \<longrightarrow> underlying_memory (machine_state (detype N s)) x = underlying_memory (machine_state (detype N s')) x) \<and> (\<forall>x. P x \<longrightarrow> device_state (machine_state (detype N s)) x = device_state (machine_state (detype N s')) x) \<and> (\<forall>x. P x \<longrightarrow> ekheap (detype N s) x = ekheap (detype N s') x) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. cdt_list (detype N s) (a, b) = cdt_list (detype N s') (a, b))) \<and> (\<forall>a. P a \<longrightarrow> (\<forall>b. is_original_cap (detype N s) (a, b) = is_original_cap (detype N s') (a, b))) \<and> (\<forall>x. S x \<longrightarrow> ready_queues (detype N s) x = ready_queues (detype N s') x) proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma detype_reads_respects:
  "reads_respects aag l \<top> (modify (detype S))" apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def in_monad reads_equiv_def2 affects_equiv_def2) apply (simp add: cur_domain_detype cur_thread_detype sched_act_detype wuc_detype machine_state_detype) apply (fastforce intro: states_equiv_for_detype) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (modify (detype S)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) s t\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) (detype S s) (detype S t) \<and> cur_thread (detype S s) = cur_thread (detype S t) \<and> cur_domain (detype S s) = cur_domain (detype S t) \<and> scheduler_action (detype S s) = scheduler_action (detype S t) \<and> work_units_completed (detype S s) = work_units_completed (detype S t) \<and> equiv_irq_state (machine_state (detype S s)) (machine_state (detype S t)) \<and> states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) (detype S s) (detype S t) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) s t\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) (detype S s) (detype S t) \<and> states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) (detype S s) (detype S t) proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma untyped_caps_do_not_overlap_global_refs:
  "\<lbrakk> cte_wp_at ((=) (UntypedCap dev word sz idx)) slot s; valid_global_refs s \<rbrakk>
     \<Longrightarrow> ptr_range word sz \<inter> global_refs s = {}" apply (simp add: cte_wp_at_caps_of_state) apply (drule (1) valid_global_refsD2) apply (fastforce simp: cap_range_def ptr_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev word sz idx)) slot s; valid_global_refs s\<rbrakk> \<Longrightarrow> ptr_range word sz \<inter> global_refs s = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some (UntypedCap dev word sz idx); valid_global_refs s\<rbrakk> \<Longrightarrow> ptr_range word sz \<inter> global_refs s = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_refs s; global_refs s \<inter> cap_range (UntypedCap dev word sz idx) = {}\<rbrakk> \<Longrightarrow> ptr_range word sz \<inter> global_refs s = {} proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma singleton_set_size:
  "{ptr..(ptr::'a::len word) + 2 ^ 0 - 1} = {ptr}" by (simp add: field_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {ptr..ptr + 2 ^ 0 - 1} = {ptr}
theory Retype_IF

lemma cap_range_of_valid_capD:
  "valid_cap cap s \<Longrightarrow> (cap_range cap = {}) \<or> (\<exists>ptr sz. (cap_range cap = ptr_range ptr sz))" apply (rule disj_subst) apply (cases cap) by (clarsimp simp: valid_cap_def valid_untyped_def cap_aligned_def cap_range_def ptr_range_def
      | intro exI | rule singleton_set_size[symmetric] | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> cap \<Longrightarrow> cap_range cap = {} \<or> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz) proof (prove)
goal (1 subgoal):
 1. s \<turnstile> cap \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz) proof (prove)
goal (12 subgoals):
 1. \<lbrakk>s \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
 2. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
 3. \<And>x31 x32 x33. \<lbrakk>s \<turnstile> cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
 4. \<And>x41 x42 x43. \<lbrakk>s \<turnstile> cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
 5. \<And>x51 x52 x53. \<lbrakk>s \<turnstile> cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
 6. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> cap; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
 7. \<And>x7. \<lbrakk>s \<turnstile> cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
 8. \<lbrakk>s \<turnstile> cap; cap = DomainCap\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
 9. \<lbrakk>s \<turnstile> cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
 10. \<And>x10. \<lbrakk>s \<turnstile> cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} \<longrightarrow> (\<exists>ptr sz. cap_range cap = ptr_range ptr sz)
A total of 12 subgoals...
theory Retype_IF

lemma set_cap_reads_respects_g:
  "reads_respects_g aag l (valid_global_objs and valid_arch_state
                                             and K (is_subject aag (fst slot))) (set_cap cap slot)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g[OF set_cap_reads_respects]) apply (wp doesnt_touch_globalsI set_cap_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (valid_global_objs and valid_arch_state and K (is_subject aag (fst slot))) (set_cap cap slot) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (set_cap cap slot)
 2. \<And>s. (valid_global_objs and valid_arch_state and K (is_subject aag (fst slot))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (set_cap cap slot)
 2. \<And>s. (valid_global_objs and valid_arch_state and K (is_subject aag (fst slot))) s \<Longrightarrow> (K (aag_can_read aag (fst slot)) and ?Q3) s proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma when_ev:
  "(C \<Longrightarrow> equiv_valid I A A P handle) \<Longrightarrow> equiv_valid I A A (\<lambda>s. C \<longrightarrow> P s) (when C handle)" by (wp | auto simp: when_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (C \<Longrightarrow> equiv_valid_inv I A P handle) \<Longrightarrow> equiv_valid_inv I A (\<lambda>s. C \<longrightarrow> P s) (when C handle)
theory Retype_IF

lemma get_cap_reads_respects_g:
  "reads_respects_g aag l (K (is_subject aag (fst slot))) (get_cap slot)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g[OF get_cap_rev]) apply (rule doesnt_touch_globalsI) apply wp apply clarsimp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (K (is_subject aag (fst slot))) (get_cap slot) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (get_cap slot)
 2. \<And>s. K (is_subject aag (fst slot)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (get_cap slot)
 2. \<And>s. K (is_subject aag (fst slot)) s \<Longrightarrow> (K (aag_can_read aag (fst slot)) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q3\<rbrace> get_cap slot \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. K (is_subject aag (fst slot)) s \<Longrightarrow> (K (aag_can_read aag (fst slot)) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st s. (globals_equiv st and ?Q3) s \<Longrightarrow> globals_equiv st s
 2. \<And>s. K (is_subject aag (fst slot)) s \<Longrightarrow> (K (aag_can_read aag (fst slot)) and ?Q3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. K (is_subject aag (fst slot)) s \<Longrightarrow> (K (aag_can_read aag (fst slot)) and ?Q3) s proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma irq_state_independent_globals_equiv[simp,intro!]:
  "irq_state_independent_A (globals_equiv st)" by (clarsimp simp: irq_state_independent_A_def globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_independent_A (globals_equiv st)
theory Retype_IF

lemma irq_state_independent_A_only_timer_irq_inv[simp]:
  "irq_state_independent_A (only_timer_irq_inv irq st)" apply (simp add: only_timer_irq_inv_def) apply (rule irq_state_independent_A_conjI) apply (simp add: domain_sep_inv_def) apply (simp add: irq_state_independent_A_def only_timer_irq_def
                   irq_is_recurring_def is_irq_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_independent_A (only_timer_irq_inv irq st) proof (prove)
goal (1 subgoal):
 1. irq_state_independent_A (domain_sep_inv False st and only_timer_irq irq) proof (prove)
goal (2 subgoals):
 1. irq_state_independent_A (domain_sep_inv False st)
 2. irq_state_independent_A (only_timer_irq irq) proof (prove)
goal (1 subgoal):
 1. irq_state_independent_A (only_timer_irq irq) proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma only_timer_irq_inv_work_units_completed[simp]:
  "only_timer_irq_inv irq st (work_units_completed_update f s)
    = only_timer_irq_inv irq st s" apply (simp add: only_timer_irq_inv_def) apply (simp add: domain_sep_inv_def) apply (simp add: irq_state_independent_A_def only_timer_irq_def
                   irq_is_recurring_def is_irq_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_timer_irq_inv irq st (work_units_completed_update f s) = only_timer_irq_inv irq st s proof (prove)
goal (1 subgoal):
 1. (domain_sep_inv False st s \<and> only_timer_irq irq (work_units_completed_update f s)) = (domain_sep_inv False st s \<and> only_timer_irq irq s) proof (prove)
goal (1 subgoal):
 1. ((\<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s) \<and> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st) \<and> only_timer_irq irq (work_units_completed_update f s)) = ((\<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s) \<and> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st) \<and> only_timer_irq irq s) proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma ex_tupleI:
  "P (fst t) (snd t) \<Longrightarrow> \<exists>a b. P a b" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (fst t) (snd t) \<Longrightarrow> \<exists>a b. P a b
theory Retype_IF

lemma equiv_valid_obtain:
  assumes fn_eq: "\<And>s t. I s t \<Longrightarrow> A s t \<Longrightarrow> P s \<Longrightarrow> P t \<Longrightarrow>  fn s = fn t"
  assumes pr: "\<And>x. equiv_valid I A B (P and (\<lambda>s. fn s = x)) f"
  shows "equiv_valid I A B P f" apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def) apply (frule(1) fn_eq, simp+) apply (cut_tac x="fn s" in pr) apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P f proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; I s t; A s t\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> B b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; I s t; A s t; fn s = fn t\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> B b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; I s t; A s t; fn s = fn t; equiv_valid I A B (P and (\<lambda>sa. fn sa = fn s)) f\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> B b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; I s t; A s t; fn s = fn t; \<forall>s ta. P s \<and> fn s = fn t \<and> P ta \<and> fn ta = fn t \<and> I s ta \<and> A s ta \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f ta). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> B s' t')\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> B b ba proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma reads_equiv_cte_wp_at:
  "\<lbrakk> reads_equiv aag s s'; is_subject aag (fst slot) \<rbrakk>
     \<Longrightarrow> cte_wp_at P slot s = cte_wp_at P slot s'" apply (frule(1) is_subject_kheap_eq) apply (simp add: cte_wp_at_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s = cte_wp_at P slot s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; is_subject aag (fst slot); kheap s (fst slot) = kheap s' (fst slot)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s = cte_wp_at P slot s' proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma reads_equiv_caps_of_state:
  "\<lbrakk> reads_equiv aag s s'; is_subject aag (fst slot) \<rbrakk>
     \<Longrightarrow> caps_of_state s slot = caps_of_state s' slot" apply (frule(1) reads_equiv_cte_wp_at[where P="(=) (the (caps_of_state s slot))"]) apply (frule(1) reads_equiv_cte_wp_at[where P="\<top>"]) apply (auto simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> caps_of_state s slot = caps_of_state s' slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; is_subject aag (fst slot); cte_wp_at ((=) (the (caps_of_state s slot))) slot s = cte_wp_at ((=) (the (caps_of_state s slot))) slot s'\<rbrakk> \<Longrightarrow> caps_of_state s slot = caps_of_state s' slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; is_subject aag (fst slot); cte_wp_at ((=) (the (caps_of_state s slot))) slot s = cte_wp_at ((=) (the (caps_of_state s slot))) slot s'; cte_wp_at (\<lambda>_. True) slot s = cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> caps_of_state s slot = caps_of_state s' slot proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma cacheRangeOp_ev[wp]:
  "(\<And>a b. equiv_valid_inv I A \<top> (oper a b))
   \<Longrightarrow> equiv_valid_inv I A \<top> (cacheRangeOp oper x y z)" apply (simp add: cacheRangeOp_def split_def) apply (rule mapM_x_ev) apply simp apply (rule hoare_TrueI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. equiv_valid_inv I A (\<lambda>_. True) (oper a b)) \<Longrightarrow> equiv_valid_inv I A (\<lambda>_. True) (cacheRangeOp oper x y z) proof (prove)
goal (1 subgoal):
 1. (\<And>a b. equiv_valid_inv I A (\<lambda>_. True) (oper a b)) \<Longrightarrow> equiv_valid_inv I A (\<lambda>_. True) (mapM_x (\<lambda>p. oper (fst p) (snd p)) (zip [lineStart x , lineStart x + word_of_nat cacheLine .e. lineStart y] [lineStart z , lineStart z + word_of_nat cacheLine .e. lineStart (z + (y - x))])) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<And>a b. equiv_valid_inv I A (\<lambda>_. True) (oper a b); xa \<in> set (zip [lineStart x , lineStart x + word_of_nat cacheLine .e. lineStart y] [lineStart z , lineStart z + word_of_nat cacheLine .e. lineStart (z + (y - x))])\<rbrakk> \<Longrightarrow> equiv_valid_inv I A (\<lambda>_. True) (oper (fst xa) (snd xa))
 2. \<And>xa. \<lbrakk>\<And>a b. equiv_valid_inv I A (\<lambda>_. True) (oper a b); xa \<in> set (zip [lineStart x , lineStart x + word_of_nat cacheLine .e. lineStart y] [lineStart z , lineStart z + word_of_nat cacheLine .e. lineStart (z + (y - x))])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> oper (fst xa) (snd xa) \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>a b. equiv_valid_inv I A (\<lambda>_. True) (oper a b); xa \<in> set (zip [lineStart x , lineStart x + word_of_nat cacheLine .e. lineStart y] [lineStart z , lineStart z + word_of_nat cacheLine .e. lineStart (z + (y - x))])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> oper (fst xa) (snd xa) \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma cleanCacheRange_PoU_ev:
  "equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) \<top> (cleanCacheRange_PoU vs ve ps)" unfolding cleanCacheRange_PoU_def by (wp machine_op_lift_ev | simp add: cleanByVA_PoU_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (cleanCacheRange_PoU vs ve ps) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (cacheRangeOp cleanByVA_PoU vs ve ps)
theory ArchRetype_IF

lemma modify_underlying_memory_update_0_ev:
  "equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) \<top>
                   (modify (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 3,
                                                            x + 1 := word_rsplit 0 ! 2,
                                                            x + 2 := word_rsplit 0 ! 1,
                                                            x + 3 := word_rsplit 0 ! 0))))" apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def in_monad) apply (fastforce intro: equiv_forI elim: equiv_forE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (modify (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 3, x + 1 := word_rsplit 0 ! 2, x + 2 := word_rsplit 0 ! 1, x + 3 := word_rsplit 0 ! 0)))) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>equiv_for P underlying_memory s t; equiv_for P device_state s t; equiv_for Q underlying_memory s t; equiv_for Q device_state s t\<rbrakk> \<Longrightarrow> equiv_for P underlying_memory (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 3, x + 1 := word_rsplit 0 ! 2, x + 2 := word_rsplit 0 ! Suc 0, x + 3 := word_rsplit 0 ! 0)) s) (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 3, x + 1 := word_rsplit 0 ! 2, x + 2 := word_rsplit 0 ! Suc 0, x + 3 := word_rsplit 0 ! 0)) t) \<and> equiv_for P device_state (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 3, x + 1 := word_rsplit 0 ! 2, x + 2 := word_rsplit 0 ! Suc 0, x + 3 := word_rsplit 0 ! 0)) s) (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 3, x + 1 := word_rsplit 0 ! 2, x + 2 := word_rsplit 0 ! Suc 0, x + 3 := word_rsplit 0 ! 0)) t) \<and> equiv_machine_state Q (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 3, x + 1 := word_rsplit 0 ! 2, x + 2 := word_rsplit 0 ! Suc 0, x + 3 := word_rsplit 0 ! 0)) s) (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 3, x + 1 := word_rsplit 0 ! 2, x + 2 := word_rsplit 0 ! Suc 0, x + 3 := word_rsplit 0 ! 0)) t) proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma storeWord_ev:
  "equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) \<top> (storeWord x 0)" unfolding storeWord_def by (wp modify_underlying_memory_update_0_ev assert_inv | simp add: no_irq_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (storeWord x 0) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (do assert (x && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 3, x + 1 := word_rsplit 0 ! 2, x + 2 := word_rsplit 0 ! 1, x + 3 := word_rsplit 0 ! 0)))
od)