theory Finalise_AC

lemma unbind_notification_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and
    bound_tcb_at (\<lambda>a. case a of None \<Rightarrow> True | Some ntfn \<Rightarrow> aag_has_auth_to aag Reset ntfn) t\<rbrace>
   unbind_notification t
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (clarsimp simp: unbind_notification_def) apply (rule hoare_seq_ext[OF _ gbn_sp]) apply (wp set_ntfn_respects hoare_vcg_ex_lift gbn_wp | wpc | simp)+ apply (clarsimp simp: pred_tcb_at_def obj_at_def split: option.splits) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and bound_tcb_at (\<lambda>a. case a of None \<Rightarrow> True | Some ntfn \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag) t\<rbrace> unbind_notification t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and bound_tcb_at (\<lambda>a. case a of None \<Rightarrow> True | Some ntfn \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag) t\<rbrace> do ntfnptr <- get_bound_notification t;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
y <- set_notification ntfnptr' (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr. \<lbrace>bound_tcb_at ((=) ntfnptr) t and (integrity aag X st and pas_refined aag and bound_tcb_at (\<lambda>a. case a of None \<Rightarrow> True | Some ntfn \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag) t)\<rbrace> case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
y <- set_notification ntfnptr' (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr s. bound_tcb_at ((=) ntfnptr) t s \<and> integrity aag X st s \<and> pas_refined aag s \<and> bound_tcb_at (case_option True (\<lambda>ntfn. (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag)) t s \<Longrightarrow> \<forall>x. ntfnptr = Some x \<longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset)) \<and> (\<exists>x. bound_tcb_at (\<lambda>a. a = Some x) t s \<and> (pasSubject aag, Reset, pasObjectAbs aag x) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb tcba x. \<lbrakk>integrity aag X st s; pas_refined aag s; kheap s t = Some (TCB tcb); (\<exists>y. tcb_bound_notification tcba = Some y) \<or> tcb = tcba; \<forall>x2. tcb_bound_notification tcba = Some x2 \<longrightarrow> tcb = tcba \<and> (pasSubject aag, Reset, pasObjectAbs aag x2) \<in> pasPolicy aag; tcb_bound_notification tcb = Some x\<rbrakk> \<Longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset)) \<and> (pasSubject aag, Reset, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!