kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_AC

lemma thread_set_tcb_state_trivial:
  "(\<And>tcb. tcb_state (f tcb) = tcb_state tcb)
   \<Longrightarrow> thread_set f t \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace>" apply (simp add: thread_set_def) apply (wpsimp wp: set_object_wp) apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD) by (auto simp: tcb_states_of_state_def get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (tcb_states_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>_ s. P (tcb_states_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_state (f tcb) = tcb_state tcb; P (tcb_states_of_state s); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (tcb_states_of_state (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f y))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_state (f tcb) = tcb_state tcb; kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_states_of_state s = tcb_states_of_state (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f y))\<rparr>)
theory Finalise_AC

lemma cancel_signal_respects[wp]:
  "\<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag t \<and>
        (\<exists>auth. aag_has_auth_to aag auth ntfnptr \<and> (auth = Receive \<or> auth = Notify))\<rbrace>
   cancel_signal t ntfnptr
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: cancel_signal_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp set_thread_state_integrity_autarch set_ntfn_respects | wpc | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag t \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify))\<rbrace> cancel_signal t ntfnptr \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag t \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify))\<rbrace> do ntfn <- get_notification ntfnptr;
queue <- case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfnptr (ntfn_set_obj ntfn (case remove1 t queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t queue)));
set_thread_state t Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and (\<lambda>s. integrity aag X st s \<and> is_subject aag t \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify)))\<rbrace> do queue <- case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfnptr (ntfn_set_obj ntfn (case remove1 t queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t queue)));
set_thread_state t Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> do queue <- case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfnptr (ntfn_set_obj ntfn (case remove1 t queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t queue)));
set_thread_state t Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (\<lambda>s. integrity aag X st s \<and> is_subject aag t \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify)))) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma update_restart_pc_integrity_autarch[wp]:
  "\<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace>
   update_restart_pc t
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: get_thread_state_def thread_get_def update_restart_pc_def) apply (wpsimp wp: as_user_integrity_autarch) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace> update_restart_pc t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag t)\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma finalise_is_fast_finalise:
  "can_fast_finalise cap
   \<Longrightarrow> finalise_cap cap fin = do fast_finalise cap fin; return (NullCap, NullCap) od" by (cases cap, simp_all add: can_fast_finalise_def liftM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. can_fast_finalise cap \<Longrightarrow> finalise_cap cap fin = do fast_finalise cap fin;
return (NullCap, NullCap)
od
theory Finalise_AC

lemma get_irq_slot_owns[wp]:
  "\<lbrace>pas_refined aag and K (is_subject_irq aag irq)\<rbrace>
   get_irq_slot irq
   \<lbrace>\<lambda>rv _. is_subject aag (fst rv)\<rbrace>" unfolding get_irq_slot_def apply wp apply (rule pas_refined_Control [symmetric]) apply (clarsimp simp: pas_refined_def irq_map_wellformed_aux_def aag_wellformed_refl) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject_irq aag irq)\<rbrace> get_irq_slot irq \<lbrace>\<lambda>rv _. is_subject aag (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject_irq aag irq)\<rbrace> gets (\<lambda>st. (interrupt_irq_node st irq, [])) \<lbrace>\<lambda>rv _. is_subject aag (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_subject_irq aag irq)) s \<Longrightarrow> is_subject aag (fst (interrupt_irq_node s irq, [])) proof (prove)
