theory Interrupt_R

lemma handleInterrupt_corres:
  "corres dc
     (einvs) (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive))
     (handle_interrupt irq) (handleInterrupt irq)"
  (is "corres dc (einvs) ?P' ?f ?g") apply (simp add: handle_interrupt_def handleInterrupt_def ) apply (rule conjI[rotated]; rule impI) apply (rule corres_guard_imp) apply (rule corres_split[OF getIRQState_corres,
                               where R="\<lambda>rv. einvs"
                                 and R'="\<lambda>rv. invs' and (\<lambda>s. rv \<noteq> IRQInactive)"]) defer apply (wp getIRQState_prop getIRQState_inv do_machine_op_bind doMachineOp_bind | simp add: do_machine_op_bind doMachineOp_bind )+ apply (rule corres_guard_imp) apply (rule corres_split) apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: dc_def no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+ apply ((wp | simp)+)[4] apply (rule corres_gen_asm2) apply (case_tac st, simp_all add: irq_state_relation_def split: irqstate.split_asm) apply (simp add: getSlotCap_def bind_assoc) apply (rule corres_guard_imp) apply (rule corres_split[OF getIRQSlot_corres]) apply simp apply (rule corres_split[OF get_cap_corres,
                                 where R="\<lambda>rv. einvs and valid_cap rv"
                                  and R'="\<lambda>rv. invs' and valid_cap' (cteCap rv)"]) apply (rule corres_underlying_split[where r'=dc]) apply (case_tac xb, simp_all add: doMachineOp_return)[1] apply (clarsimp simp add: when_def doMachineOp_return) apply (rule corres_guard_imp, rule sendSignal_corres) apply (clarsimp simp: valid_cap_def valid_cap'_def do_machine_op_bind doMachineOp_bind
                                    arch_mask_irq_signal_def maskIrqSignal_def)+ apply (rule corres_split) apply (rule corres_machine_op, rule corres_eq_trivial
                     ; (simp add:  no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+ apply ((wp | simp)+) apply clarsimp apply fastforce apply (rule corres_guard_imp) apply (rule corres_split) apply (rule corres_split[OF timerTick_corres corres_machine_op]) apply (rule corres_eq_trivial, simp+) apply wp+ apply (rule corres_machine_op) apply (rule corres_eq_trivial, (simp add: no_fail_ackInterrupt)+) apply wp+ apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc einvs (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) (handle_interrupt irq) (handleInterrupt irq) proof (prove)
goal (1 subgoal):
 1. (maxIRQ < irq \<longrightarrow> corres dc einvs (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) (do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od)) (doMachineOp (do y <- maskInterrupt True irq;
ackInterrupt irq
od))) \<and> (\<not> maxIRQ < irq \<longrightarrow> corres dc einvs (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) (do st <- get_irq_state irq;
y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do st <- getIRQState irq;
y <- case st of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od)) proof (prove)
goal (2 subgoals):
 1. \<not> maxIRQ < irq \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) (do st <- get_irq_state irq;
y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do st <- getIRQState irq;
y <- case st of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od)
 2. maxIRQ < irq \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) (do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od)) (doMachineOp (do y <- maskInterrupt True irq;
ackInterrupt irq
od)) proof (prove)
goal (4 subgoals):
 1. \<not> maxIRQ < irq \<Longrightarrow> corres dc ?Q21 ?Q'21 (do st <- get_irq_state irq;
