theory CNode_AC

lemma auth_derived_caps_of_state_impls:
  "\<lbrakk> auth_derived cap cap'; caps_of_state s ptr = Some cap';
     pas_refined aag s; is_subject aag (fst ptr) \<rbrakk>
     \<Longrightarrow> pas_cap_cur_auth aag cap" unfolding aag_cap_auth_def apply (frule (1) clas_caps_of_state) apply (frule (1) cli_caps_of_state) apply (clarsimp simp: auth_derived_def cap_links_asid_slot_def cong: cli_cap_irqs_controlled) apply (auto dest: pas_refined_mem[OF sta_untyped] pas_refined_mem[OF sta_caps]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>auth_derived cap cap'; caps_of_state s ptr = Some cap'; pas_refined aag s; is_subject aag (fst ptr)\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>auth_derived cap cap'; caps_of_state s ptr = Some cap'; pas_refined aag s; is_subject aag (fst ptr)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) cap \<and> cap_links_irq aag (pasSubject aag) cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>auth_derived cap cap'; caps_of_state s ptr = Some cap'; pas_refined aag s; is_subject aag (fst ptr); cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap'\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) cap \<and> cap_links_irq aag (pasSubject aag) cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>auth_derived cap cap'; caps_of_state s ptr = Some cap'; pas_refined aag s; is_subject aag (fst ptr); cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap'; cap_links_irq aag (pasObjectAbs aag (fst ptr)) cap'\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) cap \<and> cap_links_irq aag (pasSubject aag) cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s ptr = Some cap'; pas_refined aag s; is_subject aag (fst ptr); \<forall>asid\<in>cap_asid' cap'. label_owns_asid_slot aag (pasSubject aag) asid; cap_links_irq aag (pasSubject aag) cap'; cap_asid' cap \<subseteq> cap_asid' cap'; untyped_range cap = untyped_range cap'; obj_refs_ac cap = obj_refs_ac cap'; cap_auth_conferred cap \<subseteq> cap_auth_conferred cap'; cap_irqs_controlled cap = cap_irqs_controlled cap'\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs_ac cap'. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap'. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>cap_asid' cap. label_owns_asid_slot aag (pasSubject aag) x) proof (prove)
goal:
No subgoals!