goal (2 subgoals):
 1. \<And>s. (pas_refined aag and K (is_subject_irq aag irq)) s \<Longrightarrow> (pasSubject aag, Control, pasObjectAbs aag (fst (interrupt_irq_node s irq, []))) \<in> pasPolicy aag
 2. \<And>s. (pas_refined aag and K (is_subject_irq aag irq)) s \<Longrightarrow> pas_refined aag (?s2 s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_subject_irq aag irq)) s \<Longrightarrow> pas_refined aag (?s2 s) proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma pas_refined_Control_into_is_subject_asid:
  "\<lbrakk> pas_refined aag s; (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag \<rbrakk>
     \<Longrightarrow> is_subject_asid aag asid" apply (drule (1) pas_refined_Control) apply (blast intro: sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject_asid aag asid proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pasSubject aag = pasASIDAbs aag asid\<rbrakk> \<Longrightarrow> is_subject_asid aag asid proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma aag_cap_auth_recycle_EndpointCap:
  "\<lbrakk> pas_refined aag s; has_cancel_send_rights (EndpointCap word1 word2 f) \<rbrakk>
     \<Longrightarrow> pas_cap_cur_auth aag (EndpointCap word1 word2 f) = is_subject aag word1" unfolding aag_cap_auth_def by (auto simp: cli_no_irqs clas_no_asid cap_auth_conferred_def pas_refined_all_auth_is_owns
                 has_cancel_send_rights_def cap_rights_to_auth_def all_rights_def pas_refined_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; has_cancel_send_rights (EndpointCap word1 word2 f)\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag (EndpointCap word1 word2 f) = is_subject aag word1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; has_cancel_send_rights (EndpointCap word1 word2 f)\<rbrakk> \<Longrightarrow> ((\<forall>x\<in>obj_refs_ac (EndpointCap word1 word2 f). \<forall>auth\<in>cap_auth_conferred (EndpointCap word1 word2 f). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (EndpointCap word1 word2 f). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (EndpointCap word1 word2 f) \<and> cap_links_irq aag (pasSubject aag) (EndpointCap word1 word2 f)) = is_subject aag word1
theory Finalise_AC

lemma aag_cap_auth_Zombie:
  "pas_refined aag s \<Longrightarrow> pas_cap_cur_auth aag (Zombie word a b) = is_subject aag word" unfolding aag_cap_auth_def by (simp add: cli_no_irqs clas_no_asid cap_auth_conferred_def pas_refined_all_auth_is_owns)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> pas_cap_cur_auth aag (Zombie word a b) = is_subject aag word proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> ((\<forall>x\<in>obj_refs_ac (Zombie word a b). \<forall>auth\<in>cap_auth_conferred (Zombie word a b). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (Zombie word a b). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (Zombie word a b) \<and> cap_links_irq aag (pasSubject aag) (Zombie word a b)) = is_subject aag word
theory Finalise_AC

lemma aag_cap_auth_CNode:
  "pas_refined aag s \<Longrightarrow> pas_cap_cur_auth aag (CNodeCap word a b) = is_subject aag word" unfolding aag_cap_auth_def by (simp add: cli_no_irqs clas_no_asid cap_auth_conferred_def pas_refined_all_auth_is_owns)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> pas_cap_cur_auth aag (CNodeCap word a b) = is_subject aag word proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> ((\<forall>x\<in>obj_refs_ac (CNodeCap word a b). \<forall>auth\<in>cap_auth_conferred (CNodeCap word a b). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (CNodeCap word a b). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (CNodeCap word a b) \<and> cap_links_irq aag (pasSubject aag) (CNodeCap word a b)) = is_subject aag word
theory Finalise_AC

lemma aag_cap_auth_Thread:
  "pas_refined aag s \<Longrightarrow> pas_cap_cur_auth aag (ThreadCap word) = is_subject aag word" unfolding aag_cap_auth_def by (simp add: cli_no_irqs clas_no_asid cap_auth_conferred_def pas_refined_all_auth_is_owns)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> pas_cap_cur_auth aag (ThreadCap word) = is_subject aag word proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> ((\<forall>x\<in>obj_refs_ac (ThreadCap word). \<forall>auth\<in>cap_auth_conferred (ThreadCap word). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ThreadCap word). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ThreadCap word) \<and> cap_links_irq aag (pasSubject aag) (ThreadCap word)) = is_subject aag word
theory Finalise_AC

lemma finalise_cap_obj_refs:
  "\<lbrace>\<lambda>_ :: det_ext state. \<forall>x \<in> obj_refs_ac cap. P x\<rbrace>
   finalise_cap cap slot
   \<lbrace>\<lambda>rv _. \<forall>x \<in> obj_refs_ac (fst rv). P x\<rbrace>" by (cases cap) (wpsimp wp: arch_finalise_cap_obj_refs simp: o_def | rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. \<forall>x\<in>obj_refs_ac cap. P x\<rbrace> finalise_cap cap slot \<lbrace>\<lambda>rv _. \<forall>x\<in>obj_refs_ac (fst rv). P x\<rbrace>
theory Finalise_AC

lemma zombie_ptr_emptyable:
  "\<lbrakk> caps_of_state s cref = Some (Zombie ptr zbits n); invs s \<rbrakk>
     \<Longrightarrow> emptyable (ptr, cref_half) s" apply (clarsimp simp: emptyable_def tcb_at_def st_tcb_def2) apply (rule ccontr) apply (clarsimp simp: get_tcb_ko_at) apply (drule if_live_then_nonz_capD[rotated]) apply (auto simp: live_def)[2] apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state
                        zobj_refs_to_obj_refs) apply (drule(2) zombies_final_helperE, clarsimp, simp+) apply (simp add: is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s\<rbrakk> \<Longrightarrow> emptyable (ptr, cref_half) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s; cref_half = tcb_cnode_index 2; get_tcb ptr s = Some tcb\<rbrakk> \<Longrightarrow> halted (tcb_state tcb) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s; cref_half = tcb_cnode_index 2; get_tcb ptr s = Some tcb; \<not> halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s; cref_half = tcb_cnode_index 2; ko_at (TCB tcb) ptr s; \<not> halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>tcb obj. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s; cref_half = tcb_cnode_index 2; \<not> halted (tcb_state tcb); TCB tcb = obj; kheap s ptr = Some obj\<rbrakk> \<Longrightarrow> live obj
 2. \<And>tcb. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s; cref_half = tcb_cnode_index 2; \<not> halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap s
 3. \<And>tcb. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s; cref_half = tcb_cnode_index 2; \<not> halted (tcb_state tcb); ex_nonz_cap_to ptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s; cref_half = tcb_cnode_index 2; \<not> halted (tcb_state tcb); ex_nonz_cap_to ptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb a b cap. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s; cref_half = tcb_cnode_index 2; \<not> halted (tcb_state tcb); caps_of_state s (a, b) = Some cap; ptr \<in> obj_refs cap; \<not> is_zombie cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb cap. \<lbrakk>caps_of_state s cref = Some (Zombie ptr zbits n); invs s; cref_half = tcb_cnode_index 2; \<not> halted (tcb_state tcb); ptr \<in> obj_refs cap; \<not> is_zombie cap; \<not> is_zombie (Zombie ptr zbits n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma aag_Control_into_owns_irq:
  "\<lbrakk> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag; pas_refined aag s \<rbrakk>
     \<Longrightarrow> is_subject_irq aag irq" apply (drule (1) pas_refined_Control) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag; pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject_irq aag irq proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pasSubject aag = pasIRQAbs aag irq\<rbrakk> \<Longrightarrow> is_subject_irq aag irq proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma owns_slot_owns_irq:
  "\<lbrakk> is_subject aag (fst slot); pas_refined aag s;
     caps_of_state s slot = Some rv; cap_irq_opt rv = Some irq \<rbrakk>
     \<Longrightarrow> is_subject_irq aag irq" apply (rule aag_Control_into_owns_irq[rotated], assumption) apply (drule (1) cli_caps_of_state) apply (clarsimp simp: cap_links_irq_def cap_irq_opt_def split: cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; caps_of_state s slot = Some rv; cap_irq_opt rv = Some irq\<rbrakk> \<Longrightarrow> is_subject_irq aag irq proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; caps_of_state s slot = Some rv; cap_irq_opt rv = Some irq\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag (fst slot); pas_refined aag s; cap_irq_opt rv = Some irq; cap_links_irq aag (pasObjectAbs aag (fst slot)) rv\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma replaceable_zombie_not_transferable:
  "replaceable s slot (Zombie ref sz n) cap \<Longrightarrow> \<not> is_transferable (Some cap)" by (intro notI) (erule is_transferable.cases; simp add:replaceable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replaceable s slot (Zombie ref sz n) cap \<Longrightarrow> \<not> is_transferable_cap cap
theory Finalise_AC

lemma rec_del_respects'_pre:
  "s \<turnstile>
  \<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and
   simple_sched_action and valid_rec_del_call call and emptyable (slot_rdcall call) and
   (\<lambda>s. \<not> exposed_rdcall call \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall call) s) and
   K (is_subject aag (fst (slot_rdcall call))) and
   K (case call of ReduceZombieCall cap sl _ \<Rightarrow> \<forall>x \<in> obj_refs_ac cap. is_subject aag x | _ \<Rightarrow> True)\<rbrace>
  rec_del call
  \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>,
  \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>" apply (rule spec_strengthen_postE[OF rec_del_respects'_pre']) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>(\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag and einvs and simple_sched_action and valid_rec_del_call call and emptyable (slot_rdcall call) and (\<lambda>s. \<not> exposed_rdcall call \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall call) s) and K (is_subject aag (fst (slot_rdcall call))) and K (case call of ReduceZombieCall cap sl x \<Rightarrow> \<forall>x\<in>obj_refs_ac cap. is_subject aag x | _ \<Rightarrow> True)\<rbrace> rec_del call \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s r. ((\<lambda>sa. trp \<longrightarrow> (case call of FinaliseSlotCall sl x \<Rightarrow> cleanup_info_wf (snd s) aag | _ \<Rightarrow> True) \<and> integrity aag X st sa) and pas_refined aag) r \<Longrightarrow> ((\<lambda>s. trp \<longrightarrow> integrity aag X st s) and pas_refined aag) r
theory Finalise_AC

lemma finalise_cap_transferable:
  "\<lbrace>P and K (is_transferable_cap cap)\<rbrace>
   finalise_cap cap final
   \<lbrace>\<lambda>rv s. rv = (NullCap, NullCap) \<and> P s\<rbrace>" by (rule hoare_gen_asm) (erule is_transferable_capE; wpsimp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and K (is_transferable_cap cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv s. rv = (NullCap, NullCap) \<and> P s\<rbrace>
theory Finalise_AC

lemma set_eobject_integrity_autarch:
  "\<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace>
   set_eobject ptr obj
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: set_eobject_def) apply wp apply (simp add: integrity_subjects_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace> set_eobject ptr obj \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag ptr)\<rbrace> do es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(ptr \<mapsto> obj)) es)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>y. is_subject aag ptr)) s \<Longrightarrow> integrity aag X st (ekheap_update (\<lambda>_. (ekheap s)(ptr \<mapsto> obj)) s) proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma cancel_badged_sends_pas_refined[wp]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
   cancel_badged_sends epptr badge
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" unfolding cancel_badged_sends_def by (wpsimp simp: filterM_mapM wp: mapM_wp_inv set_thread_state_pas_refined get_simple_ko_wp)

