kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_IF

lemma gets_descendants_of_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=)
                            (pas_refined aag and K (is_subject aag (fst slot)))
                            (gets (descendants_of slot \<circ> cdt))" apply (rule gets_evrv'') apply clarsimp by (rule descendants_of_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (pas_refined aag and K (is_subject aag (fst slot))) (gets (descendants_of slot \<circ> cdt)) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<and> (pas_refined aag and K (is_subject aag (fst slot))) s \<and> (pas_refined aag and K (is_subject aag (fst slot))) t \<longrightarrow> (descendants_of slot \<circ> cdt) s = (descendants_of slot \<circ> cdt) t proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = descendants_of slot (cdt t)
theory CNode_IF

lemma silc_dom_equiv_trans[elim]:
  "\<lbrakk> silc_dom_equiv aag s t; silc_dom_equiv aag t u \<rbrakk>
     \<Longrightarrow> silc_dom_equiv aag s u" by (auto simp: silc_dom_equiv_def elim: equiv_for_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_dom_equiv aag s t; silc_dom_equiv aag t u\<rbrakk> \<Longrightarrow> silc_dom_equiv aag s u
theory CNode_IF

lemma silc_dom_equiv_sym[elim]:
  "silc_dom_equiv aag s t \<Longrightarrow> silc_dom_equiv aag t s" by (auto simp: silc_dom_equiv_def elim: equiv_for_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_dom_equiv aag s t \<Longrightarrow> silc_dom_equiv aag t s
theory CNode_IF

lemma dmo_getActiveIRQ_reads_respects_g :
  "reads_respects_g aag l (invs and only_timer_irq_inv irq st) (do_machine_op (getActiveIRQ in_kernel))" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule dmo_getActiveIRQ_reads_respects) apply (rule doesnt_touch_globalsI) apply (wp dmo_getActiveIRQ_globals_equiv | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_g aag l (invs and only_timer_irq_inv irq st) (do_machine_op (getActiveIRQ in_kernel)) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (do_machine_op (getActiveIRQ in_kernel))
 2. doesnt_touch_globals ?Q1 (do_machine_op (getActiveIRQ in_kernel))
 3. \<And>s. (invs and only_timer_irq_inv irq st) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (do_machine_op (getActiveIRQ in_kernel))
 2. \<And>s. (invs and only_timer_irq_inv irq st) s \<Longrightarrow> (invs and only_timer_irq_inv ?irq5 ?st5 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (invs and only_timer_irq_inv irq st) s \<Longrightarrow> (invs and only_timer_irq_inv ?irq5 ?st5 and ?Q1) s proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma preemption_point_reads_respects_f:
  "reads_respects_f aag l (invs and only_timer_irq_inv irq st' and silc_inv aag st) preemption_point" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_f) apply (rule preemption_point_reads_respects) apply (wp, force+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (invs and only_timer_irq_inv irq st' and silc_inv aag st) preemption_point proof (prove)
goal (2 subgoals):
 1. reads_respects_f aag l ?Q preemption_point
 2. \<And>s. (invs and only_timer_irq_inv irq st' and silc_inv aag st) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P3 preemption_point
 2. \<lbrace>silc_inv aag ?st3 and ?Q3\<rbrace> preemption_point \<lbrace>\<lambda>_. silc_inv aag ?st3\<rbrace>
 3. \<And>s. (invs and only_timer_irq_inv irq st' and silc_inv aag st) s \<Longrightarrow> (silc_inv aag ?st3 and ?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>silc_inv aag ?st3 and ?Q3\<rbrace> preemption_point \<lbrace>\<lambda>_. silc_inv aag ?st3\<rbrace>
 2. \<And>s. (invs and only_timer_irq_inv irq st' and silc_inv aag st) s \<Longrightarrow> (silc_inv aag ?st3 and (invs and only_timer_irq_inv ?irq6 ?st6) and ?Q3) s proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma reads_equiv_f_g_conj:
  "reads_equiv_f_g aag s s' \<equiv> reads_equiv_f aag s s' \<and> reads_equiv_g aag s s'" by (simp add: reads_equiv_f_g_def reads_equiv_f_def reads_equiv_g_def conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_f_g aag s s' \<equiv> reads_equiv_f aag s s' \<and> reads_equiv_g aag s s'
theory CNode_IF

lemma reads_equiv_valid_rv_inv_f:
  assumes a: "reads_equiv_valid_rv_inv A aag R P f"
  assumes b: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  shows "equiv_valid_rv_inv (reads_equiv_f aag) A R P f" apply (clarsimp simp: equiv_valid_2_def reads_equiv_f_def) apply (insert a, clarsimp simp: equiv_valid_2_def) apply (drule_tac x=s in spec, drule_tac x=t in spec, clarsimp) apply (drule (1) bspec, clarsimp) apply (drule (1) bspec, clarsimp) apply (drule state_unchanged[OF b])+ by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv (reads_equiv_f aag) A R 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; reads_equiv aag s t; silc_dom_equiv aag s t; A s t\<rbrakk> \<Longrightarrow> R a aa \<and> reads_equiv aag b ba \<and> silc_dom_equiv aag b ba \<and> A 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; reads_equiv aag s t; silc_dom_equiv aag s t; A s t; \<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> reads_equiv aag s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> R a aa \<and> reads_equiv aag b ba \<and> silc_dom_equiv aag b ba \<and> A 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; reads_equiv aag s t; silc_dom_equiv aag s t; A s t; \<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> reads_equiv aag s' t' \<and> A s' t'\<rbrakk> \<Longrightarrow> R a aa \<and> reads_equiv aag b ba \<and> silc_dom_equiv aag b ba \<and> A 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; reads_equiv aag s t; silc_dom_equiv aag s t; A s t; \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> R a rvb \<and> reads_equiv aag b t' \<and> A b t'\<rbrakk> \<Longrightarrow> R a aa \<and> reads_equiv aag b ba \<and> silc_dom_equiv aag b ba \<and> A 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; reads_equiv aag s t; silc_dom_equiv aag s t; A s t; R a aa; reads_equiv aag b ba; A b ba\<rbrakk> \<Longrightarrow> silc_dom_equiv aag b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>P s; P t; reads_equiv aag s t; silc_dom_equiv aag s t; A s t; R a aa; reads_equiv aag b ba; A b ba; s = b; t = ba\<rbrakk> \<Longrightarrow> silc_dom_equiv aag b ba
theory CNode_IF

lemma set_cap_silc_inv':
  "\<lbrace>silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
                             \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
                                          pasObjectAbs aag (fst lslot) = SilcLabel))
                    and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>
   set_cap cap slot
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_pre) apply (rule set_cap_silc_inv) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<Longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s
theory CNode_IF

lemma set_cap_reads_respects_f:
  "reads_respects_f aag l
     (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
                               \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
                                            pasObjectAbs aag (fst lslot) = SilcLabel))
                      and K (is_subject aag (fst slot))) (set_cap cap slot)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_f[OF set_cap_reads_respects]) apply (wp set_cap_silc_inv') apply (auto simp: silc_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (is_subject aag (fst slot))) (set_cap cap slot) proof (prove)
goal (2 subgoals):
 1. reads_respects_f aag l ?Q (set_cap cap slot)
 2. \<And>s. (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (is_subject aag (fst slot))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>silc_inv aag ?st3 and ?Q3\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. silc_inv aag ?st3\<rbrace>
 2. \<And>s. (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (is_subject aag (fst slot))) s \<Longrightarrow> (silc_inv aag ?st3 and K (aag_can_read aag (fst slot)) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (silc_inv aag ?st3 and ?Q3) s \<Longrightarrow> (silc_inv aag ?st3 and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s
 2. \<And>s. (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (is_subject aag (fst slot))) s \<Longrightarrow> (silc_inv aag ?st3 and K (aag_can_read aag (fst slot)) and ?Q3) s proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma select_ext_ev:
  "(\<And>s t. I s t \<Longrightarrow> A s t \<Longrightarrow> a s \<in> S \<Longrightarrow> a t \<in> S \<Longrightarrow> a s = a t)
   \<Longrightarrow> equiv_valid_inv I A (\<top> :: det_state \<Rightarrow> bool) (select_ext a S)" apply (clarsimp simp: select_ext_def gets_def get_def assert_def return_def bind_def) apply (simp add: equiv_valid_def2 equiv_valid_2_def return_def fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t) \<Longrightarrow> equiv_valid_inv I A (\<lambda>_. True) (select_ext a S) proof (prove)
goal (1 subgoal):
 1. (\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t) \<Longrightarrow> equiv_valid_inv I A (\<lambda>_. True) (\<lambda>s. (\<Union>aa\<in>fst ((if a s \<in> S then return () else fail) s). fst (case aa of (y, sa) \<Rightarrow> ({(a s, sa)}, False)), (\<exists>x\<in>fst ((if a s \<in> S then return () else fail) s). snd (case x of (y, sa) \<Rightarrow> ({(a s, sa)}, False))) \<or> snd ((if a s \<in> S then return () else fail) s))) proof (prove)
goal:
No subgoals!
theory ArchCNode_IF

lemma set_object_globals_equiv'':
  "\<lbrace>globals_equiv s and (\<lambda> s. ptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>t. ptr \<noteq> idle_thread t)\<rbrace>
   set_object ptr obj
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" by (wpsimp wp: set_object_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. ptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>t. ptr \<noteq> idle_thread t)\<rbrace> set_object ptr obj \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchCNode_IF

lemma arch_globals_equiv_irq_state_update[CNode_IF_assms, simp]:
  "arch_globals_equiv ct it kh kh' as as' ms (irq_state_update f ms') =
   arch_globals_equiv ct it kh kh' as as' ms ms'"
  "arch_globals_equiv ct it kh kh' as as' (irq_state_update f ms) ms' =
   arch_globals_equiv ct it kh kh' as as' ms ms'" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_globals_equiv ct it kh kh' as as' ms (irq_state_update f ms') = arch_globals_equiv ct it kh kh' as as' ms ms' &&& arch_globals_equiv ct it kh kh' as as' (irq_state_update f ms) ms' = arch_globals_equiv ct it kh kh' as as' ms ms'
theory ArchCNode_IF

lemma is_irq_at_triv[CNode_IF_assms]:
  assumes a: "\<And>P. \<lbrace>(\<lambda>s. P (irq_masks (machine_state s))) and Q\<rbrace>
                   f
                   \<lbrace>\<lambda>rv s. P (irq_masks (machine_state s))\<rbrace>"
  shows "\<lbrace>(\<lambda>s. P (is_irq_at s)) and Q\<rbrace> f \<lbrace>\<lambda>rv s. P (is_irq_at s)\<rbrace>" apply (clarsimp simp: valid_def is_irq_at_def irq_at_def Let_def) apply (erule use_valid[OF _ a]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (is_irq_at s)) and Q\<rbrace> f \<lbrace>\<lambda>rv s. P (is_irq_at s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P (\<lambda>irq pos. irq_oracle pos \<noteq> 0x3FF \<and> \<not> irq_masks (machine_state s) (irq_oracle pos) \<and> (irq_oracle pos \<noteq> 0x3FF \<and> \<not> irq_masks (machine_state s) (irq_oracle pos) \<longrightarrow> irq_oracle pos = irq)); Q s\<rbrakk> \<Longrightarrow> P (\<lambda>irq pos. irq_oracle pos \<noteq> 0x3FF \<and> \<not> irq_masks (machine_state b) (irq_oracle pos) \<and> (irq_oracle pos \<noteq> 0x3FF \<and> \<not> irq_masks (machine_state b) (irq_oracle pos) \<longrightarrow> irq_oracle pos = irq)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P (\<lambda>irq pos. irq_oracle pos \<noteq> 0x3FF \<and> \<not> irq_masks (machine_state s) (irq_oracle pos) \<and> (irq_oracle pos \<noteq> 0x3FF \<and> \<not> irq_masks (machine_state s) (irq_oracle pos) \<longrightarrow> irq_oracle pos = irq)); Q s\<rbrakk> \<Longrightarrow> ((\<lambda>s. P (\<lambda>irq pos. irq_oracle pos \<noteq> 0x3FF \<and> \<not> irq_masks (machine_state s) (irq_oracle pos) \<and> (irq_oracle pos \<noteq> 0x3FF \<and> \<not> irq_masks (machine_state s) (irq_oracle pos) \<longrightarrow> irq_oracle pos = irq))) and Q) s proof (prove)
goal:
No subgoals!
theory ArchCNode_IF

lemma is_irq_at_not_masked[CNode_IF_assms]:
  "is_irq_at s irq pos \<Longrightarrow> \<not> irq_masks (machine_state s) irq" by (clarsimp simp: is_irq_at_def irq_at_def split: option.splits simp: Let_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_irq_at s irq pos \<Longrightarrow> \<not> irq_masks (machine_state s) irq
theory ArchCNode_IF

lemma dmo_getActiveIRQ_reads_respects[CNode_IF_assms]:
  notes gets_ev[wp del]
  shows "reads_respects aag l (invs and only_timer_irq_inv irq st)
                       (do_machine_op (getActiveIRQ in_kernel))" apply (rule use_spec_ev) apply (rule do_machine_op_spec_reads_respects') apply (simp add: getActiveIRQ_def) apply (wp irq_state_increment_reads_respects_memory irq_state_increment_reads_respects_device
             gets_ev[where f="irq_oracle \<circ> irq_state"] equiv_valid_inv_conj_lift
             gets_irq_masks_equiv_valid modify_wp
          | simp add: no_irq_def)+ apply (rule only_timer_irq_inv_determines_irq_masks, blast+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (invs and only_timer_irq_inv irq st) (do_machine_op (getActiveIRQ in_kernel)) proof (prove)
goal (1 subgoal):
 1. \<And>sta. spec_reads_respects sta aag l (invs and only_timer_irq_inv irq st) (do_machine_op (getActiveIRQ in_kernel)) proof (prove)
goal (2 subgoals):
 1. \<And>st. equiv_valid_inv (equiv_machine_state (aag_can_read aag) and equiv_irq_state) (equiv_machine_state (aag_can_affect aag l)) (?Q2 st) (getActiveIRQ in_kernel)
 2. \<And>sta s. (invs and only_timer_irq_inv irq st) s \<Longrightarrow> ?Q2 sta (machine_state s) proof (prove)
goal (2 subgoals):
 1. \<And>st. equiv_valid_inv (equiv_machine_state (aag_can_read aag) and equiv_irq_state) (equiv_machine_state (aag_can_affect aag l)) (?Q2 st) (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>sta s. (invs and only_timer_irq_inv irq st) s \<Longrightarrow> ?Q2 sta (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>sta s. invs s \<and> only_timer_irq_inv irq st s \<Longrightarrow> \<not> irq_masks (machine_state s) (?irq18 sta) \<and> (\<forall>x. x \<noteq> ?irq18 sta \<longrightarrow> irq_masks (machine_state s) x) proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma gets_any_evrv:
  "equiv_valid_rv_inv I A \<top>\<top> \<top> (gets f)" by (clarsimp simp: equiv_valid_2_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (\<lambda>_ _. True) (\<lambda>_. True) (gets f)
theory Retype_IF

lemma select_f_any_evrv:
  "equiv_valid_rv_inv I A \<top>\<top> \<top> (select_f f)" by (clarsimp simp: equiv_valid_2_def select_f_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (\<lambda>_ _. True) (\<lambda>_. True) (select_f f)
theory Retype_IF

lemma select_f_any_ev2:
  "equiv_valid_2 I A A \<top>\<top> \<top> \<top> (select_f f) (select_f f')" by (clarsimp simp: equiv_valid_2_def select_f_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A A (\<lambda>_ _. True) (\<lambda>_. True) (\<lambda>_. True) (select_f f) (select_f f')
theory Retype_IF

lemma equiv_machine_state_machine_state_rest_update:
  "equiv_machine_state P s t
   \<Longrightarrow> equiv_machine_state P (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)" by (fastforce intro: equiv_forI elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_machine_state P s t \<Longrightarrow> equiv_machine_state P (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)
theory Retype_IF

lemma machine_op_lift_ev:
  "equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) \<top> (machine_op_lift mop)" apply (rule equiv_valid_guard_imp) apply (rule machine_op_lift_ev') apply clarsimp apply (intro conjI impI) apply (drule equiv_machine_state_machine_state_rest_update, fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (machine_op_lift mop) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) ?Q (machine_op_lift mop)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t x y. (equiv_machine_state P s t \<longrightarrow> equiv_machine_state P (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (equiv_machine_state Q s t \<longrightarrow> equiv_machine_state Q (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>))) s proof (prove)
goal (1 subgoal):
 1. \<And>s t x y. (equiv_machine_state P s t \<longrightarrow> equiv_machine_state P (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (equiv_machine_state Q s t \<longrightarrow> equiv_machine_state Q (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) proof (prove)
goal (4 subgoals):
 1. \<And>s t x y. equiv_machine_state P s t \<Longrightarrow> equiv_for P underlying_memory (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)
 2. \<And>s t x y. equiv_machine_state P s t \<Longrightarrow> equiv_for P device_state (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)
 3. \<And>s t x y. equiv_machine_state Q s t \<Longrightarrow> equiv_for Q underlying_memory (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)
 4. \<And>s t x y. equiv_machine_state Q s t \<Longrightarrow> equiv_for Q device_state (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>) proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma machine_op_lift_irq_state[wp]:
  "machine_op_lift mop \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace>" by (simp add: machine_op_lift_def machine_rest_lift_def | wp | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace>