theory Ipc_R

lemma completeSignal_corres:
  "corres dc (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs
             \<comment> \<open>and obj_at (\<lambda>ko. ko = Notification ntfn \<and> Ipc_A.isActive ntfn) ntfnptr*\<close> )
             (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' isActive ntfnptr)
             (complete_signal ntfnptr tcb) (completeSignal ntfnptr tcb)" apply (simp add: complete_signal_def completeSignal_def) apply (rule corres_guard_imp) apply (rule_tac R'="\<lambda>ntfn. ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace'
                         and valid_ntfn' ntfn and (\<lambda>_. isActive ntfn)"
                                in corres_split[OF getNotification_corres]) apply (rule corres_gen_asm2) apply (case_tac "ntfn_obj rv") apply (clarsimp simp: ntfn_relation_def isActive_def
                       split: ntfn.splits Structures_H.notification.splits)+ apply (rule corres_guard2_imp) apply (simp add: badgeRegister_def badge_register_def) apply (rule corres_split[OF asUser_setRegister_corres setNotification_corres]) apply (clarsimp simp: ntfn_relation_def) apply (wp set_simple_ko_valid_objs get_simple_ko_wp getNotification_wp | clarsimp simp: valid_ntfn'_def)+ apply (clarsimp simp: valid_pspace'_def) apply (frule_tac P="(\<lambda>k. k = ntfn)" in obj_at_valid_objs', assumption) apply (clarsimp simp: projectKOs valid_obj'_def valid_ntfn'_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) (complete_signal ntfnptr tcb) (completeSignal ntfnptr tcb) proof (prove)
goal (1 subgoal):
 1. corres dc (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) (do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn
od | _ \<Rightarrow> fail
od) (do ntfn <- getNotification ntfnptr;
case ntfnObj ntfn of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | _ \<Rightarrow> haskell_fail []
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn
od | _ \<Rightarrow> fail
od) (do ntfn <- getNotification ntfnptr;
case ntfnObj ntfn of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | _ \<Rightarrow> haskell_fail []
od)
 2. \<And>s. (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) s \<Longrightarrow> ?Q s
 3. \<And>s. (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. ntfn_relation rv rv' \<Longrightarrow> corres dc (?R4 rv) (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' rv' and (\<lambda>_. EndpointDecls_H.isActive rv')) (case ntfn_obj rv of Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od | _ \<Rightarrow> fail) (case ntfnObj rv' of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | _ \<Rightarrow> haskell_fail [])
 2. \<lbrace>?Q4\<rbrace> get_notification ntfnptr \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' ntfn and (\<lambda>_. EndpointDecls_H.isActive ntfn)\<rbrace>
 4. \<And>s. (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q4) s
 5. \<And>s. (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>ntfn_relation rv rv'; EndpointDecls_H.isActive rv'\<rbrakk> \<Longrightarrow> corres dc (?R4 rv) (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od | _ \<Rightarrow> fail) (case ntfnObj rv' of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | _ \<Rightarrow> haskell_fail [])
 2. \<lbrace>?Q4\<rbrace> get_notification ntfnptr \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' ntfn and (\<lambda>_. EndpointDecls_H.isActive ntfn)\<rbrace>
 4. \<And>s. (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q4) s
 5. \<And>s. (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. \<lbrakk>ntfn_relation rv rv'; EndpointDecls_H.isActive rv'; ntfn_obj rv = Structures_A.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> corres dc (?R4 rv) (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od | _ \<Rightarrow> fail) (case ntfnObj rv' of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | _ \<Rightarrow> haskell_fail [])
 2. \<And>rv rv' x2. \<lbrakk>ntfn_relation rv rv'; EndpointDecls_H.isActive rv'; ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (?R4 rv) (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od | _ \<Rightarrow> fail) (case ntfnObj rv' of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | _ \<Rightarrow> haskell_fail [])
 3. \<And>rv rv' x3. \<lbrakk>ntfn_relation rv rv'; EndpointDecls_H.isActive rv'; ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (?R4 rv) (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od | _ \<Rightarrow> fail) (case ntfnObj rv' of Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser tcb $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | _ \<Rightarrow> haskell_fail [])
 4. \<lbrace>?Q4\<rbrace> get_notification ntfnptr \<lbrace>?R4\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' ntfn and (\<lambda>_. EndpointDecls_H.isActive ntfn)\<rbrace>
 6. \<And>s. (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q4) s
 7. \<And>s. (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv x3. ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3 \<Longrightarrow> corres dc (?R4 rv) (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' (NTFN (Structures_H.ntfn.ActiveNtfn x3) (ntfn_bound_tcb rv))) (do y <- as_user tcb (setRegister badge_register x3);
set_notification ntfnptr (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn)
od) (do y <- asUser tcb (setRegister Notification_H.badgeRegister x3);
setNotification ntfnptr (NTFN Structures_H.ntfn.IdleNtfn (ntfn_bound_tcb rv))
od)
 2. \<lbrace>?Q4\<rbrace> get_notification ntfnptr \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' ntfn and (\<lambda>_. EndpointDecls_H.isActive ntfn)\<rbrace>
 4. \<And>s. (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q4) s
 5. \<And>s. (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>rv x3. ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3 \<Longrightarrow> corres dc (?R4 rv) (?Q'47 rv x3) (do y <- as_user tcb (setRegister badge_register x3);
set_notification ntfnptr (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn)
od) (do y <- asUser tcb (setRegister Notification_H.badgeRegister x3);
setNotification ntfnptr (NTFN Structures_H.ntfn.IdleNtfn (ntfn_bound_tcb rv))
od)
 2. \<And>rv x3 s. \<lbrakk>ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' (NTFN (Structures_H.ntfn.ActiveNtfn x3) (ntfn_bound_tcb rv))) s\<rbrakk> \<Longrightarrow> ?Q'47 rv x3 s
 3. \<lbrace>?Q4\<rbrace> get_notification ntfnptr \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' ntfn and (\<lambda>_. EndpointDecls_H.isActive ntfn)\<rbrace>
 5. \<And>s. (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q4) s
 6. \<And>s. (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>rv x3. ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3 \<Longrightarrow> corres dc (?R4 rv) (?Q'47 rv x3) (do y <- as_user tcb (setRegister ARM.badgeRegister x3);
set_notification ntfnptr (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn)
od) (do y <- asUser tcb (setRegister ARM.badgeRegister x3);
setNotification ntfnptr (NTFN Structures_H.ntfn.IdleNtfn (ntfn_bound_tcb rv))
od)
 2. \<And>rv x3 s. \<lbrakk>ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' (NTFN (Structures_H.ntfn.ActiveNtfn x3) (ntfn_bound_tcb rv))) s\<rbrakk> \<Longrightarrow> ?Q'47 rv x3 s
 3. \<lbrace>?Q4\<rbrace> get_notification ntfnptr \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' ntfn and (\<lambda>_. EndpointDecls_H.isActive ntfn)\<rbrace>
 5. \<And>s. (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q4) s
 6. \<And>s. (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>rv x3 y ya. \<lbrakk>ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; dc y ya\<rbrakk> \<Longrightarrow> ntfn_relation (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn) (NTFN Structures_H.ntfn.IdleNtfn (ntfn_bound_tcb rv))
 2. \<And>rv x3. ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3 \<Longrightarrow> \<lbrace>?Q60 rv\<rbrace> as_user tcb (setRegister ARM.badgeRegister x3) \<lbrace>\<lambda>y. ntfn_at ntfnptr\<rbrace>
 3. \<And>rv x3. ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3 \<Longrightarrow> \<lbrace>?Q'50 rv x3\<rbrace> asUser tcb (setRegister ARM.badgeRegister x3) \<lbrace>\<lambda>y. ntfn_at' ntfnptr\<rbrace>
 4. \<And>rv x3 s. \<lbrakk>ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' (NTFN (Structures_H.ntfn.ActiveNtfn x3) (ntfn_bound_tcb rv))) s\<rbrakk> \<Longrightarrow> (tcb_at' tcb and ?Q'50 rv x3) s
 5. \<lbrace>?Q4\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>rv. tcb_at tcb and ?Q60 rv\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' ntfn and (\<lambda>_. EndpointDecls_H.isActive ntfn)\<rbrace>
 7. \<And>s. (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q4) s
 8. \<And>s. (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv x3. ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3 \<Longrightarrow> \<lbrace>?Q60 rv\<rbrace> as_user tcb (setRegister ARM.badgeRegister x3) \<lbrace>\<lambda>y. ntfn_at ntfnptr\<rbrace>
 2. \<And>rv x3. ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3 \<Longrightarrow> \<lbrace>?Q'50 rv x3\<rbrace> asUser tcb (setRegister ARM.badgeRegister x3) \<lbrace>\<lambda>y. ntfn_at' ntfnptr\<rbrace>
 3. \<And>rv x3 s. \<lbrakk>ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' (NTFN (Structures_H.ntfn.ActiveNtfn x3) (ntfn_bound_tcb rv))) s\<rbrakk> \<Longrightarrow> (tcb_at' tcb and ?Q'50 rv x3) s
 4. \<lbrace>?Q4\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>rv. tcb_at tcb and ?Q60 rv\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and valid_ntfn' ntfn and (\<lambda>_. EndpointDecls_H.isActive ntfn)\<rbrace>
 6. \<And>s. (ntfn_at ntfnptr and tcb_at tcb and pspace_aligned and valid_objs) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q4) s
 7. \<And>s. (ntfn_at' ntfnptr and tcb_at' tcb and valid_pspace' and obj_at' EndpointDecls_H.isActive ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'4) s proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>ntfn_at' ntfnptr s; tcb_at' tcb s; valid_pspace' s; obj_at' EndpointDecls_H.isActive ntfnptr s; ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts \<and> (case ntfnBoundTCB ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> EndpointDecls_H.isActive ntfn proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>ntfn_at' ntfnptr s; tcb_at' tcb s; obj_at' EndpointDecls_H.isActive ntfnptr s; ko_at' ntfn ntfnptr s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s\<rbrakk> \<Longrightarrow> (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts \<and> (case ntfnBoundTCB ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> EndpointDecls_H.isActive ntfn proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>ntfn_at' ntfnptr s; tcb_at' tcb s; obj_at' EndpointDecls_H.isActive ntfnptr s; ko_at' ntfn ntfnptr s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; \<exists>k. k = ntfn \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s)\<rbrakk> \<Longrightarrow> (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts \<and> (case ntfnBoundTCB ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> EndpointDecls_H.isActive ntfn proof (prove)
goal:
No subgoals!