kings-crown/FVELER_Isabelle huggingface dataset:
theory Access_AC

lemma aag_wellformed_delete_derived':
  "\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
     \<Longrightarrow> (s, DeleteDerived, r) \<in> aag" unfolding policy_wellformed_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> \<Longrightarrow> (s, DeleteDerived, r) \<in> aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; (\<forall>agent'. (l, Control, agent') \<in> aag \<longrightarrow> l = agent') \<and> (\<forall>a. (l, a, l) \<in> aag) \<and> (\<forall>s r ep. (s, Grant, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag) \<and> (mirqs \<longrightarrow> (\<forall>irq ntfn. irq \<in> irqs \<and> (irq, Notify, ntfn) \<in> aag \<longrightarrow> (l, Notify, ntfn) \<in> aag)) \<and> (\<forall>s ep. (s, Call, ep) \<in> aag \<longrightarrow> (s, SyncSend, ep) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (r, Reply, s) \<in> aag) \<and> (\<forall>s r. (s, Reply, r) \<in> aag \<longrightarrow> (r, DeleteDerived, s) \<in> aag) \<and> (\<forall>l1 l2 l3. (l1, DeleteDerived, l2) \<in> aag \<longrightarrow> (l2, DeleteDerived, l3) \<in> aag \<longrightarrow> (l1, DeleteDerived, l3) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<and> (r, Grant, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag)\<rbrakk> \<Longrightarrow> (s, DeleteDerived, r) \<in> aag
theory Access_AC

lemma aag_wellformed_delete_derived:
  "\<lbrakk> (s, Reply, r) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
     \<Longrightarrow> (r, DeleteDerived, s) \<in> aag" unfolding policy_wellformed_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Reply, r) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> \<Longrightarrow> (r, DeleteDerived, s) \<in> aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Reply, r) \<in> aag; (\<forall>agent'. (l, Control, agent') \<in> aag \<longrightarrow> l = agent') \<and> (\<forall>a. (l, a, l) \<in> aag) \<and> (\<forall>s r ep. (s, Grant, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag) \<and> (mirqs \<longrightarrow> (\<forall>irq ntfn. irq \<in> irqs \<and> (irq, Notify, ntfn) \<in> aag \<longrightarrow> (l, Notify, ntfn) \<in> aag)) \<and> (\<forall>s ep. (s, Call, ep) \<in> aag \<longrightarrow> (s, SyncSend, ep) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (r, Reply, s) \<in> aag) \<and> (\<forall>s r. (s, Reply, r) \<in> aag \<longrightarrow> (r, DeleteDerived, s) \<in> aag) \<and> (\<forall>l1 l2 l3. (l1, DeleteDerived, l2) \<in> aag \<longrightarrow> (l2, DeleteDerived, l3) \<in> aag \<longrightarrow> (l1, DeleteDerived, l3) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<and> (r, Grant, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag)\<rbrakk> \<Longrightarrow> (r, DeleteDerived, s) \<in> aag
theory Access_AC

lemma aag_wellformed_delete_derived_trans:
  "\<lbrakk> (l1, DeleteDerived, l2) \<in> aag; (l2, DeleteDerived, l3) \<in> aag;
     policy_wellformed aag mirqs irqs l\<rbrakk>
     \<Longrightarrow> (l1, DeleteDerived, l3) \<in> aag" unfolding policy_wellformed_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(l1, DeleteDerived, l2) \<in> aag; (l2, DeleteDerived, l3) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> \<Longrightarrow> (l1, DeleteDerived, l3) \<in> aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(l1, DeleteDerived, l2) \<in> aag; (l2, DeleteDerived, l3) \<in> aag; (\<forall>agent'. (l, Control, agent') \<in> aag \<longrightarrow> l = agent') \<and> (\<forall>a. (l, a, l) \<in> aag) \<and> (\<forall>s r ep. (s, Grant, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag) \<and> (mirqs \<longrightarrow> (\<forall>irq ntfn. irq \<in> irqs \<and> (irq, Notify, ntfn) \<in> aag \<longrightarrow> (l, Notify, ntfn) \<in> aag)) \<and> (\<forall>s ep. (s, Call, ep) \<in> aag \<longrightarrow> (s, SyncSend, ep) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (r, Reply, s) \<in> aag) \<and> (\<forall>s r. (s, Reply, r) \<in> aag \<longrightarrow> (r, DeleteDerived, s) \<in> aag) \<and> (\<forall>l1 l2 l3. (l1, DeleteDerived, l2) \<in> aag \<longrightarrow> (l2, DeleteDerived, l3) \<in> aag \<longrightarrow> (l1, DeleteDerived, l3) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<and> (r, Grant, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag)\<rbrakk> \<Longrightarrow> (l1, DeleteDerived, l3) \<in> aag
