theory Ipc_R

lemma finaliseCapTrue_standin_tcb_at' [wp]:
  "\<lbrace>tcb_at' x\<rbrace> finaliseCapTrue_standin cap v2 \<lbrace>\<lambda>_. tcb_at' x\<rbrace>" apply (simp add: finaliseCapTrue_standin_def Let_def) apply (safe) apply (wp getObject_ntfn_inv
            | wpc
            | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' x\<rbrace> finaliseCapTrue_standin cap v2 \<lbrace>\<lambda>_. tcb_at' x\<rbrace> proof (prove)
goal (1 subgoal):
 1. (cap = capability.DomainCap \<longrightarrow> (isNotificationCap capability.DomainCap \<longrightarrow> (isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>) \<and> (\<not> isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (do y <- unbindMaybeNotification (capNtfnPtr capability.DomainCap);
cancelAllSignals (capNtfnPtr capability.DomainCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>)) \<and> (\<not> isNotificationCap capability.DomainCap \<longrightarrow> isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>)) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> (isNotificationCap capability.NullCap \<longrightarrow> (isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>) \<and> (\<not> isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (do y <- unbindMaybeNotification (capNtfnPtr capability.NullCap);
cancelAllSignals (capNtfnPtr capability.NullCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>)) \<and> (\<not> isNotificationCap capability.NullCap \<longrightarrow> isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>)) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (isNotificationCap cap \<longrightarrow> (isEndpointCap cap \<longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>) \<and> (\<not> isEndpointCap cap \<longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>)) \<and> (\<not> isNotificationCap cap \<longrightarrow> isEndpointCap cap \<longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>))) proof (prove)
goal (9 subgoals):
 1. \<lbrakk>cap = capability.DomainCap; isNotificationCap capability.DomainCap; isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 2. \<lbrakk>cap = capability.DomainCap; isNotificationCap capability.DomainCap; \<not> isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (do y <- unbindMaybeNotification (capNtfnPtr capability.DomainCap);
cancelAllSignals (capNtfnPtr capability.DomainCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 3. \<lbrakk>cap = capability.DomainCap; \<not> isNotificationCap capability.DomainCap; isEndpointCap capability.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 4. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; isNotificationCap capability.NullCap; isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 5. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; isNotificationCap capability.NullCap; \<not> isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (do y <- unbindMaybeNotification (capNtfnPtr capability.NullCap);
cancelAllSignals (capNtfnPtr capability.NullCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 6. \<lbrakk>capability.NullCap \<noteq> capability.DomainCap; cap = capability.NullCap; \<not> isNotificationCap capability.NullCap; isEndpointCap capability.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 7. \<lbrakk>cap \<noteq> capability.DomainCap; cap \<noteq> capability.NullCap; isNotificationCap cap; isEndpointCap cap\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 8. \<lbrakk>cap \<noteq> capability.DomainCap; cap \<noteq> capability.NullCap; isNotificationCap cap; \<not> isEndpointCap cap\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace>
 9. \<lbrakk>cap \<noteq> capability.DomainCap; cap \<noteq> capability.NullCap; \<not> isNotificationCap cap; isEndpointCap cap\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' x\<rbrace> do y <- when v2 (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. tcb_at' x\<rbrace> proof (prove)
goal:
No subgoals!