theory Interrupt_DR

lemma handle_interrupt_corres:
  "dcorres dc \<top> (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (Interrupt_A.handle_interrupt x)" apply (clarsimp simp:Interrupt_A.handle_interrupt_def) apply (clarsimp simp:get_irq_state_def gets_def bind_assoc) apply (rule conjI; rule impI) apply (subst Interrupt_D.handle_interrupt_def, simp) apply (subst Retype_AI.do_machine_op_bind) apply (rule maskInterrupt_empty_fail) apply (rule ackInterrupt_empty_fail) using corres_guard2_imp handle_interrupt_corres_branch apply blast apply (rule dcorres_absorb_get_r)+ apply (clarsimp split:irq_state.splits simp:corres_free_fail | rule conjI)+ apply (simp add:Interrupt_D.handle_interrupt_def bind_assoc) apply (rule corres_guard_imp) apply (rule_tac Q'="(=) s'" in corres_split[OF dcorres_get_irq_slot]) apply (rule_tac R'="\<lambda>rv.  (\<lambda>s. (is_ntfn_cap rv \<longrightarrow> ntfn_at (obj_ref_of rv) s)) and invs and valid_etcbs"
               in corres_split) apply (rule option_get_cap_corres; simp) apply (case_tac rv'a) prefer 4 apply (simp_all add:when_def) apply (clarsimp simp:transform_cap_def when_def is_ntfn_cap_def | rule conjI)+ apply (rule corres_dummy_return_l) apply (rule corres_split_forwards' [where Q'="\<lambda>rv. \<top>" and Q = "\<lambda>rv. \<top>"]) apply (rule corres_guard_imp[OF send_signal_corres]) apply (simp+) apply (clarsimp simp:handle_interrupt_corres_branch dc_def[symmetric])+ apply (simp add: corres_guard_imp[OF handle_interrupt_corres_branch])+ apply (clarsimp simp:transform_cap_def when_def is_ntfn_cap_def
                   split:arch_cap.splits)+ apply (simp add: corres_guard_imp[OF handle_interrupt_corres_branch])+ apply (wp hoare_vcg_prop[where P=True] valid_state_get_cap_wp|simp add:get_irq_slot_def)+ apply (clarsimp simp:invs_def ) apply (strengthen irq_node_image_not_idle,simp add:valid_state_def) apply (clarsimp simp:Interrupt_D.handle_interrupt_def gets_def) apply (rule conjI; rule impI) apply (rule dcorres_absorb_get_l)+ apply (clarsimp simp:CSpace_D.get_irq_slot_def) apply (subgoal_tac "caps_of_state s'b (interrupt_irq_node s'b x,[])\<noteq> None") apply (drule irq_state_IRQSignal_NullCap) apply ((simp add:invs_def valid_state_def)+) apply (frule caps_of_state_transform_opt_cap) apply clarsimp apply clarsimp apply (drule(1) irq_node_image_not_idle[where y = x]) apply (clarsimp simp:not_idle_thread_def) apply (clarsimp simp:transform_cslot_ptr_def) apply (subgoal_tac "cdl_irq_node (transform s'b) x = (interrupt_irq_node s'b x)") apply clarsimp apply (rule corres_guard_imp,rule corres_dummy_return_pl) apply (simp add: bind_assoc) apply (rule dcorres_rhs_noop_above[OF timer_tick_dcorres]) apply (rule dcorres_symb_exec_r[OF dcorres_machine_op_noop]) apply (wp dmo_dwp hoare_TrueI| simp)+ apply (clarsimp simp:transform_def invs_def valid_state_def dest!: valid_irq_node_cte_at_irq_slot)+ apply (simp add:cte_wp_at_caps_of_state) apply (rule dcorres_absorb_get_l)+ apply (clarsimp simp:CSpace_D.get_irq_slot_def handle_reserved_irq_def) apply (subgoal_tac "caps_of_state s'b (interrupt_irq_node s'b x,[])\<noteq> None") apply (drule irq_state_IRQSignal_NullCap) apply ((simp add:invs_def valid_state_def)+) apply (frule caps_of_state_transform_opt_cap) apply clarsimp apply clarsimp apply (drule(1) irq_node_image_not_idle[where y = x]) apply (clarsimp simp:not_idle_thread_def) apply (clarsimp simp:transform_cslot_ptr_def) apply (subgoal_tac "cdl_irq_node (transform s'b) x = (interrupt_irq_node s'b x)") apply clarsimp apply (rule corres_guard_imp) apply (rule dcorres_machine_op_noop) apply wp apply (clarsimp simp:transform_def invs_def valid_state_def dest!: valid_irq_node_cte_at_irq_slot)+ apply (simp add:cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (Interrupt_A.handle_interrupt x) proof (prove)
goal (1 subgoal):
 1. (maxIRQ < x \<longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do_machine_op (do y <- maskInterrupt True x;
ackInterrupt x
od))) \<and> (\<not> maxIRQ < x \<longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do st <- get_irq_state x;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (1 subgoal):
 1. (maxIRQ < x \<longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do_machine_op (do y <- maskInterrupt True x;
ackInterrupt x
od))) \<and> (\<not> maxIRQ < x \<longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do s <- get;
y <- case interrupt_states s x of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (2 subgoals):
 1. maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do_machine_op (do y <- maskInterrupt True x;
ackInterrupt x
od))
 2. \<not> maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do s <- get;
y <- case interrupt_states s x of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (2 subgoals):
 1. maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (return ()) (do_machine_op (do y <- maskInterrupt True x;
ackInterrupt x
od))
 2. \<not> maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do s <- get;
y <- case interrupt_states s x of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (4 subgoals):
 1. maxIRQ < x \<Longrightarrow> empty_fail (maskInterrupt True x)
 2. \<And>xa. maxIRQ < x \<Longrightarrow> empty_fail (ackInterrupt x)
 3. maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (return ()) (do rv <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 4. \<not> maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do s <- get;
y <- case interrupt_states s x of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (3 subgoals):
 1. \<And>xa. maxIRQ < x \<Longrightarrow> empty_fail (ackInterrupt x)
 2. maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (return ()) (do rv <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<not> maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do s <- get;
y <- case interrupt_states s x of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (2 subgoals):
 1. maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (return ()) (do rv <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<not> maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do s <- get;
y <- case interrupt_states s x of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
using this:
\<lbrakk>corres_underlying ?sr ?nf ?nf' ?r ?P ?Q' ?f ?g; \<And>s. ?P' s \<Longrightarrow> ?Q' s\<rbrakk> \<Longrightarrow> corres_underlying ?sr ?nf ?nf' ?r ?P ?P' ?f ?g
dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do y <- do_machine_op (maskInterrupt True ?x);
do_machine_op (ackInterrupt ?x)
od)

goal (2 subgoals):
 1. maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (return ()) (do rv <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<not> maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do s <- get;
y <- case interrupt_states s x of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (1 subgoal):
 1. \<not> maxIRQ < x \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (do s <- get;
y <- case interrupt_states s x of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>\<not> maxIRQ < x; True; (invs and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- case interrupt_states s' x of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
when (Structures_A.is_ntfn_cap cap \<and> AllowSend \<in> Structures_A.cap_rights cap) $ Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal x
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do slot <- KHeap_A.get_irq_slot x;
cap <- CSpaceAcc_A.get_cap slot;
y <- when (Structures_A.is_ntfn_cap cap \<and> AllowWrite \<in> Structures_A.cap_rights cap) (Ipc_A.send_signal (obj_ref_of cap) (cap_ep_badge cap));
do_machine_op (maskInterrupt True x)
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do irq_slot <- gets (CSpace_D.get_irq_slot x);
gets (opt_cap irq_slot) >>= case_option (return ()) (case_cdl_cap (return ()) (\<lambda>bool set1 set2. return ()) (\<lambda>word1 word2 set. return ()) (\<lambda>obj x rights. if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return ()) (\<lambda>word set. return ()) (\<lambda>word. return ()) (\<lambda>word1 word2 nat1 nat2. return ()) (\<lambda>word. return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. return ()) (\<lambda>word bool1 bool2. return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word. return ()) (\<lambda>bool word set nat cdl_frame_cap_type option. return ()) (\<lambda>word cdl_frame_cap_type option. return ()) (\<lambda>word cdl_frame_cap_type option. return ()) (return ()) (\<lambda>word nat. return ()) (\<lambda>word set. return ()) (return ()) (\<lambda>word. return ()) (\<lambda>word. return ()) (\<lambda>word. return ()) (\<lambda>word. return ()))
od) (do xa <- KHeap_A.get_irq_slot x;
xa <- CSpaceAcc_A.get_cap xa;
xa <- when (Structures_A.is_ntfn_cap xa \<and> AllowWrite \<in> Structures_A.cap_rights xa) (Ipc_A.send_signal (obj_ref_of xa) (cap_ep_badge xa));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 s') (?Q'60 s') (do irq_slot <- gets (CSpace_D.get_irq_slot x);
gets (opt_cap irq_slot) >>= case_option (return ()) (case_cdl_cap (return ()) (\<lambda>bool set1 set2. return ()) (\<lambda>word1 word2 set. return ()) (\<lambda>obj x rights. if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return ()) (\<lambda>word set. return ()) (\<lambda>word. return ()) (\<lambda>word1 word2 nat1 nat2. return ()) (\<lambda>word. return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. return ()) (\<lambda>word bool1 bool2. return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word. return ()) (\<lambda>bool word set nat cdl_frame_cap_type option. return ()) (\<lambda>word cdl_frame_cap_type option. return ()) (\<lambda>word cdl_frame_cap_type option. return ()) (return ()) (\<lambda>word nat. return ()) (\<lambda>word set. return ()) (return ()) (\<lambda>word. return ()) (\<lambda>word. return ()) (\<lambda>word. return ()) (\<lambda>word. return ()))
od) (do xa <- KHeap_A.get_irq_slot x;
xa <- CSpaceAcc_A.get_cap xa;
xa <- when (Structures_A.is_ntfn_cap xa \<and> AllowWrite \<in> Structures_A.cap_rights xa) (Ipc_A.send_signal (obj_ref_of xa) (cap_ep_badge xa));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; transform s' = s\<rbrakk> \<Longrightarrow> ?Q60 s' s
 3. \<And>s' s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; s' = s\<rbrakk> \<Longrightarrow> ?Q'60 s' s
 4. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (6 subgoals):
 1. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R64 s' rv) (?R'64 s' rv') (gets (opt_cap rv) >>= case_option (return ()) (case_cdl_cap (return ()) (\<lambda>bool set1 set2. return ()) (\<lambda>word1 word2 set. return ()) (\<lambda>obj x rights. if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return ()) (\<lambda>word set. return ()) (\<lambda>word. return ()) (\<lambda>word1 word2 nat1 nat2. return ()) (\<lambda>word. return ()) (return ()) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. return ()) (\<lambda>word bool1 bool2. return ()) (\<lambda>word. return ()) (return ()) (return ()) (return ()) (\<lambda>word. return ()) (\<lambda>bool word set nat cdl_frame_cap_type option. return ()) (\<lambda>word cdl_frame_cap_type option. return ()) (\<lambda>word cdl_frame_cap_type option. return ()) (return ()) (\<lambda>word nat. return ()) (\<lambda>word set. return ()) (return ()) (\<lambda>word. return ()) (\<lambda>word. return ()) (\<lambda>word. return ()) (\<lambda>word. return ()))) (do xa <- CSpaceAcc_A.get_cap rv';
xa <- when (Structures_A.is_ntfn_cap xa \<and> AllowWrite \<in> Structures_A.cap_rights xa) (Ipc_A.send_signal (obj_ref_of xa) (cap_ep_badge xa));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q64 s'\<rbrace> gets (CSpace_D.get_irq_slot x) \<lbrace>?R64 s'\<rbrace>
 3. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.get_irq_slot x \<lbrace>?R'64 s'\<rbrace>
 4. \<And>s' s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q64 s') s
 5. \<And>s' s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (=) s') s
 6. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (9 subgoals):
 1. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> dcorres (?r'66 s' rv rv') (?P67 s' rv) (?P'69 s' rv') (gets (opt_cap rv)) (CSpaceAcc_A.get_cap rv')
 2. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; ?r'66 s' rv rv' rva rv'a\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q68 s' rv\<rbrace> gets (opt_cap rv) \<lbrace>?R66 s' rv rv'\<rbrace>
 4. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'70 s' rv'\<rbrace> CSpaceAcc_A.get_cap rv' \<lbrace>\<lambda>rv. (\<lambda>s. Structures_A.is_ntfn_cap rv \<longrightarrow> ntfn_at (obj_ref_of rv) s) and invs and valid_etcbs\<rbrace>
 5. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q64 s'\<rbrace> gets (CSpace_D.get_irq_slot x) \<lbrace>\<lambda>rv. ?P67 s' rv and ?Q68 s' rv\<rbrace>
 6. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.get_irq_slot x \<lbrace>\<lambda>rv'. ?P'69 s' rv' and ?Q'70 s' rv'\<rbrace>
 7. \<And>s' s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q64 s') s
 8. \<And>s' s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (=) s') s
 9. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (8 subgoals):
 1. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a)\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q68 s' rv\<rbrace> gets (opt_cap rv) \<lbrace>?R66 s' rv rv'\<rbrace>
 3. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'70 s' rv'\<rbrace> CSpaceAcc_A.get_cap rv' \<lbrace>\<lambda>rv. (\<lambda>s. Structures_A.is_ntfn_cap rv \<longrightarrow> ntfn_at (obj_ref_of rv) s) and invs and valid_etcbs\<rbrace>
 4. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q64 s'\<rbrace> gets (CSpace_D.get_irq_slot x) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q68 s' rv\<rbrace>
 5. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.get_irq_slot x \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread (fst rv') and valid_etcbs and ?Q'70 s' rv'\<rbrace>
 6. \<And>s' s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q64 s') s
 7. \<And>s' s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (=) s') s
 8. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (19 subgoals):
 1. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' rv rv' rva rv'a x21 x22 x23 x24. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<And>s' rv rv' rva rv'a x31 x32 x33. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 4. \<And>s' rv rv' rva rv'a x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 5. \<And>s' rv rv' rva rv'a x51 x52 x53. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 6. \<And>s' rv rv' rva rv'a x61 x62 x63. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 7. \<And>s' rv rv' rva rv'a x7. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 8. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 9. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 10. \<And>s' rv rv' rva rv'a x10. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
