theory CNode_AC

lemma derive_cap_untyped_range_subset:
  "\<lbrace>\<lambda>s :: det_ext state. \<forall>x \<in> untyped_range cap. P x s\<rbrace>
   derive_cap slot cap
   \<lbrace>\<lambda>rv s. \<forall>x \<in> untyped_range rv. P x s\<rbrace>, -" unfolding derive_cap_def apply (rule hoare_pre) apply (simp cong: cap.case_cong) apply (wp arch_derive_cap_untyped_range_subset | wpc)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>untyped_range cap. P x s\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. \<forall>x\<in>untyped_range rv. P x s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>untyped_range cap. P x s\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>\<lambda>rv s. \<forall>x\<in>untyped_range rv. P x s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>\<lambda>rv s. \<forall>x\<in>untyped_range rv. P x s\<rbrace>, -
 2. \<And>s. \<forall>x\<in>untyped_range cap. P x s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE y <- ensure_no_children slot;
returnOk (UntypedCap dev ptr sz f)
odE | EndpointCap word1 word2 set \<Rightarrow> returnOk (EndpointCap word1 word2 set) | NotificationCap word1 word2 set \<Rightarrow> returnOk (NotificationCap word1 word2 set) | CNodeCap word nat list \<Rightarrow> returnOk (CNodeCap word nat list) | ThreadCap word \<Rightarrow> returnOk (ThreadCap word) | DomainCap \<Rightarrow> returnOk DomainCap | IRQHandlerCap word \<Rightarrow> returnOk (IRQHandlerCap word) | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk NullCap \<lbrace>\<lambda>rv s. \<forall>x\<in>untyped_range rv. P x s\<rbrace>, -
 2. \<And>s. \<forall>x\<in>untyped_range cap. P x s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x\<in>untyped_range cap. P x s \<Longrightarrow> (cap = NullCap \<longrightarrow> (\<forall>x\<in>untyped_range NullCap. P x s)) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True \<and> (\<forall>x\<in>untyped_range (UntypedCap x xa xb xc). P x s)) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (\<forall>x\<in>untyped_range (EndpointCap x xa xb). P x s)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (\<forall>x\<in>untyped_range (NotificationCap x xa xb). P x s)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (\<forall>x\<in>untyped_range NullCap. P x s)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> (\<forall>x\<in>untyped_range (CNodeCap x xa xb). P x s)) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> (\<forall>x\<in>untyped_range (ThreadCap x). P x s)) \<and> (cap = DomainCap \<longrightarrow> (\<forall>x\<in>untyped_range DomainCap. P x s)) \<and> (cap = IRQControlCap \<longrightarrow> (\<forall>x\<in>untyped_range NullCap. P x s)) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> (\<forall>x\<in>untyped_range (IRQHandlerCap x). P x s)) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> (\<forall>x\<in>untyped_range NullCap. P x s)) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>x\<in>untyped_range (ArchObjectCap x). P x s)) proof (prove)
goal:
No subgoals!