theory Access_AC

lemma aag_wellformed_call_to_syncsend:
  "\<lbrakk> (s, Call, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
     \<Longrightarrow> (s, SyncSend, ep) \<in> aag" unfolding policy_wellformed_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Call, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> \<Longrightarrow> (s, SyncSend, ep) \<in> aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Call, ep) \<in> aag; (\<forall>agent'. (l, Control, agent') \<in> aag \<longrightarrow> l = agent') \<and> (\<forall>a. (l, a, l) \<in> aag) \<and> (\<forall>s r ep. (s, Grant, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag) \<and> (mirqs \<longrightarrow> (\<forall>irq ntfn. irq \<in> irqs \<and> (irq, Notify, ntfn) \<in> aag \<longrightarrow> (l, Notify, ntfn) \<in> aag)) \<and> (\<forall>s ep. (s, Call, ep) \<in> aag \<longrightarrow> (s, SyncSend, ep) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (r, Reply, s) \<in> aag) \<and> (\<forall>s r. (s, Reply, r) \<in> aag \<longrightarrow> (r, DeleteDerived, s) \<in> aag) \<and> (\<forall>l1 l2 l3. (l1, DeleteDerived, l2) \<in> aag \<longrightarrow> (l2, DeleteDerived, l3) \<in> aag \<longrightarrow> (l1, DeleteDerived, l3) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<and> (r, Grant, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag)\<rbrakk> \<Longrightarrow> (s, SyncSend, ep) \<in> aag
theory Access_AC

lemma aag_wellformed_grant_Control_to_send_by_reply:
  "\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag;
     (r, Grant, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
     \<Longrightarrow> (r, Control, s) \<in> aag" unfolding policy_wellformed_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; (r, Grant, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> \<Longrightarrow> (r, Control, s) \<in> aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; (r, Grant, ep) \<in> aag; (\<forall>agent'. (l, Control, agent') \<in> aag \<longrightarrow> l = agent') \<and> (\<forall>a. (l, a, l) \<in> aag) \<and> (\<forall>s r ep. (s, Grant, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag) \<and> (mirqs \<longrightarrow> (\<forall>irq ntfn. irq \<in> irqs \<and> (irq, Notify, ntfn) \<in> aag \<longrightarrow> (l, Notify, ntfn) \<in> aag)) \<and> (\<forall>s ep. (s, Call, ep) \<in> aag \<longrightarrow> (s, SyncSend, ep) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (r, Reply, s) \<in> aag) \<and> (\<forall>s r. (s, Reply, r) \<in> aag \<longrightarrow> (r, DeleteDerived, s) \<in> aag) \<and> (\<forall>l1 l2 l3. (l1, DeleteDerived, l2) \<in> aag \<longrightarrow> (l2, DeleteDerived, l3) \<in> aag \<longrightarrow> (l1, DeleteDerived, l3) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<and> (r, Grant, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag)\<rbrakk> \<Longrightarrow> (r, Control, s) \<in> aag
theory Access_AC

lemma aag_wellformed_grant_Control_to_recv_by_reply:
  "\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag;
     (r, Grant, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
     \<Longrightarrow> (s, Control, r) \<in> aag" unfolding policy_wellformed_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; (r, Grant, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> \<Longrightarrow> (s, Control, r) \<in> aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; (r, Grant, ep) \<in> aag; (\<forall>agent'. (l, Control, agent') \<in> aag \<longrightarrow> l = agent') \<and> (\<forall>a. (l, a, l) \<in> aag) \<and> (\<forall>s r ep. (s, Grant, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag) \<and> (mirqs \<longrightarrow> (\<forall>irq ntfn. irq \<in> irqs \<and> (irq, Notify, ntfn) \<in> aag \<longrightarrow> (l, Notify, ntfn) \<in> aag)) \<and> (\<forall>s ep. (s, Call, ep) \<in> aag \<longrightarrow> (s, SyncSend, ep) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (r, Reply, s) \<in> aag) \<and> (\<forall>s r. (s, Reply, r) \<in> aag \<longrightarrow> (r, DeleteDerived, s) \<in> aag) \<and> (\<forall>l1 l2 l3. (l1, DeleteDerived, l2) \<in> aag \<longrightarrow> (l2, DeleteDerived, l3) \<in> aag \<longrightarrow> (l1, DeleteDerived, l3) \<in> aag) \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<and> (r, Grant, ep) \<in> aag \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag)\<rbrakk> \<Longrightarrow> (s, Control, r) \<in> aag
theory Access_AC

lemma auth_graph_map_mem:
  "(x, auth, y) \<in> auth_graph_map f S = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> (x', auth, y') \<in> S)" by (simp add: auth_graph_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x, auth, y) \<in> auth_graph_map f S) = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> (x', auth, y') \<in> S)