A total of 19 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>s' rv rv' rva rv'a x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<And>s' rv rv' rva rv'a x21 x22 x23 x24. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 4. \<And>s' rv rv' rva rv'a x31 x32 x33. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 5. \<And>s' rv rv' rva rv'a x51 x52 x53. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 6. \<And>s' rv rv' rva rv'a x61 x62 x63. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 7. \<And>s' rv rv' rva rv'a x7. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 8. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 9. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 10. \<And>s' rv rv' rva rv'a x10. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap rv'a); rv'a = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' rv rv' rva) ((\<lambda>s. Structures_A.is_ntfn_cap rv'a \<longrightarrow> ntfn_at (obj_ref_of rv'a) s) and invs and valid_etcbs) (case rva of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do xa <- when (Structures_A.is_ntfn_cap rv'a \<and> AllowWrite \<in> Structures_A.cap_rights rv'a) (Ipc_A.send_signal (obj_ref_of rv'a) (cap_ep_badge rv'a));
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
A total of 19 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>s' rv rv' rva rv'a x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.NotificationCap x41 x42 x43); rv'a = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x43 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (Endpoint_D.send_signal x41) (do xa <- Ipc_A.send_signal x41 x42;
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)) \<and> (AllowWrite \<notin> x43 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od))
 2. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.NullCap; rv'a = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.NullCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<And>s' rv rv' rva rv'a x21 x22 x23 x24. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)); rv'a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 4. \<And>s' rv rv' rva rv'a x31 x32 x33. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.EndpointCap x31 x32 x33); rv'a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.EndpointCap x31 x32 x33))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 5. \<And>s' rv rv' rva rv'a x51 x52 x53. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53); rv'a = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (MasterReplyCap x51))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)) \<and> (\<not> x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.ReplyCap x51 x53))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od))
 6. \<And>s' rv rv' rva rv'a x61 x62 x63. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62); rv'a = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 7. \<And>s' rv rv' rva rv'a x7. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (TcbCap x7); rv'a = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (TcbCap x7))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 8. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.DomainCap; rv'a = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.DomainCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 9. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some IrqControlCap; rv'a = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some IrqControlCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 10. \<And>s' rv rv' rva rv'a x10. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (IrqHandlerCap x10); rv'a = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (IrqHandlerCap x10))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
