kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_DR

lemma get_active_irq_corres:
  "dcorres (\<lambda>r r'. r' = r) \<top> \<top> get_active_irq (do_machine_op (getActiveIRQ in_kernel))" apply (clarsimp simp: corres_underlying_def do_machine_op_def
                        select_f_def bind_def in_monad getActiveIRQ_def
                        return_def get_active_irq_def select_def
                 split: if_splits) apply (rule_tac x="(None, transform b)" in bexI
       , (simp add: in_alternative)+) apply (rule_tac x="(Some (irq_oracle (Suc (irq_state (machine_state b)))),
                      transform b)" in bexI
       , (simp add: in_alternative)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>r r'. r' = r) (\<lambda>_. True) (\<lambda>_. True) get_active_irq (do_machine_op (getActiveIRQ in_kernel)) proof (prove)
goal (2 subgoals):
 1. \<And>b. irq_masks (machine_state b) (irq_oracle (Suc (irq_state (machine_state b)))) \<or> irq_oracle (Suc (irq_state (machine_state b))) = 0x3FF \<or> in_kernel \<and> irq_oracle (Suc (irq_state (machine_state b))) \<in> non_kernel_IRQs \<Longrightarrow> \<exists>x\<in>fst (((\<lambda>s. (\<Union>a\<in>UNIV \<times> {s}. fst (case a of (irq, s) \<Rightarrow> ({(Some irq, s)}, False)), False)) \<sqinter> (\<lambda>s. ({(None, s)}, False))) (transform b)). case x of (r, t) \<Rightarrow> transform b = t \<and> None = r
 2. \<And>b aa. \<lbrakk>\<not> irq_masks (machine_state b) (irq_oracle (Suc (irq_state (machine_state b)))) \<and> irq_oracle (Suc (irq_state (machine_state b))) \<noteq> 0x3FF \<and> (in_kernel \<longrightarrow> irq_oracle (Suc (irq_state (machine_state b))) \<notin> non_kernel_IRQs); aa = Some (irq_oracle (Suc (irq_state (machine_state b))))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (((\<lambda>s. (\<Union>a\<in>UNIV \<times> {s}. fst (case a of (irq, s) \<Rightarrow> ({(Some irq, s)}, False)), False)) \<sqinter> (\<lambda>s. ({(None, s)}, False))) (transform b)). case x of (r, t) \<Rightarrow> transform b = t \<and> Some (irq_oracle (Suc (irq_state (machine_state b)))) = r proof (prove)
goal (1 subgoal):
 1. \<And>b aa. \<lbrakk>\<not> irq_masks (machine_state b) (irq_oracle (Suc (irq_state (machine_state b)))) \<and> irq_oracle (Suc (irq_state (machine_state b))) \<noteq> 0x3FF \<and> (in_kernel \<longrightarrow> irq_oracle (Suc (irq_state (machine_state b))) \<notin> non_kernel_IRQs); aa = Some (irq_oracle (Suc (irq_state (machine_state b))))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (((\<lambda>s. (\<Union>a\<in>UNIV \<times> {s}. fst (case a of (irq, s) \<Rightarrow> ({(Some irq, s)}, False)), False)) \<sqinter> (\<lambda>s. ({(None, s)}, False))) (transform b)). case x of (r, t) \<Rightarrow> transform b = t \<and> Some (irq_oracle (Suc (irq_state (machine_state b)))) = r proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma hr_ct_active_and_valid_etcbs:
  "\<lbrace>invs and ct_active and valid_etcbs\<rbrace> Syscall_A.handle_reply \<lbrace>\<lambda>rv. ct_active and valid_etcbs\<rbrace>" by (wp, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and valid_etcbs\<rbrace> Syscall_A.handle_reply \<lbrace>\<lambda>rv. ct_active and valid_etcbs\<rbrace>
theory Syscall_DR

lemma handle_hypervisor_fault_corres:
  "dcorres dc (\<lambda>_. True)
           (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_running and valid_etcbs)
           Syscall_D.handle_hypervisor_fault (do y \<leftarrow> local.handle_hypervisor_fault thread w; return () od)" by (cases w; simp add: Syscall_D.handle_hypervisor_fault_def returnOk_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_running and valid_etcbs) Syscall_D.handle_hypervisor_fault (do y <- local.handle_hypervisor_fault thread w;
return ()
od)
theory Refine_D

