kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_IF

lemma send_blocked_threads_have_SyncSend_auth:
  "\<lbrakk> pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); st_tcb_at (send_blocked_on ep) x s \<rbrakk>
     \<Longrightarrow> (pasObjectAbs aag x, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag" apply (drule_tac auth="SyncSend" and x=x in pas_refined_mem[rotated]) apply (rule sta_ts) apply (clarsimp simp: thread_st_auth_def split: option.split simp: tcb_states_of_state_def st_tcb_def2) apply (case_tac "tcb_state tcb", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); st_tcb_at (send_blocked_on ep) x s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); st_tcb_at (send_blocked_on ep) x s\<rbrakk> \<Longrightarrow> (x, SyncSend, ?y) \<in> state_objs_to_policy s
 2. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); st_tcb_at (send_blocked_on ep) x s; (pasObjectAbs aag x, SyncSend, pasObjectAbs aag ?y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); st_tcb_at (send_blocked_on ep) x s\<rbrakk> \<Longrightarrow> (?y, SyncSend) \<in> thread_st_auth s x
 2. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); st_tcb_at (send_blocked_on ep) x s; (pasObjectAbs aag x, SyncSend, pasObjectAbs aag ?y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); get_tcb x s = Some tcb; send_blocked_on ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> (?y, SyncSend) \<in> tcb_st_to_auth (tcb_state tcb)
 2. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); st_tcb_at (send_blocked_on ep) x s; (pasObjectAbs aag x, SyncSend, pasObjectAbs aag ?y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma get_thread_state_reads_respects:
  "reads_respects aag l (\<lambda>s. aag_can_read aag t \<or> aag_can_affect aag l t) (get_thread_state t)" unfolding get_thread_state_def apply (rule equiv_valid_guard_imp) apply (wp thread_get_reads_respects | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. aag_can_read_or_affect aag l t) (get_thread_state t) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. aag_can_read_or_affect aag l t) (thread_get tcb_state t) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (thread_get tcb_state t)
 2. \<And>s. aag_can_read_or_affect aag l t \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma send_endpoint_reads_affects_queued:
  "\<lbrakk> (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag;
     auth \<in> {Receive,Reset};
     aag_can_read aag epptr \<or> aag_can_affect aag l epptr;
     pas_refined aag s; valid_objs s; sym_refs (state_refs_of s);
     ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list; x \<in> set list \<rbrakk>
     \<Longrightarrow> aag_can_read aag x \<or> aag_can_affect aag l x" apply (frule send_endpoint_threads_blocked, (simp | assumption)+) apply (drule send_blocked_threads_have_SyncSend_auth, (simp | assumption)+) apply (auto dest: read_sync_ep_read_senders) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; auth \<in> {Receive, Reset}; aag_can_read_or_affect aag l epptr; pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list; x \<in> set list\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; auth = Receive \<or> auth = Reset; aag_can_read_or_affect aag l epptr; pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list; x \<in> set list; st_tcb_at (send_blocked_on epptr) x s\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; auth = Receive \<or> auth = Reset; aag_can_read_or_affect aag l epptr; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list; x \<in> set list; st_tcb_at (send_blocked_on epptr) x s; (pasObjectAbs aag x, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma get_cap_ret_is_subject':
  "\<lbrace>pas_refined aag and K (is_subject aag (fst ptr))\<rbrace>
   get_cap ptr
   \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> (\<forall>x\<in>obj_refs_ac rv. is_subject aag x)\<rbrace>" apply (rule hoare_strengthen_post[OF get_cap_ret_is_subject]) apply (clarsimp simp: is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag (fst ptr))\<rbrace> get_cap ptr \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> (\<forall>x\<in>obj_refs_ac rv. is_subject aag x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv) \<Longrightarrow> is_cnode_cap rv \<longrightarrow> (\<forall>x\<in>obj_refs_ac rv. is_subject aag x) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma get_receive_slots_rev:
  "reads_equiv_valid_inv A aag
     (pas_refined aag and (K (is_subject aag thread \<and>
                              ipc_buffer_has_read_auth aag (pasSubject aag) buf)))
     (get_receive_slots thread buf)" apply (case_tac buf) apply (fastforce intro: return_ev_pre) apply (simp add: lookup_cap_def split_def
         | wp empty_on_failure_ev unify_failure_ev lookup_slot_for_cnode_op_rev get_cap_rev
              lookup_slot_for_thread_rev lookup_slot_for_thread_authorised
              get_cap_ret_is_subject get_cap_ret_is_subject' load_cap_transfer_rev
         | wp (once) hoare_drop_imps
         | strengthen aag_can_read_self)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf)) (get_receive_slots thread buf) proof (prove)
