kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_AC

lemma cap_insert_pas_refined_same_object_as:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb
                    and cte_wp_at (same_object_as new_cap) src_slot
                    and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and>
                           (\<not> is_master_reply_cap new_cap) \<and> pas_cap_cur_auth aag new_cap)\<rbrace>
   cap_insert new_cap src_slot dest_slot
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (wp cap_insert_pas_refined) apply (clarsimp simp: Option.is_none_def cte_wp_at_caps_of_state) by (fastforce simp: same_object_as_commute is_master_reply_cap_def same_object_as_def
                elim: is_transferable_capE split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and cte_wp_at (same_object_as new_cap) src_slot and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> \<not> is_master_reply_cap new_cap \<and> pas_cap_cur_auth aag new_cap)\<rbrace> cap_insert new_cap src_slot dest_slot \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and cte_wp_at (same_object_as new_cap) src_slot and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> \<not> is_master_reply_cap new_cap \<and> pas_cap_cur_auth aag new_cap)) s \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and (\<lambda>s. is_transferable_in src_slot s \<and> \<not> Option.is_none (cdt s src_slot) \<longrightarrow> is_transferable_cap new_cap) and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)) s proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; is_subject aag (fst dest_slot); caps_of_state s src_slot = Some cap; same_object_as new_cap cap; is_subject aag (fst src_slot); \<not> is_master_reply_cap new_cap; pas_cap_cur_auth aag new_cap; is_transferable_cap cap; cdt s src_slot = Some (a, b)\<rbrakk> \<Longrightarrow> is_transferable_cap new_cap
theory CNode_AC

lemma empty_slot_pas_refined[wp, wp_not_transferable]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_mdb and K (is_subject aag (fst slot))\<rbrace>
   empty_slot slot irqopt
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: empty_slot_def post_cap_deletion_def) apply (wpsimp wp: set_cap_pas_refined get_cap_wp set_cdt_pas_refined
                    tcb_domain_map_wellformed_lift hoare_drop_imps) apply (strengthen aag_wellformed_delete_derived_trans[OF _ _ pas_refined_wellformed, mk_strg I _ _ A]) by (fastforce dest: all_childrenD is_transferable_all_children
                      pas_refined_mem[OF sta_cdt] pas_refined_mem[OF sta_cdt_transferable]
                      pas_refined_Control)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and K (is_subject aag (fst slot))\<rbrace> empty_slot slot irqopt \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and (\<lambda>y. is_subject aag (fst slot))\<rbrace> do cap <- get_cap slot;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- set_cap NullCap slot;
