kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_AC

lemma set_simple_ko_thread_bound_ntfns[wp]:
  "set_simple_ko f ptr val \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace>" apply (simp add: set_simple_ko_def set_object_def) apply (wp get_object_wp) apply clarify apply (clarsimp simp: thread_bound_ntfns_def obj_at_def get_tcb_def tcb_states_of_state_def
                        partial_inv_def a_type_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: kernel_object.split_asm if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_simple_ko f ptr val \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. partial_inv f obj = Some y);
kobj <- get_object ptr;
y <- assert (a_type kobj = a_type (f val));
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>)
od \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (thread_bound_ntfns s) \<Longrightarrow> \<forall>ko. ko_at ko ptr s \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> (\<forall>ko. ko_at ko ptr s \<longrightarrow> a_type ko = a_type (f val) \<longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko y koa. \<lbrakk>P (thread_bound_ntfns s); ko_at ko ptr s; a_type ko = AEndpoint \<or> a_type ko = ANTFN; partial_inv f ko = Some y; ko_at koa ptr s; a_type koa = a_type (f val)\<rbrakk> \<Longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_simple_ko_ekheap[wp]:
  "set_simple_ko f ptr ep \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>" apply (simp add: set_simple_ko_def) apply (wpsimp wp: get_object_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. partial_inv f obj = Some y);
set_object ptr (f ep)
od \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma sts_st_vrefs[wp]:
  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
   set_thread_state t st
   \<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>" apply (simp add: set_thread_state_def del: set_thread_state_ext_extended.dxo_eq) apply (wpsimp wp: set_object_wp dxo_wp_weak) apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs
                 elim!: rsubst[where P=P, OF _ ext]
                 dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace> set_thread_state t st \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := st\<rparr>));
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pspace_aligned s; valid_vspace_objs s; valid_arch_state s; P (state_vrefs s); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_state := st\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_simple_ko_vrefs[wp]:
  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
   set_simple_ko f ptr (val :: 'b)
   \<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>" apply (simp add: set_simple_ko_def set_object_def) apply (wp get_object_wp) apply (fastforce simp: state_vrefs_simple_type_upd obj_at_def elim!: rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace> set_simple_ko f ptr val \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace> do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. partial_inv f obj = Some y);
kobj <- get_object ptr;
y <- assert (a_type kobj = a_type (f val));
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>)
od \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))) s \<Longrightarrow> \<forall>ko. ko_at ko ptr s \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> (\<forall>ko. ko_at ko ptr s \<longrightarrow> a_type ko = a_type (f val) \<longrightarrow> P (state_vrefs (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>))) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma thread_set_state_vrefs:
  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
   thread_set f t
   \<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>" apply (simp add: thread_set_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs
                 dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pspace_aligned s; valid_vspace_objs s; valid_arch_state s; P (state_vrefs s); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f y))\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma thread_set_thread_st_auth_trivT:
  assumes st: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
  shows "thread_set f t \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>" apply (simp add: thread_set_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: st get_tcb_def thread_st_auth_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: kernel_object.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>P (thread_st_auth s); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f y))\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma thread_set_thread_bound_ntfns_trivT:
  assumes ntfn: "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
  shows "thread_set f t \<lbrace>\<lambda>s :: det_ext state. P (thread_bound_ntfns s)\<rbrace>" apply (simp add: thread_set_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: ntfn get_tcb_def thread_bound_ntfns_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: kernel_object.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>P (thread_bound_ntfns s); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f y))\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma thread_set_pas_refined_triv:
  assumes cps: "\<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f tcb) = getF tcb"
       and st: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
      and ntfn: "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
     shows "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
            thread_set f t \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by (wpsimp wp: tcb_domain_map_wellformed_lift thread_set_state_vrefs
           simp: pas_refined_def state_objs_to_policy_def
      | wps thread_set_caps_of_state_trivial[OF cps]
            thread_set_thread_st_auth_trivT[OF st]
            thread_set_thread_bound_ntfns_trivT[OF ntfn])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> thread_set f t \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory CNode_AC

lemma aag_owned_cdt_link:
  "\<lbrakk> cdt s x = Some y; is_subject aag (fst y);
     pas_refined aag s; \<not> is_transferable (caps_of_state s x) \<rbrakk>
     \<Longrightarrow> is_subject aag (fst x)" by (fastforce dest: sta_cdt pas_refined_mem pas_refined_Control)

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

lemma descendants_of_owned_or_transferable:
  "\<lbrakk> valid_mdb s; pas_refined aag s; p \<in> descendants_of q (cdt s); is_subject aag (fst q) \<rbrakk>
     \<Longrightarrow> is_subject aag (fst p) \<or> is_transferable (caps_of_state s p)" using all_children_descendants_of pas_refined_all_children by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; pas_refined aag s; p \<in> descendants_of q (cdt s); is_subject aag (fst q)\<rbrakk> \<Longrightarrow> is_subject aag (fst p) \<or> is_transferable_in p s proof (prove)