goal (2 subgoals):
 1. buf = None \<Longrightarrow> reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf)) (get_receive_slots thread buf)
 2. \<And>a. buf = Some a \<Longrightarrow> reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf)) (get_receive_slots thread buf) proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf)) (get_receive_slots thread buf) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma transfer_caps_reads_respects:
  "reads_respects aag l
     (pas_refined aag and pspace_aligned and valid_vspace_objs
                      and valid_arch_state and valid_mdb and valid_objs
                      and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap
                                             \<and> is_subject aag (fst (snd cap))
                                             \<and> pas_cap_cur_auth aag (fst cap)
                                             \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp = fst cap)
                                                         (snd cap) s))
                      and K (is_subject aag receiver \<and>
                             ipc_buffer_has_read_auth aag (pasSubject aag) receive_buffer))
     (transfer_caps mi caps endpoint receiver receive_buffer)" unfolding transfer_caps_def fun_app_def by (wp transfer_caps_loop_reads_respects get_receive_slots_rev
         get_receive_slots_authorised hoare_vcg_all_lift hoare_weak_lift_imp
      | wpc | simp add: ball_conj_distrib)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp = fst cap) (snd cap) s) and K (is_subject aag receiver \<and> ipc_buffer_has_read_auth aag (pasSubject aag) receive_buffer)) (transfer_caps mi caps endpoint receiver receive_buffer) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. \<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp = fst cap) (snd cap) s) and K (is_subject aag receiver \<and> ipc_buffer_has_read_auth aag (pasSubject aag) receive_buffer)) (do dest_slots <- get_receive_slots receiver receive_buffer;
mi' <- return (MI (mi_length mi) 0 0 (mi_label mi));
case receive_buffer of None \<Rightarrow> return mi' | Some receive_buffer \<Rightarrow> transfer_caps_loop endpoint receive_buffer 0 caps dest_slots mi'
od)
theory Ipc_IF

lemma load_word_offs_reads_respects:
  "reads_respects aag l (\<lambda>s. for_each_byte_of_word (\<lambda>x. aag_can_read_or_affect aag l x)
                                                   (a + of_nat x * of_nat word_size))
                  (load_word_offs a x)" unfolding load_word_offs_def fun_app_def apply (rule equiv_valid_guard_imp[OF dmo_loadWord_reads_respects]) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. for_each_byte_of_word (aag_can_read_or_affect aag l) (a + word_of_nat x * word_of_nat word_size)) (load_word_offs a x) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. for_each_byte_of_word (aag_can_read_or_affect aag l) (a + word_of_nat x * word_of_nat word_size)) (do_machine_op (loadWord (a + word_of_nat (x * word_size)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. for_each_byte_of_word (aag_can_read_or_affect aag l) (a + word_of_nat x * word_of_nat word_size) \<Longrightarrow> K (for_each_byte_of_word (aag_can_read_or_affect aag l) (a + word_of_nat (x * word_size))) s proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma as_user_reads_respects:
  "reads_respects aag l (K (det f \<and> aag_can_read_or_affect aag l thread)) (as_user thread f)" apply (simp add: as_user_def split_def) apply (rule gen_asm_ev) apply (wp set_object_reads_respects select_f_ev gets_the_ev) apply (auto intro: reads_affects_equiv_get_tcb_eq[where aag=aag]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (det f \<and> aag_can_read_or_affect aag l thread)) (as_user thread f) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. det f \<and> aag_can_read_or_affect aag l thread) (do tcb <- gets_the (get_tcb thread);
p <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od) proof (prove)
goal (1 subgoal):
 1. det f \<and> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb thread);
