kings-crown/FVELER_Isabelle huggingface dataset:
theory Access_AC

lemma cdt_change_allowed_mono:
  "\<lbrakk> cdt_change_allowed aag S (cdt s) (tcb_states_of_state s) ptr; S \<subseteq> T \<rbrakk>
     \<Longrightarrow> cdt_change_allowed aag T (cdt s) (tcb_states_of_state s) ptr" unfolding cdt_change_allowed_def cdt_direct_change_allowed.simps direct_call_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt_change_allowed aag S (cdt s) (tcb_states_of_state s) ptr; S \<subseteq> T\<rbrakk> \<Longrightarrow> cdt_change_allowed aag T (cdt s) (tcb_states_of_state s) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>pptr. cdt s \<Turnstile> pptr \<rightarrow>* ptr \<and> (pasObjectAbs aag (fst pptr) \<in> S \<or> (\<exists>tcbst ep. tcb_states_of_state s (fst pptr) = Some tcbst \<and> (ep_recv_blocked ep tcbst \<and> aag_subjects_have_auth_to S aag Call ep) \<and> snd pptr = tcb_cnode_index 3)); S \<subseteq> T\<rbrakk> \<Longrightarrow> \<exists>pptr. cdt s \<Turnstile> pptr \<rightarrow>* ptr \<and> (pasObjectAbs aag (fst pptr) \<in> T \<or> (\<exists>tcbst ep. tcb_states_of_state s (fst pptr) = Some tcbst \<and> (ep_recv_blocked ep tcbst \<and> aag_subjects_have_auth_to T aag Call ep) \<and> snd pptr = tcb_cnode_index 3))
theory Access_AC

lemma state_objs_to_policy_irq_state_independent[intro!, simp]:
  "state_objs_to_policy (s\<lparr>machine_state :=
                           machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) =
   state_objs_to_policy s" by (simp add: state_objs_to_policy_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_objs_to_policy (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = state_objs_to_policy s
theory Access_AC

lemma tcb_domain_map_wellformed_independent[intro!, simp]:
  "tcb_domain_map_wellformed aag (s\<lparr>machine_state :=
                                    machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) =
   tcb_domain_map_wellformed aag s" by (simp add: tcb_domain_map_wellformed_aux_def get_etcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_domain_map_wellformed aag (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = tcb_domain_map_wellformed aag s
theory Access_AC

lemma integrity_trans_start:
  "(\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. integrity aag X s\<rbrace>)
   \<Longrightarrow> \<lbrace>integrity aag X st and P\<rbrace> f \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding spec_valid_def valid_def using integrity_trans by simp blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. integrity aag X s\<rbrace>) \<Longrightarrow> \<lbrace>integrity aag X st and P\<rbrace> f \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> \<forall>sa. s = sa \<longrightarrow> (\<forall>(r, s')\<in>fst (f sa). integrity aag X s s')) \<Longrightarrow> \<forall>s. (integrity aag X st and P) s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). integrity aag X st s') proof (prove)
using this:
\<lbrakk>integrity_subjects ?subjects aag ?activate ?X ?s ?s'; integrity_subjects ?subjects aag ?activate ?X ?s' ?s''\<rbrakk> \<Longrightarrow> integrity_subjects ?subjects aag ?activate ?X ?s ?s''

goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> \<forall>sa. s = sa \<longrightarrow> (\<forall>(r, s')\<in>fst (f sa). integrity aag X s s')) \<Longrightarrow> \<forall>s. (integrity aag X st and P) s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). integrity aag X st s')
theory Access_AC

