theory Finalise_AC

lemma sbn_unbind_respects[wp]:
  "\<lbrace>integrity aag X st and
    (\<lambda>s. (\<exists>ntfn. bound_tcb_at (\<lambda>a. a = Some ntfn) t s \<and> aag_has_auth_to aag Reset ntfn))\<rbrace>
   set_bound_notification t None
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: set_bound_notification_def) apply (wpsimp wp: set_object_wp) apply (erule integrity_trans) apply (clarsimp simp: integrity_def obj_at_def pred_tcb_at_def integrity_asids_kh_upds) apply (rule tro_tcb_unbind) apply (fastforce dest!: get_tcb_SomeD) apply (fastforce dest!: get_tcb_SomeD) apply simp apply (simp add: tcb_bound_notification_reset_integrity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. \<exists>ntfn. bound_tcb_at (\<lambda>a. a = Some ntfn) t s \<and> (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag)\<rbrace> set_bound_notification t None \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>s. \<exists>ntfn. bound_tcb_at (\<lambda>a. a = Some ntfn) t s \<and> (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := None\<rparr>))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn y. \<lbrakk>integrity aag X st s; bound_tcb_at (\<lambda>a. a = Some ntfn) t s; (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_bound_notification := None\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn y. \<lbrakk>bound_tcb_at (\<lambda>a. a = Some ntfn) t s; (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_bound_notification := None\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag t) (Some (TCB tcb)) (Some (TCB (y\<lparr>tcb_bound_notification := None\<rparr>))) proof (prove)
goal (4 subgoals):
 1. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> Some (TCB tcb) = Some (TCB (?tcb25 s ntfn y tcb))
 2. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> Some (TCB (y\<lparr>tcb_bound_notification := None\<rparr>)) = Some (TCB (?tcb'25 s ntfn y tcb))
 3. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> ?tcb'25 s ntfn y tcb = ?tcb25 s ntfn y tcb\<lparr>tcb_bound_notification := None\<rparr>
 4. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Reset (the (tcb_bound_notification (?tcb25 s ntfn y tcb))) proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> Some (TCB (y\<lparr>tcb_bound_notification := None\<rparr>)) = Some (TCB (?tcb'25 s ntfn y tcb))
 2. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> ?tcb'25 s ntfn y tcb = tcb\<lparr>tcb_bound_notification := None\<rparr>
 3. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Reset (the (tcb_bound_notification tcb)) proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> tcb\<lparr>tcb_bound_notification := None\<rparr> = tcb\<lparr>tcb_bound_notification := None\<rparr>
 2. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Reset (the (tcb_bound_notification tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn y tcb. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag; get_tcb t s = Some y; kheap s t = Some (TCB tcb); tcb_bound_notification tcb = Some ntfn\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to {pasSubject aag} aag Reset (the (tcb_bound_notification tcb)) proof (prove)
goal:
No subgoals!