theory ArchInterrupt_AI

lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]:
  "\<lbrace>invs\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: handle_interrupt_def) apply (rule conjI; rule impI) apply (simp add: do_machine_op_bind empty_fail_ackInterrupt_ARCH empty_fail_maskInterrupt_ARCH) apply (wp dmo_maskInterrupt_invs maskInterrupt_invs_ARCH dmo_ackInterrupt send_signal_interrupt_states
            | wpc | simp add: arch_mask_irq_signal_def)+ apply (wp get_cap_wp send_signal_interrupt_states) apply (rule_tac Q="\<lambda>rv. invs and (\<lambda>s. st = interrupt_states s irq)" in hoare_post_imp) apply (clarsimp simp: ex_nonz_cap_to_def invs_valid_objs) apply (intro allI exI, erule cte_wp_at_weakenE) apply (clarsimp simp: is_cap_simps) apply (wp hoare_drop_imps resetTimer_invs_ARCH
           | simp add: get_irq_state_def handle_reserved_irq_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. (maxIRQ < irq \<longrightarrow> \<lbrace>invs\<rbrace> do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>_. invs\<rbrace>) \<and> (\<not> maxIRQ < irq \<longrightarrow> \<lbrace>invs\<rbrace> do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | 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 | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od \<lbrace>\<lambda>_. invs\<rbrace>) proof (prove)
goal (2 subgoals):
 1. maxIRQ < irq \<Longrightarrow> \<lbrace>invs\<rbrace> do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>invs\<rbrace> do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | 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 | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. maxIRQ < irq \<Longrightarrow> \<lbrace>invs\<rbrace> do rv <- do_machine_op (maskInterrupt True irq);
do_machine_op (ackInterrupt irq)
od \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>invs\<rbrace> do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | 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 | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>st slot. \<lbrakk>\<not> maxIRQ < irq; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?B45 IRQSignal slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap then \<lambda>s. invs s \<and> ex_nonz_cap_to (obj_ref_of cap) s \<and> valid_objs s else invs\<rbrace>
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R35 st\<rbrace> get_irq_slot irq \<lbrace>?B45 st\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R34 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y. invs\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R33 st\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>y. invs\<rbrace>
 5. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q23\<rbrace> get_irq_state irq \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R35 st s) \<and> (st = IRQTimer \<longrightarrow> ?R34 st s) \<and> (st = IRQReserved \<longrightarrow> ?R33 st s)\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs s\<rbrakk> \<Longrightarrow> ?Q23 s proof (prove)
goal (5 subgoals):
 1. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R35 st\<rbrace> get_irq_slot irq \<lbrace>\<lambda>a b. \<forall>cap. cte_wp_at ((=) cap) a b \<longrightarrow> (if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap then \<lambda>s. invs s \<and> ex_nonz_cap_to (obj_ref_of cap) s \<and> valid_objs s else invs) b\<rbrace>
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R34 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y. invs\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R33 st\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>y. invs\<rbrace>
 4. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q23\<rbrace> get_irq_state irq \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R35 st s) \<and> (st = IRQTimer \<longrightarrow> ?R34 st s) \<and> (st = IRQReserved \<longrightarrow> ?R33 st s)\<rbrace>
 5. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs s\<rbrakk> \<Longrightarrow> ?Q23 s proof (prove)
goal (6 subgoals):
 1. \<And>st rv s. \<lbrakk>\<not> maxIRQ < irq; st = IRQSignal; (invs and (\<lambda>s. st = interrupt_states s irq)) s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) rv s \<longrightarrow> (if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap then \<lambda>s. invs s \<and> ex_nonz_cap_to (obj_ref_of cap) s \<and> valid_objs s else invs) s
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R35 st\<rbrace> get_irq_slot irq \<lbrace>\<lambda>rv. invs and (\<lambda>s. st = interrupt_states s irq)\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R34 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y. invs\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R33 st\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>y. invs\<rbrace>
 5. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q23\<rbrace> get_irq_state irq \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R35 st s) \<and> (st = IRQTimer \<longrightarrow> ?R34 st s) \<and> (st = IRQReserved \<longrightarrow> ?R33 st s)\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs s\<rbrakk> \<Longrightarrow> ?Q23 s proof (prove)
goal (6 subgoals):
 1. \<And>a b s cap. \<lbrakk>\<not> maxIRQ < irq; invs s; IRQSignal = interrupt_states s irq; is_ntfn_cap cap; AllowSend \<in> cap_rights cap; cte_wp_at ((=) cap) (a, b) s\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> zobj_refs c) (a, b) s
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R35 st\<rbrace> get_irq_slot irq \<lbrace>\<lambda>rv. invs and (\<lambda>s. st = interrupt_states s irq)\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R34 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y. invs\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R33 st\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>y. invs\<rbrace>
 5. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q23\<rbrace> get_irq_state irq \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R35 st s) \<and> (st = IRQTimer \<longrightarrow> ?R34 st s) \<and> (st = IRQReserved \<longrightarrow> ?R33 st s)\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs s\<rbrakk> \<Longrightarrow> ?Q23 s proof (prove)
goal (6 subgoals):
 1. \<And>a b s cap c. \<lbrakk>\<not> maxIRQ < irq; invs s; IRQSignal = interrupt_states s irq; is_ntfn_cap cap; AllowSend \<in> cap_rights cap; cap = c\<rbrakk> \<Longrightarrow> obj_ref_of cap \<in> zobj_refs c
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R35 st\<rbrace> get_irq_slot irq \<lbrace>\<lambda>rv. invs and (\<lambda>s. st = interrupt_states s irq)\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R34 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y. invs\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R33 st\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>y. invs\<rbrace>
 5. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q23\<rbrace> get_irq_state irq \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R35 st s) \<and> (st = IRQTimer \<longrightarrow> ?R34 st s) \<and> (st = IRQReserved \<longrightarrow> ?R33 st s)\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs s\<rbrakk> \<Longrightarrow> ?Q23 s proof (prove)
goal (5 subgoals):
 1. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R35 st\<rbrace> get_irq_slot irq \<lbrace>\<lambda>rv. invs and (\<lambda>s. st = interrupt_states s irq)\<rbrace>
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R34 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y. invs\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R33 st\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>y. invs\<rbrace>
 4. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q23\<rbrace> get_irq_state irq \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R35 st s) \<and> (st = IRQTimer \<longrightarrow> ?R34 st s) \<and> (st = IRQReserved \<longrightarrow> ?R33 st s)\<rbrace>
 5. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs s\<rbrakk> \<Longrightarrow> ?Q23 s proof (prove)
goal:
No subgoals!