y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do st <- getIRQState irq;
y <- case st of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od)
 2. \<And>s. \<lbrakk>\<not> maxIRQ < irq; einvs s\<rbrakk> \<Longrightarrow> ?Q21 s
 3. \<And>s. \<lbrakk>\<not> maxIRQ < irq; (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) s\<rbrakk> \<Longrightarrow> ?Q'21 s
 4. maxIRQ < irq \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) (do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od)) (doMachineOp (do y <- maskInterrupt True irq;
ackInterrupt irq
od)) proof (prove)
goal (6 subgoals):
 1. \<And>st sta. \<lbrakk>\<not> maxIRQ < irq; irq_state_relation st sta\<rbrakk> \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. sta \<noteq> irqstate.IRQInactive)) (do y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do y <- case sta of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od)
 2. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q25\<rbrace> get_irq_state irq \<lbrace>\<lambda>st. einvs\<rbrace>
 3. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q'25\<rbrace> getIRQState irq \<lbrace>\<lambda>st. invs' and (\<lambda>s. st \<noteq> irqstate.IRQInactive)\<rbrace>
 4. \<And>s. \<lbrakk>\<not> maxIRQ < irq; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q25) s
 5. \<And>s. \<lbrakk>\<not> maxIRQ < irq; (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'25) s
 6. maxIRQ < irq \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) (do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od)) (doMachineOp (do y <- maskInterrupt True irq;
ackInterrupt irq
od)) proof (prove)
goal (6 subgoals):
 1. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q25\<rbrace> get_irq_state irq \<lbrace>\<lambda>st. einvs\<rbrace>
 2. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q'25\<rbrace> getIRQState irq \<lbrace>\<lambda>st. invs' and (\<lambda>s. st \<noteq> irqstate.IRQInactive)\<rbrace>
 3. \<And>s. \<lbrakk>\<not> maxIRQ < irq; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q25) s
 4. \<And>s. \<lbrakk>\<not> maxIRQ < irq; (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'25) s
 5. maxIRQ < irq \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) (do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od)) (doMachineOp (do y <- maskInterrupt True irq;
ackInterrupt irq
od))
 6. \<And>st sta. \<lbrakk>\<not> maxIRQ < irq; irq_state_relation st sta\<rbrakk> \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. sta \<noteq> irqstate.IRQInactive)) (do y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do y <- case sta of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (2 subgoals):
 1. maxIRQ < irq \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) (do rv <- do_machine_op (maskInterrupt True irq);
do_machine_op (ackInterrupt irq)
od) (do rv <- doMachineOp (maskInterrupt True irq);
doMachineOp (ackInterrupt irq)
od)
 2. \<And>st sta. \<lbrakk>\<not> maxIRQ < irq; irq_state_relation st sta\<rbrakk> \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. sta \<noteq> irqstate.IRQInactive)) (do y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do y <- case sta of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (4 subgoals):
 1. maxIRQ < irq \<Longrightarrow> corres dc ?Q39 ?Q'39 (do rv <- do_machine_op (maskInterrupt True irq);
do_machine_op (ackInterrupt irq)
od) (do rv <- doMachineOp (maskInterrupt True irq);
doMachineOp (ackInterrupt irq)
od)
 2. \<And>s. \<lbrakk>maxIRQ < irq; einvs s\<rbrakk> \<Longrightarrow> ?Q39 s
 3. \<And>s. \<lbrakk>maxIRQ < irq; (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) s\<rbrakk> \<Longrightarrow> ?Q'39 s
 4. \<And>st sta. \<lbrakk>\<not> maxIRQ < irq; irq_state_relation st sta\<rbrakk> \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. sta \<noteq> irqstate.IRQInactive)) (do y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do y <- case sta of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (7 subgoals):
 1. maxIRQ < irq \<Longrightarrow> corres ?r'43 ?P43 ?P'43 (do_machine_op (maskInterrupt True irq)) (doMachineOp (maskInterrupt True irq))
 2. \<And>rv rva. \<lbrakk>maxIRQ < irq; ?r'43 rv rva\<rbrakk> \<Longrightarrow> corres dc (?R43 rv) (?R'43 rva) (do_machine_op (ackInterrupt irq)) (doMachineOp (ackInterrupt irq))
 3. maxIRQ < irq \<Longrightarrow> \<lbrace>?Q43\<rbrace> do_machine_op (maskInterrupt True irq) \<lbrace>?R43\<rbrace>
 4. maxIRQ < irq \<Longrightarrow> \<lbrace>?Q'43\<rbrace> doMachineOp (maskInterrupt True irq) \<lbrace>?R'43\<rbrace>
 5. \<And>s. \<lbrakk>maxIRQ < irq; einvs s\<rbrakk> \<Longrightarrow> (?P43 and ?Q43) s
 6. \<And>s. \<lbrakk>maxIRQ < irq; (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) s\<rbrakk> \<Longrightarrow> (?P'43 and ?Q'43) s
 7. \<And>st sta. \<lbrakk>\<not> maxIRQ < irq; irq_state_relation st sta\<rbrakk> \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. sta \<noteq> irqstate.IRQInactive)) (do y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do y <- case sta of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (5 subgoals):
 1. maxIRQ < irq \<Longrightarrow> \<lbrace>?Q43\<rbrace> do_machine_op (maskInterrupt True irq) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. maxIRQ < irq \<Longrightarrow> \<lbrace>?Q'43\<rbrace> doMachineOp (maskInterrupt True irq) \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>s. \<lbrakk>maxIRQ < irq; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43) s
 4. \<And>s. \<lbrakk>maxIRQ < irq; (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'43) s
 5. \<And>st sta. \<lbrakk>\<not> maxIRQ < irq; irq_state_relation st sta\<rbrakk> \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. sta \<noteq> irqstate.IRQInactive)) (do y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do y <- case sta of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (1 subgoal):
 1. \<And>st sta. \<lbrakk>\<not> maxIRQ < irq; irq_state_relation st sta\<rbrakk> \<Longrightarrow> corres dc einvs (invs' and (\<lambda>s. sta \<noteq> irqstate.IRQInactive)) (do y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do y <- case sta of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (1 subgoal):
 1. \<And>st sta. \<lbrakk>\<not> maxIRQ < irq; irq_state_relation st sta; sta \<noteq> irqstate.IRQInactive\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- case st of irq_state.IRQInactive \<Rightarrow> fail | irq_state.IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | irq_state.IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | irq_state.IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od) (do y <- case sta of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (2 subgoals):
 1. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do slot <- get_irq_slot irq;
cap <- get_cap slot;
y <- when (is_ntfn_cap cap \<and> AllowWrite \<in> cap_rights cap) (send_signal (obj_ref_of cap) (cap_ep_badge cap));
arch_mask_irq_signal irq
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
y <- case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od;
doMachineOp (ackInterrupt irq)
od)
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (2 subgoals):
 1. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do x <- get_irq_slot irq;
x <- get_cap x;
x <- when (is_ntfn_cap x \<and> AllowWrite \<in> cap_rights x) (send_signal (obj_ref_of x) (cap_ep_badge x));
y <- arch_mask_irq_signal irq;
do_machine_op (ackInterrupt irq)
od) (do x <- getIRQSlot irq;
x <- getCTE x;
x <- case cteCap x of capability.NotificationCap xa xaa True xb \<Rightarrow> sendSignal (capNtfnPtr (cteCap x)) (capNtfnBadge (cteCap x)) | capability.NotificationCap xa xaa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
y <- maskIrqSignal irq;
doMachineOp (ackInterrupt irq)
od)
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (4 subgoals):
 1. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> corres dc (?Q81 st sta) (?Q'81 st sta) (do x <- get_irq_slot irq;
x <- get_cap x;
x <- when (is_ntfn_cap x \<and> AllowWrite \<in> cap_rights x) (send_signal (obj_ref_of x) (cap_ep_badge x));
y <- arch_mask_irq_signal irq;
do_machine_op (ackInterrupt irq)
od) (do x <- getIRQSlot irq;
x <- getCTE x;
x <- case cteCap x of capability.NotificationCap xa xaa True xb \<Rightarrow> sendSignal (capNtfnPtr (cteCap x)) (capNtfnBadge (cteCap x)) | capability.NotificationCap xa xaa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
y <- maskIrqSignal irq;
doMachineOp (ackInterrupt irq)
od)
 2. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; einvs s\<rbrakk> \<Longrightarrow> ?Q81 st sta s
 3. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> ?Q'81 st sta s
 4. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (6 subgoals):
 1. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> corres dc (?R85 st sta x) (?R'85 st sta xa) (do x <- get_cap x;
x <- when (is_ntfn_cap x \<and> AllowWrite \<in> cap_rights x) (send_signal (obj_ref_of x) (cap_ep_badge x));
y <- arch_mask_irq_signal irq;
do_machine_op (ackInterrupt irq)
od) (do x <- getCTE xa;
x <- case cteCap x of capability.NotificationCap xa xaa True xb \<Rightarrow> sendSignal (capNtfnPtr (cteCap x)) (capNtfnBadge (cteCap x)) | capability.NotificationCap xa xaa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
y <- maskIrqSignal irq;
doMachineOp (ackInterrupt irq)
od)
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>?R85 st sta\<rbrace>
 3. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>?R'85 st sta\<rbrace>
 4. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q85 st sta) s
 5. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'85 st sta) s
 6. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (6 subgoals):
 1. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> corres dc (?R85 irq_state.IRQSignal irqstate.IRQSignal x) (?R'85 irq_state.IRQSignal irqstate.IRQSignal (cte_map x)) (do x <- get_cap x;
x <- when (is_ntfn_cap x \<and> AllowWrite \<in> cap_rights x) (send_signal (obj_ref_of x) (cap_ep_badge x));
y <- arch_mask_irq_signal irq;
do_machine_op (ackInterrupt irq)
od) (do x <- getCTE (cte_map x);
x <- case cteCap x of capability.NotificationCap xa xaa True xb \<Rightarrow> sendSignal (capNtfnPtr (cteCap x)) (capNtfnBadge (cteCap x)) | capability.NotificationCap xa xaa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
y <- maskIrqSignal irq;
doMachineOp (ackInterrupt irq)
od)
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>?R85 st sta\<rbrace>
 3. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>?R'85 st sta\<rbrace>
 4. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q85 st sta) s
 5. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'85 st sta) s
 6. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (8 subgoals):
 1. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> corres dc (einvs and valid_cap xb) (invs' and valid_cap' (cteCap xc)) (do x <- when (is_ntfn_cap xb \<and> AllowWrite \<in> cap_rights xb) (send_signal (obj_ref_of xb) (cap_ep_badge xb));
y <- arch_mask_irq_signal irq;
do_machine_op (ackInterrupt irq)
od) (do x <- case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
y <- maskIrqSignal irq;
doMachineOp (ackInterrupt irq)
od)
 2. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q108 irq_state.IRQSignal irqstate.IRQSignal x\<rbrace> get_cap x \<lbrace>\<lambda>x. einvs and valid_cap x\<rbrace>
 3. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'106 irq_state.IRQSignal irqstate.IRQSignal (cte_map x)\<rbrace> getCTE (cte_map x) \<lbrace>\<lambda>x. invs' and valid_cap' (cteCap x)\<rbrace>
 4. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) a and ?Q108 st sta a\<rbrace>
 5. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'106 st sta a\<rbrace>
 6. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q85 st sta) s
 7. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'85 st sta) s
 8. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (11 subgoals):
 1. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> corres dc (einvs and valid_cap xb) (invs' and valid_cap' (cteCap xc)) (when (is_ntfn_cap xb \<and> AllowWrite \<in> cap_rights xb) (send_signal (obj_ref_of xb) (cap_ep_badge xb))) (case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq)
 2. \<And>st sta x xa xb xc rv rv'. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc); dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?Q113 st sta x xa xb xc rv) (?Q'113 st sta x xa xb xc rv') (do y <- arch_mask_irq_signal irq;
