kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_IF

lemma cancel_badged_sends_reads_respects_f:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects_f aag l (silc_inv aag st and is_subject aag \<circ> cur_thread and pas_refined aag
                                                 and invs and K (is_subject aag ptr))
                          (cancel_badged_sends ptr badge)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_f) apply (rule cancel_badged_sends_reads_respects[OF domains_distinct]) apply (wp cancel_badged_sends_silc_inv[where st=st] | simp | elim conjE, assumption)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and is_subject aag \<circ> cur_thread and pas_refined aag and invs and K (is_subject aag ptr)) (cancel_badged_sends ptr badge) proof (prove)
goal (2 subgoals):
 1. reads_respects_f aag l ?Q (cancel_badged_sends ptr badge)
 2. \<And>s. (silc_inv aag st and is_subject aag \<circ> cur_thread and pas_refined aag and invs and K (is_subject aag ptr)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P3 (cancel_badged_sends ptr badge)
 2. \<lbrace>silc_inv aag ?st3 and ?Q3\<rbrace> cancel_badged_sends ptr badge \<lbrace>\<lambda>_. silc_inv aag ?st3\<rbrace>
 3. \<And>s. (silc_inv aag st and is_subject aag \<circ> cur_thread and pas_refined aag and invs and K (is_subject aag ptr)) s \<Longrightarrow> (silc_inv aag ?st3 and ?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>silc_inv aag ?st3 and ?Q3\<rbrace> cancel_badged_sends ptr badge \<lbrace>\<lambda>_. silc_inv aag ?st3\<rbrace>
 2. \<And>s. (silc_inv aag st and is_subject aag \<circ> cur_thread and pas_refined aag and invs and K (is_subject aag ptr)) s \<Longrightarrow> (silc_inv aag ?st3 and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag ptr)) and ?Q3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> is_subject aag (cur_thread s) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag ptr \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> ?Q3 s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma cap_revoke_only_timer_irq_inv:
  "\<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>
   cap_revoke slot
   \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (rule hoare_wp_simps) apply (rule hoare_conjI) apply (wp only_timer_irq_pres[where P="\<top>"] cap_revoke_irq_masks | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. domain_sep_inv False st s \<and> only_timer_irq irq s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> cap_revoke slot \<lbrace>\<lambda>r. domain_sep_inv False st\<rbrace>
 2. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> cap_revoke slot \<lbrace>\<lambda>r. only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma cap_swap_reads_respects_g:
  "reads_respects_g aag l
     (\<lambda>s. is_subject aag (fst slot1) \<and> is_subject aag (fst slot2) \<and>
          valid_global_objs s \<and> valid_arch_state s)
     (cap_swap cap1 slot1 cap2 slot2)" by (wp equiv_valid_guard_imp[OF reads_respects_g] cap_swap_reads_respects
         doesnt_touch_globalsI cap_swap_globals_equiv | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. is_subject aag (fst slot1) \<and> is_subject aag (fst slot2) \<and> valid_global_objs s \<and> valid_arch_state s) (cap_swap cap1 slot1 cap2 slot2)
theory Syscall_IF

lemma cap_insert_reads_respects_g:
  "reads_respects_g aag l
     (\<lambda>s. is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot) \<and>
          valid_global_objs s \<and> valid_arch_state s)
     (cap_insert new_cap src_slot dest_slot)" by (wp equiv_valid_guard_imp[OF reads_respects_g] cap_insert_reads_respects
         doesnt_touch_globalsI cap_insert_globals_equiv | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot) \<and> valid_global_objs s \<and> valid_arch_state s) (cap_insert new_cap src_slot dest_slot)
theory Syscall_IF

lemma cap_move_reads_respects_g:
  "reads_respects_g aag l
     (\<lambda>s. is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot) \<and>
 valid_global_objs s \<and> valid_arch_state s)
     (cap_move new_cap src_slot dest_slot)" by (wp equiv_valid_guard_imp[OF reads_respects_g] cap_move_reads_respects
         doesnt_touch_globalsI cap_move_globals_equiv | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. is_subject aag (fst src_slot) \<and> is_subject aag (fst dest_slot) \<and> valid_global_objs s \<and> valid_arch_state s) (cap_move new_cap src_slot dest_slot)
