kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AC

lemma reply_cap_no_children':
  "\<lbrakk> valid_mdb s; caps_of_state s p = Some (ReplyCap t False r) \<rbrakk>
     \<Longrightarrow> \<forall>p'. cdt s p' \<noteq> Some p" using reply_cap_no_children ..

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; caps_of_state s p = Some (ReplyCap t False r)\<rbrakk> \<Longrightarrow> \<forall>p'. cdt s p' \<noteq> Some p proof (prove)
using this:
\<lbrakk>valid_mdb ?s; caps_of_state ?s ?p = Some (ReplyCap ?t False ?r)\<rbrakk> \<Longrightarrow> cdt ?s ?p' \<noteq> Some ?p

goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; caps_of_state s p = Some (ReplyCap t False r)\<rbrakk> \<Longrightarrow> \<forall>p'. cdt s p' \<noteq> Some p
theory Ipc_AC

lemma valid_list_empty:
  "\<lbrakk> valid_list_2 list m; descendants_of slot m = {}\<rbrakk>
     \<Longrightarrow> list slot = []" unfolding valid_list_2_def apply (drule no_children_empty_desc[THEN iffD2]) apply (rule classical) by (fastforce simp del: split_paired_All split_paired_Ex simp add: neq_Nil_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 list m; descendants_of slot m = {}\<rbrakk> \<Longrightarrow> list slot = [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (list p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (list p)); descendants_of slot m = {}\<rbrakk> \<Longrightarrow> list slot = [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (list p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (list p)); \<forall>c. m c \<noteq> Some slot\<rbrakk> \<Longrightarrow> list slot = [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (list p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (list p)); \<forall>c. m c \<noteq> Some slot; list slot \<noteq> []\<rbrakk> \<Longrightarrow> list slot = []
theory Ipc_AC

lemma cte_delete_one_respects_in_ipc_autharch:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and
    valid_list and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace>
   cap_delete_one slot
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" unfolding cap_delete_one_def apply (wp empty_slot_respects_in_ipc_autarch fast_finalise_reply_respects_in_ipc_autarch get_cap_wp) by (fastforce simp:cte_wp_at_caps_of_state is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace> do cap <- get_cap slot;
unless (cap = NullCap) $ do final <- is_final_cap cap;
fast_finalise cap final;
empty_slot slot NullCap
od
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (if cap = NullCap then integrity_tcb_in_ipc aag X receiver epptr ctxt st else (\<lambda>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and K (is_reply_cap cap)) s \<and> valid_mdb s \<and> valid_list s \<and> cte_wp_at is_reply_cap slot s \<and> K (is_subject aag (fst slot)) s)) s
theory Ipc_AC

lemma handle_fault_reply_respects_in_fault_reply:
  "handle_fault_reply f thread label mrs \<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>" by (cases f; wpsimp wp: as_user_respects_in_fault_reply handle_arch_fault_reply_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace> handle_fault_reply f thread label mrs \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>
theory Ipc_AC

lemma emptyable_not_master:
  "\<lbrakk> valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap \<rbrakk>
     \<Longrightarrow> emptyable slot s" apply (rule emptyable_cte_wp_atD[rotated 2]) apply (intro allI impI, assumption) by (fastforce simp:is_cap_simps cte_wp_at_caps_of_state)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> \<forall>cap. ?P cap \<longrightarrow> \<not> is_master_reply_cap cap
 2. \<lbrakk>valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> cte_wp_at ?P slot s
 3. \<lbrakk>valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<not> is_master_reply_cap cap) slot s
 2. \<lbrakk>valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> valid_objs s
theory Ipc_AC

lemma reply_from_kernel_integrity_autarch:
  "\<lbrace>integrity aag X st and pas_refined aag and valid_objs and K (is_subject aag thread)\<rbrace>
   reply_from_kernel thread x
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: reply_from_kernel_def split_def) apply (wpsimp wp: set_message_info_integrity_autarch
                    set_mrs_integrity_autarch as_user_integrity_autarch)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and K (is_subject aag thread)\<rbrace> reply_from_kernel thread x \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and (\<lambda>y. is_subject aag thread)\<rbrace> do buf <- lookup_ipc_buffer True thread;