do_machine_op (ackInterrupt irq)
od) (do y <- maskIrqSignal irq;
doMachineOp (ackInterrupt irq)
od)
 3. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>einvs and valid_cap xb\<rbrace> when (is_ntfn_cap xb \<and> AllowWrite \<in> cap_rights xb) (send_signal (obj_ref_of xb) (cap_ep_badge xb)) \<lbrace>?Q113 st sta x xa xb xc\<rbrace>
 4. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_cap' (cteCap xc)\<rbrace> case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq \<lbrace>?Q'113 st sta x xa xb xc\<rbrace>
 5. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q108 irq_state.IRQSignal irqstate.IRQSignal x\<rbrace> get_cap x \<lbrace>\<lambda>x. einvs and valid_cap x\<rbrace>
 6. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'106 irq_state.IRQSignal irqstate.IRQSignal (cte_map x)\<rbrace> getCTE (cte_map x) \<lbrace>\<lambda>x. invs' and valid_cap' (cteCap x)\<rbrace>
 7. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) a and ?Q108 st sta a\<rbrace>
 8. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'106 st sta a\<rbrace>
 9. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q85 st sta) s
 10. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'85 st sta) s
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>st sta x xa xb xc x41 x42 x43. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cteCap xc = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); xb = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (einvs and valid_cap (cap.NotificationCap x41 x42 x43)) (invs' and valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43))) (when (AllowWrite \<in> x43) (send_signal x41 x42)) (case AllowWrite \<in> x43 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq)
 2. \<And>st sta x xa xb xc x12. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; \<exists>a'. acap_relation x12 a' \<and> cteCap xc = capability.ArchObjectCap a'; xb = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres dc (einvs and valid_cap (cap.ArchObjectCap x12)) (invs' and valid_cap' (cteCap xc)) (return ()) (case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq)
 3. \<And>st sta x xa xb xc rv rv'. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc); dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?Q113 st sta x xa xb xc rv) (?Q'113 st sta x xa xb xc rv') (do y <- arch_mask_irq_signal irq;
do_machine_op (ackInterrupt irq)
od) (do y <- maskIrqSignal irq;
doMachineOp (ackInterrupt irq)
od)
 4. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>einvs and valid_cap xb\<rbrace> when (is_ntfn_cap xb \<and> AllowWrite \<in> cap_rights xb) (send_signal (obj_ref_of xb) (cap_ep_badge xb)) \<lbrace>?Q113 st sta x xa xb xc\<rbrace>
 5. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_cap' (cteCap xc)\<rbrace> case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq \<lbrace>?Q'113 st sta x xa xb xc\<rbrace>
 6. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q108 irq_state.IRQSignal irqstate.IRQSignal x\<rbrace> get_cap x \<lbrace>\<lambda>x. einvs and valid_cap x\<rbrace>
 7. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'106 irq_state.IRQSignal irqstate.IRQSignal (cte_map x)\<rbrace> getCTE (cte_map x) \<lbrace>\<lambda>x. invs' and valid_cap' (cteCap x)\<rbrace>
 8. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) a and ?Q108 st sta a\<rbrace>
 9. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'106 st sta a\<rbrace>
 10. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q85 st sta) s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>xc x41 x42 x43. \<lbrakk>\<not> maxIRQ < irq; cteCap xc = capability.NotificationCap x41 x42 True (AllowRead \<in> x43); AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> corres dc (einvs and valid_cap (cap.NotificationCap x41 x42 x43)) (invs' and valid_cap' (capability.NotificationCap x41 x42 True (AllowRead \<in> x43))) (send_signal x41 x42) (sendSignal x41 x42)
 2. \<And>st sta x xa xb xc x12. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; \<exists>a'. acap_relation x12 a' \<and> cteCap xc = capability.ArchObjectCap a'; xb = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres dc (einvs and valid_cap (cap.ArchObjectCap x12)) (invs' and valid_cap' (cteCap xc)) (return ()) (case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq)
 3. \<And>st sta x xa xb xc rv rv'. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc); dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?Q113 st sta x xa xb xc rv) (?Q'113 st sta x xa xb xc rv') (do y <- arch_mask_irq_signal irq;
