theory Finalise_R

lemma finaliseCapTrue_standin_ct_not_ksQ:
  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
   finaliseCapTrue_standin cap final
   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" apply (simp add: finaliseCapTrue_standin_def Let_def) apply (safe) apply (wp cancelAllIPC_ct_not_ksQ cancelAllSignals_ct_not_ksQ
                hoare_drop_imps unbindMaybeNotification_ct_not_ksQ
             | wpc
             | clarsimp simp: isNotificationCap_def isReplyCap_def split:capability.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> finaliseCapTrue_standin cap final \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (cap = capability.DomainCap \<longrightarrow> (isNotificationCap capability.DomainCap \<longrightarrow> (isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>) \<and> (\<not> isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr capability.DomainCap);
cancelAllSignals (capNtfnPtr capability.DomainCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>)) \<and> (\<not> isNotificationCap capability.DomainCap \<longrightarrow> (isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>) \<and> (\<not> isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>))) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> (isNotificationCap capability.NullCap \<longrightarrow> (isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>) \<and> (\<not> isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr capability.NullCap);
cancelAllSignals (capNtfnPtr capability.NullCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>)) \<and> (\<not> isNotificationCap capability.NullCap \<longrightarrow> (isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>) \<and> (\<not> isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>))) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (isReplyCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> (isEndpointCap cap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>) \<and> (\<not> isEndpointCap cap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>)) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isEndpointCap cap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>) \<and> (\<not> isEndpointCap cap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>))) \<and> (\<not> isReplyCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> (isEndpointCap cap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>) \<and> (\<not> isEndpointCap cap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>)) \<and> (\<not> isNotificationCap cap \<longrightarrow> isEndpointCap cap \<longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>)))) proof (prove)
goal (15 subgoals):
 1. \<lbrakk>cap = capability.DomainCap; isNotificationCap capability.DomainCap; isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<lbrakk>cap = capability.DomainCap; isNotificationCap capability.DomainCap; \<not> isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr capability.DomainCap);
cancelAllSignals (capNtfnPtr capability.DomainCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 3. \<lbrakk>cap = capability.DomainCap; \<not> isNotificationCap capability.DomainCap; isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 4. \<lbrakk>cap = capability.DomainCap; \<not> isNotificationCap capability.DomainCap; \<not> isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 5. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; isNotificationCap capability.NullCap; isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 6. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; isNotificationCap capability.NullCap; \<not> isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr capability.NullCap);
cancelAllSignals (capNtfnPtr capability.NullCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 7. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; \<not> isNotificationCap capability.NullCap; isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 8. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; \<not> isNotificationCap capability.NullCap; \<not> isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 9. \<lbrakk>cap \<noteq> capability.DomainCap; cap \<noteq> capability.NullCap; isReplyCap cap; isNotificationCap cap; isEndpointCap cap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 10. \<lbrakk>cap \<noteq> capability.DomainCap; cap \<noteq> capability.NullCap; isReplyCap cap; isNotificationCap cap; \<not> isEndpointCap cap\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
A total of 15 subgoals... proof (prove)
goal:
No subgoals!