y <- as_user thread (setRegister badge_register 0);
len <- set_mrs thread buf (snd x);
set_message_info thread (MI len 0 0 (fst x))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchIpc_AC

lemma arch_derive_cap_auth_derived[Ipc_AC_assms]:
  "\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. rv \<noteq> NullCap \<longrightarrow> auth_derived rv (ArchObjectCap acap)\<rbrace>, -" by (case_tac acap;
      simp add: derive_cap_def arch_derive_cap_def;
      wpc?;
      wp?;
      simp add: auth_derived_def cap_auth_conferred_def arch_cap_auth_conferred_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. rv \<noteq> NullCap \<longrightarrow> auth_derived rv (ArchObjectCap acap)\<rbrace>, -
theory ArchIpc_AC

lemma tcb_context_no_change[Ipc_AC_assms]:
  "\<exists>ctxt. tcb = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt (tcb_arch tcb)\<rparr>" apply (cases tcb, clarsimp) apply (case_tac tcb_arch) apply (auto simp: arch_tcb_context_set_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>ctxt. tcb = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt (tcb_arch tcb)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>tcb_ctable tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch more. tcb = \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch, \<dots> = more\<rparr> \<Longrightarrow> \<exists>ctxt. tcb_arch = arch_tcb_context_set ctxt tcb_arch proof (prove)
goal (1 subgoal):
 1. \<And>tcb_ctable tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch more tcb_context. \<lbrakk>tcb = \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch, \<dots> = more\<rparr>; tcb_arch = \<lparr>tcb_context = tcb_context\<rparr>\<rbrakk> \<Longrightarrow> \<exists>ctxt. tcb_arch = arch_tcb_context_set ctxt tcb_arch proof (prove)
goal:
No subgoals!
theory ArchIpc_AC

lemma handle_arch_fault_reply_respects[Ipc_AC_assms]:
  "\<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace>
   handle_arch_fault_reply fault thread x y
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (wpsimp simp: handle_arch_fault_reply_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace> handle_arch_fault_reply fault thread x y \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchIpc_AC

lemma auth_ipc_buffers_kheap_update[Ipc_AC_assms]:
  "\<lbrakk> x \<in> auth_ipc_buffers st thread; kheap st thread = Some (TCB tcb);
     kheap s thread = Some (TCB tcb'); tcb_ipcframe tcb = tcb_ipcframe tcb' \<rbrakk>
     \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread" by (clarsimp simp: auth_ipc_buffers_member_def get_tcb_def caps_of_state_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> auth_ipc_buffers st thread; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); tcb_ipcframe tcb = tcb_ipcframe tcb'\<rbrakk> \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread
theory ArchIpc_AC

lemma auth_ipc_buffers_machine_state_update[Ipc_AC_assms, simp]:
  "auth_ipc_buffers (machine_state_update f s) = auth_ipc_buffers s" by (clarsimp simp: auth_ipc_buffers_def get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. auth_ipc_buffers (machine_state_update f s) = auth_ipc_buffers s
theory ArchIpc_AC

lemma cap_insert_ext_integrity_asids_in_ipc[Ipc_AC_assms, wp]:
  "cap_insert_ext src_parent src_slot dest_slot src_p dest_p
   \<lbrace>\<lambda>s. integrity_asids aag subjects x asid st
          (s\<lparr>kheap := \<lambda>a. if a = receiver then kheap st receiver else kheap s a\<rparr>)\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity_asids aag subjects x asid st (s\<lparr>kheap := \<lambda>a. if a = receiver then kheap st receiver else kheap s a\<rparr>)\<rbrace> cap_insert_ext src_parent src_slot dest_slot src_p dest_p \<lbrace>\<lambda>_ s. integrity_asids aag subjects x asid st (s\<lparr>kheap := \<lambda>a. if a = receiver then kheap st receiver else kheap s a\<rparr>)\<rbrace>
theory Tcb_AC

lemma setup_reply_master_respects:
  "\<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace>
   setup_reply_master t
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp get_cap_wp set_cap_integrity_autarch[unfolded K_def pred_conj_def]
            set_original_integrity_autarch)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace> setup_reply_master t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag t)\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>y. is_subject aag t)) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. (integrity aag X st and K (is_subject aag (fst (t, tcb_cnode_index 2)))) s \<and> is_subject aag (fst (t, tcb_cnode_index 2)) else integrity aag X st) s proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma restart_integrity_autarch:
  "\<lbrace>integrity aag X st and K (is_subject aag t) and einvs and tcb_at t and pas_refined aag\<rbrace>
   restart t
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: restart_def) apply (wp set_thread_state_integrity_autarch setup_reply_master_respects
            hoare_drop_imps
         | simp add: if_apply_def2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag t) and einvs and tcb_at t and pas_refined aag\<rbrace> restart t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag t) and einvs and tcb_at t and pas_refined aag\<rbrace> do state <- get_thread_state t;