(* 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> cancel_badged_sends epptr badge \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do ep <- get_endpoint epptr;
case ep of SendEP queue \<Rightarrow> do set_endpoint epptr IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue');
set_endpoint epptr ep';
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory Finalise_AC

lemma rsubst':
  "\<lbrakk> P s s'; s=t; s'=t' \<rbrakk> \<Longrightarrow> P t t'" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s s'; s = t; s' = t'\<rbrakk> \<Longrightarrow> P t t'
theory Finalise_AC

lemma cap_delete_respects:
  "\<lbrace>integrity aag X st and cdt_change_allowed' aag slot and pas_refined aag
                       and einvs and simple_sched_action and emptyable slot\<rbrace>
   cap_delete slot
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (simp add: cap_delete_def) (wpsimp wp: rec_del_respects_CTEDelete_transferable)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and cdt_change_allowed' aag slot and pas_refined aag and einvs and simple_sched_action and emptyable slot\<rbrace> cap_delete slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Finalise_AC

lemma cap_delete_respects':
  "\<lbrace>integrity aag X st and K (is_subject aag (fst slot)) and pas_refined aag
                       and einvs and simple_sched_action and emptyable slot\<rbrace>
   cap_delete slot
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (wp cap_delete_respects) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag (fst slot)) and pas_refined aag and einvs and simple_sched_action and emptyable slot\<rbrace> cap_delete slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Finalise_AC

lemma cap_delete_pas_refined:
  "\<lbrace>cdt_change_allowed' aag slot and pas_refined aag and einvs
                                 and simple_sched_action and emptyable slot\<rbrace>
   cap_delete slot
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by (simp add: cap_delete_def) (wpsimp wp: rec_del_respects_CTEDelete_transferable)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdt_change_allowed' aag slot and pas_refined aag and einvs and simple_sched_action and emptyable slot\<rbrace> cap_delete slot \<lbrace>\<lambda>_. pas_refined aag\<rbrace>