kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchPasUpdates

lemma state_asids_to_policy_aux_pasMayActivate_update:
  "state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs =
   state_asids_to_policy_aux aag caps asid_tab vrefs" apply (rule equalityI) apply clarify apply (erule state_asids_to_policy_aux.cases
          | simp
          | fastforce intro: state_asids_to_policy_aux.intros)+ apply clarify apply (erule state_asids_to_policy_aux.cases) apply (simp, subst pasObjectAbs_pasMayActivate_update[symmetric]
               , subst pasASIDAbs_pasMayActivate_update[symmetric]
               , rule state_asids_to_policy_aux.intros
               , assumption+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs = state_asids_to_policy_aux aag caps asid_tab vrefs proof (prove)
goal (2 subgoals):
 1. state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs \<subseteq> state_asids_to_policy_aux aag caps asid_tab vrefs
 2. state_asids_to_policy_aux aag caps asid_tab vrefs \<subseteq> state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux aag caps asid_tab vrefs
 2. state_asids_to_policy_aux aag caps asid_tab vrefs \<subseteq> state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy_aux aag caps asid_tab vrefs \<subseteq> state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_asids_to_policy_aux aag caps asid_tab vrefs \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ptr acap asid. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasASIDAbs aag asid; caps ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs aag asid; aa = ab; b = pasObjectAbs aag pdptr; asid_tab (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> vrefs poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs
 3. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs aag poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asid; asid_tab (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs proof (prove)
goal:
No subgoals!
theory ArchPasUpdates

lemma state_asids_to_policy_pasMayActivate_update[PasUpdates_assms]:
  "state_asids_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s =
   state_asids_to_policy aag s" by (simp add: state_asids_to_policy_aux_pasMayActivate_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s = state_asids_to_policy aag s
theory ArchPasUpdates

lemma state_asids_to_policy_aux_pasMayEditReadyQueues_update:
  "state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs =
   state_asids_to_policy_aux aag caps asid_tab vrefs" apply (rule equalityI) apply (clarify) apply (erule state_asids_to_policy_aux.cases
          | simp
          | fastforce intro: state_asids_to_policy_aux.intros)+ apply (clarify) apply (erule state_asids_to_policy_aux.cases) apply (simp, subst pasObjectAbs_pasMayEditReadyQueues_update[symmetric]
               , subst pasASIDAbs_pasMayEditReadyQueues_update[symmetric]
               , rule state_asids_to_policy_aux.intros
               , assumption+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs = state_asids_to_policy_aux aag caps asid_tab vrefs proof (prove)
goal (2 subgoals):
 1. state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs \<subseteq> state_asids_to_policy_aux aag caps asid_tab vrefs
 2. state_asids_to_policy_aux aag caps asid_tab vrefs \<subseteq> state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux aag caps asid_tab vrefs
 2. state_asids_to_policy_aux aag caps asid_tab vrefs \<subseteq> state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy_aux aag caps asid_tab vrefs \<subseteq> state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_asids_to_policy_aux aag caps asid_tab vrefs \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ptr acap asid. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasASIDAbs aag asid; caps ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs aag asid; aa = ab; b = pasObjectAbs aag pdptr; asid_tab (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> vrefs poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs
 3. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs aag poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asid; asid_tab (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs proof (prove)
goal:
No subgoals!
theory ArchPasUpdates

lemma state_asids_to_policy_pasMayEditReadyQueues_update[PasUpdates_assms]:
  "state_asids_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s =
   state_asids_to_policy aag s" by (simp add: state_asids_to_policy_aux_pasMayEditReadyQueues_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s = state_asids_to_policy aag s
theory IRQMasks_IF

lemma detype_irq_masks[simp]:
  "irq_masks (machine_state (detype S s)) = irq_masks_of_state s" by (simp add: detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_masks_of_state (detype S s) = irq_masks_of_state s
theory IRQMasks_IF

lemma invoke_irq_handler_irq_masks:
  "\<lbrace>domain_sep_inv False st and (\<lambda>s. (\<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s))\<rbrace>
   invoke_irq_handler blah
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" by (clarsimp simp: valid_def domain_sep_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and (\<lambda>s. \<exists>ptr'. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s)\<rbrace> invoke_irq_handler blah \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
theory IRQMasks_IF

lemma empty_slot_irq_masks:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and K (irq_opt = NullCap)\<rbrace>
   empty_slot slot irq_opt
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" apply (rule hoare_gen_asm) apply (wpsimp simp: empty_slot_def post_cap_deletion_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and K (irq_opt = NullCap)\<rbrace> empty_slot slot irq_opt \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. irq_opt = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> empty_slot slot irq_opt \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory IRQMasks_IF

lemma spec_strengthen_errE:
  "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E'\<rbrace>; \<And>s r. E' s r \<Longrightarrow> E s r \<rbrakk>
     \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" by (auto simp: spec_validE_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E'\<rbrace>; \<And>s r. E' s r \<Longrightarrow> E s r\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory IRQMasks_IF

lemma rec_del_irq_masks:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace>
   rec_del call
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" apply (rule use_spec) apply (rule hoare_pre_spec_validE) apply (rule spec_strengthen_postE) apply (rule spec_strengthen_errE[OF rec_del_irq_masks']) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> rec_del call \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<turnstile> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> rec_del call \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?P'2 s\<rbrace> rec_del call \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>s. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s \<Longrightarrow> ?P'2 s s proof (prove)
goal (3 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?P'2 s\<rbrace> rec_del call \<lbrace>?Q'5 s\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>s sa r. ?Q'5 s sa r \<Longrightarrow> P (irq_masks_of_state r)
 3. \<And>s. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s \<Longrightarrow> ?P'2 s s proof (prove)
goal (3 subgoals):
 1. \<And>s sa r. (domain_sep_inv False (?st9 s) and (\<lambda>sa. ?P9 s (irq_masks_of_state sa))) r \<Longrightarrow> P (irq_masks_of_state r)
 2. \<And>s sa r. (case call of FinaliseSlotCall x y \<Rightarrow> y \<or> fst sa \<longrightarrow> snd sa = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False (?st9 s) r \<and> ?P9 s (irq_masks_of_state r) \<Longrightarrow> P (irq_masks_of_state r)
 3. \<And>s. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s \<Longrightarrow> ((\<lambda>sa. ?P9 s (irq_masks_of_state sa)) and domain_sep_inv False (?st9 s)) s proof (prove)
goal:
No subgoals!
theory IRQMasks_IF

lemma cap_delete_irq_masks:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace>
   cap_delete blah
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>,\<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" by (simp add: cap_delete_def) (wpsimp wp: rec_del_irq_masks)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> cap_delete blah \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
theory IRQMasks_IF

lemma invoke_irq_control_irq_masks:
  "\<lbrace>domain_sep_inv False (st :: 's state) and irq_control_inv_valid ivk\<rbrace>
   invoke_irq_control ivk
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" apply (cases ivk) apply (clarsimp simp: irq_control_inv_valid_def domain_sep_inv_def valid_def) apply (clarsimp simp: arch_invoke_irq_control_irq_masks) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and irq_control_inv_valid ivk\<rbrace> invoke_irq_control ivk \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. ivk = IRQControl x11 x12 x13 \<Longrightarrow> \<lbrace>domain_sep_inv False st and irq_control_inv_valid ivk\<rbrace> invoke_irq_control ivk \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x2. ivk = ArchIRQControl x2 \<Longrightarrow> \<lbrace>domain_sep_inv False st and irq_control_inv_valid ivk\<rbrace> invoke_irq_control ivk \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2. ivk = ArchIRQControl x2 \<Longrightarrow> \<lbrace>domain_sep_inv False st and irq_control_inv_valid ivk\<rbrace> invoke_irq_control ivk \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory IRQMasks_IF

lemma checked_insert_irq_masks[wp]:
  "check_cap_at a b (check_cap_at c d (cap_insert e f g)) \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>" by (wpsimp simp: check_cap_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> check_cap_at a b (check_cap_at c d (cap_insert e f g)) \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
theory IRQMasks_IF

lemma preemption_point_irq_masks[wp]:
  "preemption_point \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>" by (wp preemption_point_inv, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> preemption_point \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
theory IRQMasks_IF

lemma finalise_slot_irq_masks:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace>
   finalise_slot p e
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" by (simp add: finalise_slot_def | wp rec_del_irq_masks)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> finalise_slot p e \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
theory IRQMasks_IF

lemma handle_yield_irq_masks_of_state[wp]:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace>
   handle_yield
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" by (wpsimp simp: handle_yield_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace> handle_yield \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
theory IRQMasks_IF

lemma handle_event_irq_masks:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (st :: 's state) and invs\<rbrace>
   handle_event ev
   \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>" apply ((case_tac ev, rename_tac syscall, case_tac syscall);
         (solves \<open>(simp add: handle_send_def handle_call_def
                   | wp handle_invocation_irq_masks[where st=st]
                        handle_interrupt_irq_masks[where st=st]
                         hoare_vcg_all_lift
                   | wpc
                   | wp (once) hoare_drop_imps)+\<close>)?) apply simp apply (wp handle_interrupt_irq_masks[where st=st] | wpc | simp)+ apply (rule_tac Q="\<lambda>rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and>
                             (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)" in hoare_strengthen_post) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace> handle_event ev \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. ev = Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace> handle_event ev \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. ev = Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace> liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. ev = Interrupt \<Longrightarrow> \<lbrace>?Q126\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>x s. (x = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>xa. x = Some xa \<longrightarrow> P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> xa \<le> maxIRQ)\<rbrace>
 2. \<And>s. \<lbrakk>ev = Interrupt; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs) s\<rbrakk> \<Longrightarrow> ?Q126 s proof (prove)
goal (3 subgoals):
 1. ev = Interrupt \<Longrightarrow> \<lbrace>?Q126\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)\<rbrace>
 2. \<And>rv s. \<lbrakk>ev = Interrupt; P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)\<rbrakk> \<Longrightarrow> (rv = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. rv = Some x \<longrightarrow> P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> x \<le> maxIRQ)
 3. \<And>s. \<lbrakk>ev = Interrupt; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs) s\<rbrakk> \<Longrightarrow> ?Q126 s proof (prove)
goal:
No subgoals!
theory ArchIRQMasks_IF

lemma delete_objects_irq_masks[IRQMasks_IF_assms, wp]:
  "delete_objects ptr bits \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>" apply (simp add: delete_objects_def) apply (wp dmo_wp no_irq_mapM_x no_irq | simp add: freeMemory_def no_irq_storeWord)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> do y <- do_machine_op (freeMemory ptr bits);
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchIRQMasks_IF

lemma arch_invoke_irq_control_irq_masks[IRQMasks_IF_assms]:
  "\<lbrace>domain_sep_inv False st and arch_irq_control_inv_valid invok\<rbrace>
   arch_invoke_irq_control invok
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" apply (case_tac invok) apply (clarsimp simp: arch_irq_control_inv_valid_def domain_sep_inv_def valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and arch_irq_control_inv_valid invok\<rbrace> arch_invoke_irq_control invok \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. invok = ArchIRQControlIssue x1 x2 x3 x4 \<Longrightarrow> \<lbrace>domain_sep_inv False st and arch_irq_control_inv_valid invok\<rbrace> arch_invoke_irq_control invok \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchIRQMasks_IF

lemma dmo_getActiveIRQ_irq_masks[IRQMasks_IF_assms, wp]:
  "do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>" apply (rule hoare_pre, rule dmo_wp) apply (simp add: getActiveIRQ_def | wp | simp add: no_irq_def | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrace>?P3 s\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>a b. P (irq_masks_of_state (s\<lparr>machine_state := b\<rparr>))\<rbrace>
 2. \<And>s. P (irq_masks_of_state s) \<Longrightarrow> ?P3 s (machine_state s) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma set_irq_state_reads_respects:
  "reads_respects aag l \<top> (set_irq_state state irq)" unfolding set_irq_state_def fun_app_def apply (wp dmo_maskInterrupt_reads_respects) apply (subst equiv_valid_def2) apply (rule_tac P="\<top>" and P'="\<top>" in modify_ev2) apply (fastforce elim: affects_equivE reads_equivE equiv_forE intro: equiv_forI
                   intro!: reads_equiv_interrupt_states_update affects_equiv_interrupt_states_update) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_irq_state state irq) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>);
do_machine_op (maskInterrupt (state = IRQInactive) irq)
od) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P' (modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>))
 2. \<lbrace>?P''\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ?P' (modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>))
 2. \<lbrace>?P''\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv aag (s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) (t\<lparr>interrupt_states := (interrupt_states t)(irq := state)\<rparr>) \<and> affects_equiv aag l (s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) (t\<lparr>interrupt_states := (interrupt_states t)(irq := state)\<rparr>)
 2. \<lbrace>?P''\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> True \<and> ?P'' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>s. True \<Longrightarrow> True \<and> ?P'' s proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma deleted_irq_handler_reads_respects:
  "reads_respects aag l \<top> (deleted_irq_handler irq)" unfolding deleted_irq_handler_def by (rule set_irq_state_reads_respects)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (deleted_irq_handler irq) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_irq_state IRQInactive irq)
theory Finalise_IF

lemma scheduler_action_states_equiv[simp]:
  "states_equiv_for P Q R S st (scheduler_action_update f s) = states_equiv_for P Q R S st s" by (simp add: states_equiv_for_def equiv_for_def equiv_asids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P Q R S st (scheduler_action_update f s) = states_equiv_for P Q R S st s