kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_IF

lemma not_ntfn_queue_invisible:
  "\<lbrakk> \<not> ntfn_queue_invisible aag l eplist; eplist = WaitingNtfn list \<rbrakk>
     \<Longrightarrow> (\<exists>t \<in> set list. aag_can_read aag t \<or> aag_can_affect aag l t)" by (auto simp: labels_are_invisible_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> ntfn_queue_invisible aag l eplist; eplist = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<exists>t\<in>set list. aag_can_read aag t \<or> aag_can_affect aag l t
theory Finalise_IF

lemma get_bound_notification_reads_respects':
  "reads_respects aag l (K(is_subject aag thread)) (get_bound_notification thread)" unfolding get_bound_notification_def thread_get_def apply (wp | simp)+ apply clarify apply (rule requiv_get_tcb_eq) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag thread)) (get_bound_notification thread) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag thread)) (do tcb <- gets_the $ get_tcb thread;
return $ tcb_bound_notification tcb
od) proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb thread s = get_tcb thread t proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>is_subject aag thread; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> get_tcb thread s = get_tcb thread t proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>is_subject aag thread; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv (?aag15 s t) s t
 2. \<And>s t. \<lbrakk>is_subject aag thread; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> is_subject (?aag15 s t) thread proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma thread_get_reads_respects:
  "reads_respects aag l (K (aag_can_read aag thread \<or> aag_can_affect aag l thread))
                  (thread_get f thread)" unfolding thread_get_def fun_app_def apply (wp gets_the_ev) apply (auto intro: reads_affects_equiv_get_tcb_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag thread \<or> aag_can_affect aag l thread)) (thread_get f thread) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag thread \<or> aag_can_affect aag l thread)) (do tcb <- gets_the (get_tcb thread);