A total of 17 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (Endpoint_D.send_signal x41) (do xa <- Ipc_A.send_signal x41 x42;
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> AllowWrite \<notin> x43 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.NullCap; rv'a = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.NullCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 4. \<And>s' rv rv' rva rv'a x21 x22 x23 x24. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)); rv'a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 5. \<And>s' rv rv' rva rv'a x31 x32 x33. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.EndpointCap x31 x32 x33); rv'a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.EndpointCap x31 x32 x33))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 6. \<And>s' rv rv' rva rv'a x51 x52 x53. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53); rv'a = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (MasterReplyCap x51))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)) \<and> (\<not> x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.ReplyCap x51 x53))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od))
 7. \<And>s' rv rv' rva rv'a x61 x62 x63. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62); rv'a = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 8. \<And>s' rv rv' rva rv'a x7. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (TcbCap x7); rv'a = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (TcbCap x7))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 9. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.DomainCap; rv'a = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.DomainCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 10. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some IrqControlCap; rv'a = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some IrqControlCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (Endpoint_D.send_signal x41 >>= return) (do xa <- Ipc_A.send_signal x41 x42;
y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> AllowWrite \<notin> x43 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.NullCap; rv'a = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.NullCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 4. \<And>s' rv rv' rva rv'a x21 x22 x23 x24. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)); rv'a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 5. \<And>s' rv rv' rva rv'a x31 x32 x33. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.EndpointCap x31 x32 x33); rv'a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.EndpointCap x31 x32 x33))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 6. \<And>s' rv rv' rva rv'a x51 x52 x53. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53); rv'a = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (MasterReplyCap x51))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)) \<and> (\<not> x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.ReplyCap x51 x53))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od))
 7. \<And>s' rv rv' rva rv'a x61 x62 x63. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62); rv'a = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 8. \<And>s' rv rv' rva rv'a x7. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (TcbCap x7); rv'a = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (TcbCap x7))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 9. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.DomainCap; rv'a = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.DomainCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 10. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some IrqControlCap; rv'a = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some IrqControlCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