do_machine_op (ackInterrupt irq)
od) (do y <- maskIrqSignal irq;
doMachineOp (ackInterrupt irq)
od)
 4. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>einvs and valid_cap xb\<rbrace> when (is_ntfn_cap xb \<and> AllowWrite \<in> cap_rights xb) (send_signal (obj_ref_of xb) (cap_ep_badge xb)) \<lbrace>?Q113 st sta x xa xb xc\<rbrace>
 5. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_cap' (cteCap xc)\<rbrace> case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq \<lbrace>?Q'113 st sta x xa xb xc\<rbrace>
 6. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q108 irq_state.IRQSignal irqstate.IRQSignal x\<rbrace> get_cap x \<lbrace>\<lambda>x. einvs and valid_cap x\<rbrace>
 7. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'106 irq_state.IRQSignal irqstate.IRQSignal (cte_map x)\<rbrace> getCTE (cte_map x) \<lbrace>\<lambda>x. invs' and valid_cap' (cteCap x)\<rbrace>
 8. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) a and ?Q108 st sta a\<rbrace>
 9. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'106 st sta a\<rbrace>
 10. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q85 st sta) s
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>xc x41 x42 x43 s. \<lbrakk>\<not> maxIRQ < irq; cteCap xc = capability.NotificationCap x41 x42 True (AllowRead \<in> x43); AllowWrite \<in> x43; (einvs and valid_cap (cap.NotificationCap x41 x42 x43)) s\<rbrakk> \<Longrightarrow> (einvs and ntfn_at x41) s
 2. \<And>xc x41 x42 x43 s. \<lbrakk>\<not> maxIRQ < irq; cteCap xc = capability.NotificationCap x41 x42 True (AllowRead \<in> x43); AllowWrite \<in> x43; (invs' and valid_cap' (capability.NotificationCap x41 x42 True (AllowRead \<in> x43))) s\<rbrakk> \<Longrightarrow> (invs' and ntfn_at' x41) s
 3. \<And>st sta x xa xb xc x12. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; \<exists>a'. acap_relation x12 a' \<and> cteCap xc = capability.ArchObjectCap a'; xb = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres dc (einvs and valid_cap (cap.ArchObjectCap x12)) (invs' and valid_cap' (cteCap xc)) (return ()) (case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq)
 4. \<And>st sta x xa xb xc rv rv'. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc); dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?Q113 st sta x xa xb xc rv) (?Q'113 st sta x xa xb xc rv') (do y <- arch_mask_irq_signal irq;
