theory ArchDetSchedDomainTime_AI

lemma handle_interrupt_valid_domain_time [DetSchedDomainTime_AI_assms]:
  "\<lbrace>\<lambda>s :: det_ext state. 0 < domain_time s \<rbrace>
   handle_interrupt i
   \<lbrace>\<lambda>rv s.  domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread \<rbrace>" (is "\<lbrace> ?dtnot0 \<rbrace> _ \<lbrace> _ \<rbrace>") unfolding handle_interrupt_def apply (case_tac "maxIRQ < i", solves \<open>wpsimp wp: hoare_false_imp\<close>) apply clarsimp apply (wpsimp simp: arch_mask_irq_signal_def) apply (rule hoare_post_imp[where Q="\<lambda>_. ?dtnot0" and a="send_signal p c" for p c], fastforce) apply wpsimp apply (rule hoare_post_imp[where Q="\<lambda>_. ?dtnot0" and a="get_cap p" for p], fastforce) apply (wpsimp wp: timer_tick_valid_domain_time simp: handle_reserved_irq_def)+ apply (rule hoare_post_imp[where Q="\<lambda>_. ?dtnot0" and a="get_irq_state i" for i], fastforce) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> handle_interrupt i \<lbrace>\<lambda>rv s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> if maxIRQ < i then do_machine_op $ do maskInterrupt True i;
ackInterrupt i
od else do st <- get_irq_state i;
case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot i;
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 i
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq i;
do_machine_op $ ackInterrupt i
od \<lbrace>\<lambda>rv s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> maxIRQ < i \<Longrightarrow> \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> if maxIRQ < i then do_machine_op $ do maskInterrupt True i;
ackInterrupt i
od else do st <- get_irq_state i;
case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot i;
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 i
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq i;
do_machine_op $ ackInterrupt i
od \<lbrace>\<lambda>rv s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> maxIRQ < i \<Longrightarrow> \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> do st <- get_irq_state i;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot i;
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 i
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq i;
do_machine_op (ackInterrupt i)
od \<lbrace>\<lambda>rv s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>a b cap. \<lbrakk>\<not> maxIRQ < i; is_ntfn_cap cap; AllowSend \<in> cap_rights cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q233 a b (ds_id IRQSignal) (a, b) cap\<rbrace> send_signal (obj_ref_of cap) (cap_ep_badge cap) \<lbrace>\<lambda>x4 x5. domain_time x5 = 0 \<longrightarrow> scheduler_action x5 = choose_new_thread\<rbrace>
 2. \<And>st slot. \<lbrakk>\<not> maxIRQ < i; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?B211 st slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap then ?Q233 (fst slot) (snd slot) st slot cap else (\<lambda>x5. domain_time x5 = 0 \<longrightarrow> scheduler_action x5 = choose_new_thread)\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R201 st\<rbrace> get_irq_slot i \<lbrace>?B211 st\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R200 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R199 st\<rbrace> handle_reserved_irq i \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 6. \<not> maxIRQ < i \<Longrightarrow> \<lbrace>?Q189\<rbrace> get_irq_state i \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R201 st s) \<and> (st = IRQTimer \<longrightarrow> ?R200 st s) \<and> (st = IRQReserved \<longrightarrow> ?R199 st s)\<rbrace>
 7. \<And>s. \<lbrakk>\<not> maxIRQ < i; 0 < domain_time s\<rbrakk> \<Longrightarrow> ?Q189 s proof (prove)
goal (7 subgoals):
 1. \<And>a b cap. \<lbrakk>\<not> maxIRQ < i; is_ntfn_cap cap; AllowSend \<in> cap_rights cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q233 a b (ds_id IRQSignal) (a, b) cap\<rbrace> send_signal (obj_ref_of cap) (cap_ep_badge cap) \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. \<And>st slot. \<lbrakk>\<not> maxIRQ < i; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?B211 st slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap then ?Q233 (fst slot) (snd slot) st slot cap else (\<lambda>x5. domain_time x5 = 0 \<longrightarrow> scheduler_action x5 = choose_new_thread)\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R201 st\<rbrace> get_irq_slot i \<lbrace>?B211 st\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R200 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 5. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R199 st\<rbrace> handle_reserved_irq i \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 6. \<not> maxIRQ < i \<Longrightarrow> \<lbrace>?Q189\<rbrace> get_irq_state i \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R201 st s) \<and> (st = IRQTimer \<longrightarrow> ?R200 st s) \<and> (st = IRQReserved \<longrightarrow> ?R199 st s)\<rbrace>
 7. \<And>s. \<lbrakk>\<not> maxIRQ < i; 0 < domain_time s\<rbrakk> \<Longrightarrow> ?Q189 s proof (prove)
goal (6 subgoals):
 1. \<And>st slot. \<lbrakk>\<not> maxIRQ < i; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?B211 st slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap then \<lambda>x4. 0 < domain_time x4 else (\<lambda>x5. domain_time x5 = 0 \<longrightarrow> scheduler_action x5 = choose_new_thread)\<rbrace>
 2. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R201 st\<rbrace> get_irq_slot i \<lbrace>?B211 st\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R200 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R199 st\<rbrace> handle_reserved_irq i \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 5. \<not> maxIRQ < i \<Longrightarrow> \<lbrace>?Q189\<rbrace> get_irq_state i \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R201 st s) \<and> (st = IRQTimer \<longrightarrow> ?R200 st s) \<and> (st = IRQReserved \<longrightarrow> ?R199 st s)\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < i; 0 < domain_time s\<rbrakk> \<Longrightarrow> ?Q189 s proof (prove)
goal (6 subgoals):
 1. \<And>st slot. \<lbrakk>\<not> maxIRQ < i; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?B211 st slot\<rbrace> get_cap slot \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R201 st\<rbrace> get_irq_slot i \<lbrace>?B211 st\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R200 st\<rbrace> do do_extended_op timer_tick;
do_machine_op resetTimer
od \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < i; st = IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R199 st\<rbrace> handle_reserved_irq i \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 5. \<not> maxIRQ < i \<Longrightarrow> \<lbrace>?Q189\<rbrace> get_irq_state i \<lbrace>\<lambda>st s. (st = IRQInactive \<longrightarrow> True) \<and> (st = IRQSignal \<longrightarrow> ?R201 st s) \<and> (st = IRQTimer \<longrightarrow> ?R200 st s) \<and> (st = IRQReserved \<longrightarrow> ?R199 st s)\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < i; 0 < domain_time s\<rbrakk> \<Longrightarrow> ?Q189 s proof (prove)
goal (2 subgoals):
 1. \<not> maxIRQ < i \<Longrightarrow> \<lbrace>?Q189\<rbrace> get_irq_state i \<lbrace>\<lambda>st s. (st = IRQSignal \<longrightarrow> 0 < domain_time s) \<and> (st = IRQTimer \<longrightarrow> 0 < domain_time s) \<and> (st = IRQReserved \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
 2. \<And>s. \<lbrakk>\<not> maxIRQ < i; 0 < domain_time s\<rbrakk> \<Longrightarrow> ?Q189 s proof (prove)
goal (2 subgoals):
 1. \<not> maxIRQ < i \<Longrightarrow> \<lbrace>?Q189\<rbrace> get_irq_state i \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. \<And>s. \<lbrakk>\<not> maxIRQ < i; 0 < domain_time s\<rbrakk> \<Longrightarrow> ?Q189 s proof (prove)
goal:
No subgoals!