kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_IF

lemma update_waiting_ntfn_globals_equiv:
  "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs
                    and ko_at (Notification ntfn) ntfnptr and pspace_distinct
                    and sym_refs \<circ> state_refs_of and (\<lambda>s. idle_thread s \<notin> set queue)
                    and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace>
   update_waiting_ntfn ntfnptr queue bound_tcb badge
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding update_waiting_ntfn_def supply possible_switch_to_extended.dxo_eq[simp del] apply (wpsimp wp: set_thread_state_globals_equiv as_user_globals_equiv
                    set_notification_globals_equiv dxo_wp_weak) by (auto simp: neq_Nil_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and ko_at (Notification ntfn) ntfnptr and pspace_distinct and sym_refs \<circ> state_refs_of and (\<lambda>s. idle_thread s \<notin> set queue) and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace> update_waiting_ntfn ntfnptr queue bound_tcb badge \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and ko_at (Notification ntfn) ntfnptr and pspace_distinct and sym_refs \<circ> state_refs_of and (\<lambda>s. idle_thread s \<notin> set queue) and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace> do assert (queue \<noteq> []);
(dest, rest) <- return $ (hd queue, tl queue);
set_notification ntfnptr $ \<lparr>ntfn_obj = case rest of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn rest, ntfn_bound_tcb = bound_tcb\<rparr>;
set_thread_state dest Running;
as_user dest $ setRegister badge_register badge;
do_extended_op (possible_switch_to dest)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and ko_at (Notification ntfn) ntfnptr and pspace_distinct and sym_refs \<circ> state_refs_of and (\<lambda>s. idle_thread s \<notin> set queue) and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace> do assert (queue \<noteq> []);
(dest, rest) <- return $ (hd queue, tl queue);
set_notification ntfnptr $ \<lparr>ntfn_obj = case rest of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn rest, ntfn_bound_tcb = bound_tcb\<rparr>;
set_thread_state dest Running;
as_user dest $ setRegister badge_register badge;
do_extended_op (possible_switch_to dest)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; ko_at (Notification ntfn) ntfnptr sa; pspace_distinct sa; sym_refs (state_refs_of sa); idle_thread sa \<notin> set queue; ntfn_obj ntfn = WaitingNtfn queue; queue \<noteq> []; hd queue = idle_thread sa\<rbrakk> \<Longrightarrow> False
theory Ipc_IF

lemma handle_double_fault_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
   handle_double_fault tptr ex1 ex2
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding handle_double_fault_def by (wp set_thread_state_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> handle_double_fault tptr ex1 ex2 \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> set_thread_state tptr Inactive \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory Ipc_IF

lemma send_ipc_valid_global_objs:
  "\<lbrace>valid_global_objs\<rbrace>
   send_ipc block call badge can_grant can_grant_reply thread epptr
   \<lbrace>\<lambda>_. valid_global_objs\<rbrace>" unfolding send_ipc_def by (wp dxo_wp_weak hoare_drop_imps hoare_vcg_all_lift | simp | wpc | intro conjI impI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs\<rbrace> send_ipc block call badge can_grant can_grant_reply thread epptr \<lbrace>\<lambda>_. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs\<rbrace> do ep <- get_endpoint epptr;
case (ep, block) of (IdleEP, True) \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP [thread]
od | (IdleEP, False) \<Rightarrow> return () | (SendEP queue, True) \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP (queue @ [thread])
od | (SendEP queue, False) \<Rightarrow> return () | (RecvEP [], x) \<Rightarrow> fail | (RecvEP (dest # queue), x) \<Rightarrow> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap thread dest reply_can_grant else set_thread_state thread Inactive
od
od \<lbrace>\<lambda>_. valid_global_objs\<rbrace>
theory Ipc_IF

lemma handle_fault_globals_equiv:
  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
                     and pspace_distinct and pspace_aligned and valid_global_objs
                     and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault ex)\<rbrace>
   handle_fault thread ex
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding handle_fault_def apply (wp handle_double_fault_globals_equiv) apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state" and
                    E="\<lambda>_. globals_equiv st and valid_arch_state" in hoare_post_impErr) apply (wp send_fault_ipc_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault ex)\<rbrace> handle_fault thread ex \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault ex)\<rbrace> do _ <- gets_the $ get_tcb thread;
send_fault_ipc thread ex <catch> handle_double_fault thread ex;
return ()
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>uu_. \<lbrace>?B1 uu_\<rbrace> send_fault_ipc thread ex \<lbrace>\<lambda>x. globals_equiv st\<rbrace>, \<lbrace>\<lambda>x s. globals_equiv st s \<and> valid_arch_state s\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 3. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault ex)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>uu_. \<lbrace>?B1 uu_\<rbrace> send_fault_ipc thread ex \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state\<rbrace>
 2. \<And>_ rv s. (globals_equiv st and valid_arch_state) s \<Longrightarrow> globals_equiv st s
 3. \<And>_ e s. (globals_equiv st and valid_arch_state) s \<Longrightarrow> globals_equiv st s \<and> valid_arch_state s
 4. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 5. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault ex)) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma handle_fault_reply_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
   handle_fault_reply fault thread x y
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" by (cases fault; wpsimp wp: as_user_globals_equiv handle_arch_fault_reply_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> handle_fault_reply fault thread x y \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Ipc_IF

