kings-crown/FVELER_Isabelle huggingface dataset:
theory Access_AC

lemma cdt_change_allowed_to_child:
  "\<lbrakk> cdt_change_allowed aag subjects m tcbsts pptr; m ptr = Some pptr \<rbrakk>
     \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr" apply (elim cdt_change_allowedE) apply (erule cdt_change_allowedI[rotated]) by (fastforce intro: rtrancl_into_rtrancl simp: cdt_parent_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt_change_allowed aag subjects m tcbsts pptr; m ptr = Some pptr\<rbrakk> \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr proof (prove)
goal (1 subgoal):
 1. \<And>pptra. \<lbrakk>m ptr = Some pptr; m \<Turnstile> pptra \<rightarrow>* pptr; cdt_direct_change_allowed aag subjects tcbsts pptra\<rbrakk> \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr proof (prove)
goal (1 subgoal):
 1. \<And>pptra. \<lbrakk>m ptr = Some pptr; m \<Turnstile> pptra \<rightarrow>* pptr\<rbrakk> \<Longrightarrow> m \<Turnstile> pptra \<rightarrow>* ptr
theory Access_AC

lemma trinterrupts_trans:
  "\<lbrakk> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x)
                                              (interrupt_irq_node s' x, interrupt_states s' x));
     (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x)
                                              (interrupt_irq_node s'' x, interrupt_states s'' x)) \<rbrakk>
     \<Longrightarrow> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x)
                                                  (interrupt_irq_node s'' x, interrupt_states s'' x))" apply (simp add: integrity_interrupts_def del: split_paired_All) apply metis done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x)\<rbrakk> \<Longrightarrow> \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. interrupt_irq_node s x = interrupt_irq_node s' x \<and> interrupt_states s x = interrupt_states s' x \<or> pasIRQAbs aag x \<in> subjects; \<forall>x. interrupt_irq_node s' x = interrupt_irq_node s'' x \<and> interrupt_states s' x = interrupt_states s'' x \<or> pasIRQAbs aag x \<in> subjects\<rbrakk> \<Longrightarrow> \<forall>x. interrupt_irq_node s x = interrupt_irq_node s'' x \<and> interrupt_states s x = interrupt_states s'' x \<or> pasIRQAbs aag x \<in> subjects proof (prove)
goal:
No subgoals!
theory Access_AC

lemma trrqs_trans:
  "\<lbrakk> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d)
                                  (ready_queues s d p) (ready_queues s' d p));
     (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d)
                                   (ready_queues s' d p) (ready_queues s'' d p)) \<rbrakk>
     \<Longrightarrow> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d)
                                       (ready_queues s d p) (ready_queues s'' d p))" apply (clarsimp simp: integrity_ready_queues_def) apply (metis append_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p)\<rbrakk> \<Longrightarrow> \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p) proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrakk>\<forall>d. pasDomainAbs aag d \<inter> subjects = {} \<longrightarrow> (\<forall>p. \<exists>threads. threads @ ready_queues s d p = ready_queues s' d p); \<forall>d. pasDomainAbs aag d \<inter> subjects = {} \<longrightarrow> (\<forall>p. \<exists>threads. threads @ ready_queues s' d p = ready_queues s'' d p); pasDomainAbs aag d \<inter> subjects = {}; \<not> pasMayEditReadyQueues aag\<rbrakk> \<Longrightarrow> \<exists>threads. threads @ ready_queues s d p = ready_queues s'' d p proof (prove)
goal:
No subgoals!
theory Access_AC

lemma cdt_direct_change_allowed_backward:
  "\<lbrakk> integrity_obj_state aag activate subjects s s';
     cdt_direct_change_allowed aag subjects (tcb_states_of_state s') ptr \<rbrakk>
     \<Longrightarrow> cdt_direct_change_allowed aag subjects (tcb_states_of_state s) ptr" apply (erule cdt_direct_change_allowed.cases) subgoal by (rule cdca_owned) apply (erule tcb_states_of_state_kheapE) by (drule spec,
      erule integrity_objE, erule cdca_owned;
      (elim exE)?;
      simp;
      rule cdca_reply[rotated], assumption, assumption,
      fastforce elim:tcb_states_of_state_kheapI simp:direct_call_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_state aag activate subjects s s'; cdt_direct_change_allowed aag subjects (tcb_states_of_state s') ptr\<rbrakk> \<Longrightarrow> cdt_direct_change_allowed aag subjects (tcb_states_of_state s) ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>integrity_obj_state aag activate subjects s s'; pasObjectAbs aag (fst ptr) \<in> subjects\<rbrakk> \<Longrightarrow> cdt_direct_change_allowed aag subjects (tcb_states_of_state s) ptr
 2. \<And>tcbst ep. \<lbrakk>integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' (fst ptr) = Some tcbst; direct_call subjects aag ep tcbst; snd ptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cdt_direct_change_allowed aag subjects (tcb_states_of_state s) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_state aag activate subjects s s'; pasObjectAbs aag (fst ptr) \<in> subjects\<rbrakk> \<Longrightarrow> cdt_direct_change_allowed aag subjects (tcb_states_of_state s) ptr proof (prove)
