theory Finalise_R

lemma finaliseCap_True_invs[wp]:
  "\<lbrace>invs'\<rbrace> finaliseCap cap final True \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: finaliseCap_def Let_def) apply safe apply (wp irqs_masked_lift| simp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> global.finaliseCap cap final True \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (cap = capability.DomainCap \<longrightarrow> (isNotificationCap capability.DomainCap \<longrightarrow> (isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>invs'\<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. invs'\<rbrace>)) \<and> (\<not> isNotificationCap capability.DomainCap \<longrightarrow> isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>)) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> (isNotificationCap capability.NullCap \<longrightarrow> (isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>invs'\<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. invs'\<rbrace>)) \<and> (\<not> isNotificationCap capability.NullCap \<longrightarrow> isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>)) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (isNotificationCap cap \<longrightarrow> (isEndpointCap cap \<longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> isEndpointCap cap \<longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>)) \<and> (\<not> isNotificationCap cap \<longrightarrow> isEndpointCap cap \<longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>))) proof (prove)
goal (9 subgoals):
 1. \<lbrakk>cap = capability.DomainCap; isNotificationCap capability.DomainCap; isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<lbrakk>cap = capability.DomainCap; isNotificationCap capability.DomainCap; \<not> isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<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. invs'\<rbrace>
 3. \<lbrakk>cap = capability.DomainCap; \<not> isNotificationCap capability.DomainCap; isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; isNotificationCap capability.NullCap; isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; isNotificationCap capability.NullCap; \<not> isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<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. invs'\<rbrace>
 6. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; \<not> isNotificationCap capability.NullCap; isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<lbrakk>cap \<noteq> capability.DomainCap; cap \<noteq> capability.NullCap; isNotificationCap cap; isEndpointCap cap\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<lbrakk>cap \<noteq> capability.DomainCap; cap \<noteq> capability.NullCap; isNotificationCap cap; \<not> isEndpointCap cap\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 9. \<lbrakk>cap \<noteq> capability.DomainCap; cap \<noteq> capability.NullCap; \<not> isNotificationCap cap; isEndpointCap cap\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!