theory Ipc_R

lemma deriveCap_not_null:
  "\<lbrace>\<top>\<rbrace> deriveCap slot cap \<lbrace>\<lambda>rv. K (rv \<noteq> NullCap \<longrightarrow> cap \<noteq> NullCap)\<rbrace>,-" apply (simp add: deriveCap_def split del: if_split) apply (case_tac cap) apply (simp_all add: Let_def isCap_simps) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> global.deriveCap slot cap \<lbrace>\<lambda>rv. K (rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, - proof (prove)
goal (12 subgoals):
 1. \<And>x1. cap = capability.ThreadCap x1 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
 2. cap = capability.NullCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
 3. \<And>x31 x32 x33 x34. cap = capability.NotificationCap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
 4. \<And>x4. cap = capability.IRQHandlerCap x4 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
 5. \<And>x51 x52 x53 x54 x55 x56. cap = capability.EndpointCap x51 x52 x53 x54 x55 x56 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
 6. cap = capability.DomainCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
 7. \<And>x71 x72 x73. cap = capability.Zombie x71 x72 x73 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
 8. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
 9. \<And>x91 x92 x93. cap = capability.ReplyCap x91 x92 x93 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
 10. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE y <- ensureNoChildren slot;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Arch.deriveCap slot (capCap cap) else returnOk cap \<lbrace>\<lambda>rv y. rv \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.NullCap\<rbrace>, -
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. cap = capability.NullCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> returnOk capability.NullCap \<lbrace>\<lambda>rv y. rv = capability.NullCap\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap = capability.NullCap; True\<rbrakk> \<Longrightarrow> capability.NullCap = capability.NullCap proof (prove)
goal:
No subgoals!