lemma wp_integrity_clean:
  "\<lbrakk> \<And>s. Q s \<Longrightarrow> integrity aag X s (g s); \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. integrity aag X st and Q\<rbrace> \<rbrakk>
     \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. integrity aag X st (g s)\<rbrace> " by (rule hoare_post_imp[of "\<lambda>_. integrity aag X st and Q"])
      (fastforce elim: integrity_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. Q s \<Longrightarrow> integrity aag X s (g s); \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. integrity aag X st and Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. integrity aag X st (g s)\<rbrace>
theory ArchAccess_AC

lemma acap_class_reply[Access_AC_assms]:
  "acap_class acap \<noteq> ReplyClass t" by (cases acap; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. acap_class acap \<noteq> ReplyClass t
theory ArchAccess_AC

lemma arch_troa_tro_alt[Access_AC_assms, elim!]:
  "arch_integrity_obj_atomic aag subjects l ko ko'
   \<Longrightarrow> arch_integrity_obj_alt aag subjects l ko ko'" by (fastforce elim: arch_integrity_obj_atomic.cases intro: arch_integrity_obj_alt.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_integrity_obj_atomic aag subjects l ko ko' \<Longrightarrow> arch_integrity_obj_alt aag subjects l ko ko'
theory ArchAccess_AC

lemma clear_asidpool_trans[elim]:
  "\<lbrakk> asid_pool_integrity subjects aag pool pool';
     asid_pool_integrity subjects aag pool' pool'' \<rbrakk>
     \<Longrightarrow> asid_pool_integrity subjects aag pool pool''" unfolding asid_pool_integrity_def by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid_pool_integrity subjects aag pool pool'; asid_pool_integrity subjects aag pool' pool''\<rbrakk> \<Longrightarrow> asid_pool_integrity subjects aag pool pool'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. pool' x \<noteq> pool x \<longrightarrow> pool' x = None \<and> aag_subjects_have_auth_to subjects aag Control (the (pool x)); \<forall>x. pool'' x \<noteq> pool' x \<longrightarrow> pool'' x = None \<and> aag_subjects_have_auth_to subjects aag Control (the (pool' x))\<rbrakk> \<Longrightarrow> \<forall>x. pool'' x \<noteq> pool x \<longrightarrow> pool'' x = None \<and> aag_subjects_have_auth_to subjects aag Control (the (pool x))
theory ArchAccess_AC

lemma cap_asid'_member[simp]:
  "asid \<in> cap_asid' cap = (\<exists>acap. cap = ArchObjectCap acap \<and> asid \<in> acap_asid' acap)" by (cases cap; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (asid \<in> cap_asid' cap) = (\<exists>acap. cap = ArchObjectCap acap \<and> asid \<in> acap_asid' acap)
theory ArchAccess_AC

lemma arch_tro_alt_trans_spec[Access_AC_assms]:
  "\<lbrakk> arch_integrity_obj_alt aag subjects l ko ko';
     arch_integrity_obj_alt aag subjects l ko' ko'' \<rbrakk>
     \<Longrightarrow> arch_integrity_obj_alt aag subjects l ko ko''" by (fastforce simp: arch_integrity_obj_alt.simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_integrity_obj_alt aag subjects l ko ko'; arch_integrity_obj_alt aag subjects l ko' ko''\<rbrakk> \<Longrightarrow> arch_integrity_obj_alt aag subjects l ko ko''
theory ArchAccess_AC

lemma as_user_state_vrefs[Access_AC_assms, wp]:
  "as_user t f \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace>" apply (simp add: as_user_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: state_vrefs_def vs_refs_no_global_pts_def get_tcb_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: option.split_asm Structures_A.kernel_object.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> as_user t f \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa. \<lbrakk>P (state_vrefs s); (x, xa) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory ArchAccess_AC

lemma auth_ipc_buffers_tro[Access_AC_assms]:
  "\<lbrakk> integrity_obj_state aag activate subjects s s';
     x \<in> auth_ipc_buffers s' p; pasObjectAbs aag p \<notin> subjects \<rbrakk>
     \<Longrightarrow> x \<in> auth_ipc_buffers s p " by (drule_tac x = p in spec)
     (erule integrity_objE;
      fastforce simp: tcb_states_of_state_def get_tcb_def auth_ipc_buffers_def
               split: cap.split_asm arch_cap.split_asm if_split_asm bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_state aag activate subjects s s'; x \<in> auth_ipc_buffers s' p; pasObjectAbs aag p \<notin> subjects\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers s p
theory ArchAccess_AC

lemma trasids_trans[Access_AC_assms]:
  "\<lbrakk> (\<forall>x a. integrity_asids aag subjects x a s s');
     (\<forall>x a. integrity_asids aag subjects x a s' s'') \<rbrakk>
     \<Longrightarrow> (\<forall>x a. integrity_asids aag subjects x a s s'')" by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x a. integrity_asids aag subjects x a s s'; \<forall>x a. integrity_asids aag subjects x a s' s''\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag subjects x a s s''
theory ArchAccess_AC

lemma integrity_asids_refl[Access_AC_assms, simp]:
  "integrity_asids aag subjects x a s s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_asids aag subjects x a s s
theory ArchAccess_AC

lemma integrity_asids_update_autarch[Access_AC_assms]:
  "\<lbrakk> \<forall>x a. integrity_asids aag subjects x a st s; is_subject aag ptr \<rbrakk>
     \<Longrightarrow> \<forall>x a. integrity_asids aag subjects x a st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x a. integrity_asids aag subjects x a st s; is_subject aag ptr\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag subjects x a st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)
theory ArchAccess_AC

lemma auth_ipc_buffers_member_def:
  "x \<in> auth_ipc_buffers s p =
   (\<exists>tcb p' R vms xx. get_tcb p s = Some tcb
                   \<and> tcb_ipcframe tcb = (ArchObjectCap (PageCap False p' R vms xx))
                   \<and> caps_of_state s (p, tcb_cnode_index 4) =
                      Some (ArchObjectCap (PageCap False p' R vms xx))
                   \<and> AllowWrite \<in> R
                   \<and> x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms)))
                                    msg_align_bits)" unfolding auth_ipc_buffers_def by (clarsimp simp: caps_of_state_tcb' split: option.splits cap.splits arch_cap.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> auth_ipc_buffers s p) = (\<exists>tcb p' R vms xx. get_tcb p s = Some tcb \<and> tcb_ipcframe tcb = ArchObjectCap (PageCap False p' R vms xx) \<and> caps_of_state s (p, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap False p' R vms xx)) \<and> AllowWrite \<in> R \<and> x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits) proof (prove)
goal (1 subgoal):
 1. (x \<in> (case get_tcb p s of None \<Rightarrow> {} | Some tcb \<Rightarrow> case tcb_ipcframe tcb of ArchObjectCap (PageCap True p' R vms xa) \<Rightarrow> {} | ArchObjectCap (PageCap False p' R vms xa) \<Rightarrow> if AllowWrite \<in> R then ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits else {} | ArchObjectCap _ \<Rightarrow> {} | _ \<Rightarrow> {})) = (\<exists>tcb p' R vms xx. get_tcb p s = Some tcb \<and> tcb_ipcframe tcb = ArchObjectCap (PageCap False p' R vms xx) \<and> caps_of_state s (p, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap False p' R vms xx)) \<and> AllowWrite \<in> R \<and> x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits)
theory ArchAccess_AC

lemma auth_ipc_buffers_member[Access_AC_assms]:
  "\<lbrakk> x \<in> auth_ipc_buffers s p; valid_objs s \<rbrakk>
     \<Longrightarrow> \<exists>tcb acap. get_tcb p s = Some tcb
                  \<and> tcb_ipcframe tcb = (ArchObjectCap acap)
                  \<and> caps_of_state s (p, tcb_cnode_index 4) = Some (ArchObjectCap acap)
                  \<and> Write \<in> arch_cap_auth_conferred acap
                  \<and> x \<in> aobj_ref' acap" by (fastforce simp: auth_ipc_buffers_def caps_of_state_tcb' arch_cap_auth_conferred_def
                      vspace_cap_rights_to_auth_def ipcframe_subset_page
               split: option.splits cap.splits arch_cap.splits bool.splits if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> auth_ipc_buffers s p; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>tcb acap. get_tcb p s = Some tcb \<and> tcb_ipcframe tcb = ArchObjectCap acap \<and> caps_of_state s (p, tcb_cnode_index 4) = Some (ArchObjectCap acap) \<and> Write \<in> arch_cap_auth_conferred acap \<and> x \<in> aobj_ref' acap
theory ArchAccess_AC

lemma asid_pool_integrity_mono[Access_AC_assms]:
  "\<lbrakk> asid_pool_integrity S aag cont cont'; S \<subseteq> T \<rbrakk> \<Longrightarrow> asid_pool_integrity T aag cont cont'" unfolding asid_pool_integrity_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid_pool_integrity S aag cont cont'; S \<subseteq> T\<rbrakk> \<Longrightarrow> asid_pool_integrity T aag cont cont' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. cont' x \<noteq> cont x \<longrightarrow> cont' x = None \<and> aag_subjects_have_auth_to S aag Control (the (cont x)); S \<subseteq> T\<rbrakk> \<Longrightarrow> \<forall>x. cont' x \<noteq> cont x \<longrightarrow> cont' x = None \<and> aag_subjects_have_auth_to T aag Control (the (cont x))
theory ArchAccess_AC

lemma integrity_asids_mono[Access_AC_assms]:
    "\<lbrakk> integrity_asids aag S x a s s'; S \<subseteq> T; pas_refined aag s; valid_objs s \<rbrakk>
       \<Longrightarrow> integrity_asids aag T x a s s'" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_asids aag S x a s s'; S \<subseteq> T; pas_refined aag s; valid_objs s\<rbrakk> \<Longrightarrow> integrity_asids aag T x a s s'
theory ArchAccess_AC

lemma pas_refined_irq_state_independent[intro!, simp]:
  "pas_refined x (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) =
   pas_refined x s" by (simp add: pas_refined_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined x (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = pas_refined x s
theory Dpolicy

lemma transform_asid_rev_transform_mapping [simp]:
  "valid_asid_mapping mapping \<Longrightarrow>
   (transform_asid_rev o fst) ` set_option (transform_mapping mapping) = fst ` set_option mapping" apply (simp add:transform_mapping_def map_option_case) apply (case_tac mapping) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_mapping mapping \<Longrightarrow> (transform_asid_rev \<circ> fst) ` set_option (transform_mapping mapping) = fst ` set_option mapping proof (prove)
goal (1 subgoal):
 1. case mapping of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> asid < 2 ^ local.asid_bits \<Longrightarrow> (\<lambda>x. transform_asid_rev (fst x)) ` set_option (case mapping of None \<Rightarrow> None | Some x \<Rightarrow> Some (transform_asid (fst x), snd x)) = fst ` set_option mapping proof (prove)
goal (2 subgoals):
 1. \<lbrakk>case mapping of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> asid < 2 ^ local.asid_bits; mapping = None\<rbrakk> \<Longrightarrow> (\<lambda>x. transform_asid_rev (fst x)) ` set_option (case mapping of None \<Rightarrow> None | Some x \<Rightarrow> Some (transform_asid (fst x), snd x)) = fst ` set_option mapping
 2. \<And>a. \<lbrakk>case mapping of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> asid < 2 ^ local.asid_bits; mapping = Some a\<rbrakk> \<Longrightarrow> (\<lambda>x. transform_asid_rev (fst x)) ` set_option (case mapping of None \<Rightarrow> None | Some x \<Rightarrow> Some (transform_asid (fst x), snd x)) = fst ` set_option mapping proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma fst_transform_cslot_ptr:
  "fst ptr = fst (transform_cslot_ptr ptr)" apply (case_tac ptr) apply (clarsimp simp:transform_cslot_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst ptr = fst (transform_cslot_ptr ptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b. ptr = (a, b) \<Longrightarrow> fst ptr = fst (transform_cslot_ptr ptr) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma transform_cslot_pre_onto:
  "snd ptr < 2 ^ word_bits \<Longrightarrow> \<exists>ptr'. ptr = transform_cslot_ptr ptr'" apply (rule_tac x="transform_cslot_ptr_rev ptr" in exI) apply (case_tac ptr) apply (clarsimp simp: transform_cslot_ptr_def transform_cslot_ptr_rev_def) apply (clarsimp simp: nat_to_bl_def bin_bl_bin' bintrunc_mod2p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd ptr < 2 ^ word_bits \<Longrightarrow> \<exists>ptr'. ptr = transform_cslot_ptr ptr' proof (prove)
goal (1 subgoal):
 1. snd ptr < 2 ^ word_bits \<Longrightarrow> ptr = transform_cslot_ptr (transform_cslot_ptr_rev ptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>snd ptr < 2 ^ word_bits; ptr = (a, b)\<rbrakk> \<Longrightarrow> ptr = transform_cslot_ptr (transform_cslot_ptr_rev ptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b < 2 ^ word_bits; ptr = (a, b)\<rbrakk> \<Longrightarrow> b = nat (bl_to_bin (the (nat_to_bl word_bits b))) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma is_real_cap_transform:
  "cap = transform_cap cap' \<Longrightarrow> is_real_cap cap" by (auto simp:transform_cap_def is_real_cap_def split:cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap = transform_cap cap' \<Longrightarrow> is_real_cap cap
theory Dpolicy

lemma is_real_cap_infer_tcb_pending_op:
  "is_real_cap (infer_tcb_pending_op a tcb)" by (auto simp:infer_tcb_pending_op_def is_real_cap_def split:Structures_A.thread_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_real_cap (infer_tcb_pending_op a tcb)
theory Dpolicy

lemma is_real_cap_infer_tcb_bound_notification:
  "is_real_cap (infer_tcb_bound_notification a)" by (auto simp: infer_tcb_bound_notification_def is_real_cap_def split: cdl_cap.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_real_cap (infer_tcb_bound_notification a)
theory Dpolicy

lemma valid_sched_etcbs[elim]:
  "valid_sched s \<Longrightarrow> valid_etcbs s" by (simp add: valid_sched_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_sched s \<Longrightarrow> valid_etcbs s
theory Dpolicy

lemma opt_cap_Some_rev:
  "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap \<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr = transform_cslot_ptr ptr'" apply (rule transform_cslot_pre_onto) apply (subst not_le[symmetric]) apply (rule notI) apply (drule_tac ptr=ptr in opt_cap_None_word_bits; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr = transform_cslot_ptr ptr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap\<rbrakk> \<Longrightarrow> snd ptr < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap\<rbrakk> \<Longrightarrow> \<not> 2 ^ word_bits \<le> snd ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; 2 ^ word_bits \<le> snd ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma obj_refs_transform:
  "\<not> (\<exists>x sz i dev. cap = cap.UntypedCap dev x sz i) \<Longrightarrow> obj_refs_ac cap = cdl_obj_refs (transform_cap cap)" apply (case_tac cap; clarsimp) apply (rename_tac arch_cap) apply (case_tac arch_cap; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<nexists>x sz i dev. cap = cap.UntypedCap dev x sz i \<Longrightarrow> obj_refs_ac cap = cdl_obj_refs (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> aobj_ref' x12 = cdl_obj_refs (transform_cap (ArchObjectCap x12)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. cap = ArchObjectCap arch_cap \<Longrightarrow> aobj_ref' arch_cap = cdl_obj_refs (transform_cap (ArchObjectCap arch_cap)) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma untyped_range_transform:
  "(\<exists>x sz i dev. cap = cap.UntypedCap dev x sz i) \<Longrightarrow> untyped_range cap = cdl_obj_refs (transform_cap cap)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x sz i dev. cap = cap.UntypedCap dev x sz i \<Longrightarrow> untyped_range cap = cdl_obj_refs (transform_cap cap)
theory Dpolicy

lemma not_is_bound_ntfn_cap_transform_cap[simp]: "\<not>is_bound_ntfn_cap (transform_cap cn)" apply (case_tac cn; simp add: is_bound_ntfn_cap_def) apply (rename_tac foo) apply (case_tac foo; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_bound_ntfn_cap (transform_cap cn) proof (prove)
goal (1 subgoal):
 1. \<And>x12. cn = ArchObjectCap x12 \<Longrightarrow> \<not> (case transform_cap (ArchObjectCap x12) of BoundNotificationCap a \<Rightarrow> True | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>foo. cn = ArchObjectCap foo \<Longrightarrow> \<not> (case transform_cap (ArchObjectCap foo) of BoundNotificationCap a \<Rightarrow> True | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma idle_thread_no_authority:
  "\<lbrakk> invs s; caps_of_state s ptr = Some cap; auth \<in> cap_auth_conferred cap \<rbrakk> \<Longrightarrow>
     fst ptr \<noteq> idle_thread s" apply (rule notI) apply (drule idle_thread_null_cap, simp+) apply (simp add:cap_auth_conferred_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s ptr = Some cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s ptr = Some cap; auth \<in> cap_auth_conferred cap; fst ptr = idle_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s ptr = Some cap.NullCap; auth \<in> cap_auth_conferred cap.NullCap; fst ptr = idle_thread s; cap = cap.NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma idle_thread_no_untyped_range:
  "\<lbrakk> invs s; caps_of_state s ptr = Some cap; auth \<in> untyped_range cap \<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s" apply (rule notI) apply (drule idle_thread_null_cap, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s ptr = Some cap; auth \<in> untyped_range cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s ptr = Some cap; auth \<in> untyped_range cap; fst ptr = idle_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!