theory Syscall_IF

lemma invoke_domain_reads_respects_f_g:
  "reads_respects_f_g aag l \<bottom> (invoke_domain thread domain)" by (clarsimp simp: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (\<lambda>_. False) (invoke_domain thread domain)
theory Syscall_IF

lemma syscall_reads_respects_f_g:
  assumes reads_res_m_fault:
    "reads_respects_f_g aag l P m_fault"
  assumes reads_res_m_error:
    "\<And>v. reads_respects_f_g aag l (Q'' v) (m_error v)"
  assumes reads_res_h_fault:
    "\<And>v. reads_respects_f_g aag l (Q' v) (h_fault v)"
  assumes reads_res_m_finalise:
    "\<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v)"
  assumes reads_res_h_error:
    "\<And>v. reads_respects_f_g aag l (R' v) (h_error v)"
  assumes m_fault_hoare:
    "\<lbrace>P\<rbrace> m_fault \<lbrace>case_sum Q' Q''\<rbrace>"
  assumes m_error_hoare:
    "\<And>v. \<lbrace>Q'' v\<rbrace> m_error v \<lbrace>case_sum R' R''\<rbrace>"
  shows "reads_respects_f_g aag l P (syscall m_fault h_fault m_error h_error m_finalise)" unfolding Syscall_A.syscall_def without_preemption_def fun_app_def by (wp assms equiv_valid_guard_imp[OF liftE_bindE_ev]
      | rule hoare_strengthen_post[OF m_error_hoare]
      | rule hoare_strengthen_post[OF m_fault_hoare]
      | wpc
      | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l P (syscall m_fault h_fault m_error h_error m_finalise) proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l P (doE r_fault <- liftE m_fault;
case r_fault of Inl f \<Rightarrow> liftE (h_fault f) | Inr a \<Rightarrow> doE r_error <- liftE (m_error a);
case r_error of Inl e \<Rightarrow> liftE (h_error e) | Inr b \<Rightarrow> m_finalise b
odE
odE)
theory Syscall_IF

lemma requiv_g_cur_thread_eq:
  "reads_equiv_g aag s t \<Longrightarrow> (cur_thread s) = (cur_thread t)" apply (frule reads_equiv_gD) apply (clarsimp simp add: requiv_cur_thread_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_g aag s t \<Longrightarrow> cur_thread s = cur_thread t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_g aag s t; reads_equiv aag s t \<and> globals_equiv s t\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread t proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma lookup_cap_and_slot_reads_respects_g':
  "reads_equiv_valid_g_inv (affects_equiv aag l) aag
                           (pas_refined aag and K (is_subject aag t) and P)
                           (lookup_cap_and_slot t cptr)" apply (rule equiv_valid_guard_imp) apply (rule lookup_cap_and_slot_reads_respects_g) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and K (is_subject aag t) and P) (lookup_cap_and_slot t cptr) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (lookup_cap_and_slot t cptr)
 2. \<And>s. (pas_refined aag and K (is_subject aag t) and P) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_subject aag t) and P) s \<Longrightarrow> (pas_refined aag and K (is_subject aag t)) s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma authorised_for_globals_triv:
  "\<forall>x y. f x \<noteq> InvokeArchObject y
   \<Longrightarrow> \<lbrace>\<top>\<rbrace> m \<lbrace>authorised_for_globals_inv \<circ> f\<rbrace>, -" by (clarsimp simp: validE_R_def validE_def valid_def authorised_for_globals_inv_def
              split: invocation.splits sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. f x \<noteq> InvokeArchObject y \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> m \<lbrace>authorised_for_globals_inv \<circ> f\<rbrace>, -
theory Syscall_IF

lemma set_thread_state_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_g aag (l :: 'a subject_label) (is_subject aag \<circ> cur_thread and valid_arch_state)
                      (set_thread_state ref ts)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g) apply (rule set_thread_state_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (rule set_thread_state_globals_equiv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (is_subject aag \<circ> cur_thread and valid_arch_state) (set_thread_state ref ts) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (set_thread_state ref ts)
 2. \<And>s. (is_subject aag \<circ> cur_thread and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P3 (set_thread_state ref ts)
 2. doesnt_touch_globals ?Q3 (set_thread_state ref ts)
 3. \<And>s. (is_subject aag \<circ> cur_thread and valid_arch_state) s \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (set_thread_state ref ts)
 2. \<And>s. (is_subject aag \<circ> cur_thread and valid_arch_state) s \<Longrightarrow> ((\<lambda>s. is_subject aag (cur_thread s)) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q3\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (is_subject aag \<circ> cur_thread and valid_arch_state) s \<Longrightarrow> ((\<lambda>s. is_subject aag (cur_thread s)) and ?Q3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (is_subject aag \<circ> cur_thread and valid_arch_state) s \<Longrightarrow> ((\<lambda>s. is_subject aag (cur_thread s)) and valid_arch_state) s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma set_thread_state_only_timer_irq_inv:
  "\<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>
   set_thread_state ref ts
   \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (wp only_timer_irq_pres | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma ct_active_cur_thread_not_idle_thread:
  "\<lbrakk> valid_idle s; ct_active s \<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s" by (clarsimp simp: invs_def valid_idle_def ct_in_state_def pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; ct_active s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s
theory Syscall_IF

lemma ct_active_not_idle:
  "\<lbrakk> invs s; ct_active s \<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s" by (clarsimp simp: ct_active_cur_thread_not_idle_thread invs_valid_idle)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ct_active s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s
theory Syscall_IF

lemma delete_caller_cap_reads_respects_f:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag
                                                 and K (is_subject aag (fst (x, tcb_cnode_index 3))))
                          (delete_caller_cap x)" unfolding delete_caller_cap_def by (rule cap_delete_one_reads_respects_f[OF domains_distinct])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and K (is_subject aag (fst (x, tcb_cnode_index 3)))) (delete_caller_cap x) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and K (is_subject aag (fst (x, tcb_cnode_index 3)))) (cap_delete_one (x, tcb_cnode_index 3))
theory Syscall_IF

lemma delete_caller_cap_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   delete_caller_cap x
   \<lbrace>\<lambda>r. globals_equiv st\<rbrace>" unfolding delete_caller_cap_def by (wp cap_delete_one_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> delete_caller_cap x \<lbrace>\<lambda>r. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> cap_delete_one (x, tcb_cnode_index 3) \<lbrace>\<lambda>r. globals_equiv st\<rbrace>
theory Syscall_IF

lemma lookup_cap_cap_fault:
  "\<lbrace>invs\<rbrace> lookup_cap c b -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>" apply (simp add: lookup_cap_def) apply wp apply (case_tac xa) apply (simp add: validE_E_def) apply (wp) apply (fold validE_E_def) apply (wp lookup_slot_for_thread_cap_fault) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_cap c b -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> doE (ref', uu_) <- lookup_slot_for_thread c b;
liftE (get_cap ref')
odE -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrace>?B1 xa\<rbrace> case xa of (ref', uu_) \<Rightarrow> liftE (get_cap ref') -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread c b \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>xa a b. xa = (a, b) \<Longrightarrow> \<lbrace>?B1 xa\<rbrace> case xa of (ref', uu_) \<Rightarrow> liftE (get_cap ref') -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread c b \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>x a b. x = (a, b) \<Longrightarrow> \<lbrace>?B1 (a, b)\<rbrace> get_cap a \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread c b \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> lookup_slot_for_thread c b \<lbrace>\<lambda>x1 x2. True\<rbrace>, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> lookup_slot_for_thread c b -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> invs s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma cap_fault_on_failure_ev':
  "equiv_valid_inv (reads_equiv_f aag) A P f \<Longrightarrow>
       equiv_valid_inv (reads_equiv_f aag) A P (cap_fault_on_failure cptr rp f)" unfolding cap_fault_on_failure_def handleE'_def by (wp | wpc | simp add: o_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (reads_equiv_f aag) A P f \<Longrightarrow> equiv_valid_inv (reads_equiv_f aag) A P (cap_fault_on_failure cptr rp f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (reads_equiv_f aag) A P f \<Longrightarrow> equiv_valid_inv (reads_equiv_f aag) A P (do v <- f;
case v of Inl e \<Rightarrow> (throwError \<circ> CapFault cptr rp) e | Inr v' \<Rightarrow> return (Inr v')
od)
theory Syscall_IF

lemma handle_recv_reads_respects_f_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_f_g aag l
       (silc_inv aag st and einvs and ct_active and pas_refined aag
                        and pas_cur_domain aag and is_subject aag \<circ> cur_thread)
       (handle_recv is_blocking)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_f_g) apply (wp handle_recv_reads_respects_f[where st=st, OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp handle_recv_globals_equiv) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (handle_recv is_blocking) proof (prove)
goal (2 subgoals):
 1. reads_respects_f_g aag l ?Q (handle_recv is_blocking)
 2. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects_f aag l ?P3 (handle_recv is_blocking)
 2. doesnt_touch_globals ?Q3 (handle_recv is_blocking)
 3. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (handle_recv is_blocking)
 2. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q3\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st s. (globals_equiv st and ?Q3) s \<Longrightarrow> (globals_equiv st and invs and ct_active) s
 2. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and ?Q3) s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma dmo_return_reads_respects:
  "reads_respects aag l \<top> (do_machine_op (return ()))" apply (rule use_spec_ev) apply (rule do_machine_op_spec_reads_respects; wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (return ())) proof (prove)
goal (1 subgoal):
 1. \<And>st. spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (return ())) proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma get_irq_slot_reads_respects':
  "reads_respects aag l (K (aag_can_read_label aag (pasIRQAbs aag irq))) (get_irq_slot irq)" unfolding get_irq_slot_def apply (rule equiv_valid_guard_imp) apply (rule gets_ev) apply (simp add: reads_equiv_def states_equiv_for_def equiv_for_def affects_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_irq aag irq)) (get_irq_slot irq) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_irq aag irq)) (gets (\<lambda>st. (interrupt_irq_node st irq, []))) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (gets (\<lambda>st. (interrupt_irq_node st irq, [])))
 2. \<And>s. K (aag_can_read_irq aag irq) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. K (aag_can_read_irq aag irq) s \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> (interrupt_irq_node s irq, []) = (interrupt_irq_node t irq, []) proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma get_irq_slot_can_read_from_slot:
  "\<lbrace>K (aag_can_read_label aag (pasIRQAbs aag irq)) and pas_refined aag\<rbrace>
   get_irq_slot irq
   \<lbrace>\<lambda>r. K (aag_can_read_label aag (pasObjectAbs aag (fst r)))\<rbrace>" unfolding get_irq_slot_def apply (wp gets_wp) apply (simp add: pas_refined_def policy_wellformed_def irq_map_wellformed_aux_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (aag_can_read_irq aag irq) and pas_refined aag\<rbrace> get_irq_slot irq \<lbrace>\<lambda>r. K (aag_can_read aag (fst r))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (aag_can_read_irq aag irq) and pas_refined aag\<rbrace> gets (\<lambda>st. (interrupt_irq_node st irq, [])) \<lbrace>\<lambda>r. K (aag_can_read aag (fst r))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (K (aag_can_read_irq aag irq) and pas_refined aag) s \<Longrightarrow> K (aag_can_read aag (fst (interrupt_irq_node s irq, []))) s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma get_irq_state_rev':
  "reads_equiv_valid_inv A aag (K (aag_can_read_label aag (pasIRQAbs aag irq))) (get_irq_state irq)" unfolding get_irq_state_def apply (rule equiv_valid_guard_imp[OF gets_ev]) apply (fastforce simp: reads_equiv_def2
                   elim: states_equiv_forE_interrupt_states
                  intro: aag_can_read_irq_self) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (aag_can_read_irq aag irq)) (get_irq_state irq) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (aag_can_read_irq aag irq)) (gets (\<lambda>s. interrupt_states s irq)) proof (prove)
goal (1 subgoal):
 1. \<And>s. K (aag_can_read_irq aag irq) s \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> interrupt_states s irq = interrupt_states t irq proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma handle_yield_reads_respects:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects aag (l :: 'a subject_label) (pas_refined aag) handle_yield" by (wpsimp wp: domains_distinct tcb_sched_action_reads_respects
           simp: handle_yield_def reads_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag) handle_yield