do_machine_op (ackInterrupt irq)
od) (do y <- maskIrqSignal irq;
doMachineOp (ackInterrupt irq)
od)
 5. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>einvs and valid_cap xb\<rbrace> when (is_ntfn_cap xb \<and> AllowWrite \<in> cap_rights xb) (send_signal (obj_ref_of xb) (cap_ep_badge xb)) \<lbrace>?Q113 st sta x xa xb xc\<rbrace>
 6. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_cap' (cteCap xc)\<rbrace> case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq \<lbrace>?Q'113 st sta x xa xb xc\<rbrace>
 7. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q108 irq_state.IRQSignal irqstate.IRQSignal x\<rbrace> get_cap x \<lbrace>\<lambda>x. einvs and valid_cap x\<rbrace>
 8. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'106 irq_state.IRQSignal irqstate.IRQSignal (cte_map x)\<rbrace> getCTE (cte_map x) \<lbrace>\<lambda>x. invs' and valid_cap' (cteCap x)\<rbrace>
 9. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) a and ?Q108 st sta a\<rbrace>
 10. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'106 st sta a\<rbrace>
A total of 13 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>a b xb xc. \<lbrakk>\<not> maxIRQ < irq; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?Q113 irq_state.IRQSignal irqstate.IRQSignal (a, b) (cte_map (a, b)) xb xc ()) (?Q'113 irq_state.IRQSignal irqstate.IRQSignal (a, b) (cte_map (a, b)) xb xc ()) (do y <- do_machine_op (maskInterrupt True irq);
do_machine_op (ackInterrupt irq)
od) (do y <- doMachineOp (maskInterrupt True irq);
doMachineOp (ackInterrupt irq)
od)
 2. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>einvs and valid_cap xb\<rbrace> when (is_ntfn_cap xb \<and> AllowWrite \<in> cap_rights xb) (send_signal (obj_ref_of xb) (cap_ep_badge xb)) \<lbrace>?Q113 st sta x xa xb xc\<rbrace>
 3. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_cap' (cteCap xc)\<rbrace> case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq \<lbrace>?Q'113 st sta x xa xb xc\<rbrace>
 4. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q108 irq_state.IRQSignal irqstate.IRQSignal x\<rbrace> get_cap x \<lbrace>\<lambda>x. einvs and valid_cap x\<rbrace>
 5. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'106 irq_state.IRQSignal irqstate.IRQSignal (cte_map x)\<rbrace> getCTE (cte_map x) \<lbrace>\<lambda>x. invs' and valid_cap' (cteCap x)\<rbrace>
 6. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) a and ?Q108 st sta a\<rbrace>
 7. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'106 st sta a\<rbrace>
 8. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q85 st sta) s
 9. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'85 st sta) s
 10. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (13 subgoals):
 1. \<And>a b xb xc. \<lbrakk>\<not> maxIRQ < irq; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> corres (?r'150 a b xb xc) (?P158 irq_state.IRQSignal irqstate.IRQSignal (a, b) (cte_map (a, b)) xb xc ()) (?P'156 irq_state.IRQSignal irqstate.IRQSignal (a, b) (cte_map (a, b)) xb xc ()) (do_machine_op (maskInterrupt True irq)) (doMachineOp (maskInterrupt True irq))
 2. \<And>a b xb xc y ya. \<lbrakk>\<not> maxIRQ < irq; cap_relation xb (cteCap xc); ?r'150 a b xb xc y ya\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?R150 a b xb xc y) (?R'150 a b xb xc ya) (do_machine_op (ackInterrupt irq)) (doMachineOp (ackInterrupt irq))
 3. \<And>a b xb xc. \<lbrakk>\<not> maxIRQ < irq; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>?Q157 irq_state.IRQSignal irqstate.IRQSignal (a, b) (cte_map (a, b)) xb xc ()\<rbrace> do_machine_op (maskInterrupt True irq) \<lbrace>?R150 a b xb xc\<rbrace>
 4. \<And>a b xb xc. \<lbrakk>\<not> maxIRQ < irq; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'155 irq_state.IRQSignal irqstate.IRQSignal (a, b) (cte_map (a, b)) xb xc ()\<rbrace> doMachineOp (maskInterrupt True irq) \<lbrace>?R'150 a b xb xc\<rbrace>
 5. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>einvs and valid_cap xb\<rbrace> when (is_ntfn_cap xb \<and> AllowWrite \<in> cap_rights xb) (send_signal (obj_ref_of xb) (cap_ep_badge xb)) \<lbrace>\<lambda>a. ?P158 st sta x xa xb xc a and ?Q157 st sta x xa xb xc a\<rbrace>
 6. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_cap' (cteCap xc)\<rbrace> case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq \<lbrace>\<lambda>a. ?P'156 st sta x xa xb xc a and ?Q'155 st sta x xa xb xc a\<rbrace>
 7. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q108 irq_state.IRQSignal irqstate.IRQSignal x\<rbrace> get_cap x \<lbrace>\<lambda>x. einvs and valid_cap x\<rbrace>
 8. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'106 irq_state.IRQSignal irqstate.IRQSignal (cte_map x)\<rbrace> getCTE (cte_map x) \<lbrace>\<lambda>x. invs' and valid_cap' (cteCap x)\<rbrace>
 9. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) a and ?Q108 st sta a\<rbrace>
 10. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'106 st sta a\<rbrace>