theory Access_AC

lemma auth_graph_map_memE:
  assumes hyp: "(x, auth, y) \<in> auth_graph_map f S"
  obtains x' and y' where "x = f x'" and "y = f y'" and "(x', auth, y') \<in> S" using hyp[THEN auth_graph_map_mem[THEN iffD1]] by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x' y'. \<lbrakk>x = f x'; y = f y'; (x', auth, y') \<in> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
\<exists>x' y'. x = f x' \<and> y = f y' \<and> (x', auth, y') \<in> S

goal (1 subgoal):
 1. (\<And>x' y'. \<lbrakk>x = f x'; y = f y'; (x', auth, y') \<in> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory Access_AC

lemma auth_graph_map_memI:
  "\<lbrakk> (x', auth, y') \<in> S; x = f x'; y = f y' \<rbrakk>
     \<Longrightarrow> (x, auth, y) \<in> auth_graph_map f S" by (fastforce simp add: auth_graph_map_mem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x', auth, y') \<in> S; x = f x'; y = f y'\<rbrakk> \<Longrightarrow> (x, auth, y) \<in> auth_graph_map f S
theory Access_AC

lemma auth_graph_map_mono:
  "S \<subseteq> S' \<Longrightarrow> auth_graph_map G S \<subseteq> auth_graph_map G S'" unfolding auth_graph_map_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> S' \<Longrightarrow> auth_graph_map G S \<subseteq> auth_graph_map G S' proof (prove)
goal (1 subgoal):
 1. S \<subseteq> S' \<Longrightarrow> {(G x, auth, G y) |x auth y. (x, auth, y) \<in> S} \<subseteq> {(G x, auth, G y) |x auth y. (x, auth, y) \<in> S'}
theory Access_AC

lemma is_transferable_None[simp]: "is_transferable None" using is_transferable.simps by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_transferable None proof (prove)
using this:
is_transferable ?opt_cap = (?opt_cap = None \<or> ?opt_cap = Some NullCap \<or> (\<exists>t R. ?opt_cap = Some (ReplyCap t False R)))

goal (1 subgoal):
 1. is_transferable None
theory Access_AC

lemma is_transferable_Null[simp]: "is_transferable_cap NullCap" using is_transferable.simps by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_transferable_cap NullCap proof (prove)
using this:
is_transferable ?opt_cap = (?opt_cap = None \<or> ?opt_cap = Some NullCap \<or> (\<exists>t R. ?opt_cap = Some (ReplyCap t False R)))

goal (1 subgoal):
 1. is_transferable_cap NullCap
theory Access_AC

lemma is_transferable_Reply[simp]: "is_transferable_cap (ReplyCap t False R)" using is_transferable.simps by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_transferable_cap (ReplyCap t False R) proof (prove)
using this:
is_transferable ?opt_cap = (?opt_cap = None \<or> ?opt_cap = Some NullCap \<or> (\<exists>t R. ?opt_cap = Some (ReplyCap t False R)))

goal (1 subgoal):
 1. is_transferable_cap (ReplyCap t False R)
theory Access_AC

