theory Helpers_SD

lemma derive_cap_wp:
  "\<lbrace> P (derived_cap cap) \<rbrace> derive_cap slot cap \<lbrace>P\<rbrace>, -" apply (clarsimp simp: derive_cap_def derived_cap_def) apply (clarsimp simp: validE_R_def derive_cap_def split:cdl_cap.splits) apply (safe, (wp whenE_wp |
                clarsimp simp: ensure_no_children_def)+ ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P (derived_cap cap)\<rbrace> derive_cap slot cap \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>P (case cap of ReplyCap x xa \<Rightarrow> NullCap | MasterReplyCap x \<Rightarrow> NullCap | IrqControlCap \<Rightarrow> NullCap | FrameCap d p r sz b x \<Rightarrow> FrameCap d p r sz b None | ZombieCap x \<Rightarrow> NullCap | _ \<Rightarrow> cap)\<rbrace> case cap of UntypedCap x xa xb \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap x xa \<Rightarrow> returnOk NullCap | MasterReplyCap oref \<Rightarrow> returnOk NullCap | IrqControlCap \<Rightarrow> returnOk NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap | PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap | ZombieCap x \<Rightarrow> returnOk NullCap | _ \<Rightarrow> returnOk cap \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (cap = NullCap \<longrightarrow> \<lbrace>P NullCap\<rbrace> returnOk NullCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x21 x22 x23. cap = UntypedCap x21 x22 x23 \<longrightarrow> \<lbrace>P (UntypedCap x21 x22 x23)\<rbrace> doE y <- ensure_no_children slot;
returnOk (UntypedCap x21 x22 x23)
odE \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<longrightarrow> \<lbrace>P (EndpointCap x31 x32 x33)\<rbrace> returnOk (EndpointCap x31 x32 x33) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<longrightarrow> \<lbrace>P (NotificationCap x41 x42 x43)\<rbrace> returnOk (NotificationCap x41 x42 x43) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> ((\<exists>x51 x52. cap = ReplyCap x51 x52) \<longrightarrow> \<lbrace>P NullCap\<rbrace> returnOk NullCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> ((\<exists>x6. cap = MasterReplyCap x6) \<longrightarrow> \<lbrace>P NullCap\<rbrace> returnOk NullCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x71 x72 x73 x74. cap = CNodeCap x71 x72 x73 x74 \<longrightarrow> \<lbrace>P (CNodeCap x71 x72 x73 x74)\<rbrace> returnOk (CNodeCap x71 x72 x73 x74) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x8. cap = TcbCap x8 \<longrightarrow> \<lbrace>P (TcbCap x8)\<rbrace> returnOk (TcbCap x8) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (cap = DomainCap \<longrightarrow> \<lbrace>P DomainCap\<rbrace> returnOk DomainCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x101 x102 x103 x104 x105 x106. cap = PendingSyncSendCap x101 x102 x103 x104 x105 x106 \<longrightarrow> \<lbrace>P (PendingSyncSendCap x101 x102 x103 x104 x105 x106)\<rbrace> returnOk (PendingSyncSendCap x101 x102 x103 x104 x105 x106) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x111 x112 x113. cap = PendingSyncRecvCap x111 x112 x113 \<longrightarrow> \<lbrace>P (PendingSyncRecvCap x111 x112 x113)\<rbrace> returnOk (PendingSyncRecvCap x111 x112 x113) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x12. cap = PendingNtfnRecvCap x12 \<longrightarrow> \<lbrace>P (PendingNtfnRecvCap x12)\<rbrace> returnOk (PendingNtfnRecvCap x12) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (cap = RestartCap \<longrightarrow> \<lbrace>P RestartCap\<rbrace> returnOk RestartCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (cap = RunningCap \<longrightarrow> \<lbrace>P RunningCap\<rbrace> returnOk RunningCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (cap = IrqControlCap \<longrightarrow> \<lbrace>P NullCap\<rbrace> returnOk NullCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x16. cap = IrqHandlerCap x16 \<longrightarrow> \<lbrace>P (IrqHandlerCap x16)\<rbrace> returnOk (IrqHandlerCap x16) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x171 x172 x173 x174 x175. (\<exists>x176. cap = FrameCap x171 x172 x173 x174 x175 x176) \<longrightarrow> \<lbrace>P (FrameCap x171 x172 x173 x174 x175 None)\<rbrace> returnOk (FrameCap x171 x172 x173 x174 x175 None) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x181 x182 x183. cap = PageTableCap x181 x182 x183 \<longrightarrow> \<lbrace>P (PageTableCap x181 x182 x183)\<rbrace> throw \<sqinter> returnOk (PageTableCap x181 x182 x183) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x191 x192 x193. cap = PageDirectoryCap x191 x192 x193 \<longrightarrow> \<lbrace>P (PageDirectoryCap x191 x192 x193)\<rbrace> throw \<sqinter> returnOk (PageDirectoryCap x191 x192 x193) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (cap = AsidControlCap \<longrightarrow> \<lbrace>P AsidControlCap\<rbrace> returnOk AsidControlCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x211 x212. cap = AsidPoolCap x211 x212 \<longrightarrow> \<lbrace>P (AsidPoolCap x211 x212)\<rbrace> returnOk (AsidPoolCap x211 x212) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x221 x222. cap = IOPortsCap x221 x222 \<longrightarrow> \<lbrace>P (IOPortsCap x221 x222)\<rbrace> returnOk (IOPortsCap x221 x222) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (cap = IOSpaceMasterCap \<longrightarrow> \<lbrace>P IOSpaceMasterCap\<rbrace> returnOk IOSpaceMasterCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x24. cap = IOSpaceCap x24 \<longrightarrow> \<lbrace>P (IOSpaceCap x24)\<rbrace> returnOk (IOSpaceCap x24) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x25. cap = IOPageTableCap x25 \<longrightarrow> \<lbrace>P (IOPageTableCap x25)\<rbrace> returnOk (IOPageTableCap x25) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> ((\<exists>x26. cap = ZombieCap x26) \<longrightarrow> \<lbrace>P NullCap\<rbrace> returnOk NullCap \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<forall>x27. cap = BoundNotificationCap x27 \<longrightarrow> \<lbrace>P (BoundNotificationCap x27)\<rbrace> returnOk (BoundNotificationCap x27) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) proof (prove)
goal:
No subgoals!