kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AC

lemma do_fault_transfer_respects_in_ipc:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
    K ((\<not> is_subject aag receiver \<longrightarrow>
        (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver =
                                                      ptr_range buf' msg_align_bits)) \<and>
       (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace>
   do_fault_transfer badge sender receiver recv_buf
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" apply (simp add: do_fault_transfer_def split_def) apply (wp as_user_respects_in_ipc set_message_info_respects_in_ipc set_mrs_respects_in_ipc
         | wpc | simp | rule hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and K ((pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace> do_fault_transfer badge sender receiver recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and (\<lambda>y. (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace> do fault <- thread_get tcb_fault sender;
f <- case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- make_fault_msg f sender;
sent <- set_mrs receiver recv_buf (snd p);
y <- set_message_info receiver (MI sent 0 0 (fst p));
as_user receiver (setRegister badge_register badge)
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma do_ipc_transfer_respects_in_ipc:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and
    pspace_aligned and valid_vspace_objs and valid_arch_state and
    valid_objs and valid_mdb and st_tcb_at can_receive_ipc receiver and
    (\<lambda>s. grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace>
   do_ipc_transfer sender epopt badge grant receiver
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" apply (simp add: do_ipc_transfer_def) apply (wp do_normal_transfer_respects_in_ipc do_fault_transfer_respects_in_ipc
            lookup_ipc_buffer_ptr_range_in_ipc lookup_ipc_buffer_aligned hoare_vcg_conj_lift
         | wpc | simp | rule hoare_drop_imps)+ apply (auto intro: st_tcb_at_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and st_tcb_at can_receive_ipc receiver and (\<lambda>s. grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace> do_ipc_transfer sender epopt badge grant receiver \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and st_tcb_at can_receive_ipc receiver and (\<lambda>s. grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace> do recv_buffer <- lookup_ipc_buffer True receiver;
fault <- thread_get tcb_fault sender;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False sender;
do_normal_transfer sender send_buffer epopt badge grant receiver recv_buffer
od | Some f \<Rightarrow> do_fault_transfer badge sender receiver recv_buffer
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity_tcb_in_ipc aag X receiver epptr TRContext st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc receiver s \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<Longrightarrow> integrity_tcb_in_ipc aag ?X82 receiver ?epptr82 ?tst82 st s \<and> integrity_tcb_in_ipc aag ?X87 receiver ?epptr87 ?tst87 st s proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma sts_ext_running_noop:
  "\<lbrace>P and st_tcb_at (runnable) receiver\<rbrace> set_thread_state_ext receiver \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: set_thread_state_ext_def get_thread_state_def thread_get_def
         | wp set_scheduler_action_wp)+ apply (clarsimp simp add: st_tcb_at_def obj_at_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and st_tcb_at runnable receiver\<rbrace> set_thread_state_ext receiver \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<and> st_tcb_at runnable receiver s \<Longrightarrow> \<not> runnable (tcb_state (the (get_tcb receiver s))) \<and> cur_thread s = receiver \<and> scheduler_action s = resume_cur_thread \<longrightarrow> (\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> P (scheduler_action_update (\<lambda>_. choose_new_thread) s) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma set_thread_state_running_respects_in_ipc:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
    st_tcb_at(receive_blocked_on epptr) receiver and K (aag_has_auth_to aag SyncSend epptr)\<rbrace>
   set_thread_state receiver Running
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st\<rbrace>" apply (simp add: set_thread_state_def) apply (wpsimp wp: set_object_wp sts_ext_running_noop) apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def
                    get_tcb_rev update_tcb_state_in_ipc
              cong: if_cong elim: update_tcb_state_in_ipc[unfolded fun_upd_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and st_tcb_at (receive_blocked_on epptr) receiver and K ((pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)\<rbrace> set_thread_state receiver Running \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and st_tcb_at (receive_blocked_on epptr) receiver and (\<lambda>y. (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)\<rbrace> do tcb <- gets_the (get_tcb receiver);
y <- set_object receiver (TCB (tcb\<lparr>tcb_state := Running\<rparr>));
set_thread_state_ext receiver
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>integrity_tcb_in_ipc aag X receiver epptr TRContext st s; st_tcb_at (receive_blocked_on epptr) receiver s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; get_tcb receiver s = Some y\<rbrakk> \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (y\<lparr>tcb_state := Running\<rparr>))\<rparr>) \<and> st_tcb_at runnable receiver (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (y\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma integrity_tcb_in_ipc_refl:
  "\<lbrakk> st_tcb_at can_receive_ipc receiver s; \<not> is_subject aag receiver; pas_refined aag s \<rbrakk>
     \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRContext s s" unfolding integrity_tcb_in_ipc_def apply (clarsimp simp: st_tcb_def2) apply (rule tii_context [OF get_tcb_SomeD get_tcb_SomeD], assumption+) apply (rule tcb_context_no_change) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at can_receive_ipc receiver s; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s\<rbrakk> \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRContext s s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at can_receive_ipc receiver s; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s\<rbrakk> \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag s \<and> integrity aag X s (s\<lparr>kheap := (kheap s)(receiver := kheap s receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers s receiver then underlying_memory (machine_state s) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap s receiver) (kheap s receiver) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; get_tcb receiver s = Some tcb; can_receive_ipc (tcb_state tcb)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap s receiver) (kheap s receiver) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; get_tcb receiver s = Some tcb; can_receive_ipc (tcb_state tcb)\<rbrakk> \<Longrightarrow> \<exists>ctxt'. tcb = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>
 2. \<And>tcb. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; get_tcb receiver s = Some tcb; can_receive_ipc (tcb_state tcb)\<rbrakk> \<Longrightarrow> TRContext = TRContext proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag s; get_tcb receiver s = Some tcb; can_receive_ipc (tcb_state tcb)\<rbrakk> \<Longrightarrow> TRContext = TRContext proof (prove)
goal:
No subgoals!
theory Ipc_AC

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

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

lemma spec_valid_direct:
  "(P s \<Longrightarrow> s \<turnstile> \<lbrace>\<top>\<rbrace> f \<lbrace> Q \<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" by (simp add: spec_valid_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P s \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>
theory Ipc_AC

lemma cap_insert_reply_cap_respects_in_ipc:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and
    K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and>
       is_subject aag caller \<and> is_subject aag (fst master_slot))\<rbrace>
   cap_insert (ReplyCap caller False R) master_slot (receiver, tcb_cnode_index 3)
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>" unfolding cap_insert_def by (wpsimp wp: set_original_respects_in_ipc_reply cap_insert_ext_integrity_in_ipc_reply
                 update_cdt_reply_in_ipc set_cap_respects_in_ipc_reply
                 set_untyped_cap_as_full_not_untyped get_cap_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller \<and> is_subject aag (fst master_slot))\<rbrace> cap_insert (ReplyCap caller False R) master_slot (receiver, tcb_cnode_index 3) \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller \<and> is_subject aag (fst master_slot))\<rbrace> do src_cap <- get_cap master_slot;
dest_original <- return $ is_cap_revocable (ReplyCap caller False R) src_cap;
old_cap <- get_cap (receiver, tcb_cnode_index 3);
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap (ReplyCap caller False R) master_slot;
set_cap (ReplyCap caller False R) (receiver, tcb_cnode_index 3);
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original master_slot) (ReplyCap caller False R) dest_original;
src_p <- gets (\<lambda>s. cdt s master_slot);
dest_p <- gets (\<lambda>s. cdt s (receiver, tcb_cnode_index 3));
update_cdt (\<lambda>cdt. cdt((receiver, tcb_cnode_index 3) := if src_parent then Some master_slot else cdt master_slot));
do_extended_op (cap_insert_ext src_parent master_slot (receiver, tcb_cnode_index 3) src_p dest_p);
set_original (receiver, tcb_cnode_index 3) dest_original
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>
theory Ipc_AC

lemma exists_cons_append:
  "\<exists>xs. xs @ ys = zs \<Longrightarrow> \<exists>xs. xs @ ys = z # zs" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>xs. xs @ ys = zs \<Longrightarrow> \<exists>xs. xs @ ys = z # zs
theory Ipc_AC

lemma setup_caller_cap_respects_in_ipc_reply:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and
    K (is_subject aag sender \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st)\<rbrace>
   setup_caller_cap sender receiver grant
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>" unfolding setup_caller_cap_def by (wpsimp wp: cap_insert_reply_cap_respects_in_ipc set_thread_state_respects_in_ipc_autarch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and K (is_subject aag sender \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st)\<rbrace> setup_caller_cap sender receiver grant \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and K (is_subject aag sender \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st)\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>
theory Ipc_AC

lemma valid_tcb_fault_update:
  "\<lbrakk> valid_tcb p t s; valid_fault fault \<rbrakk> \<Longrightarrow> valid_tcb p (t\<lparr>tcb_fault := Some fault\<rparr>) s" by (simp add: valid_tcb_def ran_tcb_cap_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_tcb p t s; valid_fault fault\<rbrakk> \<Longrightarrow> valid_tcb p (t\<lparr>tcb_fault := Some fault\<rparr>) s
theory Ipc_AC

lemma thread_set_fault_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
   thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by (wpsimp wp: send_ipc_pas_refined thread_set_pas_refined
                 thread_set_refs_trivial thread_set_obj_at_impossible)

(* 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 (tcb_fault_update (\<lambda>_. Some fault)) thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory Ipc_AC

lemma obj_at_conj_distrib:
  "obj_at (\<lambda>ko. P ko \<and> Q ko) p s = (obj_at (\<lambda>ko. P ko) p s \<and> obj_at (\<lambda>ko. Q ko) p s)" by (auto simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>ko. P ko \<and> Q ko) p s = (obj_at P p s \<and> obj_at Q p s)
theory Ipc_AC

lemma handle_fault_integrity_autarch:
  "\<lbrace>pas_refined aag and integrity aag X st and is_subject aag \<circ> cur_thread and invs
                    and K (valid_fault fault) and K (is_subject aag thread)\<rbrace>
   handle_fault thread fault
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: handle_fault_def) apply (wp set_thread_state_integrity_autarch send_fault_ipc_integrity_autarch
         | simp add: handle_double_fault_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and is_subject aag \<circ> cur_thread and invs and K (valid_fault fault) and K (is_subject aag thread)\<rbrace> handle_fault thread fault \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and is_subject aag \<circ> cur_thread and invs and (\<lambda>y. valid_fault fault) and (\<lambda>y. is_subject aag thread)\<rbrace> do _ <- gets_the (get_tcb thread);
send_fault_ipc thread fault <catch> handle_double_fault thread fault
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma tcb_st_to_auth_Restart_Inactive [simp]:
  "tcb_st_to_auth (if P then Restart else Inactive) = {}" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_st_to_auth (if P then Restart else Inactive) = {}
theory Ipc_AC

lemma fault_tcb_atI:
  "\<lbrakk>kheap s ptr = Some (TCB tcb); P (tcb_fault tcb) \<rbrakk> \<Longrightarrow> fault_tcb_at P ptr s" by (fastforce simp:pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some (TCB tcb); P (tcb_fault tcb)\<rbrakk> \<Longrightarrow> fault_tcb_at P ptr s
theory Ipc_AC

lemma fault_tcb_atE:
  assumes hyp: "fault_tcb_at P ptr s"
  obtains tcb where "kheap s ptr = Some (TCB tcb)" and "P (tcb_fault tcb)" using hyp by (fastforce simp: pred_tcb_at_def elim: obj_atE)

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

goal (1 subgoal):
 1. (\<And>tcb. \<lbrakk>kheap s ptr = Some (TCB tcb); P (tcb_fault tcb)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory Ipc_AC

lemma set_thread_state_running_respects_in_ipc_reply:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
    st_tcb_at awaiting_reply receiver and fault_tcb_at ((=) None) receiver and
    K (aag_has_auth_to aag Reply receiver)\<rbrace>
   set_thread_state receiver Running
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp sts_ext_running_noop) apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def
              cong: if_cong
             elim!: fault_tcb_atE elim: update_tcb_state_in_ipc_reply[unfolded fun_upd_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and st_tcb_at awaiting_reply receiver and fault_tcb_at ((=) None) receiver and K ((pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag)\<rbrace> set_thread_state receiver Running \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and st_tcb_at awaiting_reply receiver and fault_tcb_at ((=) None) receiver and (\<lambda>y. (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag)\<rbrace> do tcb <- gets_the (get_tcb receiver);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh receiver = Some y);
return (the (kh receiver))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (tcb\<lparr>tcb_state := Running\<rparr>))\<rparr>)
od;
set_thread_state_ext receiver
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr TRContext st and st_tcb_at awaiting_reply receiver and fault_tcb_at ((=) None) receiver and (\<lambda>y. (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag)) s \<Longrightarrow> get_tcb receiver s \<noteq> None \<longrightarrow> (\<exists>y. kheap s receiver = Some y) \<longrightarrow> a_type (the (kheap s receiver)) = ATCB \<longrightarrow> (integrity_tcb_in_ipc aag X receiver epptr TRFinal st and st_tcb_at runnable receiver) (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (the (get_tcb receiver s)\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma fast_finalise_reply_respects_in_ipc_autarch:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and K (is_reply_cap cap)\<rbrace>
   fast_finalise cap final
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>" by (rule hoare_gen_asm) (fastforce simp: is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and K (is_reply_cap cap)\<rbrace> fast_finalise cap final \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>
theory Ipc_AC

lemma empty_slot_list_integrity':
  notes split_paired_All[simp del]
  shows "\<lbrace>list_integ P st and (\<lambda>s . cdt_list s slot = []) and K (P slot)\<rbrace>
         empty_slot_ext slot slot_p
         \<lbrace>\<lambda>_. list_integ P st\<rbrace>" apply (simp add: empty_slot_ext_def split del: if_split) apply (wp update_cdt_list_wp) apply (fastforce simp: list_filter_replace_list list_integ_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>list_integ P st and (\<lambda>s. cdt_list s slot = []) and K (P slot)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_. list_integ P st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>list_integ P st and (\<lambda>s. cdt_list s slot = []) and (\<lambda>y. P slot)\<rbrace> update_cdt_list (\<lambda>list. case slot_p of None \<Rightarrow> list(slot := []) | Some p \<Rightarrow> if p = slot then list(slot := list_remove (list slot) slot) else list(p := list_replace_list (list p) slot (list slot), slot := [])) \<lbrace>\<lambda>_. list_integ P st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (list_integ P st and (\<lambda>s. cdt_list s slot = []) and (\<lambda>y. P slot)) s \<Longrightarrow> list_integ P st (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> (cdt_list s)(slot := []) | Some p \<Rightarrow> if p = slot then (cdt_list s)(slot := list_remove (cdt_list s slot) slot) else (cdt_list s)(p := list_replace_list (cdt_list s p) slot (cdt_list s slot), slot := [])) s) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma tcb_state_of_states_cdt_update_behind_kheap[simp]:
  "tcb_states_of_state (kheap_update g (cdt_update f s)) = tcb_states_of_state (kheap_update g s)" by (simp add: tcb_states_of_state_def get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_states_of_state (kheap_update g (cdt_update f s)) = tcb_states_of_state (kheap_update g s)