A total of 18 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> dcorres (?r'100 s' a b aa ba x41 x42 x43) (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (Endpoint_D.send_signal x41) (Ipc_A.send_signal x41 x42)
 2. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> \<lbrace>?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))\<rbrace> Endpoint_D.send_signal x41 \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> \<lbrace>ntfn_at x41 and invs and valid_etcbs\<rbrace> Ipc_A.send_signal x41 x42 \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s' a b aa ba x41 x42 x43 xa rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43; ?r'100 s' a b aa ba x41 x42 x43 xa rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return xa) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 5. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> AllowWrite \<notin> x43 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 6. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.NullCap; rv'a = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.NullCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 7. \<And>s' rv rv' rva rv'a x21 x22 x23 x24. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)); rv'a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 8. \<And>s' rv rv' rva rv'a x31 x32 x33. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.EndpointCap x31 x32 x33); rv'a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.EndpointCap x31 x32 x33))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 9. \<And>s' rv rv' rva rv'a x51 x52 x53. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53); rv'a = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (MasterReplyCap x51))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)) \<and> (\<not> x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.ReplyCap x51 x53))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od))
 10. \<And>s' rv rv' rva rv'a x61 x62 x63. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62); rv'a = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
A total of 21 subgoals... proof (prove)
goal (23 subgoals):
 1. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> x41 = x41
 2. \<And>s' a b aa ba x41 x42 x43 s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43; ?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43)) s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' a b aa ba x41 x42 x43 s. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43; (ntfn_at x41 and invs and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and valid_etcbs) s
 4. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> \<lbrace>?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))\<rbrace> Endpoint_D.send_signal x41 \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> \<lbrace>ntfn_at x41 and invs and valid_etcbs\<rbrace> Ipc_A.send_signal x41 x42 \<lbrace>\<lambda>x _. True\<rbrace>
 6. \<And>s' a b aa ba x41 x42 x43 xa rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43; dc xa rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return xa) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 7. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> AllowWrite \<notin> x43 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 8. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.NullCap; rv'a = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.NullCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 9. \<And>s' rv rv' rva rv'a x21 x22 x23 x24. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)); rv'a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 10. \<And>s' rv rv' rva rv'a x31 x32 x33. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.EndpointCap x31 x32 x33); rv'a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.EndpointCap x31 x32 x33))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
