theory Access_AC

lemma cap_auth_caps_of_state:
  "\<lbrakk> caps_of_state s p = Some cap; pas_refined aag s \<rbrakk>
     \<Longrightarrow> aag_cap_auth aag (pasObjectAbs aag (fst p)) cap" unfolding aag_cap_auth_def apply (intro conjI) apply clarsimp apply (drule (2) sta_caps) apply (drule_tac f="pasObjectAbs aag" in auth_graph_map_memI[OF _ refl refl]) apply (fastforce simp: pas_refined_def) apply clarsimp apply (drule (2) sta_untyped [THEN pas_refined_mem] ) apply simp apply (drule (1) clas_caps_of_state) apply simp apply (drule (1) cli_caps_of_state) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> aag_cap_auth aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst p), auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst p), Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap \<and> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (4 subgoals):
 1. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasObjectAbs aag (fst p), auth, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst p), Control, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap
 4. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (4 subgoals):
 1. \<And>x auth. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s; x \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst p), auth, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst p), Control, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap
 4. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (4 subgoals):
 1. \<And>x auth. \<lbrakk>pas_refined aag s; x \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap; (fst p, auth, x) \<in> state_objs_to_policy s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst p), auth, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst p), Control, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap
 4. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (4 subgoals):
 1. \<And>x auth. \<lbrakk>pas_refined aag s; x \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap; (pasObjectAbs aag (fst p), auth, pasObjectAbs aag x) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst p), auth, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst p), Control, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap
 4. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (3 subgoals):
 1. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>x\<in>untyped_range cap. (pasObjectAbs aag (fst p), Control, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap
 3. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s; x \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst p), Control, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap
 3. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>pas_refined aag s; x \<in> untyped_range cap; (pasObjectAbs aag (fst p), Control, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst p), Control, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap
 3. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap
 2. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst p)) cap
 2. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; cap_links_irq aag (pasObjectAbs aag (fst p)) cap\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst p)) cap proof (prove)
goal:
No subgoals!