when (\<not> runnable state \<and> state \<noteq> IdleThreadState) (do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma cdt_NullCap:
  "\<lbrakk> valid_mdb s; caps_of_state s src = Some NullCap \<rbrakk>
     \<Longrightarrow> cdt s src = None" by (rule ccontr) (force dest: mdb_cte_atD simp: valid_mdb_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; caps_of_state s src = Some NullCap\<rbrakk> \<Longrightarrow> cdt s src = None
theory Tcb_AC

lemma setup_reply_master_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_mdb and K (is_subject aag t)\<rbrace>
   setup_reply_master t
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp get_cap_wp set_cap_pas_refined set_original_wp)+ by (force dest: cdt_NullCap simp: aag_cap_auth_master_Reply cte_wp_at_caps_of_state)

(* 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 t)\<rbrace> setup_reply_master t \<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 t)\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<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 (\<lambda>y. is_subject aag t)) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_transferable_in (t, tcb_cnode_index 2) s \<and> \<not> Option.is_none (cdt s (t, tcb_cnode_index 2)) \<longrightarrow> is_transferable_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<or> (pasObjectAbs aag (fst $ the $ cdt s (t, tcb_cnode_index 2)), Control, pasObjectAbs aag (fst (t, tcb_cnode_index 2))) \<in> pasPolicy aag) and K (aag_cap_auth aag (pasObjectAbs aag (fst (t, tcb_cnode_index 2))) (ReplyCap t True {AllowGrant, AllowWrite}))) (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) else pas_refined aag) s
theory Tcb_AC