A total of 13 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a b xb xc. \<lbrakk>\<not> maxIRQ < irq; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>?Q157 irq_state.IRQSignal irqstate.IRQSignal (a, b) (cte_map (a, b)) xb xc ()\<rbrace> do_machine_op (maskInterrupt True irq) \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>a b xb xc. \<lbrakk>\<not> maxIRQ < irq; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'155 irq_state.IRQSignal irqstate.IRQSignal (a, b) (cte_map (a, b)) xb xc ()\<rbrace> doMachineOp (maskInterrupt True irq) \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>einvs and valid_cap xb\<rbrace> when (is_ntfn_cap xb \<and> AllowWrite \<in> cap_rights xb) (send_signal (obj_ref_of xb) (cap_ep_badge xb)) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q157 st sta x xa xb xc a\<rbrace>
 4. \<And>st sta x xa xb xc. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x; cap_relation xb (cteCap xc)\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_cap' (cteCap xc)\<rbrace> case cteCap xc of capability.NotificationCap x xa bool1 xb \<Rightarrow> case bool1 of True \<Rightarrow> sendSignal (capNtfnPtr (cteCap xc)) (capNtfnBadge (cteCap xc)) | False \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q'155 st sta x xa xb xc a\<rbrace>
 5. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q108 irq_state.IRQSignal irqstate.IRQSignal x\<rbrace> get_cap x \<lbrace>\<lambda>x. einvs and valid_cap x\<rbrace>
 6. \<And>st sta x xa. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; xa = cte_map x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'106 irq_state.IRQSignal irqstate.IRQSignal (cte_map x)\<rbrace> getCTE (cte_map x) \<lbrace>\<lambda>x. invs' and valid_cap' (cteCap x)\<rbrace>
 7. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 st sta\<rbrace> get_irq_slot irq \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) a and ?Q108 st sta a\<rbrace>
 8. \<And>st sta. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 st sta\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'106 st sta a\<rbrace>
 9. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; einvs s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q85 st sta) s
 10. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'85 st sta) s
