theory ArchCNode_AC

lemma arch_derive_cap_obj_refs_auth[CNode_AC_assms]:
  "\<lbrace>K (\<forall>r\<in>obj_refs_ac (ArchObjectCap cap).
       \<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). aag_has_auth_to aag auth r)\<rbrace>
   arch_derive_cap cap
   \<lbrace>(\<lambda>x s. \<forall>r\<in>obj_refs_ac x. \<forall>auth\<in>cap_auth_conferred x. aag_has_auth_to aag auth r)\<rbrace>, -" unfolding arch_derive_cap_def apply (rule hoare_pre) apply (wp | wpc)+ apply (clarsimp simp: cap_auth_conferred_def arch_cap_auth_conferred_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (\<forall>r\<in>obj_refs_ac (ArchObjectCap cap). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag)\<rbrace> arch_derive_cap cap \<lbrace>\<lambda>x s. \<forall>r\<in>obj_refs_ac x. \<forall>auth\<in>cap_auth_conferred x. (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (\<forall>r\<in>obj_refs_ac (ArchObjectCap cap). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag)\<rbrace> case cap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | _ \<Rightarrow> returnOk (ArchObjectCap cap) \<lbrace>\<lambda>x s. \<forall>r\<in>obj_refs_ac x. \<forall>auth\<in>cap_auth_conferred x. (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap cap) | _ \<Rightarrow> returnOk (ArchObjectCap cap) \<lbrace>\<lambda>x s. \<forall>r\<in>obj_refs_ac x. \<forall>auth\<in>cap_auth_conferred x. (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag\<rbrace>, -
 2. \<And>s. K (\<forall>r\<in>obj_refs_ac (ArchObjectCap cap). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. K (\<forall>r\<in>obj_refs_ac (ArchObjectCap cap). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag) s \<Longrightarrow> (\<forall>x xa. cap = ASIDPoolCap x xa \<longrightarrow> (\<forall>r\<in>obj_refs_ac (ArchObjectCap cap). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag)) \<and> (cap = ASIDControlCap \<longrightarrow> (\<forall>r\<in>obj_refs_ac (ArchObjectCap cap). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag)) \<and> (\<forall>x xa xb xc xd. cap = PageCap x xa xb xc xd \<longrightarrow> (\<forall>r\<in>obj_refs_ac (ArchObjectCap (PageCap x xa xb xc None)). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (PageCap x xa xb xc None)). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag)) \<and> (\<forall>x xa. cap = PageTableCap x xa \<longrightarrow> (xa = None \<longrightarrow> True) \<and> (\<forall>x. xa = Some x \<longrightarrow> (\<forall>r\<in>obj_refs_ac (ArchObjectCap cap). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag))) \<and> (\<forall>x xa. cap = PageDirectoryCap x xa \<longrightarrow> (xa = None \<longrightarrow> True) \<and> (\<forall>x. xa = Some x \<longrightarrow> (\<forall>r\<in>obj_refs_ac (ArchObjectCap cap). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag))) proof (prove)
goal:
No subgoals!