kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AC

lemma complete_signal_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and bound_tcb_at ((=) (Some ntfnptr)) thread\<rbrace>
   complete_signal ntfnptr thread
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: complete_signal_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp set_simple_ko_pas_refined set_thread_state_pas_refined | wpc)+ apply clarsimp done

(* 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 bound_tcb_at ((=) (Some ntfnptr)) thread\<rbrace> complete_signal ntfnptr thread \<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 bound_tcb_at ((=) (Some ntfnptr)) thread\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and bound_tcb_at ((=) (Some ntfnptr)) thread)\<rbrace> case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and bound_tcb_at ((=) (Some ntfnptr)) thread)) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and bound_tcb_at ((=) (Some ntfnptr)) thread)) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> (pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma get_mi_valid':
  "\<lbrace>\<top>\<rbrace> get_message_info a \<lbrace>\<lambda>rv _. valid_message_info rv\<rbrace>" apply (simp add: get_message_info_def) apply (wp, rule hoare_post_imp, rule data_to_message_info_valid) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_message_info a \<lbrace>\<lambda>rv _. valid_message_info rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do x <- as_user a (getRegister msg_info_register);
return (data_to_message_info x)
od \<lbrace>\<lambda>rv _. valid_message_info rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> as_user a (getRegister msg_info_register) \<lbrace>?Q3\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma get_mi_length:
  "\<lbrace>\<top>\<rbrace> get_message_info sender \<lbrace>\<lambda>rv _. unat (mi_length rv) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace>" apply (rule hoare_post_imp [OF _ get_mi_valid']) apply (clarsimp simp: valid_message_info_def msg_align_bits' msg_max_length_def word_le_nat_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_message_info sender \<lbrace>\<lambda>rv _. unat (mi_length rv) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. valid_message_info rv \<Longrightarrow> unat (mi_length rv) < 2 ^ (msg_align_bits - word_size_bits) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma set_extra_badge_integrity_autarch:
  "\<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag thread \<and> ipc_buffer_has_auth aag thread (Some buf)
                             \<and> buffer_cptr_index + n < 2 ^ (msg_align_bits - word_size_bits)\<rbrace>
   set_extra_badge buf badge n
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding set_extra_badge_def by (wp store_word_offs_integrity_autarch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag thread \<and> ipc_buffer_has_auth aag thread (Some buf) \<and> buffer_cptr_index + n < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> set_extra_badge buf badge n \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_subject aag thread \<and> ipc_buffer_has_auth aag thread (Some buf) \<and> buffer_cptr_index + n < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> store_word_offs buf (buffer_cptr_index + n) badge \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Ipc_AC

lemma do_normal_transfer_send_integrity_autarch:
  notes lec_valid_cap[wp del]
  shows
  "\<lbrace>pas_refined aag and integrity aag X st and pspace_aligned and
    valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and
    K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver rbuf
                               \<and> (grant \<longrightarrow> is_subject aag sender))\<rbrace>
   do_normal_transfer sender sbuf endpoint badge grant receiver rbuf
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding do_normal_transfer_def by (wpsimp wp: as_user_integrity_autarch set_message_info_integrity_autarch
                 copy_mrs_pas_refined copy_mrs_integrity_autarch transfer_caps_integrity_autarch
                 lookup_extra_caps_authorised lookup_extra_caps_length get_mi_length get_mi_valid'
                 hoare_weak_lift_imp hoare_vcg_conj_lift hoare_vcg_ball_lift lec_valid_cap')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver rbuf \<and> (grant \<longrightarrow> is_subject aag sender))\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver rbuf \<and> (grant \<longrightarrow> is_subject aag sender))\<rbrace> do mi <- get_message_info sender;
caps <- if grant then lookup_extra_caps sender sbuf mi <catch> K (return []) else return [];
mrs_transferred <- copy_mrs sender sbuf receiver rbuf (mi_length mi);
mi' <- transfer_caps mi caps endpoint receiver rbuf;
set_message_info receiver $ MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi);
as_user receiver $ setRegister badge_register badge
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Ipc_AC

lemma do_fault_transfer_integrity_autarch:
  "\<lbrace>integrity aag X st and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver recv_buf)\<rbrace>
   do_fault_transfer badge sender receiver recv_buf
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding do_fault_transfer_def split_def by (wpsimp wp: as_user_integrity_autarch set_message_info_integrity_autarch
                 set_mrs_integrity_autarch thread_get_wp')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver recv_buf)\<rbrace> do_fault_transfer badge sender receiver recv_buf \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver recv_buf)\<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);
set_message_info receiver $ MI sent 0 0 (fst p);
as_user receiver $ setRegister badge_register badge
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Ipc_AC

lemma set_untyped_cap_as_full_not_untyped:
  "\<lbrace>P and K (\<not> is_untyped_cap cap')\<rbrace>
   set_untyped_cap_as_full cap cap' slot
   \<lbrace>\<lambda>_. P\<rbrace>" unfolding set_untyped_cap_as_full_def apply wp apply (rule hoare_pre_cont) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and K (\<not> is_untyped_cap cap')\<rbrace> set_untyped_cap_as_full cap cap' slot \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and K (\<not> is_untyped_cap cap')\<rbrace> if is_untyped_cap cap \<and> is_untyped_cap cap' \<and> obj_ref_of cap = obj_ref_of cap' \<and> cap_bits_untyped cap = cap_bits_untyped cap' then set_cap (max_free_index_update cap) slot else return () \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (3 subgoals):
 1. is_untyped_cap cap \<and> is_untyped_cap cap' \<and> obj_ref_of cap = obj_ref_of cap' \<and> cap_bits_untyped cap = cap_bits_untyped cap' \<Longrightarrow> \<lbrace>?Q1\<rbrace> set_cap (max_free_index_update cap) slot \<lbrace>\<lambda>_. P\<rbrace>
 2. \<not> (is_untyped_cap cap \<and> is_untyped_cap cap' \<and> obj_ref_of cap = obj_ref_of cap' \<and> cap_bits_untyped cap = cap_bits_untyped cap') \<Longrightarrow> \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>s. (P and K (\<not> is_untyped_cap cap')) s \<Longrightarrow> (is_untyped_cap cap \<and> is_untyped_cap cap' \<and> obj_ref_of cap = obj_ref_of cap' \<and> cap_bits_untyped cap = cap_bits_untyped cap' \<longrightarrow> ?Q1 s) \<and> (\<not> (is_untyped_cap cap \<and> is_untyped_cap cap' \<and> obj_ref_of cap = obj_ref_of cap' \<and> cap_bits_untyped cap = cap_bits_untyped cap') \<longrightarrow> ?R1 s) proof (prove)
goal (2 subgoals):
 1. \<not> (is_untyped_cap cap \<and> is_untyped_cap cap' \<and> obj_ref_of cap = obj_ref_of cap' \<and> cap_bits_untyped cap = cap_bits_untyped cap') \<Longrightarrow> \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. (P and K (\<not> is_untyped_cap cap')) s \<Longrightarrow> (is_untyped_cap cap \<and> is_untyped_cap cap' \<and> obj_ref_of cap = obj_ref_of cap' \<and> cap_bits_untyped cap = cap_bits_untyped cap' \<longrightarrow> False) \<and> (\<not> (is_untyped_cap cap \<and> is_untyped_cap cap' \<and> obj_ref_of cap = obj_ref_of cap' \<and> cap_bits_untyped cap = cap_bits_untyped cap') \<longrightarrow> ?R1 s) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma cap_insert_integrity_autarch_not_untyped:
  "\<lbrace>integrity aag X st and K (\<not> is_untyped_cap cap \<and> is_subject aag (fst dest_slot))\<rbrace>
   cap_insert cap src_slot dest_slot
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: cap_insert_def) apply (wp set_original_integrity_autarch cap_insert_ext_extended.list_integ_lift
            cap_insert_list_integrity update_cdt_fun_upd_integrity_autarch gets_inv
            set_cap_integrity_autarch set_untyped_cap_as_full_not_untyped assert_inv) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (\<not> is_untyped_cap cap \<and> is_subject aag (fst dest_slot))\<rbrace> cap_insert cap src_slot dest_slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. \<not> is_untyped_cap cap \<and> is_subject aag (fst dest_slot))\<rbrace> do src_cap <- get_cap src_slot;