goal (1 subgoal):
 1. \<And>tcbst ep. \<lbrakk>integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' (fst ptr) = Some tcbst; direct_call subjects aag ep tcbst; snd ptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cdt_direct_change_allowed aag subjects (tcb_states_of_state s) ptr proof (prove)
goal (1 subgoal):
 1. \<And>tcbst ep tcb. \<lbrakk>integrity_obj_state aag activate subjects s s'; direct_call subjects aag ep tcbst; snd ptr = tcb_cnode_index 3; kheap s' (fst ptr) = Some (TCB tcb); tcb_state tcb = tcbst\<rbrakk> \<Longrightarrow> cdt_direct_change_allowed aag subjects (tcb_states_of_state s) ptr
theory Access_AC

lemma can_receive_ipc_backward:
  "\<lbrakk> integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' p = Some a;
     can_receive_ipc a; pasObjectAbs aag p \<notin> subjects \<rbrakk>
     \<Longrightarrow> case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x" apply (drule_tac x = p in spec) apply (erule integrity_objE;
         (fastforce simp: tcb_states_of_state_def get_tcb_def
                         call_blocked_def allowed_call_blocked_def
                   split: option.splits kernel_object.splits
         | cases a \<comment> \<open>only split when needed\<close>)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' p = Some a; can_receive_ipc a; pasObjectAbs aag p \<notin> subjects\<rbrakk> \<Longrightarrow> case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_states_of_state s' p = Some a; can_receive_ipc a; pasObjectAbs aag p \<notin> subjects; integrity_obj aag activate subjects (pasObjectAbs aag p) (kheap s p) (kheap s' p)\<rbrakk> \<Longrightarrow> case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x proof (prove)
goal:
No subgoals!
theory Access_AC

lemma integrity_refl [simp]:
  "integrity_subjects S aag activate X s s" unfolding integrity_subjects_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_subjects S aag activate X s s proof (prove)
goal (1 subgoal):
 1. integrity_obj_state aag activate S s s \<and> (\<forall>x. integrity_eobj aag S (pasObjectAbs aag x) (ekheap s x) (ekheap s x)) \<and> integrity_cdt_state aag S s s \<and> integrity_cdt_list_state aag S s s \<and> (\<forall>x. integrity_interrupts aag S x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s x, interrupt_states s x)) \<and> (\<forall>d p. integrity_ready_queues aag S (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s d p)) \<and> (\<forall>x. integrity_mem aag S x (tcb_states_of_state s) (tcb_states_of_state s) (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag S x (tcb_states_of_state s) (tcb_states_of_state s) (device_state (machine_state s) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag S x a s s)
theory Access_AC

lemma set_object_integrity_autarch:
  "\<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace>
   set_object ptr obj
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (wpsimp wp: set_object_wp) apply (rule integrity_update_autarch, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace> set_object ptr obj \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; is_subject aag ptr\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal:
No subgoals!
theory Access_AC

lemma thread_st_auth[iff]: "thread_st_auth (f s) = thread_st_auth s" by (simp add: thread_st_auth_def pspace get_tcb_def swp_def tcb_states_of_state_def)

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

lemma thread_bound_ntfns[iff]: "thread_bound_ntfns (f s) = thread_bound_ntfns s" by (simp add: thread_bound_ntfns_def pspace get_tcb_def swp_def split: option.splits)

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

lemma integrity_update_eq[iff]:
  "tcb_states_of_state (f s) = tcb_states_of_state s" by (simp add: pspace tcb_states_of_state_def get_tcb_def)

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

lemma eintegrity_sa_update[simp]:
  "integrity aag X st (scheduler_action_update f s) = integrity aag X st s" by (simp add: integrity_subjects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity aag X st (scheduler_action_update f s) = integrity aag X st s
theory Access_AC

lemma trans_state_back[simp]:
  "trans_state (\<lambda>_. exst s) s = s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trans_state (\<lambda>_. exst s) s = s
theory Access_AC

lemma all_children_descendants_of:
  "\<lbrakk> all_children P m; p \<in> descendants_of q m; P q \<rbrakk> \<Longrightarrow> P p" apply (simp add: descendants_of_def) apply (erule trancl_induct[where P=P]) apply (unfold cdt_parent_of_def) apply (erule(2) all_childrenD)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>all_children P m; p \<in> descendants_of q m; P q\<rbrakk> \<Longrightarrow> P p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>all_children P m; m \<Turnstile> q \<rightarrow> p; P q\<rbrakk> \<Longrightarrow> P p proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>all_children P m; P q; m \<Turnstile> q \<leadsto> y\<rbrakk> \<Longrightarrow> P y
 2. \<And>y z. \<lbrakk>all_children P m; P q; m \<Turnstile> q \<rightarrow> y; m \<Turnstile> y \<leadsto> z; P y\<rbrakk> \<Longrightarrow> P z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>all_children P m; P q; m y = Some q\<rbrakk> \<Longrightarrow> P y
 2. \<And>y z. \<lbrakk>all_children P m; P q; m \<Turnstile> q \<rightarrow> y; m z = Some y; P y\<rbrakk> \<Longrightarrow> P z proof (prove)
goal:
No subgoals!
theory Access_AC

lemma all_children_parent_of_rtrancl:
  "\<lbrakk> all_children P m; m \<Turnstile> q \<rightarrow>* p; P q \<rbrakk> \<Longrightarrow> P p" by (drule rtranclD, elim conjE disjE; blast dest: all_children_parent_of_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>all_children P m; m \<Turnstile> q \<rightarrow>* p; P q\<rbrakk> \<Longrightarrow> P p
theory Access_AC

lemma caps_of_state_def':
  "caps_of_state s slot =
   (case kheap s (fst slot) of
      Some (TCB tcb) \<Rightarrow> tcb_cnode_map tcb (snd slot)
    | Some (CNode sz content) \<Rightarrow> (if well_formed_cnode_n sz content then content (snd slot) else None)
    | _ \<Rightarrow> None)" by (fastforce simp: caps_of_state_cte_wp_at cte_wp_at_cases2
               split: option.splits kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s slot = (case kheap s (fst slot) of None \<Rightarrow> None | Some (CNode sz content) \<Rightarrow> if well_formed_cnode_n sz content then content (snd slot) else None | Some (TCB tcb) \<Rightarrow> tcb_cnode_map tcb (snd slot) | Some _ \<Rightarrow> None)
theory Access_AC

lemma caps_of_state_cnode:
  "\<lbrakk> kheap s pos = Some (CNode sz content); well_formed_cnode_n sz content\<rbrakk>
     \<Longrightarrow> caps_of_state s (pos,addr) = content addr" by (simp add:caps_of_state_def')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s pos = Some (CNode sz content); well_formed_cnode_n sz content\<rbrakk> \<Longrightarrow> caps_of_state s (pos, addr) = content addr
theory Access_AC

lemma caps_of_state_tcb:
  "kheap s pos = Some (TCB tcb) \<Longrightarrow> caps_of_state s (pos,addr) = tcb_cnode_map tcb addr" by (simp add:caps_of_state_def')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s pos = Some (TCB tcb) \<Longrightarrow> caps_of_state s (pos, addr) = tcb_cnode_map tcb addr
theory Access_AC

lemma tcb_cnode_map_simps[simp]:
  "tcb_cnode_map tcb (tcb_cnode_index 0) = Some (tcb_ctable tcb)"
  "tcb_cnode_map tcb (tcb_cnode_index (Suc 0)) = Some (tcb_vtable tcb)"
  "tcb_cnode_map tcb (tcb_cnode_index 2) = Some (tcb_reply tcb)"
  "tcb_cnode_map tcb (tcb_cnode_index 3) = Some (tcb_caller tcb)"
  "tcb_cnode_map tcb (tcb_cnode_index 4) = Some (tcb_ipcframe tcb)" by (simp_all add: tcb_cnode_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tcb_cnode_map tcb (tcb_cnode_index 0) = Some (tcb_ctable tcb) &&& tcb_cnode_map tcb (tcb_cnode_index (Suc 0)) = Some (tcb_vtable tcb)) &&& tcb_cnode_map tcb (tcb_cnode_index 2) = Some (tcb_reply tcb) &&& tcb_cnode_map tcb (tcb_cnode_index 3) = Some (tcb_caller tcb) &&& tcb_cnode_map tcb (tcb_cnode_index 4) = Some (tcb_ipcframe tcb)
theory Access_AC

lemma parent_of_rtrancl_no_descendant:
  "\<lbrakk> m \<Turnstile> pptr \<rightarrow>* ptr; descendants_of pptr m = {} \<rbrakk> \<Longrightarrow> pptr = ptr" by (fastforce simp add:rtrancl_eq_or_trancl descendants_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> pptr \<rightarrow>* ptr; descendants_of pptr m = {}\<rbrakk> \<Longrightarrow> pptr = ptr
theory Access_AC

lemma tcb_atD:
  "tcb_at ptr s \<Longrightarrow> \<exists>tcb. kheap s ptr = Some (TCB tcb)" by (cases "the (kheap s ptr)";fastforce simp:obj_at_def is_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at ptr s \<Longrightarrow> \<exists>tcb. kheap s ptr = Some (TCB tcb)
theory Access_AC

lemma tcb_atE:
  assumes hyp: "tcb_at ptr s"
  obtains tcb where "kheap s ptr = Some (TCB tcb)" using hyp[THEN tcb_atD] by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. kheap s ptr = Some (TCB tcb) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
\<exists>tcb. kheap s ptr = Some (TCB tcb)

goal (1 subgoal):
 1. (\<And>tcb. kheap s ptr = Some (TCB tcb) \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory Access_AC

lemma tcb_atI:
  "kheap s ptr = Some (TCB tcb) \<Longrightarrow> tcb_at ptr s" by (simp add:obj_at_def is_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s ptr = Some (TCB tcb) \<Longrightarrow> tcb_at ptr s
theory Access_AC

lemma is_transferable_weak_derived:
  "weak_derived cap cap' \<Longrightarrow> is_transferable_cap cap = is_transferable_cap cap'" unfolding is_transferable.simps weak_derived_def copy_of_def same_object_as_def by (fastforce simp: is_cap_simps split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived cap cap' \<Longrightarrow> is_transferable_cap cap = is_transferable_cap cap' proof (prove)
goal (1 subgoal):
 1. (if is_untyped_cap cap' then cap' = cap else (case (cap', cap) of (UntypedCap dev r bits free, x) \<Rightarrow> False | (IRQControlCap, IRQHandlerCap n) \<Rightarrow> False | (IRQControlCap, _) \<Rightarrow> same_region_as cap' cap | (ArchObjectCap ac, ArchObjectCap ac') \<Rightarrow> same_aobject_as ac ac' | (ArchObjectCap ac, _) \<Rightarrow> same_region_as cap' cap | (_, x) \<Rightarrow> same_region_as cap' cap) \<and> is_reply_cap cap' = is_reply_cap cap \<and> is_master_reply_cap cap' = is_master_reply_cap cap) \<and> cap_asid cap = cap_asid cap' \<and> cap_asid_base cap = cap_asid_base cap' \<and> cap_vptr cap = cap_vptr cap' \<or> cap' = cap \<Longrightarrow> (Some cap = None \<or> Some cap = Some NullCap \<or> (\<exists>t R. Some cap = Some (ReplyCap t False R))) = (Some cap' = None \<or> Some cap' = Some NullCap \<or> (\<exists>t R. Some cap' = Some (ReplyCap t False R)))
theory Access_AC

lemma aag_cdt_link_Control:
  "\<lbrakk> cdt s x = Some y; \<not> is_transferable(caps_of_state s x); pas_refined aag s \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag Control (fst y) (fst x)" by (fastforce elim: pas_refined_mem[rotated] sta_cdt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt s x = Some y; \<not> is_transferable_in x s; pas_refined aag s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag
theory Access_AC

lemma aag_cdt_link_DeleteDerived:
  "\<lbrakk> cdt s x = Some y; pas_refined aag s \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag  DeleteDerived (fst y) (fst x)" by (fastforce elim: pas_refined_mem[rotated] sta_cdt_transferable)

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

lemma tcb_states_of_state_to_auth:
  "\<lbrakk> tcb_states_of_state s thread = Some tcbst; pas_refined aag s \<rbrakk>
     \<Longrightarrow> \<forall>(obj,auth) \<in> tcb_st_to_auth tcbst. abs_has_auth_to aag auth thread obj" apply clarsimp apply (erule pas_refined_mem[rotated]) apply (rule sta_ts) apply (simp add:thread_st_auth_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_states_of_state s thread = Some tcbst; pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>(obj, auth)\<in>tcb_st_to_auth tcbst. (pasObjectAbs aag thread, auth, pasObjectAbs aag obj) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>tcb_states_of_state s thread = Some tcbst; pas_refined aag s; (a, b) \<in> tcb_st_to_auth tcbst\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, b, pasObjectAbs aag a) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>tcb_states_of_state s thread = Some tcbst; (a, b) \<in> tcb_st_to_auth tcbst\<rbrakk> \<Longrightarrow> (thread, b, a) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>tcb_states_of_state s thread = Some tcbst; (a, b) \<in> tcb_st_to_auth tcbst\<rbrakk> \<Longrightarrow> (a, b) \<in> thread_st_auth s thread proof (prove)
goal:
No subgoals!
theory Access_AC

lemma tcb_states_of_state_to_auth':
  "\<lbrakk> tcb_states_of_state s thread = Some tcbst;
     pas_refined aag s; (obj,auth) \<in> tcb_st_to_auth tcbst \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag auth thread obj" using tcb_states_of_state_to_auth by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_states_of_state s thread = Some tcbst; pas_refined aag s; (obj, auth) \<in> tcb_st_to_auth tcbst\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, auth, pasObjectAbs aag obj) \<in> pasPolicy aag proof (prove)
using this:
\<lbrakk>tcb_states_of_state ?s ?thread = Some ?tcbst; pas_refined aag ?s\<rbrakk> \<Longrightarrow> \<forall>(obj, auth)\<in>tcb_st_to_auth ?tcbst. (pasObjectAbs aag ?thread, auth, pasObjectAbs aag obj) \<in> pasPolicy aag

goal (1 subgoal):
 1. \<lbrakk>tcb_states_of_state s thread = Some tcbst; pas_refined aag s; (obj, auth) \<in> tcb_st_to_auth tcbst\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, auth, pasObjectAbs aag obj) \<in> pasPolicy aag
theory Access_AC

lemma ep_recv_blocked_def:
  "ep_recv_blocked ep st \<longleftrightarrow> (\<exists>pl. st = BlockedOnReceive ep pl)" by (simp split: thread_state.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_recv_blocked ep st = (\<exists>pl. st = BlockedOnReceive ep pl)
theory Access_AC

lemma owns_thread_owns_cspace:
  "\<lbrakk> is_subject aag thread; pas_refined aag s; get_tcb thread s = Some tcb;
     is_cnode_cap (tcb_ctable tcb); x \<in> obj_refs_ac (tcb_ctable tcb) \<rbrakk>
     \<Longrightarrow> is_subject aag x" apply (drule get_tcb_SomeD) apply (drule cte_wp_at_tcbI[where t="(thread, tcb_cnode_index 0)"
                                and P="\<lambda>cap. cap = tcb_ctable tcb", simplified]) apply (auto simp: cte_wp_at_caps_of_state is_cap_simps cap_auth_conferred_def
              elim: caps_of_state_pasObjectAbs_eq[where p = "(thread, tcb_cnode_index 0)"]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag thread; pas_refined aag s; get_tcb thread s = Some tcb; is_cnode_cap (tcb_ctable tcb); x \<in> obj_refs_ac (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag thread; pas_refined aag s; is_cnode_cap (tcb_ctable tcb); x \<in> obj_refs_ac (tcb_ctable tcb); kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_subject aag thread; pas_refined aag s; is_cnode_cap (tcb_ctable tcb); x \<in> obj_refs_ac (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> tcb_ctable = ?getF2 \<and> (tcb_ctable_update, \<lambda>_ _ _. True) = ?setF2
 2. \<lbrakk>is_subject aag thread; pas_refined aag s; is_cnode_cap (tcb_ctable tcb); x \<in> obj_refs_ac (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> ?getF2 tcb = tcb_ctable tcb
 3. \<lbrakk>is_subject aag thread; pas_refined aag s; is_cnode_cap (tcb_ctable tcb); x \<in> obj_refs_ac (tcb_ctable tcb); cte_wp_at (\<lambda>cap. cap = tcb_ctable tcb) (thread, tcb_cnode_index 0) s\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal:
No subgoals!