A total of 11 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs s \<and> valid_list s \<and> valid_sched s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (pspace_aligned' and pspace_distinct' and (\<lambda>a. invs' a \<and> valid_objs' a))) s
 3. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (2 subgoals):
 1. \<And>st sta s. \<lbrakk>st = irq_state.IRQSignal; \<not> maxIRQ < irq; sta = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (pspace_aligned' and pspace_distinct' and (\<lambda>a. invs' a \<and> valid_objs' a))) s
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (1 subgoal):
 1. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc einvs invs' (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od) proof (prove)
goal (3 subgoals):
 1. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres dc (?Q259 st sta) (?Q'259 st sta) (do y <- do y <- timer_tick;
do_machine_op resetTimer
od;
do_machine_op (ackInterrupt irq)
od) (do y <- do y <- timerTick;
doMachineOp resetTimer
od;
doMachineOp (ackInterrupt irq)
od)
 2. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; einvs s\<rbrakk> \<Longrightarrow> ?Q259 st sta s
 3. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; invs' s\<rbrakk> \<Longrightarrow> ?Q'259 st sta s proof (prove)
goal (6 subgoals):
 1. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> corres (?r'263 st sta) (?P263 st sta) (?P'263 st sta) (do y <- timer_tick;
do_machine_op resetTimer
od) (do y <- timerTick;
doMachineOp resetTimer
od)
 2. \<And>st sta y ya. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; ?r'263 st sta y ya\<rbrakk> \<Longrightarrow> corres dc (?R263 st sta y) (?R'263 st sta ya) (do_machine_op (ackInterrupt irq)) (doMachineOp (ackInterrupt irq))
 3. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q263 st sta\<rbrace> do y <- timer_tick;