p <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>det f \<and> aag_can_read_or_affect aag l thread; True\<rbrakk> \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb thread s = get_tcb thread t) s \<and> K (det f) s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb thread s))))). True \<and> True)) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma validE_E_wp_post_taut:
   "\<lbrace>P\<rbrace> f -, \<lbrace>\<top>\<top>\<rbrace>" by (auto simp: validE_E_def validE_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>_ _. True\<rbrace>
theory Ipc_IF

lemma aag_has_read_auth_can_read_or_affect_ipc_buffer:
  "ipc_buffer_has_read_auth aag (pasSubject aag) buf
   \<Longrightarrow> aag_can_read_or_affect_ipc_buffer aag l buf" apply (clarsimp simp: ipc_buffer_has_read_auth_def aag_can_read_or_affect_ipc_buffer_def
                 split: option.splits) apply (rule reads_read) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ipc_buffer_has_read_auth aag (pasSubject aag) buf \<Longrightarrow> aag_can_read_or_affect_ipc_buffer aag l buf proof (prove)
goal (1 subgoal):
 1. \<And>x2 x. \<lbrakk>buf = Some x2; x \<in> ptr_range x2 msg_align_bits; is_aligned x2 msg_align_bits; \<forall>x\<in>ptr_range x2 msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag; aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag x \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>x2 x. \<lbrakk>buf = Some x2; x \<in> ptr_range x2 msg_align_bits; is_aligned x2 msg_align_bits; \<forall>x\<in>ptr_range x2 msg_align_bits. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag; aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag x \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma ev_irrelevant_bind:
  assumes inv: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  assumes ev: "equiv_valid I A A P g"
  shows "equiv_valid I A A P (do y \<leftarrow> f; g od)" apply (simp add: equiv_valid_def2) apply (rule equiv_valid_rv_guard_imp) apply (rule equiv_valid_2_bind) apply (rule ev[simplified equiv_valid_def2]) apply (wp equiv_valid_rv_trivial[OF inv] inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (do y <- f;
g
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (=) P (do y <- f;
g
od) proof (prove)
goal (2 subgoals):
 1. equiv_valid_rv_inv I A (=) ?P (do y <- f;
g
od)
 2. \<And>s. P s \<Longrightarrow> ?P s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. ?R'3 rv rv' \<Longrightarrow> equiv_valid_2 I A A (=) (?Q3 rv) (?Q'3 rv') g g
 2. equiv_valid_rv_inv I A ?R'3 ?P3 f
 3. \<lbrace>?S3\<rbrace> f \<lbrace>?Q3\<rbrace>
 4. \<lbrace>?S3\<rbrace> f \<lbrace>?Q'3\<rbrace>
 5. \<And>s. P s \<Longrightarrow> ?P3 s \<and> ?S3 s proof (prove)
goal (4 subgoals):
 1. equiv_valid_rv_inv I A ?R'3 ?P3 f
 2. \<lbrace>?S3\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<lbrace>?S3\<rbrace> f \<lbrace>\<lambda>rv'. P\<rbrace>
 4. \<And>s. P s \<Longrightarrow> ?P3 s \<and> ?S3 s proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma set_mrs_returns_a_constant:
  "\<exists>x. \<lbrace>\<top>\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace>" apply (case_tac buf) apply (rule exI) apply ((simp add: set_mrs_def | wp | rule impI)+)[1] apply (rule exI) apply (simp add: set_mrs_def split del: if_split | wp | rule impI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace> proof (prove)
goal (2 subgoals):
 1. buf = None \<Longrightarrow> \<exists>x. \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace>
 2. \<And>a. buf = Some a \<Longrightarrow> \<exists>x. \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace> proof (prove)
goal (2 subgoals):
 1. buf = None \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = ?x1\<rbrace>
 2. \<And>a. buf = Some a \<Longrightarrow> \<exists>x. \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<exists>x. \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = ?x18 a\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma set_mrs_ret_eq:
  "\<forall>(s::'s::state_ext state) (t::'s::state_ext state).
   \<forall>(rva, s') \<in> fst (set_mrs thread buf msgs s).
   \<forall>(rvb, t') \<in> fst (set_mrs thread buf msgs t). rva = rvb" apply (clarsimp) apply (cut_tac thread=thread and buf=buf and msgs=msgs in set_mrs_returns_a_constant) apply (erule exE) apply (subgoal_tac "a = x \<and> aa = x") apply simp apply (rule conjI) apply (erule (1) use_valid | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. \<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (set_mrs thread buf msgs s); (aa, ba) \<in> fst (set_mrs thread buf msgs t)\<rbrakk> \<Longrightarrow> a = aa proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (set_mrs thread buf msgs s); (aa, ba) \<in> fst (set_mrs thread buf msgs t); \<exists>x. \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace>\<rbrakk> \<Longrightarrow> a = aa proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba x. \<lbrakk>(a, b) \<in> fst (set_mrs thread buf msgs s); (aa, ba) \<in> fst (set_mrs thread buf msgs t); \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace>\<rbrakk> \<Longrightarrow> a = aa proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba x. \<lbrakk>(a, b) \<in> fst (set_mrs thread buf msgs s); (aa, ba) \<in> fst (set_mrs thread buf msgs t); \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace>; a = x \<and> aa = x\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>s t a b aa ba x. \<lbrakk>(a, b) \<in> fst (set_mrs thread buf msgs s); (aa, ba) \<in> fst (set_mrs thread buf msgs t); \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace>\<rbrakk> \<Longrightarrow> a = x \<and> aa = x proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba x. \<lbrakk>(a, b) \<in> fst (set_mrs thread buf msgs s); (aa, ba) \<in> fst (set_mrs thread buf msgs t); \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace>\<rbrakk> \<Longrightarrow> a = x \<and> aa = x proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba x. \<lbrakk>(a, b) \<in> fst (set_mrs thread buf msgs s); (aa, ba) \<in> fst (set_mrs thread buf msgs t); \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace>\<rbrakk> \<Longrightarrow> a = x
 2. \<And>s t a b aa ba x. \<lbrakk>(a, b) \<in> fst (set_mrs thread buf msgs s); (aa, ba) \<in> fst (set_mrs thread buf msgs t); \<lbrace>\<lambda>_. True\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. rv = x\<rbrace>\<rbrakk> \<Longrightarrow> aa = x proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma tl_tl_in_set:
  "tl xs = (x # xs') \<Longrightarrow> set xs' \<subseteq> set xs" by (case_tac xs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tl xs = x # xs' \<Longrightarrow> set xs' \<subseteq> set xs
theory Ipc_IF

lemma ko_at_eq:
  "ko_at obj pos s \<longleftrightarrow> kheap s pos = Some obj" by (force simp:obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at obj pos s = (kheap s pos = Some obj)
theory Ipc_IF

lemma make_fault_msg_reads_respects:
  "reads_respects aag l (K (aag_can_read_or_affect aag l sender)) (make_fault_msg rva sender)" apply (case_tac rva) by (wp as_user_reads_respects make_arch_fault_msg_reads_respects
       | simp split del: if_split add: det_getRegister det_getRestartPC
       | rule det_mapM
       | rule subset_refl)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l sender)) (make_fault_msg rva sender) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. rva = CapFault x11 x12 x13 \<Longrightarrow> reads_respects aag l (K (aag_can_read_or_affect aag l sender)) (make_fault_msg rva sender)
 2. \<And>x2. rva = UnknownSyscallException x2 \<Longrightarrow> reads_respects aag l (K (aag_can_read_or_affect aag l sender)) (make_fault_msg rva sender)
 3. \<And>x31 x32. rva = UserException x31 x32 \<Longrightarrow> reads_respects aag l (K (aag_can_read_or_affect aag l sender)) (make_fault_msg rva sender)
 4. \<And>x4. rva = ArchFault x4 \<Longrightarrow> reads_respects aag l (K (aag_can_read_or_affect aag l sender)) (make_fault_msg rva sender)
theory Ipc_IF

lemma do_fault_transfer_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects aag l
       (K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_auth aag receiver buf \<and>
           (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)))
       (do_fault_transfer badge sender receiver buf)" unfolding do_fault_transfer_def by (wp as_user_set_register_reads_respects' as_user_reads_respects set_message_info_reads_respects
         set_mrs_reads_respects' make_fault_msg_reads_respects thread_get_reads_respects
      | wpc
      | simp add: split_def det_setRegister
      | wp (once) hoare_drop_imps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_auth aag receiver buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) (do_fault_transfer badge sender receiver buf) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_auth aag receiver buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) (do fault <- thread_get tcb_fault sender;
f <- case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
(label, msg) <- make_fault_msg f sender;
sent <- set_mrs receiver buf msg;
set_message_info receiver $ MI sent 0 0 label;
as_user receiver $ setRegister badge_register badge
od)