theory Finalise_R

lemma fast_finaliseCap_corres:
  "\<lbrakk> final_matters' cap' \<longrightarrow> final = final'; cap_relation cap cap';
     can_fast_finalise cap \<rbrakk>
   \<Longrightarrow> corres dc
           (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap
                       \<and> cte_wp_at ((=) cap) sl s)
           (\<lambda>s. invs' s \<and> s \<turnstile>' cap')
           (fast_finalise cap final)
           (do
               p \<leftarrow> finaliseCap cap' final' True;
               assert (capRemovable (fst p) (cte_map ptr) \<and> snd p = NullCap)
            od)" apply (cases cap, simp_all add: finaliseCap_def isCap_simps
                                  corres_liftM2_simp[unfolded liftM_def]
                                  o_def dc_def[symmetric] when_def
                                  can_fast_finalise_def capRemovable_def
                       split del: if_split cong: if_cong) apply (clarsimp simp: final_matters'_def) apply (rule corres_guard_imp) apply (rule corres_rel_imp) apply (rule ep_cancel_corres) apply simp apply (simp add: valid_cap_def) apply (simp add: valid_cap'_def) apply (clarsimp simp: final_matters'_def) apply (rule corres_guard_imp) apply (rule corres_split[OF unbindMaybeNotification_corres]) apply (rule cancelAllSignals_corres) apply (wp abs_typ_at_lifts unbind_maybe_notification_invs typ_at_lifts hoare_drop_imps getNotification_wp
            | wpc)+ apply (clarsimp simp: valid_cap_def) apply (clarsimp simp: valid_cap'_def projectKOs valid_obj'_def
                 dest!: invs_valid_objs' obj_at_valid_objs' ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>final_matters' cap' \<longrightarrow> final = final'; cap_relation cap cap'; can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap \<and> cte_wp_at ((=) cap) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s) (fast_finalise cap final) (do p <- global.finaliseCap cap' final' True;
assert (capRemovable (fst p) (cte_map ptr) \<and> snd p = capability.NullCap)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>final_matters' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) \<longrightarrow> final = final'; cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> cte_wp_at ((=) (cap.EndpointCap x31 x32 x33)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) s) (if final then cancel_all_ipc x31 else return ()) (if final' then cancelAllIPC x31 else return ())
 2. \<And>x41 x42 x43. \<lbrakk>final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final = final'; cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s) (if final then do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od else return ()) (if final' then do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od else return ()) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> cte_wp_at ((=) (cap.EndpointCap x31 x32 x33)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) s) (cancel_all_ipc x31) (cancelAllIPC x31)
 2. \<And>x41 x42 x43. \<lbrakk>final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final = final'; cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s) (if final then do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od else return ()) (if final' then do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od else return ()) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'\<rbrakk> \<Longrightarrow> corres dc (?Q42 x31 x32 x33) (?Q'42 x31 x32 x33) (cancel_all_ipc x31) (cancelAllIPC x31)
 2. \<And>x31 x32 x33 s. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; invs s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> cte_wp_at ((=) (cap.EndpointCap x31 x32 x33)) sl s\<rbrakk> \<Longrightarrow> ?Q42 x31 x32 x33 s
 3. \<And>x31 x32 x33 s. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; invs' s \<and> valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) s\<rbrakk> \<Longrightarrow> ?Q'42 x31 x32 x33 s
 4. \<And>x41 x42 x43. \<lbrakk>final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final = final'; cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s) (if final then do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od else return ()) (if final' then do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od else return ()) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'\<rbrakk> \<Longrightarrow> corres (?r'46 x31 x32 x33) (?Q42 x31 x32 x33) (?Q'42 x31 x32 x33) (cancel_all_ipc x31) (cancelAllIPC x31)
 2. \<And>x31 x32 x33 x y. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; ?r'46 x31 x32 x33 x y\<rbrakk> \<Longrightarrow> dc x y
 3. \<And>x31 x32 x33 s. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; invs s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> cte_wp_at ((=) (cap.EndpointCap x31 x32 x33)) sl s\<rbrakk> \<Longrightarrow> ?Q42 x31 x32 x33 s
 4. \<And>x31 x32 x33 s. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; invs' s \<and> valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) s\<rbrakk> \<Longrightarrow> ?Q'42 x31 x32 x33 s
 5. \<And>x41 x42 x43. \<lbrakk>final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final = final'; cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s) (if final then do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od else return ()) (if final' then do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od else return ()) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x y. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; dc x y\<rbrakk> \<Longrightarrow> dc x y
 2. \<And>x31 x32 x33 s. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; invs s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> cte_wp_at ((=) (cap.EndpointCap x31 x32 x33)) sl s\<rbrakk> \<Longrightarrow> (invs and valid_sched and ep_at x31) s
 3. \<And>x31 x32 x33 s. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; invs' s \<and> valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) s\<rbrakk> \<Longrightarrow> (invs' and ep_at' x31) s
 4. \<And>x41 x42 x43. \<lbrakk>final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final = final'; cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s) (if final then do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od else return ()) (if final' then do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od else return ()) proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 s. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; invs s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> cte_wp_at ((=) (cap.EndpointCap x31 x32 x33)) sl s\<rbrakk> \<Longrightarrow> (invs and valid_sched and ep_at x31) s
 2. \<And>x31 x32 x33 s. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; invs' s \<and> valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) s\<rbrakk> \<Longrightarrow> (invs' and ep_at' x31) s
 3. \<And>x41 x42 x43. \<lbrakk>final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final = final'; cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s) (if final then do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od else return ()) (if final' then do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od else return ()) proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 s. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33; final; final'; invs' s \<and> valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) s\<rbrakk> \<Longrightarrow> (invs' and ep_at' x31) s
 2. \<And>x41 x42 x43. \<lbrakk>final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final = final'; cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s) (if final then do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od else return ()) (if final' then do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od else return ()) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43. \<lbrakk>final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final = final'; cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s) (if final then do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od else return ()) (if final' then do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od else return ()) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s) (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od) (do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od) proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'\<rbrakk> \<Longrightarrow> corres dc (?Q57 x41 x42 x43) (?Q'57 x41 x42 x43) (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od) (do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od)
 2. \<And>x41 x42 x43 s. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s\<rbrakk> \<Longrightarrow> ?Q57 x41 x42 x43 s
 3. \<And>x41 x42 x43 s. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s\<rbrakk> \<Longrightarrow> ?Q'57 x41 x42 x43 s proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 y ya. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R61 x41 x42 x43 y) (?R'61 x41 x42 x43 ya) (cancel_all_signals x41) (cancelAllSignals x41)
 2. \<And>x41 x42 x43. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q61 x41 x42 x43\<rbrace> unbind_maybe_notification x41 \<lbrace>?R61 x41 x42 x43\<rbrace>
 3. \<And>x41 x42 x43. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'61 x41 x42 x43\<rbrace> unbindMaybeNotification x41 \<lbrace>?R'61 x41 x42 x43\<rbrace>
 4. \<And>x41 x42 x43 s. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s\<rbrakk> \<Longrightarrow> (invs and ntfn_at x41 and ?Q61 x41 x42 x43) s
 5. \<And>x41 x42 x43 s. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s\<rbrakk> \<Longrightarrow> (invs' and ntfn_at' x41 and ?Q'61 x41 x42 x43) s proof (prove)
goal (4 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q61 x41 x42 x43\<rbrace> unbind_maybe_notification x41 \<lbrace>\<lambda>y. invs and valid_sched and ntfn_at x41\<rbrace>
 2. \<And>x41 x42 x43. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'61 x41 x42 x43\<rbrace> unbindMaybeNotification x41 \<lbrace>\<lambda>ya. invs' and ntfn_at' x41\<rbrace>
 3. \<And>x41 x42 x43 s. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s\<rbrakk> \<Longrightarrow> (invs and ntfn_at x41 and ?Q61 x41 x42 x43) s
 4. \<And>x41 x42 x43 s. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s\<rbrakk> \<Longrightarrow> (invs' and ntfn_at' x41 and ?Q'61 x41 x42 x43) s proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 s. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; invs s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s\<rbrakk> \<Longrightarrow> (invs and ntfn_at x41 and (\<lambda>s. invs s \<and> valid_sched s \<and> ntfn_at x41 s)) s
 2. \<And>x41 x42 x43 s. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s\<rbrakk> \<Longrightarrow> (invs' and ntfn_at' x41 and (\<lambda>s. invs' s \<and> ntfn_at' x41 s)) s proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 s. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43; final; final'; invs' s \<and> valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s\<rbrakk> \<Longrightarrow> (invs' and ntfn_at' x41 and (\<lambda>s. invs' s \<and> ntfn_at' x41 s)) s proof (prove)
goal:
No subgoals!