kings-crown/FVELER_Isabelle huggingface dataset:
theory Machine_AI

lemma no_fail_invalidateCacheRange_I[simp, wp]:
  "no_fail \<top> (invalidateCacheRange_I s e p)" by (simp add: invalidateCacheRange_I_def, wp no_fail_invalidateByVA_I)

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

lemma no_fail_invalidateCacheRange_RAM[simp, wp]:
  "no_fail \<top> (invalidateCacheRange_RAM s e p)" apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def) apply (wpsimp wp: no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (invalidateCacheRange_RAM s e p) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (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_fail_branchFlushRange[simp, wp]:
  "no_fail \<top> (branchFlushRange s e p)" by (simp add: branchFlushRange_def, wp no_fail_branchFlush)

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

lemma no_fail_cleanCaches_PoU[simp, wp]:
  "no_fail \<top> cleanCaches_PoU" by (simp add: cleanCaches_PoU_def, rule no_fail_pre,
      wp no_fail_dsb no_fail_clean_D_PoU no_fail_invalidate_I_PoU, simp)

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

lemma no_fail_cleanInvalidateL1Caches[simp, wp]:
  "no_fail \<top> cleanInvalidateL1Caches" by (simp add: cleanInvalidateL1Caches_def, rule no_fail_pre,
      wp no_fail_dsb no_fail_cleanInvalidate_D_PoC no_fail_invalidate_I_PoU, simp)

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

lemma no_fail_clearMemory[simp, wp]:
  "no_fail (\<lambda>_. is_aligned p 2) (clearMemory p b)" apply (simp add: clearMemory_def mapM_x_mapM) apply (rule no_fail_pre) apply (wp no_fail_mapM' no_fail_storeWord no_fail_cleanCacheRange_PoU) apply (clarsimp simp: upto_enum_step_def) apply (erule aligned_add_aligned) apply (simp add: word_size_def) apply (rule is_aligned_mult_triv2 [where n = 2, simplified]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. is_aligned p 2) (clearMemory p b) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. is_aligned p 2) (do x <- mapM (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + word_of_nat b - 1];
cleanCacheRange_RAM p (p + word_of_nat b - 1) (addrFromPPtr p)
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P (do x <- mapM (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + word_of_nat b - 1];
cleanCacheRange_RAM p (p + word_of_nat b - 1) (addrFromPPtr 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>_. \<forall>x\<in>set [p , p + word_size .e. p + word_of_nat b - 1]. is_aligned x 2) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 2; \<not> p + word_of_nat b - 1 < p; x \<le> (word_of_nat b - 1) div word_size\<rbrakk> \<Longrightarrow> is_aligned (p + x * word_size) 2 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> p + word_of_nat b - 1 < p; x \<le> (word_of_nat b - 1) div word_size\<rbrakk> \<Longrightarrow> is_aligned (x * word_size) 2
 2. \<And>x. \<lbrakk>\<not> p + word_of_nat b - 1 < p; x \<le> (word_of_nat b - 1) div word_size\<rbrakk> \<Longrightarrow> 2 \<le> 2 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> p + word_of_nat b - 1 < p; x \<le> (word_of_nat b - 1) div 4\<rbrakk> \<Longrightarrow> is_aligned (x * 4) 2
 2. \<And>x. \<lbrakk>\<not> p + word_of_nat b - 1 < p; x \<le> (word_of_nat b - 1) div word_size\<rbrakk> \<Longrightarrow> 2 \<le> 2 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> p + word_of_nat b - 1 < p; x \<le> (word_of_nat b - 1) div word_size\<rbrakk> \<Longrightarrow> 2 \<le> 2 proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_fail_freeMemory[simp, wp]:
  "no_fail (\<lambda>_. is_aligned p 2) (freeMemory p b)" apply (simp add: freeMemory_def mapM_x_mapM) apply (rule no_fail_pre) apply (wp no_fail_mapM' no_fail_storeWord) apply (clarsimp simp: upto_enum_step_def) apply (erule aligned_add_aligned) apply (simp add: word_size_def) apply (rule is_aligned_mult_triv2 [where n = 2, simplified]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. is_aligned p 2) (freeMemory p b) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. is_aligned p 2) (do x <- mapM (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + 2 ^ b - 1];
return ()
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P (do x <- mapM (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + 2 ^ b - 1];
return ()
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>_. \<forall>x\<in>set [p , p + word_size .e. p + 2 ^ b - 1]. is_aligned x 2) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 2; \<not> p + 2 ^ b - 1 < p; x \<le> (2 ^ b - 1) div word_size\<rbrakk> \<Longrightarrow> is_aligned (p + x * word_size) 2 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> p + 2 ^ b - 1 < p; x \<le> (2 ^ b - 1) div word_size\<rbrakk> \<Longrightarrow> is_aligned (x * word_size) 2
 2. \<And>x. \<lbrakk>\<not> p + 2 ^ b - 1 < p; x \<le> (2 ^ b - 1) div word_size\<rbrakk> \<Longrightarrow> 2 \<le> 2 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> p + 2 ^ b - 1 < p; x \<le> (2 ^ b - 1) div 4\<rbrakk> \<Longrightarrow> is_aligned (x * 4) 2
 2. \<And>x. \<lbrakk>\<not> p + 2 ^ b - 1 < p; x \<le> (2 ^ b - 1) div word_size\<rbrakk> \<Longrightarrow> 2 \<le> 2 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> p + 2 ^ b - 1 < p; x \<le> (2 ^ b - 1) div word_size\<rbrakk> \<Longrightarrow> 2 \<le> 2 proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_fail_getActiveIRQ[wp]:
  "no_fail \<top> (getActiveIRQ in_kernel)" apply (simp add: getActiveIRQ_def) apply (rule no_fail_pre) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (getActiveIRQ in_kernel) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (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) proof (prove)
goal (2 subgoals):
 1. no_fail ?P1 (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)
 2. \<And>s. True \<Longrightarrow> ?P1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. ((\<lambda>_. True) and (\<lambda>sa. (if irq_masks s ((irq_oracle \<circ> irq_state) sa) \<or> (irq_oracle \<circ> irq_state) sa = 0x3FF \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) sa \<in> non_kernel_IRQs then \<lambda>_. True else (\<lambda>_. True)) sa)) (sa\<lparr>irq_state := Suc (irq_state sa)\<rparr>))) s)) s proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma getActiveIRQ_inv [wp]:
  "\<lbrakk>irq_state_independent P\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: getActiveIRQ_def) apply wp apply (simp add: irq_state_independent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_independent P \<Longrightarrow> \<lbrace>P\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. irq_state_independent P \<Longrightarrow> \<lbrace>P\<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. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>irq_state_independent P; P s\<rbrakk> \<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> P (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<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> P (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_fail_ackInterrupt[wp]: "no_fail \<top> (ackInterrupt irq)" by (simp add: ackInterrupt_def)

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