old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src_slot;
y <- set_cap cap dest_slot;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
y <- update_cdt (\<lambda>cdt. cdt(dest_slot := if should_be_parent_of src_cap (is_original src_slot) cap (is_cap_revocable cap src_cap) then Some src_slot else cdt src_slot));
y <- cap_insert_ext (should_be_parent_of src_cap (is_original src_slot) cap (is_cap_revocable cap src_cap)) src_slot dest_slot src_p dest_p;
set_original dest_slot (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>y. \<not> is_untyped_cap cap \<and> is_subject aag (fst dest_slot))) s \<Longrightarrow> ((\<lambda>s. (integrity aag X st and K (is_subject aag (fst dest_slot))) s \<and> K (is_subject aag (fst dest_slot)) s \<and> K (cdt_change_allowed' aag dest_slot st) s \<and> K (is_subject aag (fst dest_slot)) s) and K (\<not> is_untyped_cap cap)) s proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma pred_tcb_atE:
  assumes hyp: "pred_tcb_at proj pred t s"
  obtains tcb where "kheap s t = Some (TCB tcb)" and " pred (proj (tcb_to_itcb tcb))" using hyp by (fastforce elim: obj_atE simp: pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<lbrakk>kheap s t = Some (TCB tcb); pred (proj (tcb_to_itcb tcb))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
pred_tcb_at proj pred t s

goal (1 subgoal):
 1. (\<And>tcb. \<lbrakk>kheap s t = Some (TCB tcb); pred (proj (tcb_to_itcb tcb))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory Ipc_AC

lemma pred_tcb_atI:
  "\<lbrakk> kheap s t = Some (TCB tcb); pred (proj (tcb_to_itcb tcb)) \<rbrakk>
     \<Longrightarrow> pred_tcb_at proj pred t s" by (fastforce simp:pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s t = Some (TCB tcb); pred (proj (tcb_to_itcb tcb))\<rbrakk> \<Longrightarrow> pred_tcb_at proj pred t s
theory Ipc_AC

lemma handle_fault_reply_respects:
  "\<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace>
   handle_fault_reply fault thread x y
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (cases fault; wpsimp wp: as_user_integrity_autarch handle_arch_fault_reply_respects)

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

lemma as_user_respects_in_ipc:
  "\<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>
   as_user thread m
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def) apply (wp gets_the_wp get_wp put_wp mapM_x_wp'
       | wpc
       | simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+ apply (clarsimp simp: st_tcb_def2 tcb_at_def fun_upd_def[symmetric]) apply (auto elim: update_tcb_context_in_ipc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace> as_user thread m \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace> do tcb <- gets_the (get_tcb thread);
(a, uc') <- select_f (m (arch_tcb_context_get (tcb_arch tcb)));
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh thread = Some y);
return (the (kh thread))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return a
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity_tcb_in_ipc aag X thread epptr TRContext st s \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> (\<forall>x\<in>fst (m (arch_tcb_context_get (tcb_arch (the (get_tcb thread s))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap s thread = Some y) \<longrightarrow> a_type (the (kheap s thread)) = ATCB \<longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRContext st (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (the (get_tcb thread s)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb thread s)))\<rparr>)) else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa tcb. \<lbrakk>integrity_tcb_in_ipc aag X thread epptr TRContext st s; (x, xa) \<in> fst (m (arch_tcb_context_get (tcb_arch y))); get_tcb thread s = Some y; kheap s thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRContext st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma set_message_info_respects_in_ipc:
  "\<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>
   set_message_info thread m
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>" unfolding set_message_info_def by (wp as_user_respects_in_ipc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace> set_message_info thread m \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace> as_user thread $ setRegister msg_info_register $ message_info_to_data m \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>
theory Ipc_AC

lemma set_untyped_cap_as_full_integrity_tcb_in_ipc_autarch:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
    K (is_subject aag (fst src_slot))\<rbrace>
   set_untyped_cap_as_full src_cap new_cap src_slot
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" apply (rule hoare_pre) apply (clarsimp simp: set_untyped_cap_as_full_def) apply (intro conjI impI) apply (wp set_cap_respects_in_ipc_autarch | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and K (is_subject aag (fst src_slot))\<rbrace> set_untyped_cap_as_full src_cap new_cap src_slot \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_untyped_cap_as_full src_cap new_cap src_slot \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>
 2. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr TRContext st and K (is_subject aag (fst src_slot))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. (is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap \<longrightarrow> \<lbrace>?Q\<rbrace> set_cap (max_free_index_update src_cap) src_slot \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>) \<and> ((obj_ref_of src_cap = obj_ref_of new_cap \<longrightarrow> is_untyped_cap new_cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped new_cap) \<longrightarrow> \<lbrace>?Q\<rbrace> return () \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>)
 2. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr TRContext st and K (is_subject aag (fst src_slot))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap \<Longrightarrow> \<lbrace>?Q\<rbrace> set_cap (max_free_index_update src_cap) src_slot \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>
 2. obj_ref_of src_cap = obj_ref_of new_cap \<longrightarrow> is_untyped_cap new_cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped new_cap \<Longrightarrow> \<lbrace>?Q\<rbrace> return () \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>
 3. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr TRContext st and K (is_subject aag (fst src_slot))) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma cap_inserintegrity_in_ipc_autarch:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
    K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot))\<rbrace>
   cap_insert new_cap src_slot dest_slot
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: cap_insert_def cong: if_cong) apply (wpsimp wp: set_original_respects_in_ipc_autarch
                    set_untyped_cap_as_full_integrity_tcb_in_ipc_autarch
                    update_cdt_fun_upd_respects_in_ipc_autarch
                    set_cap_respects_in_ipc_autarch get_cap_wp
                    cap_insert_ext_integrity_in_ipc_autarch) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot))\<rbrace> cap_insert new_cap src_slot dest_slot \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> cap_insert new_cap src_slot dest_slot \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> do src_cap <- get_cap src_slot;
old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap new_cap src_slot;
y <- set_cap new_cap dest_slot;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
y <- update_cdt (\<lambda>cdt. cdt(dest_slot := if should_be_parent_of src_cap (is_original src_slot) new_cap (is_cap_revocable new_cap src_cap) then Some src_slot else cdt src_slot));
y <- cap_insert_ext (should_be_parent_of src_cap (is_original src_slot) new_cap (is_cap_revocable new_cap src_cap)) src_slot dest_slot src_p dest_p;
set_original dest_slot (is_cap_revocable new_cap src_cap)
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal:
No subgoals!