theory Finalise_AC

lemma unbind_maybe_notification_respects:
  "\<lbrace>integrity aag X st and invs and pas_refined aag and
    obj_at (\<lambda>ko. \<exists>ntfn. ko = (Notification ntfn) \<and>
                        (case (ntfn_bound_tcb ntfn) of None \<Rightarrow> True
                                                     | Some t \<Rightarrow> aag_has_auth_to aag Reset a)) a\<rbrace>
   unbind_maybe_notification a
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (clarsimp simp: unbind_maybe_notification_def) apply (rule hoare_pre) apply (wp set_ntfn_respects get_simple_ko_wp hoare_vcg_ex_lift gbn_wp | wpc | simp)+ apply clarsimp apply (frule_tac P="\<lambda>ntfn. ntfn = Some a"
                in ntfn_bound_tcb_at[OF invs_sym_refs invs_valid_objs], (simp add: obj_at_def)+) apply (auto simp: pred_tcb_at_def obj_at_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and invs and pas_refined aag and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some t \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag a) \<in> pasPolicy aag)) a\<rbrace> unbind_maybe_notification a \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and invs and pas_refined aag and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some t \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag a) \<in> pasPolicy aag)) a\<rbrace> do ntfn <- get_notification a;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do ntfn <- get_notification a;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. (integrity aag X st and invs and pas_refined aag and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some t \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag a) \<in> pasPolicy aag)) a) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st s \<and> invs s \<and> pas_refined aag s \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some t \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag a) \<in> pasPolicy aag)) a s \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) a s \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset)) \<and> (\<exists>xa. bound_tcb_at (\<lambda>a. a = Some xa) x s \<and> (pasSubject aag, Reset, pasObjectAbs aag xa) \<in> pasPolicy aag)) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>integrity aag X st s; invs s; pas_refined aag s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some t \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag a) \<in> pasPolicy aag)) a s; ko_at (Notification ntfn) a s; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset)) \<and> (\<exists>xa. bound_tcb_at (\<lambda>a. a = Some xa) x s \<and> (pasSubject aag, Reset, pasObjectAbs aag xa) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>integrity aag X st s; invs s; pas_refined aag s; (pasSubject aag, Reset, pasObjectAbs aag a) \<in> pasPolicy aag; kheap s a = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; bound_tcb_at (\<lambda>ntfn. ntfn = Some a) x s\<rbrakk> \<Longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset)) \<and> (\<exists>xa. bound_tcb_at (\<lambda>a. a = Some xa) x s \<and> (pasSubject aag, Reset, pasObjectAbs aag xa) \<in> pasPolicy aag) proof (prove)
goal:
No subgoals!