lemma handle_event_invs_and_valid_sched:
  "\<lbrace>invs and valid_sched and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)
      and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> Syscall_A.handle_event e
  \<lbrace>\<lambda>rv. invs and valid_sched\<rbrace>" by ((wp he_invs handle_event_valid_sched), clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_sched and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> Syscall_A.handle_event e \<lbrace>\<lambda>rv. invs and valid_sched\<rbrace>
theory Deterministic_AC

lemma list_filter_distr[simp]: "list_filter (list @ list') P = (list_filter list P) @ (list_filter list' P)" apply (induct list,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_filter (list @ list') P = list_filter list P @ list_filter list' P proof (prove)
goal:
No subgoals!
theory Deterministic_AC

lemma list_filter_empty[simp]: "\<forall>x \<in> set list. P x \<Longrightarrow> list_filter list P = []" apply (induct list,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set list. P x \<Longrightarrow> list_filter list P = [] proof (prove)
goal:
No subgoals!
theory Deterministic_AC

lemma list_filter_replace_list: "\<forall>x \<in> set list'. P x \<Longrightarrow> P a \<Longrightarrow>
 filtered_eq P (list_replace_list list a list') list" apply (induct list,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set list'. P x; P a\<rbrakk> \<Longrightarrow> filtered_eq P (list_replace_list list a list') list proof (prove)
goal:
No subgoals!
theory Deterministic_AC

lemma list_filter_insert_after: "P b \<Longrightarrow>
 filtered_eq P (list_insert_after list a b) list" apply (induct list,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P b \<Longrightarrow> filtered_eq P (list_insert_after list a b) list proof (prove)
goal:
No subgoals!
theory Deterministic_AC

lemma list_filter_swap: "P b \<Longrightarrow> P a \<Longrightarrow>
 filtered_eq P (list_swap list a b) list" apply (induct list,(simp add: list_swap_def)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P b; P a\<rbrakk> \<Longrightarrow> filtered_eq P (list_swap list a b) list proof (prove)
goal:
No subgoals!
theory Deterministic_AC

lemma list_filter_replace: "P b \<Longrightarrow> P a \<Longrightarrow>
 filtered_eq P (list_replace list a b) list" apply (induct list,(simp add: list_replace_def)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P b; P a\<rbrakk> \<Longrightarrow> filtered_eq P (list_replace list a b) list proof (prove)
goal:
No subgoals!
theory Deterministic_AC

lemma list_integE:
  assumes hyp: "list_integ P t t'"
  obtains "P x" | "(filtered_eq P (cdt_list t x) (cdt_list t' x))" using hyp list_integ_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P x \<Longrightarrow> thesis; filtered_eq P (cdt_list t x) (cdt_list t' x) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis proof (prove)
using this:
list_integ P t t'
list_integ ?P ?t ?t' \<equiv> \<forall>x. ?P x \<or> filtered_eq ?P (cdt_list ?t x) (cdt_list ?t' x)

goal (1 subgoal):
 1. \<lbrakk>P x \<Longrightarrow> thesis; filtered_eq P (cdt_list t x) (cdt_list t' x) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
theory Deterministic_AC

lemma null_filter: "\<forall>x \<in> set list. \<not> P x \<Longrightarrow> list_filter list P = list" apply (induct list,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set list. \<not> P x \<Longrightarrow> list_filter list P = list proof (prove)
goal:
No subgoals!
theory Deterministic_AC

lemma neq_filtered_ex: "list \<noteq> list' \<Longrightarrow> filtered_eq P list list' \<Longrightarrow> \<exists>x \<in> set list \<union> set list'. P x" apply (rule ccontr) apply (simp add: null_filter) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list \<noteq> list'; filtered_eq P list list'\<rbrakk> \<Longrightarrow> \<exists>x\<in>set list \<union> set list'. P x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list \<noteq> list'; filtered_eq P list list'; \<not> (\<exists>x\<in>set list \<union> set list'. P x)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AC

lemma weaken_filter: "(\<forall>s. P s \<longrightarrow> T s) \<Longrightarrow> filtered_eq T (list_filter list P) list" apply (induct list,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> T s \<Longrightarrow> filtered_eq T (list_filter list P) list proof (prove)
goal:
No subgoals!
theory Deterministic_AC

lemma weaken_filter_eq: "(\<forall>s. P s \<longrightarrow> T s) \<Longrightarrow> filtered_eq P list list' \<Longrightarrow> filtered_eq T list list'" apply (subst weaken_filter[symmetric],assumption) apply (simp add: weaken_filter) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> T s; filtered_eq P list list'\<rbrakk> \<Longrightarrow> filtered_eq T list list' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> T s; filtered_eq P list list'\<rbrakk> \<Longrightarrow> filtered_eq T (list_filter list P) list' proof (prove)
goal:
No subgoals!
theory Types

lemma ptr_range_0[simp]: "ptr_range (p :: obj_ref) 0 = {p}" unfolding ptr_range_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_range p 0 = {p} proof (prove)
goal (1 subgoal):
 1. {p..p + 2 ^ 0 - 1} = {p}
theory ArchAccess

lemma state_vrefs[iff]: "state_vrefs (f s) = state_vrefs s" by (simp add: state_vrefs_def pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_vrefs (f s) = state_vrefs s
theory ArchAccess

lemma arch_update_state_vrefs[simp]:
  "state_vrefs (arch_state_update f s) = state_vrefs s" by (simp add: state_vrefs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_vrefs (arch_state_update f s) = state_vrefs s
theory ArchAccess

lemma (in Arch_arch_update_eq) integrity_asids_update[simp]:
  "integrity_asids aag subjects x a (f st) s = integrity_asids aag subjects x a st s"
  "integrity_asids aag subjects x a st (f s) = integrity_asids aag subjects x a st s" by (auto simp: integrity_asids_def arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_asids aag subjects x a (f st) s = integrity_asids aag subjects x a st s &&& integrity_asids aag subjects x a st (f s) = integrity_asids aag subjects x a st s
theory ArchAccess

lemma integrity_asids_cnode_update':
  "\<lbrakk> kheap st p = Some (CNode sz cs); integrity_asids aag subjects x a st (s\<lparr>kheap := rest\<rparr>) \<rbrakk>
     \<Longrightarrow> integrity_asids aag subjects x a st (s\<lparr>kheap := \<lambda>x. if x = p then v else rest x\<rparr>)" by (simp add: integrity_asids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap st p = Some (CNode sz cs); integrity_asids aag subjects x a st (s\<lparr>kheap := rest\<rparr>)\<rbrakk> \<Longrightarrow> integrity_asids aag subjects x a st (s\<lparr>kheap := \<lambda>x. if x = p then v else rest x\<rparr>)
theory ArchAccess

lemma integrity_asids_tcb_update':
  "\<lbrakk> kheap st p = Some (TCB tcb); integrity_asids aag subjects x a st (s\<lparr>kheap := rest\<rparr>) \<rbrakk>
     \<Longrightarrow> integrity_asids aag subjects x a st (s\<lparr>kheap := \<lambda>x. if x = p then v else rest x\<rparr>)" by (simp add: integrity_asids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap st p = Some (TCB tcb); integrity_asids aag subjects x a st (s\<lparr>kheap := rest\<rparr>)\<rbrakk> \<Longrightarrow> integrity_asids aag subjects x a st (s\<lparr>kheap := \<lambda>x. if x = p then v else rest x\<rparr>)
theory ArchAccess

lemma integrity_asids_ep_update':
  "\<lbrakk> kheap st p = Some (Endpoint ep); integrity_asids aag subjects x a st (s\<lparr>kheap := rest\<rparr>) \<rbrakk>
     \<Longrightarrow> integrity_asids aag subjects x a st (s\<lparr>kheap := \<lambda>x. if x = p then v else rest x\<rparr>)" by (simp add: integrity_asids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap st p = Some (Endpoint ep); integrity_asids aag subjects x a st (s\<lparr>kheap := rest\<rparr>)\<rbrakk> \<Longrightarrow> integrity_asids aag subjects x a st (s\<lparr>kheap := \<lambda>x. if x = p then v else rest x\<rparr>)
theory ArchAccess

lemma integrity_asids_ntfn_update':
  "\<lbrakk> kheap st p = Some (Notification ntfn); integrity_asids aag subjects x a st (s\<lparr>kheap := rest\<rparr>) \<rbrakk>
     \<Longrightarrow> integrity_asids aag subjects x a st (s\<lparr>kheap := \<lambda>x. if x = p then v else rest x\<rparr>)" by (simp add: integrity_asids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap st p = Some (Notification ntfn); integrity_asids aag subjects x a st (s\<lparr>kheap := rest\<rparr>)\<rbrakk> \<Longrightarrow> integrity_asids aag subjects x a st (s\<lparr>kheap := \<lambda>x. if x = p then v else rest x\<rparr>)
theory ArchAccess

lemma integrity_asids_kh_upds':
  "integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> CNode sz cs)\<rparr>) s"
  "integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB tcb)\<rparr>) s"
  "integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> Endpoint ep)\<rparr>) s"
  "integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> Notification ntfn)\<rparr>) s" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> CNode sz cs)\<rparr>) s &&& integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB tcb)\<rparr>) s) &&& integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> Endpoint ep)\<rparr>) s &&& integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> Notification ntfn)\<rparr>) s
theory ArchAccess

lemma integrity_asids_kh_update:
  "integrity_asids aag subject x a (s\<lparr>kheap := kh\<rparr>) (s\<lparr>kheap := kh'\<rparr>)
   \<Longrightarrow> integrity_asids aag subject x a (s\<lparr>kheap := kh(p := v)\<rparr>) (s\<lparr>kheap := kh'(p := v)\<rparr>)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_asids aag subject x a (s\<lparr>kheap := kh\<rparr>) (s\<lparr>kheap := kh'\<rparr>) \<Longrightarrow> integrity_asids aag subject x a (s\<lparr>kheap := kh(p := v)\<rparr>) (s\<lparr>kheap := kh'(p := v)\<rparr>)
theory Access

lemma receive_blocked_on_def2:
  "receive_blocked_on ref ts = ((ref, Receive) \<in> tcb_st_to_auth ts)" by (cases ts, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. receive_blocked_on ref ts = ((ref, Receive) \<in> tcb_st_to_auth ts)
theory Access

lemma send_blocked_on_def2:
  "send_blocked_on ref ts = ((ref, SyncSend) \<in> tcb_st_to_auth ts)" by (cases ts, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. send_blocked_on ref ts = ((ref, SyncSend) \<in> tcb_st_to_auth ts)
theory Access

lemma tro_tagI[intro!]:
  "tro_tag t" unfolding tro_tag_def ..

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tro_tag t proof (prove)
goal (1 subgoal):
 1. True
theory Access

lemma tro_tag_to_prime:
  "tro_tag t = tro_tag' t" unfolding tro_tag_def tro_tag'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tro_tag t = tro_tag' t proof (prove)
goal (1 subgoal):
 1. True = True
theory Access_AC

lemma aag_wellformed_Control:
  "\<lbrakk> (x, Control, y) \<in> aag; policy_wellformed aag mirqs irqs x \<rbrakk> \<Longrightarrow> x = y" unfolding policy_wellformed_def by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, Control, y) \<in> aag; policy_wellformed aag mirqs irqs x\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, Control, y) \<in> aag; (\<forall>agent'. (x, Control, agent') \<in> aag \<longrightarrow> x = agent') \<and> (\<forall>a. (x, a, x) \<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> (x, 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> x = y
theory Access_AC

lemma aag_wellformed_refl:
  "\<lbrakk> policy_wellformed aag mirqs irqs x \<rbrakk> \<Longrightarrow> (x, a, x) \<in> aag" unfolding policy_wellformed_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. policy_wellformed aag mirqs irqs x \<Longrightarrow> (x, a, x) \<in> aag proof (prove)
goal (1 subgoal):
 1. (\<forall>agent'. (x, Control, agent') \<in> aag \<longrightarrow> x = agent') \<and> (\<forall>a. (x, a, x) \<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> (x, 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) \<Longrightarrow> (x, a, x) \<in> aag
theory Access_AC

lemma aag_wellformed_grant_Control_to_recv:
  "\<lbrakk> (s, Grant, ep) \<in> aag; (r, Receive, 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, Grant, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> \<Longrightarrow> (s, Control, r) \<in> aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Grant, 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, Control, r) \<in> aag
theory Access_AC

lemma aag_wellformed_grant_Control_to_send:
  "\<lbrakk> (s, Grant, ep) \<in> aag; (r, Receive, 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, Grant, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> \<Longrightarrow> (r, Control, s) \<in> aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, Grant, 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> (r, Control, s) \<in> aag
theory Access_AC

lemma aag_wellformed_reply:
  "\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
     \<Longrightarrow> (r, Reply, 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; policy_wellformed aag mirqs irqs l\<rbrakk> \<Longrightarrow> (r, Reply, s) \<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> (r, Reply, s) \<in> aag