theory Finalise_R

lemma finaliseCapTrue_standin_valid_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
   finaliseCapTrue_standin cap final
   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" apply (simp add: finaliseCapTrue_standin_def Let_def) apply (safe) apply (wp | clarsimp | wpc)+ done

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