return (f tcb)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. K (aag_can_read aag thread \<or> aag_can_affect aag l thread) s \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb thread s = get_tcb thread t) s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma get_bound_notification_reads_respects:
  "reads_respects aag l (\<lambda> s. aag_can_read aag thread \<or> aag_can_affect aag l thread)
                  (get_bound_notification thread)" unfolding get_bound_notification_def apply (rule equiv_valid_guard_imp) apply (wp thread_get_reads_respects | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. aag_can_read aag thread \<or> aag_can_affect aag l thread) (get_bound_notification thread) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. aag_can_read aag thread \<or> aag_can_affect aag l thread) (thread_get tcb_bound_notification thread) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (thread_get tcb_bound_notification thread)
 2. \<And>s. aag_can_read aag thread \<or> aag_can_affect aag l thread \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma bound_tcb_at_eq:
  "\<lbrakk> sym_refs (state_refs_of s); valid_objs s; kheap s ntfnptr = Some (Notification ntfn);
     ntfn_bound_tcb ntfn = Some tcbptr; bound_tcb_at ((=) (Some ntfnptr')) tcbptr s \<rbrakk>
     \<Longrightarrow> ntfnptr = ntfnptr'" apply (drule_tac x=ntfnptr in sym_refsD[rotated]) apply (fastforce simp: state_refs_of_def) apply (auto simp: pred_tcb_at_def obj_at_def valid_obj_def valid_ntfn_def
                    is_tcb state_refs_of_def refs_of_rev
          simp del: refs_of_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of s); valid_objs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; bound_tcb_at ((=) (Some ntfnptr')) tcbptr s\<rbrakk> \<Longrightarrow> ntfnptr = ntfnptr' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; bound_tcb_at ((=) (Some ntfnptr')) tcbptr s\<rbrakk> \<Longrightarrow> (?y, ?tp) \<in> state_refs_of s ntfnptr
 2. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; bound_tcb_at ((=) (Some ntfnptr')) tcbptr s; (ntfnptr, symreftype ?tp) \<in> state_refs_of s ?y\<rbrakk> \<Longrightarrow> ntfnptr = ntfnptr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; bound_tcb_at ((=) (Some ntfnptr')) tcbptr s; (ntfnptr, symreftype NTFNBound) \<in> state_refs_of s tcbptr\<rbrakk> \<Longrightarrow> ntfnptr = ntfnptr' proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma cancel_all_signals_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs
                                           and valid_arch_state and K (aag_can_read aag ntfnptr))
                   (cancel_all_signals ntfnptr)" unfolding cancel_all_signals_def by (wp mapM_x_ev'' tcb_sched_action_reads_respects set_thread_state_runnable_reads_respects
         set_thread_state_pas_refined hoare_vcg_ball_lift
         set_thread_state_runnable_valid_sched_action
         set_simple_ko_reads_respects get_epq_SendEP_ret get_epq_RecvEP_ret
         get_simple_ko_reads_respects get_simple_ko_wp
      | wpc
      | clarsimp simp: ball_conj_distrib
      | rule subset_refl
      | wp (once) hoare_drop_imps
      | simp
      | rule hoare_strengthen_post[where Q="\<lambda>_. pas_refined aag and pspace_aligned
                                                                and valid_vspace_objs
                                                                and valid_arch_state", OF mapM_x_wp])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (aag_can_read aag ntfnptr)) (cancel_all_signals ntfnptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (aag_can_read aag ntfnptr)) (do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od)
theory Finalise_IF

lemma unbind_maybe_notification_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag l (pas_refined aag and invs and K (aag_can_read aag ntfnptr))
                  (unbind_maybe_notification ntfnptr)" unfolding unbind_maybe_notification_def by (wp set_bound_notification_none_reads_respects
         set_simple_ko_reads_respects get_simple_ko_reads_respects
      | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and invs and K (aag_can_read aag ntfnptr)) (unbind_maybe_notification ntfnptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and invs and K (aag_can_read aag ntfnptr)) (do ntfn <- get_notification ntfnptr;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification ntfnptr ntfn t
od)
theory Finalise_IF

lemma fast_finalise_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects aag l (pas_refined aag and invs and
                           K (fin \<longrightarrow> (case cap of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r
                                             | NotificationCap r badge rights \<Rightarrow> is_subject aag r
                                             | _ \<Rightarrow> True)))
                    (fast_finalise cap fin)" apply (case_tac cap, simp_all) by (wp equiv_valid_guard_imp[OF cancel_all_ipc_reads_respects]
         equiv_valid_guard_imp[OF cancel_all_signals_reads_respects]
         unbind_notification_is_subj_reads_respects
         unbind_maybe_notification_reads_respects
         get_simple_ko_reads_respects get_simple_ko_wp
      | simp add: when_def
      | wpc
      | intro conjI impI
      | fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and invs and K (fin \<longrightarrow> (case cap of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True))) (fast_finalise cap fin) proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> reads_respects aag l (pas_refined aag and invs) (return ())
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> reads_respects aag l (pas_refined aag and invs) fail
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> reads_respects aag l (pas_refined aag and invs and (\<lambda>y. fin \<longrightarrow> aag_can_read aag x31)) (when fin (cancel_all_ipc x31))
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> reads_respects aag l (pas_refined aag and invs and (\<lambda>y. fin \<longrightarrow> is_subject aag x41)) (when fin (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od))
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> reads_respects aag l (pas_refined aag and invs) (return ())
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> reads_respects aag l (pas_refined aag and invs) fail
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> reads_respects aag l (pas_refined aag and invs) fail
 8. cap = DomainCap \<Longrightarrow> reads_respects aag l (pas_refined aag and invs) fail
 9. cap = IRQControlCap \<Longrightarrow> reads_respects aag l (pas_refined aag and invs) fail
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> reads_respects aag l (pas_refined aag and invs) fail
A total of 12 subgoals...
theory Finalise_IF

lemma st_tcb_at_sym:
  "st_tcb_at ((=) x) t s = st_tcb_at (\<lambda> y. y = x) t s" by (auto simp: st_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at ((=) x) t s = st_tcb_at (\<lambda>y. y = x) t s
theory Finalise_IF

lemma blocked_cancel_ipc_reads_respects:
  "reads_respects aag l (pas_refined aag and invs and st_tcb_at ((=) state) tptr
                                                  and K (is_subject aag tptr))
                  (blocked_cancel_ipc state tptr)" unfolding blocked_cancel_ipc_def apply (wp set_thread_state_owned_reads_respects set_simple_ko_reads_respects
            get_ep_queue_reads_respects get_simple_ko_reads_respects get_blocking_object_reads_respects
         | simp add: get_blocking_object_def | wpc)+ apply (fastforce intro: aag_can_read_self owns_thread_blocked_reads_endpoint simp: st_tcb_at_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and invs and st_tcb_at ((=) state) tptr and K (is_subject aag tptr)) (blocked_cancel_ipc state tptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and invs and st_tcb_at ((=) state) tptr and K (is_subject aag tptr)) (do epptr <- get_blocking_object state;
ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
queue' <- return $ remove1 tptr queue;
ep' <- return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue');
set_endpoint epptr ep';
set_thread_state tptr Inactive
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> invs s \<and> st_tcb_at ((=) state) tptr s \<and> is_subject aag tptr \<Longrightarrow> (\<forall>x. (\<exists>xa. state = BlockedOnReceive x xa) \<longrightarrow> aag_can_read aag x \<or> aag_can_affect aag l x) \<and> (\<forall>x. (\<exists>xa. state = BlockedOnSend x xa) \<longrightarrow> aag_can_read aag x \<or> aag_can_affect aag l x) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma select_singleton_ev:
  "equiv_valid_inv I B (K (\<exists>a. A = {a})) (select A)" by (fastforce simp: equiv_valid_def2 equiv_valid_2_def select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I B (K (\<exists>a. A = {a})) (select A)
theory Finalise_IF

lemma thread_set_fault_pas_refined':
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
   thread_set (tcb_fault_update fault) thread
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by (wp thread_set_pas_refined | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> thread_set (tcb_fault_update fault) thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory Finalise_IF

lemma get_thread_state_rev:
  "reads_equiv_valid_inv A aag (K (aag_can_read aag ref)) (get_thread_state ref)" unfolding get_thread_state_def by (rule thread_get_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (aag_can_read aag ref)) (get_thread_state ref) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (aag_can_read aag ref)) (thread_get tcb_state ref)
theory Finalise_IF

lemma cancel_signal_owned_reads_respects:
  "reads_respects aag l
     (K (is_subject aag threadptr \<and> (aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr)))
     (cancel_signal threadptr ntfnptr)" unfolding cancel_signal_def by (wp set_thread_state_owned_reads_respects set_simple_ko_reads_respects
         get_simple_ko_reads_respects hoare_drop_imps
      | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag threadptr \<and> (aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr))) (cancel_signal threadptr ntfnptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag threadptr \<and> (aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr))) (do ntfn <- get_notification ntfnptr;
queue <- case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
queue' <- return $ remove1 threadptr queue;
newNTFN <- return $ ntfn_set_obj ntfn (case queue' of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn queue');
set_notification ntfnptr newNTFN;
set_thread_state threadptr Inactive
od)
theory Finalise_IF