lemma reply_from_kernel_globals_equiv:
  "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct
                    and pspace_aligned and  (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
   reply_from_kernel thread x
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding reply_from_kernel_def by (wpsimp wp: set_message_info_globals_equiv set_mrs_globals_equiv as_user_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> reply_from_kernel thread x \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> do (label, msg) <- return x;
buf <- lookup_ipc_buffer True thread;
as_user thread $ setRegister badge_register 0;
len <- set_mrs thread buf msg;
set_message_info thread $ MI len 0 0 label
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory Ipc_IF

lemma send_fault_ipc_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
  "reads_respects_g aag l
   (invs and pas_refined aag and pas_cur_domain aag
         and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault))
     (send_fault_ipc thread fault)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule send_fault_ipc_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp send_fault_ipc_globals_equiv | simp)+ by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) (send_fault_ipc thread fault) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (send_fault_ipc thread fault)
 2. doesnt_touch_globals ?Q1 (send_fault_ipc thread fault)
 3. \<And>s. (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (send_fault_ipc thread fault)
 2. \<And>s. (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) s \<Longrightarrow> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) s \<Longrightarrow> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag thread \<and> valid_fault fault \<Longrightarrow> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> valid_idle s \<and> sym_refs (state_refs_of s)
theory Ipc_IF

lemma handle_fault_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_g aag l
       (invs and pas_refined aag and pas_cur_domain aag
             and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault))
       (handle_fault thread fault)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule handle_fault_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp handle_fault_globals_equiv | simp)+ by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) (handle_fault thread fault) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (handle_fault thread fault)
 2. doesnt_touch_globals ?Q1 (handle_fault thread fault)
 3. \<And>s. (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (handle_fault thread fault)
 2. \<And>s. (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) s \<Longrightarrow> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> handle_fault thread fault \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) s \<Longrightarrow> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag thread \<and> valid_fault fault \<Longrightarrow> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> valid_idle s \<and> sym_refs (state_refs_of s)
theory Ipc_IF

lemma handle_fault_reply_reads_respects_g:
  "reads_respects_g aag l
     (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread))
     (handle_fault_reply fault thread x y)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule handle_fault_reply_reads_respects) apply (rule doesnt_touch_globalsI) apply (wp handle_fault_reply_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) (handle_fault_reply fault thread x y) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (handle_fault_reply fault thread x y)
 2. doesnt_touch_globals ?Q1 (handle_fault_reply fault thread x y)
 3. \<And>s. (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (handle_fault_reply fault thread x y)
 2. \<And>s. (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) s \<Longrightarrow> (K (aag_can_read aag thread) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> handle_fault_reply fault thread x y \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) s \<Longrightarrow> (K (aag_can_read aag thread) and ?Q1) s proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma handle_reply_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_f_g aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag
                                               and is_subject aag \<circ> cur_thread) (handle_reply)" apply (rule equiv_valid_guard_imp[OF reads_respects_f_g]) apply (rule handle_reply_reads_respects_f[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp handle_reply_globals_equiv | simp)+ apply (simp add: invs_def valid_state_def valid_pspace_def | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) handle_reply proof (prove)
goal (3 subgoals):
 1. reads_respects_f aag l ?P1 handle_reply
 2. doesnt_touch_globals ?Q1 handle_reply
 3. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 handle_reply
 2. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (silc_inv aag ?st5 and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> handle_reply \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (silc_inv aag ?st5 and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<Longrightarrow> silc_inv aag ?st5 s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> valid_idle s proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma reply_from_kernel_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_g aag l (valid_global_objs and valid_objs and valid_arch_state
                                               and valid_global_refs and pspace_distinct
                                               and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s)
                                               and K (is_subject aag thread))
                      (reply_from_kernel thread x)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule reply_from_kernel_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp reply_from_kernel_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) (reply_from_kernel thread x) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (reply_from_kernel thread x)
 2. doesnt_touch_globals ?Q1 (reply_from_kernel thread x)
 3. \<And>s. (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (reply_from_kernel thread x)
 2. \<And>s. (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) s \<Longrightarrow> (K (is_subject aag thread) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> reply_from_kernel thread x \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) s \<Longrightarrow> (K (is_subject aag thread) and ?Q1) s proof (prove)
goal:
No subgoals!
theory ArchIpc_IF

lemma lookup_ipc_buffer_reads_respects[Ipc_IF_assms]:
  "reads_respects aag l (K (aag_can_read aag thread \<or> aag_can_affect aag l thread))
                  (lookup_ipc_buffer is_receiver thread)" unfolding lookup_ipc_buffer_def by (wp thread_get_reads_respects get_cap_reads_respects | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l thread)) (lookup_ipc_buffer is_receiver thread) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l thread)) (do buffer_ptr <- thread_get tcb_ipc_buffer thread;
buffer_frame_slot <- return (thread, tcb_cnode_index 4);
buffer_cap <- get_cap buffer_frame_slot;
case buffer_cap of ArchObjectCap (PageCap x p R vms xa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> is_receiver then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None
od)
theory ArchIpc_IF

lemma as_user_equiv_but_for_labels[Ipc_IF_assms]:
  "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace>
   as_user thread f
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" unfolding as_user_def apply (wp set_object_equiv_but_for_labels | simp add: split_def)+ apply (blast dest: get_tcb_not_asid_pool_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace> as_user thread f \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace> do tcb <- gets_the $ get_tcb thread;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object thread (TCB new_tcb);
return a
od \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. equiv_but_for_labels aag L st s \<and> pasObjectAbs aag thread \<in> L \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> (\<exists>a b. (a, b) \<in> fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb thread s)))))) \<longrightarrow> \<not> typ_at (AArch AASIDPool) thread s proof (prove)
goal:
No subgoals!