case irqopt of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | ArchObjectCap x \<Rightarrow> arch_post_cap_deletion x | _ \<Rightarrow> return ()
od
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b aa ba. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; cdt s (a, b) = Some slot; (a, b) \<noteq> slot; cdt s slot = Some (aa, ba); slot \<noteq> (aa, ba)\<rbrakk> \<Longrightarrow> (is_transferable_in (a, b) s \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b aa ba. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; cdt s (a, b) = Some slot; (a, b) \<noteq> slot; cdt s slot = Some (aa, ba); slot \<noteq> (aa, ba)\<rbrakk> \<Longrightarrow> (is_transferable_in (a, b) s \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, ?l2.908 s cap a b aa ba) \<in> pasPolicy aag \<and> (?l2.908 s cap a b aa ba, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag
theory CNode_AC

lemma empty_slot_pas_refined_transferable[wp_transferable]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_mdb and (\<lambda>s. is_transferable (caps_of_state s slot))\<rbrace>
   empty_slot slot irqopt
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: empty_slot_def post_cap_deletion_def) apply (wpsimp wp: set_cap_pas_refined get_cap_wp set_cdt_pas_refined
                    tcb_domain_map_wellformed_lift hoare_drop_imps) apply (strengthen aag_wellformed_delete_derived_trans[OF _ _ pas_refined_wellformed, mk_strg I _ _ A]) by (fastforce simp: cte_wp_at_caps_of_state
                dest: all_childrenD is_transferable_all_children
                      pas_refined_mem[OF sta_cdt] pas_refined_mem[OF sta_cdt_transferable])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and is_transferable_in slot\<rbrace> empty_slot slot irqopt \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and is_transferable_in slot\<rbrace> do cap <- get_cap slot;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- set_cap NullCap slot;
case irqopt of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | ArchObjectCap x \<Rightarrow> arch_post_cap_deletion x | _ \<Rightarrow> return ()
od
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b aa ba. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; is_transferable_in slot s; cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; cdt s (a, b) = Some slot; (a, b) \<noteq> slot; cdt s slot = Some (aa, ba); slot \<noteq> (aa, ba)\<rbrakk> \<Longrightarrow> (is_transferable_in (a, b) s \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b aa ba. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; is_transferable_in slot s; cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; cdt s (a, b) = Some slot; (a, b) \<noteq> slot; cdt s slot = Some (aa, ba); slot \<noteq> (aa, ba)\<rbrakk> \<Longrightarrow> (is_transferable_in (a, b) s \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, ?l2.908 s cap a b aa ba) \<in> pasPolicy aag \<and> (?l2.908 s cap a b aa ba, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag
theory CNode_AC

lemma obj_ref_weak_derived:
  "weak_derived cap cap' \<Longrightarrow> obj_refs_ac cap = obj_refs_ac cap'" unfolding obj_refs_def weak_derived_def copy_of_def same_object_as_def by (cases cap; fastforce simp: is_cap_simps aobj_ref'_same_aobject split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived cap cap' \<Longrightarrow> obj_refs_ac cap = obj_refs_ac 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> obj_refs_ac cap = obj_refs_ac cap'
theory CNode_AC

lemma cap_swap_for_delete_pas_refined[wp]:
  "\<lbrace>pas_refined aag and invs and K (is_subject aag (fst slot) \<and> is_subject aag (fst slot'))\<rbrace>
   cap_swap_for_delete slot slot'
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: cap_swap_for_delete_def) apply (wp get_cap_wp | simp)+ apply (clarsimp simp: cte_wp_at_caps_of_state ) apply (fastforce dest!: cap_cur_auth_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and K (is_subject aag (fst slot) \<and> is_subject aag (fst slot'))\<rbrace> cap_swap_for_delete slot slot' \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and (\<lambda>y. is_subject aag (fst slot) \<and> is_subject aag (fst slot'))\<rbrace> when (slot \<noteq> slot') (do cap1 <- get_cap slot;
cap2 <- get_cap slot';
cap_swap cap1 slot cap2 slot'
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> invs s \<and> is_subject aag (fst slot) \<and> is_subject aag (fst slot') \<Longrightarrow> slot \<noteq> slot' \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) slot' s \<longrightarrow> cte_wp_at (weak_derived cap) slot s \<and> cte_wp_at (weak_derived capa) slot' s \<and> pas_cap_cur_auth aag cap \<and> pas_cap_cur_auth aag capa)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>pas_refined aag s; invs s; is_subject aag (fst slot); is_subject aag (fst slot'); slot \<noteq> slot'; caps_of_state s slot = Some cap; caps_of_state s slot' = Some capa\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag cap \<and> pas_cap_cur_auth aag capa proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_endpoint_respects:
  "\<lbrace>integrity aag X st and ep_at epptr and
    K (\<exists>auth. aag_has_auth_to aag auth epptr \<and> auth \<in> {Receive, SyncSend, Reset})\<rbrace>
   set_endpoint 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_ep integrity_asids_kh_upds) done

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

lemma mapM_mapM_x_valid:
  "\<lbrace>P\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv. Q\<rbrace> = \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. Q\<rbrace>" by (simp add: mapM_x_mapM liftM_def[symmetric] hoare_liftM_subst)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv. Q\<rbrace> = \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. Q\<rbrace>
theory CNode_AC

lemma sts_thread_bound_ntfns[wp]:
  "set_thread_state t st \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace>" apply (simp add: set_thread_state_def) apply (wpsimp wp: set_object_wp dxo_wp_weak) apply (clarsimp simp: thread_bound_ntfns_def get_tcb_def
                 split: if_split option.splits kernel_object.splits
                 elim!: rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_thread_state t st \<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);
y <- set_object t (TCB (tcb\<lparr>tcb_state := st\<rparr>));
do_extended_op (set_thread_state_ext t)
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 (y\<lparr>tcb_state := st\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma sts_thread_st_auth[wp]:
  "\<lbrace>\<lambda>s. P ((thread_st_auth s)(t := tcb_st_to_auth st))\<rbrace>
   set_thread_state t st
   \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace>" apply (simp add: set_thread_state_def) apply (wpsimp wp: set_object_wp dxo_wp_weak) apply (clarsimp simp: get_tcb_def thread_st_auth_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((thread_st_auth s)(t := tcb_st_to_auth st))\<rbrace> set_thread_state t st \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((thread_st_auth s)(t := tcb_st_to_auth st))\<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 (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>P ((thread_st_auth s)(t := tcb_st_to_auth st)); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (thread_st_auth (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_state := st\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma sbn_thread_bound_ntfns[wp]:
  "\<lbrace>\<lambda>s. P ((thread_bound_ntfns s)(t := ntfn))\<rbrace>
   set_bound_notification t ntfn
   \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace>" apply (simp add: set_bound_notification_def) apply (wpsimp wp: set_object_wp dxo_wp_weak) apply (clarsimp simp: get_tcb_def thread_bound_ntfns_def
                 elim!: rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((thread_bound_ntfns s)(t := ntfn))\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((thread_bound_ntfns s)(t := ntfn))\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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)(t := ntfn)); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_thread_state_ekheap[wp]:
  "set_thread_state t st \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>" apply (simp add: set_thread_state_def) apply (wpsimp wp: set_scheduler_action_wp simp: set_thread_state_ext_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := st\<rparr>));
set_thread_state_ext t
od \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_simple_ko_tcb_states_of_state[wp]:
  "set_simple_ko f ptr val \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace>" apply (simp add: set_simple_ko_def set_object_def) apply (wp get_object_wp) apply clarify apply (clarsimp simp: thread_st_auth_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 (tcb_states_of_state s)\<rbrace> set_simple_ko f ptr val \<lbrace>\<lambda>_ s. P (tcb_states_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_states_of_state 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 (tcb_states_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (tcb_states_of_state 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 (tcb_states_of_state (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko y koa. \<lbrakk>P (tcb_states_of_state 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 (tcb_states_of_state (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_simple_ko_thread_st_auth[wp]:
  "set_simple_ko f ptr val \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>" apply (simp add: set_simple_ko_def set_object_def) apply (wp get_object_wp) apply clarify apply (clarsimp simp: thread_st_auth_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_st_auth s)\<rbrace> set_simple_ko f ptr val \<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 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_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (thread_st_auth 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_st_auth (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko y koa. \<lbrakk>P (thread_st_auth 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_st_auth (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>)) proof (prove)
goal:
No subgoals!