using this:
\<lbrakk>all_children ?P ?m; ?p \<in> descendants_of ?q ?m; ?P ?q\<rbrakk> \<Longrightarrow> ?P ?p
\<lbrakk>valid_mdb ?s; pas_refined ?aag ?s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. is_subject ?aag (fst x) \<or> is_transferable_in x ?s) (cdt ?s)

goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; pas_refined aag s; p \<in> descendants_of q (cdt s); is_subject aag (fst q)\<rbrakk> \<Longrightarrow> is_subject aag (fst p) \<or> is_transferable_in p s
theory CNode_AC

lemma set_ntfn_respects:
  "\<lbrace>integrity aag X st and
    K (\<exists>auth. aag_has_auth_to aag auth epptr \<and> auth \<in> {Receive, Notify, Reset})\<rbrace>
   set_notification epptr ep'
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: set_simple_ko_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def partial_inv_def a_type_def) apply (erule integrity_trans) apply (clarsimp simp: integrity_def tro_ntfn integrity_asids_kh_upds) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> auth \<in> {Receive, Notify, Reset})\<rbrace> set_notification epptr ep' \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. \<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset))\<rbrace> do obj <- get_object epptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Notification y = obj);
kobj <- get_object epptr;
y <- assert (a_type kobj = ANTFN);
s <- get;
put (s\<lparr>kheap := (kheap s)(epptr \<mapsto> Notification ep')\<rparr>)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>y. \<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset))) s \<Longrightarrow> \<forall>ko. ko_at ko epptr s \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (\<exists>y. Notification y = ko) \<longrightarrow> (\<forall>ko. ko_at ko epptr s \<longrightarrow> a_type ko = ANTFN \<longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(epptr \<mapsto> Notification ep')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s auth y. \<lbrakk>integrity aag X st s; (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; auth = Receive \<or> auth = Notify \<or> auth = Reset; kheap s epptr = Some (Notification y)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = epptr then Some (Notification ep') else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s auth y. \<lbrakk>(pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; auth = Receive \<or> auth = Notify \<or> auth = Reset; kheap s epptr = Some (Notification y)\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := \<lambda>a. if a = epptr then Some (Notification ep') else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma sta_ts_mem:
  "\<lbrakk> thread_st_auth s x = S; r \<in> S \<rbrakk> \<Longrightarrow> (x, snd r, fst r) \<in> state_objs_to_policy s" using sta_ts by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>thread_st_auth s x = S; r \<in> S\<rbrakk> \<Longrightarrow> (x, snd r, fst r) \<in> state_objs_to_policy s proof (prove)
using this:
(?oref', ?auth) \<in> thread_st_auth ?s ?oref \<Longrightarrow> (?oref, ?auth, ?oref') \<in> state_objs_to_policy ?s

goal (1 subgoal):
 1. \<lbrakk>thread_st_auth s x = S; r \<in> S\<rbrakk> \<Longrightarrow> (x, snd r, fst r) \<in> state_objs_to_policy s
theory CNode_AC

lemma get_cap_auth_wp:
  "\<lbrace>\<lambda>s. pas_refined aag s \<and> is_subject aag (fst p) \<and>
        (\<forall>cap. caps_of_state s p = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> Q cap s)\<rbrace>
   get_cap p \<lbrace>Q\<rbrace>" apply (wp get_cap_wp) apply clarsimp apply (drule spec, erule mp) apply (fastforce simp: cte_wp_at_caps_of_state dest: cap_cur_auth_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pas_refined aag s \<and> is_subject aag (fst p) \<and> (\<forall>cap. caps_of_state s p = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> Q cap s)\<rbrace> get_cap p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> is_subject aag (fst p) \<and> (\<forall>cap. caps_of_state s p = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> Q cap s) \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> Q cap s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>pas_refined aag s; is_subject aag (fst p); \<forall>cap. caps_of_state s p = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> Q cap s; cte_wp_at ((=) cap) p s\<rbrakk> \<Longrightarrow> Q cap s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>pas_refined aag s; is_subject aag (fst p); cte_wp_at ((=) cap) p s\<rbrakk> \<Longrightarrow> caps_of_state s p = Some cap \<and> pas_cap_cur_auth aag cap proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma get_cap_auth_conferred:
  "\<lbrace>pas_refined aag and K (is_subject aag (fst slot))\<rbrace>
   get_cap slot
   \<lbrace>\<lambda>rv s. \<forall>x\<in>obj_refs_ac rv. \<forall>a \<in> cap_auth_conferred rv. aag_has_auth_to aag a x\<rbrace>" apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule sta_caps, simp+) apply (drule(1) pas_refined_mem) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag (fst slot))\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. \<forall>x\<in>obj_refs_ac rv. \<forall>a\<in>cap_auth_conferred rv. (pasSubject aag, a, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_subject aag (fst slot))) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. \<forall>a\<in>cap_auth_conferred cap. (pasSubject aag, a, pasObjectAbs aag x) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s cap x a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); caps_of_state s slot = Some cap; x \<in> obj_refs_ac cap; a \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (pasSubject aag, a, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s cap x a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); x \<in> obj_refs_ac cap; a \<in> cap_auth_conferred cap; (fst slot, a, x) \<in> state_objs_to_policy s\<rbrakk> \<Longrightarrow> (pasSubject aag, a, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s cap x a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); x \<in> obj_refs_ac cap; a \<in> cap_auth_conferred cap; (pasObjectAbs aag (fst slot), a, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, a, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma cap_auth_conferred_cnode_cap:
  "is_cnode_cap cap \<Longrightarrow> Control \<in> cap_auth_conferred cap" by (clarsimp simp: is_cap_simps cap_auth_conferred_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap cap \<Longrightarrow> Control \<in> cap_auth_conferred cap
theory CNode_AC

lemma UNIV_eq_single_card:
  "(UNIV = {x :: 'a}) \<Longrightarrow> (card (UNIV :: 'a set) = 1)" by (erule ssubst) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UNIV = {x} \<Longrightarrow> CARD('a) = 1
theory CNode_AC

lemma cli_cap_irqs_controlled:
  "(cap_irqs_controlled cap = cap_irqs_controlled cap') \<Longrightarrow>
    cap_links_irq aag (pasSubject aag) cap = cap_links_irq aag (pasSubject aag) cap'" by (auto simp: card_word cap_links_irq_def split: cap.splits
          dest!: UNIV_eq_single_card UNIV_eq_single_card [OF sym])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_irqs_controlled cap = cap_irqs_controlled cap' \<Longrightarrow> cap_links_irq aag (pasSubject aag) cap = cap_links_irq aag (pasSubject aag) cap'
theory CNode_AC

lemma cnode_inv_auth_derivations_If_Insert_Move:
  "cnode_inv_auth_derivations ((if P then MoveCall else InsertCall) cap src_slot dest_slot) =
   cnode_inv_auth_derivations (MoveCall cap src_slot dest_slot)" by (simp add: cnode_inv_auth_derivations_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cnode_inv_auth_derivations ((if P then MoveCall else InsertCall) cap src_slot dest_slot) = cnode_inv_auth_derivations (MoveCall cap src_slot dest_slot)
theory CNode_AC

lemma post_cap_deletion_cur_domain[wp]:
  "post_cap_deletion c \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>" by (wpsimp simp: post_cap_deletion_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> post_cap_deletion c \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
theory CNode_AC

lemma rec_del_cur_domain[wp]:
  "rec_del call \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>" by (rule rec_del_preservation; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> rec_del call \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
theory CNode_AC

lemma cap_revoke_cur_domain[wp]:
  "cap_revoke slot \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>" by (rule cap_revoke_preservation2; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
theory CNode_AC

lemma derive_cap_auth_derived:
  "\<lbrace>\<lambda>s :: det_ext state. cap \<noteq> NullCap \<longrightarrow> cte_wp_at (auth_derived cap) src_slot s\<rbrace>
   derive_cap src_slot cap
   \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (auth_derived rv) src_slot s\<rbrace>, -" apply (wpsimp wp: arch_derive_cap_auth_derived simp: derive_cap_def | wp hoare_drop_imps)+ apply (auto simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap \<noteq> NullCap \<longrightarrow> cte_wp_at (auth_derived cap) src_slot s\<rbrace> derive_cap src_slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (auth_derived rv) src_slot s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. cap \<noteq> NullCap \<longrightarrow> cte_wp_at (auth_derived cap) src_slot s \<Longrightarrow> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> cte_wp_at (auth_derived (UntypedCap x xa xb xc)) src_slot s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> cte_wp_at (auth_derived (EndpointCap x xa xb)) src_slot s) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> cte_wp_at (auth_derived (NotificationCap x xa xb)) src_slot s) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> cte_wp_at (auth_derived (CNodeCap x xa xb)) src_slot s) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> cte_wp_at (auth_derived (ThreadCap x)) src_slot s) \<and> (cap = DomainCap \<longrightarrow> cte_wp_at (auth_derived DomainCap) src_slot s) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> cte_wp_at (auth_derived (IRQHandlerCap x)) src_slot s) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> cte_wp_at (auth_derived (ArchObjectCap x)) src_slot s) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma cap_rights_to_auth_mono:
  "R \<subseteq> R' \<Longrightarrow> cap_rights_to_auth R b \<subseteq> cap_rights_to_auth R' b" by (auto simp add: cap_rights_to_auth_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> R' \<Longrightarrow> cap_rights_to_auth R b \<subseteq> cap_rights_to_auth R' b