lemma as_user_get_register_reads_respects:
  "reads_respects aag l (K (is_subject aag thread)) (as_user thread (getRegister reg))" by (fastforce simp: equiv_valid_guard_imp[OF as_user_reads_respects] det_getRegister)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag thread)) (as_user thread (getRegister reg))
theory Finalise_IF

lemma update_restart_pc_reads_respects[wp]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag l (silc_inv aag s and K (is_subject aag thread))
                        (update_restart_pc thread)" unfolding update_restart_pc_def apply (subst as_user_bind) apply (wpsimp wp: as_user_set_register_reads_respects' as_user_get_register_reads_respects) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (silc_inv aag s and K (is_subject aag thread)) (update_restart_pc thread) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (silc_inv aag s and K (is_subject aag thread)) (as_user thread (getRegister nextInstructionRegister >>= setRegister faultRegister)) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (silc_inv aag s and K (is_subject aag thread)) (do x <- as_user thread (getRegister nextInstructionRegister);
as_user thread (setRegister faultRegister x)
od) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma deleting_irq_handler_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag
                                                 and K (is_subject_irq aag irq))
                          (deleting_irq_handler irq)" unfolding deleting_irq_handler_def by (wp cap_delete_one_reads_respects_f reads_respects_f[OF get_irq_slot_reads_respects]
      | simp | blast)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and K (is_subject_irq aag irq)) (deleting_irq_handler irq) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and K (is_subject_irq aag irq)) (get_irq_slot irq >>= cap_delete_one)
theory Finalise_IF

lemma cap_swap_for_delete_reads_respects:
  "reads_respects aag l (K (is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)))
                 (cap_swap_for_delete slot1 slot2)" unfolding cap_swap_for_delete_def apply (simp add: when_def) apply (rule conjI, rule impI) apply (rule equiv_valid_guard_imp) apply (wp cap_swap_reads_respects get_cap_rev) apply (simp) apply (rule impI, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (fst slot1) \<and> is_subject aag (fst slot2))) (cap_swap_for_delete slot1 slot2) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (fst slot1) \<and> is_subject aag (fst slot2))) (when (slot1 \<noteq> slot2) $ do cap1 <- get_cap slot1;