do_machine_op resetTimer
od \<lbrace>?R263 st sta\<rbrace>
 4. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q'263 st sta\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>?R'263 st sta\<rbrace>
 5. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; einvs s\<rbrakk> \<Longrightarrow> (?P263 st sta and ?Q263 st sta) s
 6. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; invs' s\<rbrakk> \<Longrightarrow> (?P'263 st sta and ?Q'263 st sta) s proof (prove)
goal (8 subgoals):
 1. \<And>st sta y ya. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying Id False True (?r'263 st sta) (\<lambda>_. True) (\<lambda>_. True) resetTimer resetTimer
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q268 st sta\<rbrace> timer_tick \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q'268 st sta\<rbrace> timerTick \<lbrace>\<lambda>y _. True\<rbrace>
 4. \<And>st sta y ya. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; ?r'263 st sta y ya\<rbrakk> \<Longrightarrow> corres dc (?R263 st sta y) (?R'263 st sta ya) (do_machine_op (ackInterrupt irq)) (doMachineOp (ackInterrupt irq))
 5. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q263 st sta\<rbrace> do y <- timer_tick;
do_machine_op resetTimer
od \<lbrace>?R263 st sta\<rbrace>
 6. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q'263 st sta\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>?R'263 st sta\<rbrace>
 7. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; einvs s\<rbrakk> \<Longrightarrow> (cur_tcb and valid_sched and ?Q268 st sta and ?Q263 st sta) s
 8. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; invs' s\<rbrakk> \<Longrightarrow> (invs' and ?Q'268 st sta and ?Q'263 st sta) s proof (prove)
goal (8 subgoals):
 1. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) resetTimer
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q268 st sta\<rbrace> timer_tick \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q'268 st sta\<rbrace> timerTick \<lbrace>\<lambda>y _. True\<rbrace>
 4. \<And>st sta y ya. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; True\<rbrakk> \<Longrightarrow> corres dc (?R263 st sta y) (?R'263 st sta ya) (do_machine_op (ackInterrupt irq)) (doMachineOp (ackInterrupt irq))
 5. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q263 st sta\<rbrace> do y <- timer_tick;
do_machine_op resetTimer
od \<lbrace>?R263 st sta\<rbrace>
 6. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q'263 st sta\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>?R'263 st sta\<rbrace>
 7. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; einvs s\<rbrakk> \<Longrightarrow> (cur_tcb and valid_sched and ?Q268 st sta and ?Q263 st sta) s
 8. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; invs' s\<rbrakk> \<Longrightarrow> (invs' and ?Q'268 st sta and ?Q'263 st sta) s proof (prove)
goal (5 subgoals):
 1. \<And>st sta y ya. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; True\<rbrakk> \<Longrightarrow> corres dc (?R263 st sta y) (?R'263 st sta ya) (do_machine_op (ackInterrupt irq)) (doMachineOp (ackInterrupt irq))
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q263 st sta\<rbrace> do y <- timer_tick;
do_machine_op resetTimer
od \<lbrace>?R263 st sta\<rbrace>
 3. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q'263 st sta\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>?R'263 st sta\<rbrace>
 4. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; einvs s\<rbrakk> \<Longrightarrow> (cur_tcb and valid_sched and (\<lambda>s. True) and ?Q263 st sta) s
 5. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; invs' s\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>_. True) and ?Q'263 st sta) s proof (prove)
goal (5 subgoals):
 1. \<And>st sta y ya. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; True\<rbrakk> \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (ackInterrupt irq) (ackInterrupt irq)
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q263 st sta\<rbrace> do y <- timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q'263 st sta\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>\<lambda>ya _. True\<rbrace>
 4. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; einvs s\<rbrakk> \<Longrightarrow> (cur_tcb and valid_sched and (\<lambda>s. True) and ?Q263 st sta) s
 5. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; invs' s\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>_. True) and ?Q'263 st sta) s proof (prove)
goal (4 subgoals):
 1. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q263 irq_state.IRQTimer irqstate.IRQTimer\<rbrace> do y <- timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>st sta. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?Q'263 st sta\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; einvs s\<rbrakk> \<Longrightarrow> (cur_tcb and valid_sched and (\<lambda>s. True) and ?Q263 st sta) s
 4. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; invs' s\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>_. True) and ?Q'263 st sta) s proof (prove)
goal (2 subgoals):
 1. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; einvs s\<rbrakk> \<Longrightarrow> (cur_tcb and valid_sched and (\<lambda>s. True) and (\<lambda>a. True)) s
 2. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; invs' s\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>st sta s. \<lbrakk>st = irq_state.IRQTimer; \<not> maxIRQ < irq; sta = irqstate.IRQTimer; invs' s\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!