theory Finalise_AC

lemma cancel_all_ipc_respects [wp]:
  "\<lbrace>integrity aag X st and valid_objs and (sym_refs \<circ> state_refs_of)
                       and K (\<exists>auth. aag_has_auth_to aag Reset epptr)\<rbrace>
   cancel_all_ipc epptr
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: cancel_all_ipc_def get_ep_queue_def cong: endpoint.case_cong) apply (wp mapM_x_inv_wp2
            [where I="integrity aag X st"
               and V="\<lambda>q s. distinct q \<and> (\<forall>x \<in> set q. st_tcb_at (blocked_on epptr) x s)"]
            sts_respects_restart_ep sts_st_tcb_at_neq hoare_vcg_ball_lift
            set_endpoint_respects get_simple_ko_wp
         | wpc | clarsimp | blast)+ apply (frule ko_at_state_refs_ofD) apply (rule obj_at_valid_objsE, assumption, assumption) apply (rename_tac ep ko) apply (subgoal_tac "\<forall>x \<in> ep_q_refs_of ep. st_tcb_at (blocked_on epptr) (fst x) s") apply (fastforce simp: valid_obj_def valid_ep_def obj_at_def is_ep_def
                   split: endpoint.splits) apply clarsimp apply (erule (1) ep_queued_st_tcb_at') apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and valid_objs and sym_refs \<circ> state_refs_of and K (\<exists>auth. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)\<rbrace> cancel_all_ipc epptr \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<exists>auth. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>integrity aag X st and valid_objs and sym_refs \<circ> state_refs_of\<rbrace> cancel_all_ipc epptr \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>integrity aag X st and valid_objs and sym_refs \<circ> state_refs_of\<rbrace> do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> return () | SendEP list \<Rightarrow> do y <- set_endpoint epptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od | RecvEP list \<Rightarrow> do y <- set_endpoint epptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint ntfn) epptr s\<rbrakk> \<Longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint ntfn) epptr s; state_refs_of s epptr = refs_of (Endpoint ntfn)\<rbrakk> \<Longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn ko. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint ntfn) epptr s; state_refs_of s epptr = refs_of (Endpoint ntfn); kheap s epptr = Some ko; Endpoint ntfn = ko; valid_obj epptr ko s\<rbrakk> \<Longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) proof (prove)
goal (1 subgoal):
 1. \<And>s ep ko. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint ep) epptr s; state_refs_of s epptr = refs_of (Endpoint ep); kheap s epptr = Some ko; Endpoint ep = ko; valid_obj epptr ko s\<rbrakk> \<Longrightarrow> (\<forall>x. ep = SendEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) proof (prove)
goal (2 subgoals):
 1. \<And>s ep ko. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint ep) epptr s; state_refs_of s epptr = refs_of (Endpoint ep); kheap s epptr = Some ko; Endpoint ep = ko; valid_obj epptr ko s; \<forall>x\<in>ep_q_refs_of ep. st_tcb_at (blocked_on epptr) (fst x) s\<rbrakk> \<Longrightarrow> (\<forall>x. ep = SendEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s))
 2. \<And>s ep ko. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint ep) epptr s; state_refs_of s epptr = refs_of (Endpoint ep); kheap s epptr = Some ko; Endpoint ep = ko; valid_obj epptr ko s\<rbrakk> \<Longrightarrow> \<forall>x\<in>ep_q_refs_of ep. st_tcb_at (blocked_on epptr) (fst x) s proof (prove)
goal (1 subgoal):
 1. \<And>s ep ko. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint ep) epptr s; state_refs_of s epptr = refs_of (Endpoint ep); kheap s epptr = Some ko; Endpoint ep = ko; valid_obj epptr ko s\<rbrakk> \<Longrightarrow> \<forall>x\<in>ep_q_refs_of ep. st_tcb_at (blocked_on epptr) (fst x) s proof (prove)
goal (1 subgoal):
 1. \<And>s ep a b. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint ep) epptr s; state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_obj epptr (Endpoint ep) s; (a, b) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> st_tcb_at (blocked_on epptr) a s proof (prove)
goal (3 subgoals):
 1. \<And>s ep a b. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_obj epptr (Endpoint ep) s; (a, b) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s ep a b. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_obj epptr (Endpoint ep) s; (a, b) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 3. \<And>s ep a b pl pl'. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_obj epptr (Endpoint ep) s; (a, b) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> blocked_on epptr (BlockedOnSend epptr pl) \<and> blocked_on epptr (BlockedOnReceive epptr pl') proof (prove)
goal:
No subgoals!