theory ArchIpc_AI

lemma derive_cap_idle[wp, Ipc_AI_assms]:
  "\<lbrace>\<lambda>s. global_refs s \<inter> cap_range cap = {}\<rbrace>
   derive_cap slot cap
  \<lbrace>\<lambda>c s. global_refs s \<inter> cap_range c = {}\<rbrace>, -" apply (simp add: derive_cap_def) apply (rule hoare_pre) apply (wpc| wp | simp add: arch_derive_cap_def)+ apply (case_tac cap, simp_all add: cap_range_def) apply (rename_tac arch_cap) apply (case_tac arch_cap, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. global_refs s \<inter> cap_range cap = {}\<rbrace> derive_cap slot cap \<lbrace>\<lambda>c s. global_refs s \<inter> cap_range c = {}\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. global_refs s \<inter> cap_range cap = {}\<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>c s. global_refs s \<inter> cap_range c = {}\<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>c s. global_refs s \<inter> cap_range c = {}\<rbrace>, -
 2. \<And>s. global_refs s \<inter> cap_range cap = {} \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. global_refs s \<inter> cap_range cap = {} \<Longrightarrow> (cap = NullCap \<longrightarrow> global_refs s \<inter> cap_range NullCap = {}) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> global_refs s \<inter> cap_range (UntypedCap x xa xb xc) = {}) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> global_refs s \<inter> cap_range (EndpointCap x xa xb) = {}) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> global_refs s \<inter> cap_range (NotificationCap x xa xb) = {}) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> global_refs s \<inter> cap_range NullCap = {}) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> global_refs s \<inter> cap_range (CNodeCap x xa xb) = {}) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> global_refs s \<inter> cap_range (ThreadCap x) = {}) \<and> (cap = DomainCap \<longrightarrow> global_refs s \<inter> cap_range DomainCap = {}) \<and> (cap = IRQControlCap \<longrightarrow> global_refs s \<inter> cap_range NullCap = {}) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> global_refs s \<inter> cap_range (IRQHandlerCap x) = {}) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> global_refs s \<inter> cap_range NullCap = {}) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (ASIDPoolCap xa xb)) = {}) \<and> (x = ASIDControlCap \<longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap ASIDControlCap) = {}) \<and> (\<forall>xa xb xc xd. (\<exists>xe. x = PageCap xa xb xc xd xe) \<longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageCap xa xb xc xd None)) = {}) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> (\<forall>a b. xb = Some (a, b) \<longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageTableCap xa (Some (a, b)))) = {})) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (\<forall>x. xb = Some x \<longrightarrow> global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap xa (Some x))) = {}))) proof (prove)
goal (1 subgoal):
 1. \<And>s x12. \<lbrakk>global_refs s \<inter> set_option (aobj_ref x12) = {}; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa. x12 = ASIDPoolCap x xa) \<longrightarrow> x \<notin> global_refs s) \<and> (\<forall>x xa. (\<exists>xb xc xd. x12 = PageCap x xa xb xc xd) \<longrightarrow> xa \<notin> global_refs s) \<and> (\<forall>x xa. x12 = PageTableCap x xa \<longrightarrow> (\<exists>a b. xa = Some (a, b)) \<longrightarrow> x \<notin> global_refs s) \<and> (\<forall>x xa. x12 = PageDirectoryCap x xa \<longrightarrow> (\<exists>x. xa = Some x) \<longrightarrow> x \<notin> global_refs s) proof (prove)
goal (1 subgoal):
 1. \<And>s arch_cap. \<lbrakk>global_refs s \<inter> set_option (aobj_ref arch_cap) = {}; cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa. arch_cap = ASIDPoolCap x xa) \<longrightarrow> x \<notin> global_refs s) \<and> (\<forall>x xa. (\<exists>xb xc xd. arch_cap = PageCap x xa xb xc xd) \<longrightarrow> xa \<notin> global_refs s) \<and> (\<forall>x xa. arch_cap = PageTableCap x xa \<longrightarrow> (\<exists>a b. xa = Some (a, b)) \<longrightarrow> x \<notin> global_refs s) \<and> (\<forall>x xa. arch_cap = PageDirectoryCap x xa \<longrightarrow> (\<exists>x. xa = Some x) \<longrightarrow> x \<notin> global_refs s) proof (prove)
goal:
No subgoals!