lemma restart_pas_refined:
  "\<lbrace>pas_refined aag and invs and tcb_at t and K (is_subject aag t)\<rbrace>
   restart t
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: restart_def get_thread_state_def) apply (wp set_thread_state_pas_refined setup_reply_master_pas_refined thread_get_wp'
         | strengthen invs_mdb
         | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and tcb_at t and K (is_subject aag t)\<rbrace> restart t \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and tcb_at t and (\<lambda>y. is_subject aag t)\<rbrace> do state <- thread_get tcb_state t;
when (\<not> runnable state \<and> state \<noteq> IdleThreadState) (do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma option_update_thread_set_safe_lift:
  "\<lbrakk> \<And>v. \<lbrace>P\<rbrace> thread_set (f v) t \<lbrace>\<lambda>rv. P\<rbrace> \<rbrakk>
     \<Longrightarrow> \<lbrace>P\<rbrace> option_update_thread t f v \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: option_update_thread_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>v. \<lbrace>P\<rbrace> thread_set (f v) t \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> option_update_thread t f v \<lbrace>\<lambda>rv. P\<rbrace>
theory Tcb_AC

lemma set_priority_integrity_autarch[wp]:
 "\<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag tptr)\<rbrace>
  set_priority tptr prio
  \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (simp add: set_priority_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag tptr)\<rbrace> set_priority tptr prio \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Tcb_AC

lemma gts_test[wp]:
   "\<lbrace>\<top>\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. test rv = st_tcb_at test t s\<rbrace>" apply (simp add: get_thread_state_def thread_get_def) apply wp apply (clarsimp simp add: st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. test rv = st_tcb_at test t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do tcb <- gets_the (get_tcb t);
return (tcb_state tcb)
od \<lbrace>\<lambda>rv s. test rv = st_tcb_at test t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> test (tcb_state (the (get_tcb t s))) = st_tcb_at test t s proof (prove)
goal:
No subgoals!
theory Tcb_AC

lemma (in is_extended') valid_cap_syn[wp]: "I (\<lambda>s. valid_cap_syn s a)" by (rule lift_inv, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s \<turnstile> a\<rbrace> f \<lbrace>\<lambda>_ s. s \<turnstile> a\<rbrace>
theory Tcb_AC

lemma (in is_extended') no_cap_to_obj_dr_emp[wp]: "I (no_cap_to_obj_dr_emp a)" by (rule lift_inv, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_dr_emp a\<rbrace> f \<lbrace>\<lambda>_. no_cap_to_obj_dr_emp a\<rbrace>
theory Tcb_AC

lemma (in is_extended') cte_wp_at[wp]: "I (cte_wp_at P a)" by (rule lift_inv, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P a\<rbrace> f \<lbrace>\<lambda>_. cte_wp_at P a\<rbrace>
theory Tcb_AC

lemma checked_insert_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and
    K (\<not> is_master_reply_cap new_cap \<and> is_subject aag target \<and>
         is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)\<rbrace>
   check_cap_at new_cap src_slot
     (check_cap_at (ThreadCap target) slot
        (cap_insert new_cap src_slot (target, ref)))
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (unfold check_cap_at_def) apply (wp cap_insert_pas_refined_same_object_as get_cap_wp) by (fastforce simp: cte_wp_at_caps_of_state)

(* 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 (\<not> is_master_reply_cap new_cap \<and> is_subject aag target \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)\<rbrace> check_cap_at new_cap src_slot (check_cap_at (ThreadCap target) slot (cap_insert new_cap src_slot (target, ref))) \<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 K (\<not> is_master_reply_cap new_cap \<and> is_subject aag target \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)\<rbrace> do cap' <- get_cap src_slot;
when (same_object_as new_cap cap') (do cap' <- get_cap slot;
when (same_object_as (ThreadCap target) cap') (cap_insert new_cap src_slot (target, ref))
od)
od \<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 K (\<not> is_master_reply_cap new_cap \<and> is_subject aag target \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) src_slot s \<longrightarrow> (if same_object_as new_cap cap then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (if same_object_as (ThreadCap target) cap then 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 (target, ref)) \<and> is_subject aag (fst src_slot) \<and> \<not> is_master_reply_cap new_cap \<and> pas_cap_cur_auth aag new_cap) else pas_refined aag) s else pas_refined aag) s
theory Tcb_AC

lemma update_cdt_wp:
  "\<lbrace>\<lambda>s. P (s\<lparr>cdt := m (cdt s)\<rparr>)\<rbrace> update_cdt m \<lbrace>\<lambda>_. P\<rbrace>" by (simp add: update_cdt_def set_cdt_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (s\<lparr>cdt := m (cdt s)\<rparr>)\<rbrace> update_cdt m \<lbrace>\<lambda>_. P\<rbrace>
theory Tcb_AC

lemma parent_ofD: "m \<Turnstile> src \<leadsto> x \<Longrightarrow> m x = Some src" by (simp add: cdt_parent_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> src \<leadsto> x \<Longrightarrow> m x = Some src
theory Tcb_AC

lemma map_le_to_rtrancl:
  "m \<subseteq>\<^sub>m m' \<Longrightarrow> m \<Turnstile> pptr \<rightarrow>* ptr \<Longrightarrow> m' \<Turnstile> pptr \<rightarrow>* ptr" apply (erule subsetD[rotated]) apply (rule rtrancl_mono) apply (fastforce simp:cdt_parent_of_def map_le_def dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<subseteq>\<^sub>m m'; m \<Turnstile> pptr \<rightarrow>* ptr\<rbrakk> \<Longrightarrow> m' \<Turnstile> pptr \<rightarrow>* ptr proof (prove)
goal (1 subgoal):
 1. m \<subseteq>\<^sub>m m' \<Longrightarrow> (cdt_parent_rel m)\<^sup>* \<subseteq> (cdt_parent_rel m')\<^sup>* proof (prove)
goal (1 subgoal):
 1. m \<subseteq>\<^sub>m m' \<Longrightarrow> cdt_parent_rel m \<subseteq> cdt_parent_rel m' proof (prove)
goal:
No subgoals!