lemma is_transferable_NoneE:
  assumes hyp: "is_transferable opt_cap"
  obtains "opt_cap = None" | cap where "opt_cap = Some cap" and "is_transferable_cap cap" by (rule is_transferable.cases[OF hyp];simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>opt_cap = None \<Longrightarrow> thesis; \<And>cap. \<lbrakk>opt_cap = Some cap; is_transferable_cap cap\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
theory Access_AC

lemma is_transferable_Untyped[simp]: "\<not> is_transferable (Some (UntypedCap dev ptr sz freeIndex))" by (blast elim: is_transferable.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_transferable_cap (UntypedCap dev ptr sz freeIndex)
theory Access_AC

lemma is_transferable_IRQ[simp]: "\<not> is_transferable_cap IRQControlCap" by (blast elim: is_transferable.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_transferable_cap IRQControlCap
theory Access_AC

lemma is_transferable_Zombie[simp]: "\<not> is_transferable (Some (Zombie ptr sz n))" by (blast elim: is_transferable.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_transferable_cap (Zombie ptr sz n)
theory Access_AC

lemma is_transferable_Endpoint[simp]: "\<not> is_transferable (Some (EndpointCap ntfn badge R))" by (blast elim: is_transferable.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_transferable_cap (EndpointCap ntfn badge R)
theory Access_AC

lemma valid_mdb_descendants_inc[elim!]:
  "valid_mdb s \<Longrightarrow> descendants_inc (cdt s) (caps_of_state s)" by (simp add:valid_mdb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> descendants_inc (cdt s) (caps_of_state s)
theory Access_AC

lemma valid_mdb_mdb_cte_at [elim!]:
  "valid_mdb s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)" by (simp add:valid_mdb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)
theory Access_AC

lemma descendants_inc_cap_classD:
  "\<lbrakk> descendants_inc m caps; p \<in> descendants_of p' m; caps p = Some cap ; caps p' = Some cap' \<rbrakk>
     \<Longrightarrow> cap_class cap = cap_class cap'" by (fastforce dest:descendants_incD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_inc m caps; p \<in> descendants_of p' m; caps p = Some cap; caps p' = Some cap'\<rbrakk> \<Longrightarrow> cap_class cap = cap_class cap'
theory Access_AC

lemma cap_class_reply:
  "(cap_class cap = ReplyClass t) = (\<exists>r m. cap = ReplyCap t m r)" by (cases cap; simp add: acap_class_reply)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_class cap = ReplyClass t) = (\<exists>r m. cap = ReplyCap t m r)
theory Access_AC

lemma is_transferable_all_children:
  "valid_mdb s \<Longrightarrow> all_children (\<lambda>slot . is_transferable (caps_of_state s slot)) (cdt s)" apply (rule all_childrenI) apply (erule is_transferable.cases) apply (fastforce dest: mdb_cte_atD valid_mdb_mdb_cte_at
                     simp: mdb_cte_at_def cte_wp_at_def caps_of_state_def) apply (fastforce dest: mdb_cte_atD valid_mdb_mdb_cte_at
                    simp: mdb_cte_at_def cte_wp_at_def caps_of_state_def) apply (blast dest: reply_cap_no_children) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> all_children (\<lambda>slot. is_transferable_in slot s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrakk>valid_mdb s; cdt s c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_transferable_in c s proof (prove)
goal (3 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; cdt s c = Some p; caps_of_state s p = None\<rbrakk> \<Longrightarrow> is_transferable_in c s
 2. \<And>c p. \<lbrakk>valid_mdb s; cdt s c = Some p; caps_of_state s p = Some NullCap\<rbrakk> \<Longrightarrow> is_transferable_in c s
 3. \<And>c p t R. \<lbrakk>valid_mdb s; cdt s c = Some p; caps_of_state s p = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> is_transferable_in c s proof (prove)
goal (2 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; cdt s c = Some p; caps_of_state s p = Some NullCap\<rbrakk> \<Longrightarrow> is_transferable_in c s
 2. \<And>c p t R. \<lbrakk>valid_mdb s; cdt s c = Some p; caps_of_state s p = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> is_transferable_in c s proof (prove)
goal (1 subgoal):
 1. \<And>c p t R. \<lbrakk>valid_mdb s; cdt s c = Some p; caps_of_state s p = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> is_transferable_in c s proof (prove)
goal:
No subgoals!
theory Access_AC

lemma tcb_states_of_state_preserved:
  "\<lbrakk> get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb \<rbrakk>
     \<Longrightarrow> tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) = tcb_states_of_state s" by (auto split: option.splits simp: tcb_states_of_state_def get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb\<rbrakk> \<Longrightarrow> tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) = tcb_states_of_state s
theory Access_AC

lemma thread_st_auth_preserved:
  "\<lbrakk> get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb \<rbrakk>
     \<Longrightarrow> thread_st_auth (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) = thread_st_auth s" by (simp add: tcb_states_of_state_preserved thread_st_auth_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb\<rbrakk> \<Longrightarrow> thread_st_auth (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) = thread_st_auth s
theory Access_AC

lemma thread_bound_ntfns_preserved:
  "\<lbrakk> get_tcb thread s = Some tcb; tcb_bound_notification tcb' = tcb_bound_notification tcb \<rbrakk>
     \<Longrightarrow> thread_bound_ntfns (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) = thread_bound_ntfns s" by (auto simp: thread_bound_ntfns_def get_tcb_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb thread s = Some tcb; tcb_bound_notification tcb' = tcb_bound_notification tcb\<rbrakk> \<Longrightarrow> thread_bound_ntfns (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) = thread_bound_ntfns s
theory Access_AC

lemma is_transferable_null_filter[simp]:
  "is_transferable (null_filter caps ptr) = is_transferable (caps ptr)" by (auto simp: is_transferable.simps null_filter_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_transferable (null_filter caps ptr) = is_transferable (caps ptr)
theory Access_AC

lemma tcb_domain_map_wellformed_mono:
  "\<lbrakk> domains_of_state s' \<subseteq> domains_of_state s; tcb_domain_map_wellformed pas s \<rbrakk>
     \<Longrightarrow> tcb_domain_map_wellformed pas s'" by (auto simp: tcb_domain_map_wellformed_aux_def get_etcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>domains_of_state s' \<subseteq> domains_of_state s; tcb_domain_map_wellformed pas s\<rbrakk> \<Longrightarrow> tcb_domain_map_wellformed pas s'
theory Access_AC

lemma pas_refined_mem:
  "\<lbrakk> (x, auth, y) \<in> state_objs_to_policy s; pas_refined aag s \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag auth x y" by (auto simp: pas_refined_def intro: auth_graph_map_memI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, auth, y) \<in> state_objs_to_policy s; pas_refined aag s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, auth, pasObjectAbs aag y) \<in> pasPolicy aag
theory Access_AC

lemma pas_refined_wellformed[elim!]:
  "pas_refined aag s \<Longrightarrow> pas_wellformed aag" unfolding pas_refined_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> pas_wellformed aag proof (prove)
goal (1 subgoal):
 1. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag \<Longrightarrow> pas_wellformed aag
theory Access_AC

lemma caps_of_state_pasObjectAbs_eq:
  "\<lbrakk> caps_of_state s p = Some cap; Control \<in> cap_auth_conferred cap;
     is_subject aag (fst p); pas_refined aag s; x \<in> obj_refs_ac cap \<rbrakk>
     \<Longrightarrow> is_subject aag x" apply (frule sta_caps, simp+) apply (drule pas_refined_mem, simp+) apply (drule pas_refined_Control, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; Control \<in> cap_auth_conferred cap; is_subject aag (fst p); pas_refined aag s; x \<in> obj_refs_ac cap\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; Control \<in> cap_auth_conferred cap; is_subject aag (fst p); pas_refined aag s; x \<in> obj_refs_ac cap; (fst p, Control, x) \<in> state_objs_to_policy s\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; Control \<in> cap_auth_conferred cap; is_subject aag (fst p); pas_refined aag s; x \<in> obj_refs_ac cap; (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal:
No subgoals!
theory Access_AC

lemma pas_refined_state_objs_to_policy_subset:
  "\<lbrakk> pas_refined aag s;
     state_objs_to_policy s' \<subseteq> state_objs_to_policy s;
     state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s;
     state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s;
     domains_of_state s' \<subseteq> domains_of_state s;
     interrupt_irq_node s' = interrupt_irq_node s \<rbrakk>
     \<Longrightarrow> pas_refined aag s'" by (simp add: pas_refined_def)
     (blast dest: tcb_domain_map_wellformed_mono auth_graph_map_mono[where G="pasObjectAbs aag"])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; state_objs_to_policy s' \<subseteq> state_objs_to_policy s; state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s; state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s; domains_of_state s' \<subseteq> domains_of_state s; interrupt_irq_node s' = interrupt_irq_node s\<rbrakk> \<Longrightarrow> pas_refined aag s'