lemma no_fail_maskInterrupt[wp]: "no_fail \<top> (maskInterrupt irq bool)" by (simp add: maskInterrupt_def)

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

lemma no_irq_use:
  "\<lbrakk> no_irq f; (rv,s') \<in> fst (f s) \<rbrakk> \<Longrightarrow> irq_masks s' = irq_masks s" apply (simp add: no_irq_def valid_def) apply (erule_tac x="\<lambda>x. x = irq_masks s" in allE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_irq f; (rv, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> irq_masks s' = irq_masks s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>P s. P (irq_masks s) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> P (irq_masks s')); (rv, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> irq_masks s' = irq_masks s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(rv, s') \<in> fst (f s); \<forall>sa. irq_masks sa = irq_masks s \<longrightarrow> (\<forall>x\<in>fst (f sa). case x of (r, s') \<Rightarrow> irq_masks s' = irq_masks s)\<rbrakk> \<Longrightarrow> irq_masks s' = irq_masks s proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_machine_rest_lift:
  "no_irq (machine_rest_lift f)" apply (clarsimp simp: no_irq_def machine_rest_lift_def split_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (machine_rest_lift f) proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> do mr <- gets machine_state_rest;
p <- select_f (f mr);
y <- modify (machine_state_rest_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P s. P (irq_masks s) \<Longrightarrow> \<forall>x\<in>fst (f (machine_state_rest s)). P (irq_masks (s\<lparr>machine_state_rest := snd x\<rparr>)) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_isb: "no_irq  isb" by (simp add: isb_def)

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

lemma no_irq_dsb: "no_irq  dsb" by (simp add: dsb_def)

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

lemma no_irq_dmb: "no_irq  dmb" by (simp add: dmb_def)

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

lemma no_irq_cleanByVA: "no_irq  (cleanByVA w p)" by (simp add: cleanByVA_def)

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

lemma no_irq_cleanByVA_PoU: "no_irq  (cleanByVA_PoU w p)" by (simp add: cleanByVA_PoU_def)

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

lemma no_irq_invalidateLocalTLB: "no_irq  invalidateLocalTLB" by (simp add: invalidateLocalTLB_def)

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

lemma no_irq_invalidateLocalTLB_ASID: "no_irq  (invalidateLocalTLB_ASID x)" by (simp add: invalidateLocalTLB_ASID_def)

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

lemma no_irq_invalidateLocalTLB_VAASID: "no_irq  (invalidateLocalTLB_VAASID x)" by (simp add: invalidateLocalTLB_VAASID_def)

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

lemma no_irq_invalidateByVA: "no_irq  (invalidateByVA w p)" by (simp add: invalidateByVA_def)

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

lemma no_irq_invalidateByVA_I: "no_irq  (invalidateByVA_I w p)" by (simp add: invalidateByVA_I_def)

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

lemma no_irq_invalidate_I_PoU: "no_irq  invalidate_I_PoU" by (simp add: invalidate_I_PoU_def)

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

lemma no_irq_cleanInvalByVA: "no_irq  (cleanInvalByVA w p)" by (simp add: cleanInvalByVA_def)

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

lemma no_irq_branchFlush: "no_irq  (branchFlush w p)" by (simp add: branchFlush_def)

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

lemma no_irq_clean_D_PoU: "no_irq  clean_D_PoU" by (simp add: clean_D_PoU_def)

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

lemma no_irq_cleanInvalidate_D_PoC: "no_irq  cleanInvalidate_D_PoC" by (simp add: cleanInvalidate_D_PoC_def)

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

lemma no_irq_cleanInvalidateL2Range: "no_irq  (cleanInvalidateL2Range w p)" by (simp add: cleanInvalidateL2Range_def)

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

lemma no_irq_cleanL2Range: "no_irq  (cleanL2Range w p)" by (simp add: cleanL2Range_def)

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

lemma no_irq_flushBTAC: "no_irq  flushBTAC" by (simp add: flushBTAC_def)

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

lemma no_irq_writeContextID: "no_irq  writeContextID" by (simp add: writeContextID_def)

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

lemma no_irq_setHardwareASID: "no_irq (setHardwareASID hw_asid)" by (simp add: setHardwareASID_def)

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

lemma no_irq_writeTTBR0: "no_irq (writeTTBR0 pd)" by (simp add: writeTTBR0_def)

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

lemma no_irq_gets [simp]:
  "no_irq (gets f)" by (simp add: no_irq_def)

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

lemma no_irq_getIFSR: "no_irq getIFSR" by (simp add: getIFSR_def)

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

lemma no_irq_getDFSR: "no_irq getDFSR" by (simp add: getDFSR_def)

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

lemma no_irq_getFAR: "no_irq getFAR" by (simp add: getFAR_def)

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

lemma no_irq_resetTimer: "no_irq resetTimer" by (simp add: resetTimer_def)

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

lemma no_irq_debugPrint: "no_irq (debugPrint $ xs)" by (simp add: no_irq_def)

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

lemma no_irq_ackInterrupt: "no_irq (ackInterrupt irq)" by (wp | clarsimp simp: no_irq_def ackInterrupt_def)+

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

lemma no_irq_setIRQTrigger: "no_irq (setIRQTrigger irq bool)" by (wp | clarsimp simp: no_irq_def setIRQTrigger_def)+

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

lemma no_irq_loadWord: "no_irq (loadWord x)" apply (clarsimp simp: no_irq_def) apply (rule loadWord_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (loadWord x) proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> loadWord x \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_getActiveIRQ: "no_irq (getActiveIRQ in_kernel)" apply (clarsimp simp: no_irq_def) apply (rule getActiveIRQ_inv) apply (simp add: irq_state_independent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (getActiveIRQ in_kernel) proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. irq_state_independent (\<lambda>s. P (irq_masks s)) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_mapM:
  "(\<And>x. x \<in> set xs \<Longrightarrow> no_irq (f x)) \<Longrightarrow> no_irq (mapM f xs)" apply (subst no_irq_def) apply clarify apply (rule mapM_wp) prefer 2 apply (rule order_refl) apply (wp; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> set xs \<Longrightarrow> no_irq (f x)) \<Longrightarrow> no_irq (mapM f xs) proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> set xs \<Longrightarrow> no_irq (f x)) \<Longrightarrow> \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. (\<And>x. x \<in> set xs \<Longrightarrow> no_irq (f x)) \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P x. \<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> no_irq (f x); x \<in> ?S1 P\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f x \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>
 2. \<And>P. (\<And>x. x \<in> set xs \<Longrightarrow> no_irq (f x)) \<Longrightarrow> set xs \<subseteq> ?S1 P proof (prove)
goal (2 subgoals):
 1. \<And>P. (\<And>x. x \<in> set xs \<Longrightarrow> no_irq (f x)) \<Longrightarrow> set xs \<subseteq> ?S1 P
 2. \<And>P x. \<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> no_irq (f x); x \<in> ?S1 P\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f x \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P x. \<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> no_irq (f x); x \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f x \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_swp:
  "no_irq (f y x) \<Longrightarrow> no_irq (swp f x y)" by (simp add: swp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (f y x) \<Longrightarrow> no_irq (swp f x y)
theory Machine_AI

lemma no_irq_seq [wp]:
  "\<lbrakk> no_irq f; \<And>x. no_irq (g x) \<rbrakk> \<Longrightarrow> no_irq (f >>= g)" apply (subst no_irq_def) apply clarsimp apply (rule hoare_seq_ext) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_irq f; \<And>x. no_irq (g x)\<rbrakk> \<Longrightarrow> no_irq (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_irq f; \<And>x. no_irq (g x)\<rbrakk> \<Longrightarrow> \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f >>= g \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>no_irq f; \<And>x. no_irq (g x)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f >>= g \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P x. \<lbrakk>no_irq f; \<And>x. no_irq (g x)\<rbrakk> \<Longrightarrow> \<lbrace>?B1 P x\<rbrace> g x \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>
 2. \<And>P. \<lbrakk>no_irq f; \<And>x. no_irq (g x)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f \<lbrace>?B1 P\<rbrace> proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_return [simp, wp]: "no_irq (return v)" unfolding no_irq_def return_def by (rule allI, simp add: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (return v) proof (prove)
goal (1 subgoal):
 1. \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> \<lambda>s. ({(v, s)}, False) \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>
theory Machine_AI

lemma no_irq_fail [simp, wp]: "no_irq fail" unfolding no_irq_def fail_def by (rule allI, simp add: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq fail proof (prove)
goal (1 subgoal):
 1. \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> \<lambda>s. ({}, True) \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>
theory Machine_AI

lemma no_irq_assert [simp, wp]: "no_irq (assert P)" unfolding assert_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (assert P) proof (prove)
goal (1 subgoal):
 1. no_irq (if P then return () else fail)
theory Machine_AI

lemma no_irq_modify:
  "(\<And>s. irq_masks (f s) = irq_masks s) \<Longrightarrow> no_irq (modify f)" unfolding modify_def no_irq_def apply (rule allI, simp add: valid_def put_def get_def) apply (clarsimp simp: in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. irq_masks (f s) = irq_masks s) \<Longrightarrow> no_irq (modify f) proof (prove)
goal (1 subgoal):
 1. (\<And>s. irq_masks (f s) = irq_masks s) \<Longrightarrow> \<forall>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> do s <- get;
put (f s)
od \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. (\<And>s. irq_masks (f s) = irq_masks s) \<Longrightarrow> \<forall>s. P (irq_masks s) \<longrightarrow> (\<forall>x\<in>fst ((do s <- \<lambda>s. ({(s, s)}, False);
\<lambda>_. ({((), f s)}, False)
od) s). case x of (r, s') \<Rightarrow> P (irq_masks s')) proof (prove)
goal:
No subgoals!
theory Machine_AI

lemma no_irq_set_current_pd: "no_irq (set_current_pd pd)" apply (clarsimp simp: set_current_pd_def) apply (wp no_irq_dsb no_irq_writeTTBR0 no_irq_isb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (set_current_pd pd) proof (prove)
goal (1 subgoal):
 1. no_irq (do y <- dsb;
y <- writeTTBR0 (pd && 0xFFFFE000 || 0x18);
isb
od) proof (prove)
goal:
No subgoals!