kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchADT_AI

lemma lookup_pt_slot_fail:
  "is_aligned pd pd_bits \<Longrightarrow>
   lookup_pt_slot pd vptr s = ({},True) \<longleftrightarrow>
   (\<forall>pdo. kheap s pd \<noteq> Some (ArchObj (PageDirectory pdo)))" apply (frule pd_shifting'[of _ vptr]) by (auto simp add: lookup_pt_slot_def lookup_pd_slot_def liftE_def bindE_def
        returnOk_def lift_def bind_def split_def throwError_def return_def
        get_pde_def get_pd_def Union_eq get_object_def simpler_gets_def
        assert_def fail_def mask_eqs
      split: sum.splits if_split_asm Structures_A.kernel_object.splits
             arch_kernel_obj.splits pde.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> (lookup_pt_slot pd vptr s = ({}, True)) = (\<forall>pdo. kheap s pd \<noteq> Some (ArchObj (PageDirectory pdo))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd\<rbrakk> \<Longrightarrow> (lookup_pt_slot pd vptr s = ({}, True)) = (\<forall>pdo. kheap s pd \<noteq> Some (ArchObj (PageDirectory pdo)))
theory ArchADT_AI

lemma shiftr_shiftl_mask_pd_bits:
  "(((vptr :: word32) >> 20) << 2) && mask pd_bits = (vptr >> 20) << 2" apply (rule iffD2 [OF mask_eq_iff_w2p]) apply (simp add: pd_bits_def pageBits_def word_size) apply (rule shiftl_less_t2n) apply (simp_all add: pd_bits_def word_bits_def pageBits_def word_size) apply (cut_tac shiftr_less_t2n'[of vptr 20 12]) apply simp apply (simp add: mask_eq_iff) apply (cut_tac lt2p_lem[of 32 vptr], simp) apply (cut_tac word_bits_len_of, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2 proof (prove)
goal (2 subgoals):
 1. pd_bits < size (vptr >> 20 << 2)
 2. vptr >> 20 << 2 < 2 ^ pd_bits proof (prove)
goal (1 subgoal):
 1. vptr >> 20 << 2 < 2 ^ pd_bits proof (prove)
goal (2 subgoals):
 1. vptr >> 20 < 2 ^ (pd_bits - 2)
 2. pd_bits < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. vptr >> 20 < 0x1000 proof (prove)
goal (3 subgoals):
 1. vptr >> 20 < 2 ^ 12 \<Longrightarrow> vptr >> 20 < 0x1000
 2. vptr && mask (20 + 12) = vptr
 3. 12 < LENGTH(32) proof (prove)
goal (2 subgoals):
 1. vptr && mask (20 + 12) = vptr
 2. 12 < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. 12 < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. LENGTH(32) \<le> 32 proof (prove)
goal:
No subgoals!
theory ADT_AI

lemma lift_state_relationD:
  "(((tc, s), m, e), ((tc', s'), m', e')) \<in> lift_state_relation R \<Longrightarrow>
  (s,s') \<in> R \<and> tc' = tc \<and> m' = m \<and> e' = e" by (simp add: lift_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((tc, s), m, e), (tc', s'), m', e') \<in> lift_state_relation R \<Longrightarrow> (s, s') \<in> R \<and> tc' = tc \<and> m' = m \<and> e' = e
theory ADT_AI

lemma lift_state_relationI:
  "(s,s') \<in> R \<Longrightarrow> (((tc, s), m, e), ((tc, s'), m, e)) \<in> lift_state_relation R" by (fastforce simp: lift_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> R \<Longrightarrow> (((tc, s), m, e), (tc, s'), m, e) \<in> lift_state_relation R
theory ADT_AI

lemma in_lift_state_relation_eq:
  "(((tc, s), m, e), (tc', s'), m', e') \<in> lift_state_relation R \<longleftrightarrow>
   (s, s') \<in> R \<and> tc' = tc \<and> m' = m \<and> e' = e" by (auto simp add: lift_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((((tc, s), m, e), (tc', s'), m', e') \<in> lift_state_relation R) = ((s, s') \<in> R \<and> tc' = tc \<and> m' = m \<and> e' = e)
theory ArchBits_AI

lemma invs_unique_table_caps[elim!]:
  "invs s \<Longrightarrow> unique_table_caps (caps_of_state s)" by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> unique_table_caps (caps_of_state s)
theory ArchBits_AI

lemma invs_unique_refs[elim!]:
  "invs s \<Longrightarrow> unique_table_refs (caps_of_state s)" by (simp add: invs_def valid_state_def valid_arch_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> unique_table_refs (caps_of_state s)
theory ArchBits_AI

lemma invs_pd_caps:
  "invs s \<Longrightarrow> valid_table_caps s" by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_table_caps s
theory ArchBits_AI

lemma invs_valid_vs_lookup[elim!]:
  "invs s \<Longrightarrow> valid_vs_lookup s " by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_vs_lookup s
theory ArchBits_AI

lemma pbfs_atleast_pageBits:
  "pageBits \<le> pageBitsForSize sz" by (cases sz) (auto simp: pageBits_def)

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

lemma in_set_object:
  "(rv, s') \<in> fst (set_object ptr obj s) \<Longrightarrow> s' = s \<lparr> kheap := (kheap s) (ptr \<mapsto> obj) \<rparr>" by (clarsimp simp: set_object_def get_object_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (set_object ptr obj s) \<Longrightarrow> s' = s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>
theory Bits_AI

lemma lookup_error_injection:
 "lookup_error_on_failure b = injection_handler (ExceptionTypes_A.FailedLookup b)" apply (rule ext) apply (simp add: lookup_error_on_failure_def injection_handler_def o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_error_on_failure b = injection_handler (FailedLookup b) proof (prove)
goal (1 subgoal):
 1. \<And>x. lookup_error_on_failure b x = injection_handler (FailedLookup b) x proof (prove)
goal:
No subgoals!
theory Bits_AI

lemma unify_failure_injection:
  "unify_failure = injection_handler (\<lambda>x. ())" by (intro ext, simp add: unify_failure_def injection_handler_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unify_failure = injection_handler (\<lambda>x. ())
theory Bits_AI

lemma ep_cases_weak_wp:
  assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
  assumes "\<And>q. \<lbrace>P_B\<rbrace> b q \<lbrace>Q\<rbrace>"
  assumes "\<And>q. \<lbrace>P_C\<rbrace> c q \<lbrace>Q\<rbrace>"
  shows
  "\<lbrace>P_A and P_B and P_C\<rbrace>
    case ts of
      Structures_A.IdleEP \<Rightarrow> a
    | Structures_A.SendEP q \<Rightarrow> b q
    | Structures_A.RecvEP q \<Rightarrow> c q \<lbrace>Q\<rbrace>" apply (cases ts) apply (simp, rule hoare_weaken_pre, rule assms, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P_A and P_B and P_C\<rbrace> case ts of IdleEP \<Rightarrow> a | SendEP q \<Rightarrow> b q | RecvEP q \<Rightarrow> c q \<lbrace>Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. ts = IdleEP \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of IdleEP \<Rightarrow> a | SendEP q \<Rightarrow> b q | RecvEP q \<Rightarrow> c q \<lbrace>Q\<rbrace>
 2. \<And>x2. ts = SendEP x2 \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of IdleEP \<Rightarrow> a | SendEP q \<Rightarrow> b q | RecvEP q \<Rightarrow> c q \<lbrace>Q\<rbrace>
 3. \<And>x3. ts = RecvEP x3 \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of IdleEP \<Rightarrow> a | SendEP q \<Rightarrow> b q | RecvEP q \<Rightarrow> c q \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Bits_AI

lemma ntfn_cases_weak_wp:
  assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
  assumes "\<And>q. \<lbrace>P_B\<rbrace> b q \<lbrace>Q\<rbrace>"
  assumes "\<And>bdg msg. \<lbrace>P_C\<rbrace> c bdg msg \<lbrace>Q\<rbrace>"
  shows
  "\<lbrace>P_A and P_B and P_C\<rbrace>
    case ts of
      Structures_A.IdleNtfn \<Rightarrow> a
    | Structures_A.WaitingNtfn q \<Rightarrow> b q
    | Structures_A.ActiveNtfn bdg \<Rightarrow> c bdg msg \<lbrace>Q\<rbrace>" apply (cases ts) apply (simp, rule hoare_weaken_pre, rule assms, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P_A and P_B and P_C\<rbrace> case ts of IdleNtfn \<Rightarrow> a | WaitingNtfn q \<Rightarrow> b q | ActiveNtfn bdg \<Rightarrow> c bdg msg \<lbrace>Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. ts = IdleNtfn \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of IdleNtfn \<Rightarrow> a | WaitingNtfn q \<Rightarrow> b q | ActiveNtfn bdg \<Rightarrow> c bdg msg \<lbrace>Q\<rbrace>
 2. \<And>x2. ts = WaitingNtfn x2 \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of IdleNtfn \<Rightarrow> a | WaitingNtfn q \<Rightarrow> b q | ActiveNtfn bdg \<Rightarrow> c bdg msg \<lbrace>Q\<rbrace>
 3. \<And>x3. ts = ActiveNtfn x3 \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of IdleNtfn \<Rightarrow> a | WaitingNtfn q \<Rightarrow> b q | ActiveNtfn bdg \<Rightarrow> c bdg msg \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Bits_AI

lemma NullCap_valid [simp]: "s \<turnstile> cap.NullCap" by (simp add: valid_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> NullCap
theory Bits_AI

lemma empty_on_failure_wp[wp]:
  "\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv. Q []\<rbrace>
    \<Longrightarrow> \<lbrace>P\<rbrace> empty_on_failure m \<lbrace>Q\<rbrace>" by (simp add: empty_on_failure_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q []\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> empty_on_failure m \<lbrace>Q\<rbrace>
theory Bits_AI

lemma gen_invocation_typeI:
  "invocation_type l = GenInvocationLabel x \<Longrightarrow> gen_invocation_type l = x" by (simp add: gen_invocation_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invocation_type l = GenInvocationLabel x \<Longrightarrow> gen_invocation_type l = x
theory Bits_AI

lemma gen_invocation_type_eq:
  "x \<noteq> InvalidInvocation \<Longrightarrow>
  (invocation_type l = GenInvocationLabel x) = (gen_invocation_type l = x)" by (auto simp: gen_invocation_type_def split: invocation_label.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> InvalidInvocation \<Longrightarrow> (invocation_type l = GenInvocationLabel x) = (gen_invocation_type l = x)
theory Machine_AI

lemma wpc_helper_no_irq:
  "no_irq f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_irq f)" by (simp add: wpc_helper_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_irq f)
theory Machine_AI

lemma det_getRegister: "det (getRegister x)" by (simp add: getRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (getRegister x)
theory Machine_AI

lemma det_setRegister: "det (setRegister x w)" by (simp add: setRegister_def det_def modify_def get_def put_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (setRegister x w)
theory Machine_AI

lemma det_getRestartPC: "det getRestartPC" by (simp add: getRestartPC_def det_getRegister)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det getRestartPC
theory Machine_AI

lemma det_setNextPC: "det (setNextPC p)" by (simp add: setNextPC_def det_setRegister)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (setNextPC p)
theory Machine_AI

lemma ef_loadWord: "empty_fail (loadWord x)" by (fastforce simp: loadWord_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (loadWord x)
theory Machine_AI

lemma ef_storeWord: "empty_fail (storeWord x y)" by (fastforce simp: storeWord_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (storeWord x y)
theory Machine_AI

lemma no_fail_getRestartPC: "no_fail \<top> getRestartPC" by (simp add: getRestartPC_def getRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) getRestartPC
theory Machine_AI

lemma no_fail_loadWord [wp]: "no_fail (\<lambda>_. is_aligned p 2) (loadWord p)" apply (simp add: loadWord_def is_aligned_mask [symmetric]) apply (rule no_fail_pre) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. is_aligned p 2) (loadWord p) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. is_aligned p 2) (do m <- gets underlying_memory;
y <- assert (is_aligned p 2);
return (word_rcat [m (p + 3), m (p + 2), m (p + 1), m p])
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P (do m <- gets underlying_memory;
y <- assert (is_aligned p 2);
return (word_rcat [m (p + 3), m (p + 2), m (p + 1), m p])
od)
 2. \<And>s. is_aligned p 2 \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned p 2 \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. is_aligned p 2) and (\<lambda>s. is_aligned p 2 \<longrightarrow> True))) s proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_fail_storeWord: "no_fail (\<lambda>_. is_aligned p 2) (storeWord p w)" apply (simp add: storeWord_def is_aligned_mask [symmetric]) apply (rule no_fail_pre) apply (wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. is_aligned p 2) (storeWord p w) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. is_aligned p 2) (do y <- assert (is_aligned p 2);
modify (underlying_memory_update (\<lambda>m. m(p := word_rsplit w ! 3, p + 1 := word_rsplit w ! 2, p + 2 := word_rsplit w ! Suc 0, p + 3 := word_rsplit w ! 0)))
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P1 (do y <- assert (is_aligned p 2);
modify (underlying_memory_update (\<lambda>m. m(p := word_rsplit w ! 3, p + 1 := word_rsplit w ! 2, p + 2 := word_rsplit w ! Suc 0, p + 3 := word_rsplit w ! 0)))
od)
 2. \<And>s. is_aligned p 2 \<Longrightarrow> ?P1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned p 2 \<Longrightarrow> ((\<lambda>_. is_aligned p 2) and (\<lambda>s. is_aligned p 2 \<longrightarrow> True)) s proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_fail_machine_op_lift [simp]:
  "no_fail \<top> (machine_op_lift f)" by (simp add: machine_op_lift_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (machine_op_lift f)
theory Machine_AI

lemma ef_machine_op_lift [simp]:
  "empty_fail (machine_op_lift f)" by (simp add: machine_op_lift_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (machine_op_lift f)
theory Machine_AI

lemma no_fail_setNextPC: "no_fail \<top> (setNextPC pc)" by (simp add: setNextPC_def setRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (setNextPC pc)
theory Machine_AI

lemma no_fail_getFAR: "no_fail \<top> getFAR" by (simp add: getFAR_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) getFAR
theory Machine_AI

lemma no_fail_getDFSR: "no_fail \<top> getDFSR" by (simp add: getDFSR_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) getDFSR
theory Machine_AI

lemma no_fail_getIFSR: "no_fail \<top> getIFSR" by (simp add: getIFSR_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) getIFSR
theory Machine_AI

lemma no_fail_dsb: "no_fail \<top> dsb" by (simp add: dsb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) dsb
theory Machine_AI

lemma no_fail_dmb: "no_fail \<top> dmb" by (simp add: dmb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) dmb
theory Machine_AI

lemma no_fail_writeTTBR0: "no_fail \<top> (writeTTBR0 w)" by (simp add: writeTTBR0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (writeTTBR0 w)
theory Machine_AI

lemma no_fail_set_current_pd: "no_fail \<top> (set_current_pd w)" apply (simp add: set_current_pd_def) apply (rule no_fail_pre, wp no_fail_dsb no_fail_writeTTBR0 no_fail_isb, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (set_current_pd w) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (do y <- dsb;
y <- writeTTBR0 (w && 0xFFFFE000 || 0x18);
isb
od) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_fail_cleanByVA: "no_fail \<top> (cleanByVA w p)" by (simp add: cleanByVA_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cleanByVA w p)
theory Machine_AI

lemma no_fail_cleanByVA_PoU: "no_fail \<top> (cleanByVA_PoU w p)" by (simp add: cleanByVA_PoU_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cleanByVA_PoU w p)
theory Machine_AI

lemma no_fail_invalidateLocalTLB: "no_fail \<top> invalidateLocalTLB" by (simp add: invalidateLocalTLB_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) invalidateLocalTLB
theory Machine_AI

lemma no_fail_invalidateLocalTLB_VAASID: "no_fail \<top> (invalidateLocalTLB_VAASID x)" by (simp add: invalidateLocalTLB_VAASID_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (invalidateLocalTLB_VAASID x)
theory Machine_AI

lemma no_fail_invalidateByVA: "no_fail \<top> (invalidateByVA w p)" by (simp add: invalidateByVA_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (invalidateByVA w p)
theory Machine_AI

lemma no_fail_invalidateByVA_I: "no_fail \<top> (invalidateByVA_I w p)" by (simp add: invalidateByVA_I_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (invalidateByVA_I w p)
theory Machine_AI

lemma no_fail_invalidate_I_PoU: "no_fail \<top> invalidate_I_PoU" by (simp add: invalidate_I_PoU_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) invalidate_I_PoU
theory Machine_AI

lemma no_fail_cleanInvalByVA: "no_fail \<top> (cleanInvalByVA w p)" by (simp add: cleanInvalByVA_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cleanInvalByVA w p)
theory Machine_AI

lemma no_fail_branchFlush: "no_fail \<top> (branchFlush w p)" by (simp add: branchFlush_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (branchFlush w p)
theory Machine_AI

lemma no_fail_clean_D_PoU: "no_fail \<top> clean_D_PoU" by (simp add: clean_D_PoU_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) clean_D_PoU
theory Machine_AI

lemma no_fail_cleanInvalidate_D_PoC: "no_fail \<top> cleanInvalidate_D_PoC" by (simp add: cleanInvalidate_D_PoC_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) cleanInvalidate_D_PoC
theory Machine_AI

lemma no_fail_cleanInvalidateL2Range: "no_fail \<top> (cleanInvalidateL2Range w p)" by (simp add: cleanInvalidateL2Range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cleanInvalidateL2Range w p)
theory Machine_AI

lemma no_fail_invalidateL2Range: "no_fail \<top> (invalidateL2Range w p)" by (simp add: invalidateL2Range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (invalidateL2Range w p)
theory Machine_AI

lemma no_fail_cleanL2Range: "no_fail \<top> (cleanL2Range w p)" by (simp add: cleanL2Range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cleanL2Range w p)
theory Machine_AI

lemma no_fail_initL2Cache: "no_fail \<top> initL2Cache" by (simp add: initL2Cache_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) initL2Cache
theory Machine_AI

lemma no_fail_clearExMonitor: "no_fail \<top> clearExMonitor" by (simp add: clearExMonitor_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) clearExMonitor
theory Machine_AI

lemma no_fail_flushBTAC: "no_fail \<top> flushBTAC" by (simp add: flushBTAC_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) flushBTAC
theory Machine_AI

lemma no_fail_writeContextID: "no_fail \<top> writeContextID" by (simp add: writeContextID_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) writeContextID
theory Machine_AI

lemma no_fail_setHardwareASID: "no_fail \<top> (setHardwareASID hw_asid)" by (simp add: setHardwareASID_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (setHardwareASID hw_asid)
theory Machine_AI

lemma no_fail_resetTimer[wp]: "no_fail \<top> resetTimer" by (simp add: resetTimer_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) resetTimer
theory Machine_AI

lemma loadWord_inv: "\<lbrace>P\<rbrace> loadWord x \<lbrace>\<lambda>x. P\<rbrace>" unfolding loadWord_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> loadWord x \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do m <- gets underlying_memory;
assert (x && mask 2 = 0);
return (word_rcat [m (x + 3), m (x + 2), m (x + 1), m x])
od \<lbrace>\<lambda>x. P\<rbrace>
theory Machine_AI

lemma getRestartPC_inv: "\<lbrace>P\<rbrace> getRestartPC \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: getRestartPC_def getRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getRestartPC \<lbrace>\<lambda>rv. P\<rbrace>
theory Machine_AI

lemma getDFSR_inv: "\<lbrace>P\<rbrace> getDFSR \<lbrace>\<lambda>_. P\<rbrace>" by (simp add: getDFSR_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getDFSR \<lbrace>\<lambda>_. P\<rbrace>
theory Machine_AI

lemma getFAR_inv: "\<lbrace>P\<rbrace> getFAR \<lbrace>\<lambda>_. P\<rbrace>" by (simp add: getFAR_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getFAR \<lbrace>\<lambda>_. P\<rbrace>
theory Machine_AI

lemma getIFSR_inv: "\<lbrace>P\<rbrace> getIFSR \<lbrace>\<lambda>_. P\<rbrace>" by (simp add: getIFSR_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getIFSR \<lbrace>\<lambda>_. P\<rbrace>
theory Machine_AI

lemma no_fail_cacheRangeOp[simp, wp]:
  assumes nf: "\<And>a b. no_fail \<top> (oper a b)"
  shows "no_fail \<top> (cacheRangeOp oper s e p)" by (simp add: cacheRangeOp_def mapM_x_mapM) (wpsimp wp: no_fail_mapM nf)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cacheRangeOp oper s e p)
theory Machine_AI

lemma no_fail_cleanCacheRange_PoU[simp, wp]:
  "no_fail \<top> (cleanCacheRange_PoU s e p)" by (simp add: cleanCacheRange_PoU_def, wp no_fail_cleanByVA_PoU)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cleanCacheRange_PoU s e p)
theory Machine_AI

lemma no_fail_cleanCacheRange_PoC[simp, wp]:
  "no_fail \<top> (cleanCacheRange_PoC s e p)" by (simp add: cleanCacheRange_PoC_def, wp no_fail_cleanByVA)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cleanCacheRange_PoC s e p)
theory Machine_AI

lemma no_fail_cleanInvalidateCacheRange_RAM[simp, wp]:
  "no_fail \<top> (cleanInvalidateCacheRange_RAM s e p)" by (simp add: cleanInvalidateCacheRange_RAM_def, rule no_fail_pre,
      wp no_fail_dsb no_fail_cleanInvalidateL2Range no_fail_cleanInvalByVA, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cleanInvalidateCacheRange_RAM s e p)
theory Machine_AI

lemma no_fail_cleanCacheRange_RAM[simp, wp]:
  "no_fail \<top> (cleanCacheRange_RAM s e p)" apply (simp add: cleanCacheRange_RAM_def) apply (rule no_fail_pre, wp no_fail_dsb no_fail_cleanL2Range, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (cleanCacheRange_RAM s e p) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (do y <- cleanCacheRange_PoC s e p;
y <- dsb;
cleanL2Range p (p + (e - s))
od) proof (prove)
goal:
No subgoals!