theory Finalise_AC

lemma cancel_all_signals_respects[wp]:
  "\<lbrace>integrity aag X st and valid_objs and (sym_refs \<circ> state_refs_of)
                       and K (aag_has_auth_to aag Reset epptr)\<rbrace>
   cancel_all_signals epptr
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp add: cancel_all_signals_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp], rule hoare_pre) 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_ntfn_respects
          | wpc | clarsimp | blast)+ apply (frule sym_refs_ko_atD, clarsimp+) apply (rule obj_at_valid_objsE, assumption, assumption) apply (clarsimp simp: valid_obj_def valid_ntfn_def st_tcb_at_refs_of_rev st_tcb_def2
                 split: option.splits) apply fastforce+ 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 ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)\<rbrace> cancel_all_signals 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> cancel_all_signals 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 ntfn <- get_notification epptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification epptr $ 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q6 ntfn\<rbrace> case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification epptr $ 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 () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ntfn s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (ko_at (Notification ntfn) epptr and (integrity aag X st and valid_objs and sym_refs \<circ> state_refs_of)) s\<rbrakk> \<Longrightarrow> ?Q6 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Notification ntfn) epptr s; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<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>ntfn s x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Notification ntfn) epptr s; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn x; state_refs_of s epptr = set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); \<forall>x\<in>set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<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>ntfn s x ko. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Notification ntfn) epptr s; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn x; state_refs_of s epptr = set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); \<forall>x\<in>set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of ko) x s; kheap s epptr = Some ko; Notification ntfn = ko; valid_obj epptr ko s\<rbrakk> \<Longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<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>ntfn s x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Notification ntfn) epptr s; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn x; state_refs_of s epptr = set x \<times> {NTFNSignal}; \<forall>x\<in>set x. \<exists>tcb. get_tcb x s = Some tcb \<and> tcb_state tcb = BlockedOnNotification epptr; kheap s epptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = None; x \<noteq> []; \<forall>t\<in>set x. tcb_at t s; distinct x\<rbrakk> \<Longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset)) \<and> (\<forall>x\<in>set x. \<exists>tcb. get_tcb x s = Some tcb \<and> blocked_on epptr (tcb_state tcb))
 2. \<And>ntfn s x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Notification ntfn) epptr s; integrity aag X st s; valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn [x2]; state_refs_of s epptr = {(x2, NTFNBound), (x2, NTFNSignal)}; obj_at (\<lambda>ko. (epptr, TCBBound) \<in> refs_of ko) x2 s \<and> (\<exists>tcb. get_tcb x2 s = Some tcb \<and> tcb_state tcb = BlockedOnNotification epptr); kheap s epptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x2; tcb_at x2 s\<rbrakk> \<Longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset)) \<and> (\<exists>tcb. get_tcb x2 s = Some tcb \<and> blocked_on epptr (tcb_state tcb)) proof (prove)
goal:
No subgoals!