kings-crown/FVELER_Isabelle huggingface dataset:
theory Machine_AI

lemma no_irq_clearExMonitor: "no_irq clearExMonitor" apply (simp add: clearExMonitor_def) apply (wp no_irq_modify) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq clearExMonitor proof (prove)
goal (1 subgoal):
 1. no_irq (modify (exclusive_state_update (\<lambda>_. default_exclusive_state))) proof (prove)
goal (1 subgoal):
 1. \<And>s. irq_masks (s\<lparr>exclusive_state := default_exclusive_state\<rparr>) = irq_masks s proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_storeWord: "no_irq (storeWord w p)" apply (simp add: storeWord_def) apply (wp no_irq_modify) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (storeWord w p) proof (prove)
goal (1 subgoal):
 1. no_irq (do y <- assert (w && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(w := word_rsplit p ! 3, w + 1 := word_rsplit p ! 2, w + 2 := word_rsplit p ! Suc 0, w + 3 := word_rsplit p ! 0)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>x s. irq_masks (underlying_memory_update (\<lambda>m. m(w := word_rsplit p ! 3, w + 1 := word_rsplit p ! 2, w + 2 := word_rsplit p ! Suc 0, w + 3 := word_rsplit p ! 0)) s) = irq_masks s proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_cacheRangeOp[simp, wp]:
  assumes nf: "\<And>a b. no_irq (oper a b)"
  shows "no_irq (cacheRangeOp oper s e p)" apply (simp add: cacheRangeOp_def) apply (wp no_irq_mapM_x nf | wpc | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (cacheRangeOp oper s e p) proof (prove)
goal (1 subgoal):
 1. no_irq (mapM_x (\<lambda>(x, y). oper x y) (zip [lineStart s , lineStart s + word_of_nat cacheLine .e. lineStart e] [lineStart p , lineStart p + word_of_nat cacheLine .e. lineStart (p + (e - s))])) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_cleanCacheRange_PoU[simp, wp]:
  "no_irq (cleanCacheRange_PoU s e p)" by (simp add: cleanCacheRange_PoU_def, wp no_irq_cleanByVA_PoU)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (cleanCacheRange_PoU s e p)
theory Machine_AI

lemma no_irq_cleanCacheRange_PoC[simp, wp]:
  "no_irq (cleanCacheRange_PoC s e p)" by (simp add: cleanCacheRange_PoC_def, wp no_irq_cleanByVA)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (cleanCacheRange_PoC s e p)
theory Machine_AI

lemma no_irq_cleanInvalidateCacheRange_RAM[simp, wp]:
  "no_irq (cleanInvalidateCacheRange_RAM s e p)" by (simp add: cleanInvalidateCacheRange_RAM_def,
      wp no_irq_dsb no_irq_cleanInvalidateL2Range no_irq_cleanInvalByVA)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (cleanInvalidateCacheRange_RAM s e p)
theory Machine_AI

lemma no_irq_cleanCacheRange_RAM[simp, wp]:
  "no_irq (cleanCacheRange_RAM s e p)" apply (simp add: cleanCacheRange_RAM_def) apply (wp no_irq_dsb no_irq_cleanL2Range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (cleanCacheRange_RAM s e p) proof (prove)
goal (1 subgoal):
 1. no_irq (do y <- cleanCacheRange_PoC s e p;
y <- dsb;
cleanL2Range p (p + (e - s))
od) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_invalidateCacheRange_RAM[simp, wp]:
  "no_irq (invalidateCacheRange_RAM s e p)" apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def) apply (wp no_irq_invalidateL2Range no_irq_invalidateByVA no_irq_dsb no_irq_when) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (invalidateCacheRange_RAM s e p) proof (prove)
goal (1 subgoal):
 1. no_irq (do y <- when (s \<noteq> s >> 5 << 5) (cleanCacheRange_RAM s s p);
y <- when (e + 1 \<noteq> e + 1 >> 5 << 5) (cleanCacheRange_RAM (e >> 5 << 5) (e >> 5 << 5) (p + ((e >> 5 << 5) - s)));
y <- invalidateL2Range p (p + (e - s));
y <- cacheRangeOp invalidateByVA s e p;
dsb
od) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_branchFlushRange[simp, wp]:
  "no_irq (branchFlushRange s e p)" by (simp add: branchFlushRange_def, wp no_irq_branchFlush)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (branchFlushRange s e p)
theory Machine_AI

lemma no_irq_cleanInvalidateL1Caches[simp, wp]:
  "no_irq cleanInvalidateL1Caches" by (simp add: cleanInvalidateL1Caches_def,
      wp no_irq_dsb no_irq_cleanInvalidate_D_PoC no_irq_invalidate_I_PoU)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq cleanInvalidateL1Caches
theory Machine_AI

lemma no_irq_clearMemory: "no_irq (clearMemory a b)" apply (simp add: clearMemory_def) apply (wp no_irq_mapM_x no_irq_storeWord no_irq_cleanCacheRange_PoU) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (clearMemory a b) proof (prove)
goal (1 subgoal):
 1. no_irq (do y <- mapM_x (\<lambda>p. storeWord p 0) [a , a + word_size .e. a + word_of_nat b - 1];
cleanCacheRange_RAM a (a + word_of_nat b - 1) (addrFromPPtr a)
od) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma getActiveIRQ_le_maxIRQ':
  "\<lbrace>\<lambda>s. \<forall>irq > maxIRQ. irq_masks s irq\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>" apply (simp add: getActiveIRQ_def) apply wp apply clarsimp apply (rule ccontr) apply (simp add: linorder_not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>irq>maxIRQ. irq_masks s irq\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>irq>maxIRQ. irq_masks s irq\<rbrace> do is_masked <- gets irq_masks;
y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if is_masked active_irq \<or> active_irq = 0x3FF \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>irq>maxIRQ. irq_masks s irq \<Longrightarrow> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs \<longrightarrow> (\<forall>x. None = Some x \<longrightarrow> x \<le> maxIRQ)) \<and> (\<not> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs) \<longrightarrow> (\<forall>x. Some ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) = Some x \<longrightarrow> x \<le> maxIRQ)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>irq>maxIRQ. irq_masks s irq; \<not> irq_masks s (irq_oracle (Suc (irq_state s))); irq_oracle (Suc (irq_state s)) \<noteq> 0x3FF; in_kernel \<longrightarrow> irq_oracle (Suc (irq_state s)) \<notin> non_kernel_IRQs\<rbrakk> \<Longrightarrow> irq_oracle (Suc (irq_state s)) \<le> maxIRQ proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>irq>maxIRQ. irq_masks s irq; \<not> irq_masks s (irq_oracle (Suc (irq_state s))); irq_oracle (Suc (irq_state s)) \<noteq> 0x3FF; in_kernel \<longrightarrow> irq_oracle (Suc (irq_state s)) \<notin> non_kernel_IRQs; \<not> irq_oracle (Suc (irq_state s)) \<le> maxIRQ\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma getActiveIRQ_neq_Some0xFF':
  "\<lbrace>\<top>\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>" apply (simp add: getActiveIRQ_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do is_masked <- gets irq_masks;
y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if is_masked active_irq \<or> active_irq = 0x3FF \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs \<longrightarrow> None \<noteq> Some 0x3FF) \<and> (\<not> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs) \<longrightarrow> Some ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<noteq> Some 0x3FF) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma getActiveIRQ_neq_non_kernel:
  "\<lbrace>\<top>\<rbrace> getActiveIRQ True \<lbrace>\<lambda>rv s. rv \<notin> Some ` non_kernel_IRQs \<rbrace>" apply (simp add: getActiveIRQ_def) apply wp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getActiveIRQ True \<lbrace>\<lambda>rv s. rv \<notin> Some ` non_kernel_IRQs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do is_masked <- gets irq_masks;
y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if is_masked active_irq \<or> active_irq = 0x3FF \<or> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od \<lbrace>\<lambda>rv s. rv \<notin> Some ` non_kernel_IRQs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs \<longrightarrow> None \<notin> Some ` non_kernel_IRQs) \<and> (\<not> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs) \<longrightarrow> Some ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<notin> Some ` non_kernel_IRQs) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma dmo_getActiveIRQ_non_kernel[wp]:
  "\<lbrace>\<top>\<rbrace> do_machine_op (getActiveIRQ True)
   \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> irq \<in> non_kernel_IRQs \<longrightarrow> P irq s\<rbrace>" unfolding do_machine_op_def apply wpsimp apply (drule use_valid, rule getActiveIRQ_neq_non_kernel, rule TrueI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> irq \<in> non_kernel_IRQs \<longrightarrow> P irq s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (getActiveIRQ True ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> irq \<in> non_kernel_IRQs \<longrightarrow> P irq s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s xa irq. \<lbrakk>(Some irq, xa) \<in> fst (getActiveIRQ True (machine_state s)); irq \<in> non_kernel_IRQs\<rbrakk> \<Longrightarrow> P irq (s\<lparr>machine_state := xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s xa irq. \<lbrakk>irq \<in> non_kernel_IRQs; Some irq \<notin> Some ` non_kernel_IRQs\<rbrakk> \<Longrightarrow> P irq (s\<lparr>machine_state := xa\<rparr>) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma empty_fail_isb: "empty_fail  isb" by (simp add: isb_def)

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