A total of 23 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>s' a b aa ba x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>_. True) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> AllowWrite \<notin> x43 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.NullCap; rv'a = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.NullCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 4. \<And>s' rv rv' rva rv'a x21 x22 x23 x24. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)); rv'a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 5. \<And>s' rv rv' rva rv'a x31 x32 x33. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.EndpointCap x31 x32 x33); rv'a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.EndpointCap x31 x32 x33))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 6. \<And>s' rv rv' rva rv'a x51 x52 x53. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53); rv'a = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (MasterReplyCap x51))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)) \<and> (\<not> x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.ReplyCap x51 x53))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od))
 7. \<And>s' rv rv' rva rv'a x61 x62 x63. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62); rv'a = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 8. \<And>s' rv rv' rva rv'a x7. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (TcbCap x7); rv'a = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (TcbCap x7))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 9. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.DomainCap; rv'a = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.DomainCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 10. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some IrqControlCap; rv'a = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some IrqControlCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>s' a b aa ba x41 x42 x43. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba); AllowWrite \<notin> x43\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.NotificationCap x41 x42 x43))) (ntfn_at x41 and invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.NullCap; rv'a = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.NullCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<And>s' rv rv' rva rv'a x21 x22 x23 x24. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)); rv'a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 4. \<And>s' rv rv' rva rv'a x31 x32 x33. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.EndpointCap x31 x32 x33); rv'a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.EndpointCap x31 x32 x33))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 5. \<And>s' rv rv' rva rv'a x51 x52 x53. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53); rv'a = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (MasterReplyCap x51))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)) \<and> (\<not> x52 \<longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.ReplyCap x51 x53))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od))
 6. \<And>s' rv rv' rva rv'a x61 x62 x63. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62); rv'a = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 7. \<And>s' rv rv' rva rv'a x7. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (TcbCap x7); rv'a = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (TcbCap x7))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 8. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some cdl_cap.DomainCap; rv'a = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some cdl_cap.DomainCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 9. \<And>s' rv rv' rva rv'a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some IrqControlCap; rv'a = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some IrqControlCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 10. \<And>s' rv rv' rva rv'a x10. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (IrqHandlerCap x10); rv'a = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (IrqHandlerCap x10))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