cap2 <- get_cap slot2;
cap_swap cap1 slot1 cap2 slot2
od) proof (prove)
goal (1 subgoal):
 1. (slot1 \<noteq> slot2 \<longrightarrow> reads_respects aag l (\<lambda>y. is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)) (do cap1 <- get_cap slot1;
cap2 <- get_cap slot2;
cap_swap cap1 slot1 cap2 slot2
od)) \<and> (slot1 = slot2 \<longrightarrow> reads_respects aag l (\<lambda>y. is_subject aag (fst slot2)) (return ())) proof (prove)
goal (2 subgoals):
 1. slot1 \<noteq> slot2 \<Longrightarrow> reads_respects aag l (\<lambda>y. is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)) (do cap1 <- get_cap slot1;
cap2 <- get_cap slot2;
cap_swap cap1 slot1 cap2 slot2
od)
 2. slot1 = slot2 \<longrightarrow> reads_respects aag l (\<lambda>y. is_subject aag (fst slot2)) (return ()) proof (prove)
goal (3 subgoals):
 1. slot1 \<noteq> slot2 \<Longrightarrow> reads_respects aag l ?Q9 (do cap1 <- get_cap slot1;
cap2 <- get_cap slot2;
cap_swap cap1 slot1 cap2 slot2
od)
 2. \<And>s. \<lbrakk>slot1 \<noteq> slot2; is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)\<rbrakk> \<Longrightarrow> ?Q9 s
 3. slot1 = slot2 \<longrightarrow> reads_respects aag l (\<lambda>y. is_subject aag (fst slot2)) (return ()) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>slot1 \<noteq> slot2; is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)\<rbrakk> \<Longrightarrow> K (aag_can_read aag (fst slot1)) s \<and> K (aag_can_read aag (fst slot2)) s \<and> K (is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)) s
 2. slot1 = slot2 \<longrightarrow> reads_respects aag l (\<lambda>y. is_subject aag (fst slot2)) (return ()) proof (prove)
goal (1 subgoal):
 1. slot1 = slot2 \<longrightarrow> reads_respects aag l (\<lambda>y. is_subject aag (fst slot2)) (return ()) proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma rec_del_only_timer_irq:
  "\<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>
   rec_del call
   \<lbrace>\<lambda>_. only_timer_irq irq\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (rule hoare_pre, rule only_timer_irq_pres) apply (rule hoare_pre, wp rec_del_irq_masks) apply (wp rec_del_domain_sep_inv | force | rule hoare_pre, wp (once) rec_del_domain_sep_inv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> rec_del call \<lbrace>\<lambda>_. only_timer_irq irq\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> rec_del call \<lbrace>\<lambda>_. only_timer_irq irq\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and ?Q3\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>st. \<lbrace>domain_sep_inv False st and ?P3\<rbrace> rec_del call \<lbrace>\<lambda>_. domain_sep_inv False st\<rbrace>
 3. \<And>s. (domain_sep_inv False st and only_timer_irq irq) s \<Longrightarrow> (only_timer_irq irq and ?Q3 and ?P3 and domain_sep_inv False ?st3) s proof (prove)
goal (3 subgoals):
 1. \<And>P s. ((\<lambda>s. P (irq_masks_of_state s)) and ?Q3) s \<Longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st11 P)) s
 2. \<And>st. \<lbrace>domain_sep_inv False st and ?P3\<rbrace> rec_del call \<lbrace>\<lambda>_. domain_sep_inv False st\<rbrace>
 3. \<And>s. (domain_sep_inv False st and only_timer_irq irq) s \<Longrightarrow> (only_timer_irq irq and ?Q3 and ?P3 and domain_sep_inv False ?st3) s proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma rec_del_only_timer_irq_inv:
  "\<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>
   rec_del call
   \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (rule hoare_wp_simps) apply (rule hoare_conjI) apply (wp rec_del_domain_sep_inv rec_del_only_timer_irq | force simp: only_timer_irq_inv_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> rec_del call \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> rec_del call \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> rec_del call \<lbrace>\<lambda>_ s. domain_sep_inv False st s \<and> only_timer_irq irq s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> rec_del call \<lbrace>\<lambda>r. domain_sep_inv False st\<rbrace>
 2. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> rec_del call \<lbrace>\<lambda>r. only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma set_cap_only_timer_irq_inv:
  "\<lbrace>only_timer_irq_inv irq (st :: det_state) and K (domain_sep_inv_cap False cap)\<rbrace>
   set_cap cap slot
   \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (wp only_timer_irq_pres set_cap_domain_sep_inv | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st and K (domain_sep_inv_cap False cap)\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq and (\<lambda>y. domain_sep_inv_cap False cap)\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!