lemma empty_fail_dsb: "empty_fail  dsb" by (simp add: dsb_def)

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

lemma empty_fail_dmb: "empty_fail  dmb" by (simp add: dmb_def)

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

lemma empty_fail_cleanByVA: "empty_fail  (cleanByVA w p)" by (simp add: cleanByVA_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (cleanByVA w p)
theory Machine_AI

lemma empty_fail_cleanByVA_PoU: "empty_fail  (cleanByVA_PoU w p)" by (simp add: cleanByVA_PoU_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (cleanByVA_PoU w p)
theory Machine_AI

lemma empty_fail_invalidateLocalTLB: "empty_fail  invalidateLocalTLB" by (simp add: invalidateLocalTLB_def)

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

lemma empty_fail_invalidateLocalTLB_ASID: "empty_fail  (invalidateLocalTLB_ASID x)" by (simp add: invalidateLocalTLB_ASID_def)

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

lemma empty_fail_invalidateLocalTLB_VAASID: "empty_fail  (invalidateLocalTLB_VAASID x)" by (simp add: invalidateLocalTLB_VAASID_def)

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

lemma empty_fail_invalidateByVA: "empty_fail  (invalidateByVA w p)" by (simp add: invalidateByVA_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (invalidateByVA w p)
theory Machine_AI

lemma empty_fail_invalidateByVA_I: "empty_fail  (invalidateByVA_I w p)" by (simp add: invalidateByVA_I_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (invalidateByVA_I w p)
theory Machine_AI

lemma empty_fail_invalidate_I_PoU: "empty_fail  invalidate_I_PoU" by (simp add: invalidate_I_PoU_def)

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

lemma empty_fail_cleanInvalByVA: "empty_fail  (cleanInvalByVA w p)" by (simp add: cleanInvalByVA_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (cleanInvalByVA w p)
theory Machine_AI

lemma empty_fail_branchFlush: "empty_fail  (branchFlush w p)" by (simp add: branchFlush_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (branchFlush w p)
theory Machine_AI

lemma empty_fail_clean_D_PoU: "empty_fail  clean_D_PoU" by (simp add: clean_D_PoU_def)

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

lemma empty_fail_cleanInvalidate_D_PoC: "empty_fail  cleanInvalidate_D_PoC" by (simp add: cleanInvalidate_D_PoC_def)

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

lemma empty_fail_cleanInvalidateL2Range: "empty_fail  (cleanInvalidateL2Range w p)" by (simp add: cleanInvalidateL2Range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (cleanInvalidateL2Range w p)
theory Machine_AI

lemma empty_fail_invalidateL2Range: "empty_fail  (invalidateL2Range w p)" by (simp add: invalidateL2Range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (invalidateL2Range w p)
theory Machine_AI

lemma empty_fail_cleanL2Range: "empty_fail  (cleanL2Range w p)" by (simp add: cleanL2Range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (cleanL2Range w p)
theory Machine_AI

lemma empty_fail_initL2Cache: "empty_fail  initL2Cache" by (simp add: initL2Cache_def)

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

lemma empty_fail_clearExMonitor: "empty_fail  clearExMonitor" by (simp add: clearExMonitor_def)

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

lemma empty_fail_flushBTAC: "empty_fail  flushBTAC" by (simp add: flushBTAC_def)

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

lemma empty_fail_writeContextID: "empty_fail  writeContextID" by (simp add: writeContextID_def)

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

lemma empty_fail_cacheRangeOp [simp, intro!]:
  assumes ef: "\<And>a b. empty_fail (oper a b)"
  shows "empty_fail (cacheRangeOp oper s e p)" apply (simp add: cacheRangeOp_def mapM_x_mapM lineStart_def cacheLineBits_def cacheLine_def ef) apply (rule empty_fail_bind) apply (rule empty_fail_mapM) apply (auto intro: ef) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (cacheRangeOp oper s e p) proof (prove)
goal (1 subgoal):
 1. empty_fail (do x <- mapM (\<lambda>(x, y). oper x y) (zip [s >> 5 << 5 , (s >> 5 << 5) + 0x20 .e. e >> 5 << 5] [p >> 5 << 5 , (p >> 5 << 5) + 0x20 .e. p + (e - s) >> 5 << 5]);
return ()
od) proof (prove)
goal (2 subgoals):
 1. empty_fail (mapM (\<lambda>(x, y). oper x y) (zip [s >> 5 << 5 , (s >> 5 << 5) + 0x20 .e. e >> 5 << 5] [p >> 5 << 5 , (p >> 5 << 5) + 0x20 .e. p + (e - s) >> 5 << 5]))
 2. \<And>x. empty_fail (return ()) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set (zip [s >> 5 << 5 , (s >> 5 << 5) + 0x20 .e. e >> 5 << 5] [p >> 5 << 5 , (p >> 5 << 5) + 0x20 .e. p + (e - s) >> 5 << 5]) \<Longrightarrow> empty_fail (case x of (x, xa) \<Rightarrow> oper x xa)
 2. \<And>x. empty_fail (return ()) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma empty_fail_cleanCacheRange_PoC[simp, intro!]:
  "empty_fail (cleanCacheRange_PoC s e p)" by (simp add: cleanCacheRange_PoC_def empty_fail_cleanByVA)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (cleanCacheRange_PoC s e p)
theory Machine_AI

lemma empty_fail_cleanInvalidateCacheRange_RAM[simp, intro!]:
  "empty_fail (cleanInvalidateCacheRange_RAM s e p)" by (fastforce simp: cleanInvalidateCacheRange_RAM_def empty_fail_dsb
                      empty_fail_cleanInvalidateL2Range empty_fail_cleanInvalByVA)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (cleanInvalidateCacheRange_RAM s e p)
theory Machine_AI

lemma empty_fail_cleanCacheRange_RAM[simp, intro!]:
  "empty_fail (cleanCacheRange_RAM s e p)" by (fastforce simp: cleanCacheRange_RAM_def empty_fail_dsb empty_fail_cleanL2Range)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (cleanCacheRange_RAM s e p)
theory Machine_AI

lemma empty_fail_invalidateCacheRange_I[simp, intro!]:
  "empty_fail (invalidateCacheRange_I s e p)" by (simp add: invalidateCacheRange_I_def empty_fail_invalidateByVA_I)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (invalidateCacheRange_I s e p)
theory Machine_AI

lemma empty_fail_branchFlushRange[simp, intro!]:
  "empty_fail (branchFlushRange s e p)" by (simp add: branchFlushRange_def empty_fail_branchFlush)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (branchFlushRange s e p)
theory Machine_AI

lemma empty_fail_cleanCaches_PoU[simp, intro!]:
  "empty_fail cleanCaches_PoU" by (fastforce simp: cleanCaches_PoU_def empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU)

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

lemma empty_fail_cleanInvalidateL1Caches[simp, intro!]:
  "empty_fail cleanInvalidateL1Caches" by (fastforce simp: cleanInvalidateL1Caches_def empty_fail_dsb empty_fail_cleanInvalidate_D_PoC
                     empty_fail_invalidate_I_PoU)

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

lemma empty_fail_clearMemory [simp, intro!]:
  "\<And>a b. empty_fail (clearMemory a b)" by (fastforce simp: clearMemory_def mapM_x_mapM ef_storeWord)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>a b. empty_fail (clearMemory a b)
theory KHeapPre_AI

lemma same_caps_more_simps[simp]:
 "same_caps (CNode sz cs) val       = (val = CNode sz cs)"
 "same_caps (TCB tcb)     val       = (\<exists>tcb'. val = TCB tcb'
                                         \<and> (\<forall>(getF, t) \<in> ran tcb_cap_cases. getF tcb' = getF tcb))"
 "same_caps (Endpoint ep) val       = is_ep val"
 "same_caps (Notification ntfn) val = is_ntfn val"
 "same_caps (ArchObj ao) val        = (\<exists>ao'. val = ArchObj ao')" by (cases val, (fastforce simp: is_obj_defs)+)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (same_caps (CNode sz cs) val = (val = CNode sz cs) &&& same_caps (TCB tcb) val = (\<exists>tcb'. val = TCB tcb' \<and> (\<forall>(getF, t)\<in>ran tcb_cap_cases. getF tcb' = getF tcb))) &&& same_caps (Endpoint ep) val = is_ep val &&& same_caps (Notification ntfn) val = is_ntfn val &&& same_caps (ArchObj ao) val = (\<exists>ao'. val = ArchObj ao')
theory KHeapPre_AI

lemma dmo_return [simp]:
  "do_machine_op (return x) = return x" by (simp add: do_machine_op_def select_f_def return_def gets_def get_def
                bind_def modify_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do_machine_op (return x) = return x
theory KHeapPre_AI

lemma get_object_sp:
  "\<lbrace>P\<rbrace> get_object p \<lbrace>\<lambda>r. P and ko_at r p\<rbrace>" apply (simp add: get_object_def) apply wp apply (auto simp add: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_object p \<lbrace>\<lambda>r. P and ko_at r p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od \<lbrace>\<lambda>r. P and ko_at r p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> P s \<and> ko_at (the (kheap s p)) p s proof (prove)
goal:
No subgoals!
theory KHeapPre_AI

lemma non_arch_objs[intro]:
  "non_arch_obj (Endpoint ep)"
  "non_arch_obj (CNode sz cnode_contents)"
  "non_arch_obj (TCB tcb)"
  "non_arch_obj (Notification notification)" by (auto simp add: non_arch_obj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (non_arch_obj (Endpoint ep) &&& non_arch_obj (CNode sz cnode_contents)) &&& non_arch_obj (TCB tcb) &&& non_arch_obj (Notification notification)
theory KHeapPre_AI

lemma arch_obj_predE:
  "\<lbrakk>arch_obj_pred P; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> P ko = P ko'" apply (unfold arch_obj_pred_def) apply (erule allE[where ?x="ko"]) apply (erule allE[where ?x="ko'"]) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_obj_pred P; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> P ko = P ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ko ko'. non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> P ko = P ko'; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> P ko = P ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>non_arch_obj ko; non_arch_obj ko'; \<forall>ko'. non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> P ko = P ko'\<rbrakk> \<Longrightarrow> P ko = P ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>non_arch_obj ko; non_arch_obj ko'; non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> P ko = P ko'\<rbrakk> \<Longrightarrow> P ko = P ko'