A total of 17 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>s' rv rv' rva rv'a x12. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'; rva = Some (transform_cap (ArchObjectCap x12)); rv'a = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr rv') rv' (Some (transform_cap (ArchObjectCap x12)))) (invs and valid_etcbs) (case transform_cap (ArchObjectCap x12) of cdl_cap.NotificationCap obj x rights \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | _ \<Rightarrow> return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q68 s' (transform_cslot_ptr rv')\<rbrace> gets (opt_cap (transform_cslot_ptr rv')) \<lbrace>?R66 s' (transform_cslot_ptr rv') rv'\<rbrace>
 3. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'70 s' rv'\<rbrace> CSpaceAcc_A.get_cap rv' \<lbrace>\<lambda>rv. (\<lambda>s. Structures_A.is_ntfn_cap rv \<longrightarrow> ntfn_at (obj_ref_of rv) s) and invs and valid_etcbs\<rbrace>
 4. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> gets (CSpace_D.get_irq_slot x) \<lbrace>?Q68 s'\<rbrace>
 5. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.get_irq_slot x \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread (fst rv') and valid_etcbs and ?Q'70 s' rv'\<rbrace>
 6. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (10 subgoals):
 1. \<And>s' a b aa ba x11 x12a. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (AsidPoolCap x11 (fst (transform_asid x12a))))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s' a b aa ba. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some AsidControlCap)) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 3. \<And>s' a b aa ba x31 x32 x33 x34 x35. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 4. \<And>s' a b aa ba x41 x42. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.PageTableCap x41 Real (transform_mapping x42)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 5. \<And>s' a b aa ba x51 x52. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> dcorres dc (?R66 s' (transform_cslot_ptr (aa, ba)) (aa, ba) (Some (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52)))) (invs and valid_etcbs) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 6. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q68 s' (transform_cslot_ptr rv')\<rbrace> gets (opt_cap (transform_cslot_ptr rv')) \<lbrace>?R66 s' (transform_cslot_ptr rv') rv'\<rbrace>
 7. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'70 s' rv'\<rbrace> CSpaceAcc_A.get_cap rv' \<lbrace>\<lambda>rv. (\<lambda>s. Structures_A.is_ntfn_cap rv \<longrightarrow> ntfn_at (obj_ref_of rv) s) and invs and valid_etcbs\<rbrace>
 8. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> gets (CSpace_D.get_irq_slot x) \<lbrace>?Q68 s'\<rbrace>
 9. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.get_irq_slot x \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread (fst rv') and valid_etcbs and ?Q'70 s' rv'\<rbrace>
 10. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od))
flex-flex pairs:
\<lambda>s' rv rv' rva rv'a x12. ?R66 s' (transform_cslot_ptr rv') rv' (Some (case x12 of ASIDPoolCap a b \<Rightarrow> AsidPoolCap a (fst $ transform_asid b) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap a b c d e \<Rightarrow> FrameCap a b c (pageBitsForSize d) Real (transform_mapping e) | arch_cap.PageTableCap a b \<Rightarrow> cdl_cap.PageTableCap a Real (transform_mapping b) | arch_cap.PageDirectoryCap a b \<Rightarrow> cdl_cap.PageDirectoryCap a Real (map_option transform_asid b))) \<equiv>\<^sup>? \<lambda>s' rv rv' rva rv'a x12. ?R66 s' (transform_cslot_ptr rv') rv' (Some (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp))) proof (prove)
goal (5 subgoals):
 1. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q68 s' (transform_cslot_ptr rv')\<rbrace> gets (opt_cap (transform_cslot_ptr rv')) \<lbrace>?R66 s' (transform_cslot_ptr rv') rv'\<rbrace>
 2. \<And>s' rv rv'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal; rv = transform_cslot_ptr rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'70 s' rv'\<rbrace> CSpaceAcc_A.get_cap rv' \<lbrace>\<lambda>rv. (\<lambda>s. Structures_A.is_ntfn_cap rv \<longrightarrow> ntfn_at (obj_ref_of rv) s) and invs and valid_etcbs\<rbrace>
 3. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> gets (CSpace_D.get_irq_slot x) \<lbrace>?Q68 s'\<rbrace>
 4. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.get_irq_slot x \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread (fst rv') and valid_etcbs and ?Q'70 s' rv'\<rbrace>
 5. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od))
flex-flex pairs:
\<lambda>s' rv rv' rva rv'a x12. ?R66 s' (transform_cslot_ptr rv') rv' (Some (case x12 of ASIDPoolCap a b \<Rightarrow> AsidPoolCap a (fst $ transform_asid b) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap a b c d e \<Rightarrow> FrameCap a b c (pageBitsForSize d) Real (transform_mapping e) | arch_cap.PageTableCap a b \<Rightarrow> cdl_cap.PageTableCap a Real (transform_mapping b) | arch_cap.PageDirectoryCap a b \<Rightarrow> cdl_cap.PageDirectoryCap a Real (map_option transform_asid b))) \<equiv>\<^sup>? \<lambda>s' rv rv' rva rv'a x12. ?R66 s' (transform_cslot_ptr rv') rv' (Some (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp))) proof (prove)
goal (2 subgoals):
 1. \<And>s' s. \<lbrakk>\<not> maxIRQ < x; invs s; valid_etcbs s; interrupt_states s x = IRQSignal; s' = s\<rbrakk> \<Longrightarrow> valid_idle s \<and> not_idle_thread (interrupt_irq_node s x) s \<and> valid_state s
 2. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s; interrupt_states s x = IRQSignal; valid_state s; cur_tcb s\<rbrakk> \<Longrightarrow> valid_idle s \<and> not_idle_thread (interrupt_irq_node s x) s
 2. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Interrupt_D.handle_interrupt x) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (interrupt_states s' x = IRQTimer \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)) \<and> (interrupt_states s' x = IRQReserved \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQTimer\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s' s'a s'b. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQTimer; transform s' = transform s'a; s' = s'a; transform s'a = transform s'b; s'a = s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (CSpace_D.get_irq_slot x (transform s'a)) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 3. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (8 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> interrupt_states s'b x \<noteq> IRQSignal
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> if_unsafe_then_cap s'b
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> valid_global_refs s'b
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> valid_irq_node s'b
 5. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> valid_irq_handlers s'b
 6. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 7. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 8. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 3. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (5 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> valid_etcbs s'b
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> fst (interrupt_irq_node s'b x, []) \<noteq> idle_thread s'b
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 5. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (4 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> fst (interrupt_irq_node s'b x, []) \<noteq> idle_thread s'b
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 4. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (4 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (idle_thread s'b, []) = Some cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; interrupt_irq_node s'b x = idle_thread s'b\<rbrakk> \<Longrightarrow> False
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 4. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (4 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (idle_thread s'b, []) = Some cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; interrupt_irq_node s'b x = idle_thread s'b; not_idle_thread (interrupt_irq_node s'b x) s'b\<rbrakk> \<Longrightarrow> False
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 4. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 3. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 3. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (4 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 4. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (4 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (return ()) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 4. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (6 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> dcorres dc (?Q329 s'b) (?Q'329 s'b) (do return (?b333 s'b);
return ()
od) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; transform s'b = s\<rbrakk> \<Longrightarrow> ?Q329 s'b s
 3. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; s'b = s\<rbrakk> \<Longrightarrow> ?Q'329 s'b s
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 5. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 6. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (6 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> dcorres dc (?Q329 s'b) (?Q'329 s'b) (return ()) (do xa <- timer_tick;
y <- do_machine_op resetTimer;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; transform s'b = s\<rbrakk> \<Longrightarrow> ?Q329 s'b s
 3. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; s'b = s\<rbrakk> \<Longrightarrow> ?Q'329 s'b s
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 5. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 6. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (8 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> dcorres dc (?Q335 s'b) (?Q'335 s'b) (return ()) (do y <- do_machine_op resetTimer;
do_machine_op (ackInterrupt x)
od)
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> \<lbrace>?Q329 s'b\<rbrace> return () \<lbrace>\<lambda>x. ?Q335 s'b\<rbrace>
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'329 s'b\<rbrace> timer_tick \<lbrace>\<lambda>x. ?Q'335 s'b\<rbrace>
 4. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; transform s'b = s\<rbrakk> \<Longrightarrow> ?Q329 s'b s
 5. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; s'b = s\<rbrakk> \<Longrightarrow> ?Q'329 s'b s
 6. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 7. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 8. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (10 subgoals):
 1. \<And>s'b y m. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> ackInterrupt x \<lbrace>\<lambda>y ms. underlying_memory ms = m\<rbrace>
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'335 s'b\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>s'b cs. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> \<lbrace>?Q329 s'b\<rbrace> return () \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'329 s'b\<rbrace> timer_tick \<lbrace>\<lambda>x. ?Q'335 s'b\<rbrace>
 6. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; transform s'b = s\<rbrakk> \<Longrightarrow> ?Q329 s'b s
 7. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; s'b = s\<rbrakk> \<Longrightarrow> ?Q'329 s'b s
 8. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 9. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 10. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQTimer\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None
 3. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQTimer; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; cte_wp_at (\<lambda>_. True) (interrupt_irq_node s'b (?x690 s'b), []) s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> \<exists>y. caps_of_state s'b (interrupt_irq_node s'b x, []) = Some y
 2. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
sa <- get;
case opt_cap (CSpace_D.get_irq_slot x s) sa of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()
od) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a s'b. \<lbrakk>\<not> maxIRQ < x; invs s'; valid_etcbs s'; interrupt_states s' x = IRQReserved; transform s' = transform s'a; s' = s'a; transform s'a = transform s'b; s'a = s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (CSpace_D.get_irq_slot x (transform s'a)) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do y <- handle_reserved_irq x;
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x)) proof (prove)
goal (2 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (7 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> interrupt_states s'b x \<noteq> IRQSignal
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> if_unsafe_then_cap s'b
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> valid_global_refs s'b
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> valid_irq_node s'b
 5. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> valid_irq_handlers s'b
 6. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 7. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> valid_etcbs s'b
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> fst (interrupt_irq_node s'b x, []) \<noteq> idle_thread s'b
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap\<rbrakk> \<Longrightarrow> fst (interrupt_irq_node s'b x, []) \<noteq> idle_thread s'b
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (idle_thread s'b, []) = Some cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; interrupt_irq_node s'b x = idle_thread s'b\<rbrakk> \<Longrightarrow> False
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (idle_thread s'b, []) = Some cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; interrupt_irq_node s'b x = idle_thread s'b; not_idle_thread (interrupt_irq_node s'b x) s'b\<rbrakk> \<Longrightarrow> False
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_pspace s'b \<and> valid_mdb s'b \<and> valid_ioc s'b \<and> valid_idle s'b \<and> only_idle s'b \<and> if_unsafe_then_cap s'b \<and> valid_reply_caps s'b \<and> valid_reply_masters s'b \<and> valid_global_refs s'b \<and> valid_arch_state s'b \<and> valid_irq_node s'b \<and> valid_irq_handlers s'b \<and> valid_irq_states s'b \<and> valid_machine_state s'b \<and> valid_vspace_objs s'b \<and> valid_arch_caps s'b \<and> valid_global_objs s'b \<and> valid_kernel_mappings s'b \<and> equal_kernel_mappings s'b \<and> valid_asid_map s'b \<and> valid_global_vspace_mappings s'b \<and> pspace_in_kernel_window s'b \<and> cap_refs_in_kernel_window s'b \<and> pspace_respects_device_region s'b \<and> cap_refs_respects_device_region s'b \<and> cur_tcb s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (transform_cslot_ptr (interrupt_irq_node s'b x, [])) (transform s'b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case opt_cap (cdl_irq_node (transform s'b) x, 0) (transform s'b) of None \<Rightarrow> return () | Some (cdl_cap.NotificationCap obj xa rights) \<Rightarrow> if AllowWrite \<in> rights then Endpoint_D.send_signal obj else return () | Some _ \<Rightarrow> return ()) (do_machine_op (ackInterrupt x))
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (return ()) (do_machine_op (ackInterrupt x))
 2. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> dcorres dc (?Q785 s'b) (?Q'785 s'b) (return ()) (do_machine_op (ackInterrupt x))
 2. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; transform s'b = s\<rbrakk> \<Longrightarrow> ?Q785 s'b s
 3. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; s'b = s\<rbrakk> \<Longrightarrow> ?Q'785 s'b s
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 5. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s'b m. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> ackInterrupt x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; transform s'b = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; s'b = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 5. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; transform s'b = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s'b s. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b; cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x; s'b = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; caps_of_state s'b (interrupt_irq_node s'b x, []) = Some cap.NullCap; opt_cap (interrupt_irq_node s'b x, 0) (transform s'b) = Some cdl_cap.NullCap; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; valid_irq_node s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> cdl_irq_node (transform s'b) x = interrupt_irq_node s'b x
 4. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; invs s'b; valid_etcbs s'b; interrupt_states s'b x = IRQReserved\<rbrakk> \<Longrightarrow> caps_of_state s'b (interrupt_irq_node s'b x, []) \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>s'b. \<lbrakk>\<not> maxIRQ < x; valid_etcbs s'b; interrupt_states s'b x = IRQReserved; valid_pspace s'b; valid_mdb s'b; valid_ioc s'b; valid_idle s'b; only_idle s'b; if_unsafe_then_cap s'b; valid_reply_caps s'b; valid_reply_masters s'b; valid_global_refs s'b; valid_arch_state s'b; cte_wp_at (\<lambda>_. True) (interrupt_irq_node s'b (?x806 s'b), []) s'b; valid_irq_handlers s'b; valid_irq_states s'b; valid_machine_state s'b; valid_vspace_objs s'b; valid_arch_caps s'b; valid_global_objs s'b; valid_kernel_mappings s'b; equal_kernel_mappings s'b; valid_asid_map s'b; valid_global_vspace_mappings s'b; pspace_in_kernel_window s'b; cap_refs_in_kernel_window s'b; pspace_respects_device_region s'b; cap_refs_respects_device_region s'b; cur_tcb s'b\<rbrakk> \<Longrightarrow> \<exists>y. caps_of_state s'b (interrupt_irq_node s'b x, []) = Some y proof (prove)
goal:
No subgoals!