theory Finalise_R

lemma finaliseCap_corres:
  "\<lbrakk> final_matters' cap' \<Longrightarrow> final = final'; cap_relation cap cap';
          flag \<longrightarrow> can_fast_finalise cap \<rbrakk>
     \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y))
           (\<lambda>s. einvs s \<and> s \<turnstile> cap \<and> (final_matters cap \<longrightarrow> final = is_final_cap' cap s)
                       \<and> cte_wp_at ((=) cap) sl s)
           (\<lambda>s. invs' s \<and> s \<turnstile>' cap' \<and>
                 (final_matters' cap' \<longrightarrow>
                      final' = isFinal cap' (cte_map sl) (cteCaps_of s)))
           (finalise_cap cap final) (finaliseCap cap' final' flag)" 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
                       split del: if_split cong: if_cong) apply (clarsimp simp: final_matters'_def) apply (rule corres_guard_imp) apply (rule ep_cancel_corres) apply (simp add: valid_cap_def) apply (simp add: valid_cap'_def) apply (clarsimp simp add: 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 hoare_vcg_all_lift | wpc)+ apply (clarsimp simp: valid_cap_def) apply (clarsimp simp: valid_cap'_def) apply (fastforce simp: final_matters'_def shiftL_nat zbits_map_def) apply (clarsimp simp add: final_matters'_def getThreadCSpaceRoot
                               liftM_def[symmetric] o_def zbits_map_def
                               dc_def[symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[OF unbindNotification_corres]) apply (rule corres_split[OF suspend_corres]) apply (clarsimp simp: liftM_def[symmetric] o_def dc_def[symmetric] zbits_map_def) apply (rule prepareThreadDelete_corres) apply (wp unbind_notification_invs unbind_notification_simple_sched_action)+ apply (simp add: valid_cap_def) apply (simp add: valid_cap'_def) apply (simp add: final_matters'_def liftM_def[symmetric]
                     o_def dc_def[symmetric]) apply (intro impI, rule corres_guard_imp) apply (rule deletingIRQHandler_corres) apply simp apply simp apply (clarsimp simp: final_matters'_def) apply (rule_tac F="False" in corres_req) apply clarsimp apply (frule zombies_finalD, (clarsimp simp: is_cap_simps)+) apply (clarsimp simp: cte_wp_at_caps_of_state) apply simp apply (clarsimp split del: if_split simp: o_def) apply (rule corres_guard_imp [OF arch_finaliseCap_corres], (fastforce simp: valid_sched_def)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; cap_relation cap cap'; flag \<longrightarrow> can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. einvs s \<and> s \<turnstile> cap \<and> (final_matters cap \<longrightarrow> final = is_final_cap' cap s) \<and> cte_wp_at ((=) cap) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (finalise_cap cap final) (global.finaliseCap cap' final' flag) proof (prove)
goal (7 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> final = is_final_cap' (cap.EndpointCap x31 x32 x33) s \<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 \<and> (final_matters' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) \<longrightarrow> final' = isFinal (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) (cte_map sl) (cteCaps_of 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> final = is_final_cap' (cap.NotificationCap x41 x42 x43) s \<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 \<and> (final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final' = isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of 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 ())
 3. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 4. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 5. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 6. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 7. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (7 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> is_final_cap' (cap.EndpointCap x31 x32 x33) s \<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 \<and> isFinal (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) (cte_map sl) (cteCaps_of 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> final = is_final_cap' (cap.NotificationCap x41 x42 x43) s \<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 \<and> (final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final' = isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of 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 ())
 3. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 4. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 5. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 6. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 7. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (9 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 (?Q41 x31 x32 x33) (?Q'41 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> is_final_cap' (cap.EndpointCap x31 x32 x33) s \<and> cte_wp_at ((=) (cap.EndpointCap x31 x32 x33)) sl s\<rbrakk> \<Longrightarrow> ?Q41 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 \<and> isFinal (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> ?Q'41 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> final = is_final_cap' (cap.NotificationCap x41 x42 x43) s \<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 \<and> (final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final' = isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of 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 ())
 5. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 6. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 7. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 8. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 9. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (8 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.EndpointCap x31 x32 x33 \<and> is_final_cap' (cap.EndpointCap x31 x32 x33) s \<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 \<and> isFinal (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) (cte_map sl) (cteCaps_of 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> final = is_final_cap' (cap.NotificationCap x41 x42 x43) s \<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 \<and> (final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final' = isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of 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 ())
 4. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 5. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 6. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 7. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 8. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (7 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 \<and> isFinal (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) (cte_map sl) (cteCaps_of 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> final = is_final_cap' (cap.NotificationCap x41 x42 x43) s \<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 \<and> (final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final' = isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of 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 ())
 3. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 4. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 5. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 6. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 7. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (6 subgoals):
 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> final = is_final_cap' (cap.NotificationCap x41 x42 x43) s \<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 \<and> (final_matters' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) \<longrightarrow> final' = isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of 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 ())
 2. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 3. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 4. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 5. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 6. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (6 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 (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> is_final_cap' (cap.NotificationCap x41 x42 x43) s \<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 \<and> isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of s)) (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od) (do y <- unbindMaybeNotification x41;
cancelAllSignals x41
od)
 2. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 3. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 4. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 5. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 6. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (8 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 (?Q55 x41 x42 x43) (?Q'55 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> is_final_cap' (cap.NotificationCap x41 x42 x43) s \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s\<rbrakk> \<Longrightarrow> ?Q55 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 \<and> isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> ?Q'55 x41 x42 x43 s
 4. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 5. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 6. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 7. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 8. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (10 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 (?R59 x41 x42 x43 y) (?R'59 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>?Q59 x41 x42 x43\<rbrace> unbind_maybe_notification x41 \<lbrace>?R59 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'59 x41 x42 x43\<rbrace> unbindMaybeNotification x41 \<lbrace>?R'59 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> is_final_cap' (cap.NotificationCap x41 x42 x43) s \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s\<rbrakk> \<Longrightarrow> (invs and ntfn_at x41 and ?Q59 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 \<and> isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and ntfn_at' x41 and ?Q'59 x41 x42 x43) s
 6. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 7. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 8. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 9. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 10. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (9 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>?Q59 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'59 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> is_final_cap' (cap.NotificationCap x41 x42 x43) s \<and> cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) sl s\<rbrakk> \<Longrightarrow> (invs and ntfn_at x41 and ?Q59 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 \<and> isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and ntfn_at' x41 and ?Q'59 x41 x42 x43) s
 5. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 6. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 7. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 8. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 9. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (7 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_list s \<and> valid_sched s \<and> s \<turnstile> cap.NotificationCap x41 x42 x43 \<and> is_final_cap' (cap.NotificationCap x41 x42 x43) s \<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 \<and> isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and ntfn_at' x41 and (\<lambda>s. invs' s \<and> ntfn_at' x41 s)) s
 3. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 4. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 5. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 6. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 7. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (6 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_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) s \<and> isFinal (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43)) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and ntfn_at' x41 and (\<lambda>s. invs' s \<and> ntfn_at' x41 s)) s
 2. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 3. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 4. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 5. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 6. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (5 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<Longrightarrow> final = final'; cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); \<not> flag; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.CNodeCap x61 x62 x63 \<and> final = is_final_cap' (cap.CNodeCap x61 x62 x63) s \<and> cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) s \<and> (final_matters' (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) \<longrightarrow> final' = isFinal (capability.CNodeCap x61 x62 (of_bl x63) (length x63)) (cte_map sl) (cteCaps_of s))) (return (if final then cap.Zombie x61 (Some x62) (2 ^ x62) else cap.NullCap, cap.NullCap)) (if final' then return (capability.Zombie x61 (ZombieCNode x62) (shiftL (Suc 0) x62), capability.NullCap) else return (capability.NullCap, capability.NullCap))
 2. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 3. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 4. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 5. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (4 subgoals):
 1. \<And>x7. \<lbrakk>final_matters' (capability.ThreadCap x7) \<Longrightarrow> final = final'; cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> final = is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> (final_matters' (capability.ThreadCap x7) \<longrightarrow> final' = isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s))) (do y <- if final then unbind_notification x7 else return ();
y <- if final then IpcCancel_A.suspend x7 else return ();
y <- if final then prepare_thread_delete x7 else return ();
return (if final then cap.Zombie x7 None 5 else cap.NullCap, cap.NullCap)
od) (if final' then do cte_ptr <- getThreadCSpaceRoot x7;
y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
y <- Arch.prepareThreadDelete x7;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else return (capability.NullCap, capability.NullCap))
 2. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 3. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 4. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (4 subgoals):
 1. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s)) (do y <- unbind_notification x7;
y <- IpcCancel_A.suspend x7;
liftM (\<lambda>y. (cap.Zombie x7 None 5, cap.NullCap)) (prepare_thread_delete x7)
od) (do y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
liftM (\<lambda>y. (capability.Zombie x7 ZombieTCB 5, capability.NullCap)) (Arch.prepareThreadDelete x7)
od)
 2. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 3. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 4. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (6 subgoals):
 1. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (?Q99 x7) (?Q'99 x7) (do y <- unbind_notification x7;
y <- IpcCancel_A.suspend x7;
liftM (\<lambda>y. (cap.Zombie x7 None 5, cap.NullCap)) (prepare_thread_delete x7)
od) (do y <- unbindNotification x7;
y <- ThreadDecls_H.suspend x7;
liftM (\<lambda>y. (capability.Zombie x7 ZombieTCB 5, capability.NullCap)) (Arch.prepareThreadDelete x7)
od)
 2. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s\<rbrakk> \<Longrightarrow> ?Q99 x7 s
 3. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> ?Q'99 x7 s
 4. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 5. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 6. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (8 subgoals):
 1. \<And>x7 y ya. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; dc y ya\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (?R103 x7 y) (?R'103 x7 ya) (do y <- IpcCancel_A.suspend x7;
liftM (\<lambda>y. (cap.Zombie x7 None 5, cap.NullCap)) (prepare_thread_delete x7)
od) (do y <- ThreadDecls_H.suspend x7;
liftM (\<lambda>y. (capability.Zombie x7 ZombieTCB 5, capability.NullCap)) (Arch.prepareThreadDelete x7)
od)
 2. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 x7\<rbrace> unbind_notification x7 \<lbrace>?R103 x7\<rbrace>
 3. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 x7\<rbrace> unbindNotification x7 \<lbrace>?R'103 x7\<rbrace>
 4. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s\<rbrakk> \<Longrightarrow> (invs and tcb_at x7 and ?Q103 x7) s
 5. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x7 and ?Q'103 x7) s
 6. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 7. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 8. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (10 subgoals):
 1. \<And>x7 y ya yb yc. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (?R108 x7 y ya yb) (?R'108 x7 y ya yc) (liftM (\<lambda>y. (cap.Zombie x7 None 5, cap.NullCap)) (prepare_thread_delete x7)) (liftM (\<lambda>y. (capability.Zombie x7 ZombieTCB 5, capability.NullCap)) (Arch.prepareThreadDelete x7))
 2. \<And>x7 y ya. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 x7 y\<rbrace> IpcCancel_A.suspend x7 \<lbrace>?R108 x7 y ya\<rbrace>
 3. \<And>x7 y ya. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'113 x7 ya\<rbrace> ThreadDecls_H.suspend x7 \<lbrace>?R'108 x7 y ya\<rbrace>
 4. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 x7\<rbrace> unbind_notification x7 \<lbrace>\<lambda>y. einvs and tcb_at x7 and ?Q111 x7 y\<rbrace>
 5. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 x7\<rbrace> unbindNotification x7 \<lbrace>\<lambda>ya. invs' and tcb_at' x7 and ?Q'113 x7 ya\<rbrace>
 6. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s\<rbrakk> \<Longrightarrow> (invs and tcb_at x7 and ?Q103 x7) s
 7. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x7 and ?Q'103 x7) s
 8. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 9. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 10. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (10 subgoals):
 1. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> corres dc (?R108 x7 () () ()) (?R'108 x7 () () ()) (prepare_thread_delete x7) (Arch.prepareThreadDelete x7)
 2. \<And>x7 y ya. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 x7 y\<rbrace> IpcCancel_A.suspend x7 \<lbrace>?R108 x7 y ya\<rbrace>
 3. \<And>x7 y ya. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'113 x7 ya\<rbrace> ThreadDecls_H.suspend x7 \<lbrace>?R'108 x7 y ya\<rbrace>
 4. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 x7\<rbrace> unbind_notification x7 \<lbrace>\<lambda>y. einvs and tcb_at x7 and ?Q111 x7 y\<rbrace>
 5. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 x7\<rbrace> unbindNotification x7 \<lbrace>\<lambda>ya. invs' and tcb_at' x7 and ?Q'113 x7 ya\<rbrace>
 6. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s\<rbrakk> \<Longrightarrow> (invs and tcb_at x7 and ?Q103 x7) s
 7. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x7 and ?Q'103 x7) s
 8. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 9. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 10. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (9 subgoals):
 1. \<And>x7 y ya. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q111 x7 y\<rbrace> IpcCancel_A.suspend x7 \<lbrace>\<lambda>a. tcb_at x7\<rbrace>
 2. \<And>x7 y ya. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'113 x7 ya\<rbrace> ThreadDecls_H.suspend x7 \<lbrace>\<lambda>a. tcb_at' x7\<rbrace>
 3. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 x7\<rbrace> unbind_notification x7 \<lbrace>\<lambda>y. einvs and tcb_at x7 and ?Q111 x7 y\<rbrace>
 4. \<And>x7. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 x7\<rbrace> unbindNotification x7 \<lbrace>\<lambda>ya. invs' and tcb_at' x7 and ?Q'113 x7 ya\<rbrace>
 5. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s\<rbrakk> \<Longrightarrow> (invs and tcb_at x7 and ?Q103 x7) s
 6. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x7 and ?Q'103 x7) s
 7. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 8. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 9. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (5 subgoals):
 1. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ThreadCap x7 \<and> is_final_cap' (cap.ThreadCap x7) s \<and> cte_wp_at ((=) (cap.ThreadCap x7)) sl s\<rbrakk> \<Longrightarrow> (invs and tcb_at x7 and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at x7 s \<and> tcb_at x7 s)) s
 2. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x7 and (\<lambda>s. invs' s \<and> tcb_at' x7 s \<and> tcb_at' x7 s)) s
 3. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 4. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 5. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (4 subgoals):
 1. \<And>x7 s. \<lbrakk>cap' = capability.ThreadCap x7; \<not> flag; cap = cap.ThreadCap x7; final; final'; invs' s \<and> valid_cap' (capability.ThreadCap x7) s \<and> isFinal (capability.ThreadCap x7) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x7 and (\<lambda>s. invs' s \<and> tcb_at' x7 s \<and> tcb_at' x7 s)) s
 2. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 3. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 4. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (3 subgoals):
 1. \<And>x10. \<lbrakk>final_matters' (capability.IRQHandlerCap x10) \<Longrightarrow> final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> final = is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> (final_matters' (capability.IRQHandlerCap x10) \<longrightarrow> final' = isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s))) (if final then do y <- deleting_irq_handler x10;
return (cap.NullCap, cap.IRQHandlerCap x10)
od else return (cap.NullCap, cap.NullCap)) (if final' then do y <- deletingIRQHandler x10;
return (capability.NullCap, capability.IRQHandlerCap x10)
od else return (capability.NullCap, capability.NullCap))
 2. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 3. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (3 subgoals):
 1. \<And>x10. \<lbrakk>final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> final' \<longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s)) (deleting_irq_handler x10) (deletingIRQHandler x10)
 2. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 3. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (5 subgoals):
 1. \<And>x10. \<lbrakk>final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10; final'\<rbrakk> \<Longrightarrow> corres dc (?Q157 x10) (?Q'157 x10) (deleting_irq_handler x10) (deletingIRQHandler x10)
 2. \<And>x10 s. \<lbrakk>final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10; final'; invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s\<rbrakk> \<Longrightarrow> ?Q157 x10 s
 3. \<And>x10 s. \<lbrakk>final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10; final'; invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> ?Q'157 x10 s
 4. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 5. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (4 subgoals):
 1. \<And>x10 s. \<lbrakk>final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10; final'; invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.IRQHandlerCap x10 \<and> is_final_cap' (cap.IRQHandlerCap x10) s \<and> cte_wp_at ((=) (cap.IRQHandlerCap x10)) sl s\<rbrakk> \<Longrightarrow> einvs s
 2. \<And>x10 s. \<lbrakk>final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10; final'; invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> invs' s
 3. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 4. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (3 subgoals):
 1. \<And>x10 s. \<lbrakk>final = final'; cap' = capability.IRQHandlerCap x10; \<not> flag; cap = cap.IRQHandlerCap x10; final'; invs' s \<and> valid_cap' (capability.IRQHandlerCap x10) s \<and> isFinal (capability.IRQHandlerCap x10) (cte_map sl) (cteCaps_of s)\<rbrakk> \<Longrightarrow> invs' s
 2. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 3. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<Longrightarrow> final = final'; cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> final = is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> (final_matters' (capability.Zombie x111 (zbits_map x112) x113) \<longrightarrow> final' = isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s))) (do y <- assert final;
return (cap.Zombie x111 x112 x113, cap.NullCap)
od) (if final' then return (capability.Zombie x111 (zbits_map x112) x113, capability.NullCap) else fail)
 2. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113; \<not> final; \<not> final'\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> \<not> is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> \<not> isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s)) fail fail
 2. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (3 subgoals):
 1. \<And>x111 x112 x113 s s'. \<lbrakk>cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113; \<not> final; \<not> final'; (s, s') \<in> state_relation; invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> \<not> is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s; invs' s' \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s' \<and> \<not> isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s')\<rbrakk> \<Longrightarrow> False
 2. \<And>x111 x112 x113. \<lbrakk>cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113; \<not> final; \<not> final'; False\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> \<not> is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> \<not> isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s)) fail fail
 3. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (3 subgoals):
 1. \<And>x111 x112 x113 s s'. \<lbrakk>cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113; \<not> final; \<not> final'; (s, s') \<in> state_relation; invs s; invs' s'; valid_list s; valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s'; \<not> isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s'); valid_sched s; s \<turnstile> cap.Zombie x111 x112 x113; \<not> is_final_cap' (cap.Zombie x111 x112 x113) s; cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s\<rbrakk> \<Longrightarrow> False
 2. \<And>x111 x112 x113. \<lbrakk>cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113; \<not> final; \<not> final'; False\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> \<not> is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> \<not> isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s)) fail fail
 3. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (3 subgoals):
 1. \<And>x111 x112 x113 s s'. \<lbrakk>cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113; \<not> final; \<not> final'; (s, s') \<in> state_relation; invs s; invs' s'; valid_list s; valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s'; \<not> isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s'); valid_sched s; s \<turnstile> cap.Zombie x111 x112 x113; \<not> is_final_cap' (cap.Zombie x111 x112 x113) s; cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s; cte_wp_at (\<lambda>cap. is_final_cap' cap s) sl s\<rbrakk> \<Longrightarrow> False
 2. \<And>x111 x112 x113. \<lbrakk>cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113; \<not> final; \<not> final'; False\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> \<not> is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> \<not> isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s)) fail fail
 3. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>cap' = capability.Zombie x111 (zbits_map x112) x113; \<not> flag; cap = cap.Zombie x111 x112 x113; \<not> final; \<not> final'; False\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.Zombie x111 x112 x113 \<and> \<not> is_final_cap' (cap.Zombie x111 x112 x113) s \<and> cte_wp_at ((=) (cap.Zombie x111 x112 x113)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.Zombie x111 (zbits_map x112) x113) s \<and> \<not> isFinal (capability.Zombie x111 (zbits_map x112) x113) (cte_map sl) (cteCaps_of s)) fail fail
 2. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>final_matters' cap' \<Longrightarrow> final = final'; \<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; \<not> flag; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' cap' s \<and> (final_matters' cap' \<longrightarrow> final' = isFinal cap' (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then do y <- if final' then cancelAllIPC (capEPPtr cap') else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then let ptr = capNtfnPtr cap' in do y <- if final' then do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od else return ();
return (capability.NullCap, capability.NullCap)
od else if \<exists>v0 v1 v2. cap' = capability.ReplyCap v0 v1 v2 then return (capability.NullCap, capability.NullCap) else if cap' = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap' = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if (\<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3) \<and> final' then let bits = capCNodeBits cap' in return (capability.Zombie (capCNodePtr cap') (ZombieCNode bits) (shiftL (Suc 0) bits), capability.NullCap) else if (\<exists>v0. cap' = capability.ThreadCap v0) \<and> final' then let tcb = capTCBPtr cap' in do cte_ptr <- getThreadCSpaceRoot tcb;
y <- unbindNotification tcb;
y <- ThreadDecls_H.suspend tcb;
y <- Arch.prepareThreadDelete tcb;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> final' then return (cap', capability.NullCap) else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.finaliseCap (capCap cap') final' else if (\<exists>v0. cap' = capability.IRQHandlerCap v0) \<and> final' then do y <- deletingIRQHandler (capIRQ cap');
return (capability.NullCap, cap')
od else if (\<exists>v0 v1 v2. cap' = capability.Zombie v0 v1 v2) \<and> \<not> final' then fail else return (capability.NullCap, capability.NullCap)) proof (prove)
goal (1 subgoal):
 1. \<And>x12 a'. \<lbrakk>final_matters' (capability.ArchObjectCap a') \<Longrightarrow> final = final'; \<not> flag; cap = cap.ArchObjectCap x12; acap_relation x12 a'; cap' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> s \<turnstile> cap.ArchObjectCap x12 \<and> (final_matters_arch x12 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap x12) s) \<and> cte_wp_at ((=) (cap.ArchObjectCap x12)) sl s) (\<lambda>s. invs' s \<and> valid_cap' (capability.ArchObjectCap a') s \<and> (final_matters' (capability.ArchObjectCap a') \<longrightarrow> final' = isFinal (capability.ArchObjectCap a') (cte_map sl) (cteCaps_of s))) (arch_finalise_cap x12 final) (Arch.finaliseCap a' final') proof (prove)
goal:
No subgoals!