kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_IF

lemma valid_ntfn_WaitingNtfn_tl:
  "\<lbrakk> ntfn_obj ntfn = (WaitingNtfn list); valid_ntfn ntfn s;
     tl list \<noteq> []; ntfn' = ntfn\<lparr>ntfn_obj := (WaitingNtfn (tl list))\<rparr> \<rbrakk>
     \<Longrightarrow> valid_ntfn ntfn' s" apply (case_tac list, simp_all) apply (rename_tac a lista) apply (case_tac lista, simp_all) apply (clarsimp simp: valid_ntfn_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; valid_ntfn ntfn s; tl list \<noteq> []; ntfn' = ntfn_set_obj ntfn (WaitingNtfn (tl list))\<rbrakk> \<Longrightarrow> valid_ntfn ntfn' s proof (prove)
goal (1 subgoal):
 1. \<And>a lista. \<lbrakk>ntfn_obj ntfn = WaitingNtfn (a # lista); valid_ntfn ntfn s; lista \<noteq> []; ntfn' = ntfn_set_obj ntfn (WaitingNtfn lista); list = a # lista\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfn (WaitingNtfn lista)) s proof (prove)
goal (1 subgoal):
 1. \<And>a lista. \<lbrakk>ntfn_obj ntfn = WaitingNtfn (a # lista); valid_ntfn ntfn s; lista \<noteq> []; ntfn' = ntfn_set_obj ntfn (WaitingNtfn lista); list = a # lista\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfn (WaitingNtfn lista)) s proof (prove)
goal (1 subgoal):
 1. \<And>a lista aa listb. \<lbrakk>ntfn_obj ntfn = WaitingNtfn (a # aa # listb); valid_ntfn ntfn s; ntfn' = ntfn_set_obj ntfn (WaitingNtfn (aa # listb)); list = a # aa # listb; lista = aa # listb\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfn (WaitingNtfn (aa # listb))) s proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma store_word_offs_equiv_but_for_labels:
  "\<lbrace>equiv_but_for_labels aag L st and
    K (for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + of_nat offs * of_nat word_size))\<rbrace>
   store_word_offs ptr offs v
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" unfolding store_word_offs_def apply (wp modify_wp | simp add: do_machine_op_def split_def)+ apply clarsimp apply (erule use_valid[OF _ storeWord_equiv_but_for_labels]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + word_of_nat offs * word_of_nat word_size))\<rbrace> store_word_offs ptr offs v \<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 (for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + word_of_nat offs * word_of_nat word_size))\<rbrace> do s <- get;
assert (in_user_frame (ptr + word_of_nat (offs * word_size)) s);
do_machine_op $ storeWord (ptr + word_of_nat (offs * word_size)) v
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> for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + word_of_nat offs * word_of_nat word_size) \<Longrightarrow> in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s \<longrightarrow> (\<forall>x\<in>fst (storeWord (ptr + word_of_nat offs * word_of_nat word_size) v (machine_state s)). equiv_but_for_labels aag L st (s\<lparr>machine_state := snd x\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>equiv_but_for_labels aag L st s; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + word_of_nat offs * word_of_nat word_size); in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s; ((), b) \<in> fst (storeWord (ptr + word_of_nat offs * word_of_nat word_size) v (machine_state s))\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st (s\<lparr>machine_state := b\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>equiv_but_for_labels aag L st s; for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + word_of_nat offs * word_of_nat word_size); in_user_frame (ptr + word_of_nat offs * word_of_nat word_size) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st (s\<lparr>machine_state := machine_state s\<rparr>) \<and> for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + word_of_nat offs * word_of_nat word_size) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma invisible_ntfn_invisible_receivers_and_ipcbuffers:
  "\<lbrakk> labels_are_invisible aag l {pasObjectAbs aag nptr};
     (pasSubject aag, Notify, pasObjectAbs aag nptr) \<in> pasPolicy aag\<rbrakk>
     \<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag nptr} \<union>
                                     all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<union>
                                     \<Union>(all_to_which_has_auth aag Write
                                        ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)))" by (auto simp: labels_are_invisible_def aag_can_affect_label_def
                 all_to_which_has_auth_def all_with_auth_to_def
           dest: reads_read_page_read_thread reads_read_queued_thread_read_ep)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag nptr}; (pasSubject aag, Notify, pasObjectAbs aag nptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag nptr} \<union> all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)))
theory Ipc_IF

lemma invisible_ntfn_invisible_receivers_and_receivers[rotated 1]:
  "\<lbrakk> auth \<in> {Notify,Receive,SyncSend}; labels_are_invisible aag l {pasObjectAbs aag nptr};
     (pasSubject aag, auth, pasObjectAbs aag nptr) \<in> pasPolicy aag \<rbrakk>
     \<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag nptr} \<union>
                                     all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<union>
                                     (\<Union>(all_to_which_has_auth aag Receive
                                         ` all_with_auth_to aag Receive (pasObjectAbs aag nptr))) \<union>
                                     (\<Union>(all_to_which_has_auth aag Write
                                         ` all_with_auth_to aag Receive (pasObjectAbs aag nptr))))" by (auto simp: labels_are_invisible_def aag_can_affect_label_def
                 all_to_which_has_auth_def all_with_auth_to_def
           dest: read_sync_ep_read_senders read_sync_ep_read_receivers
                 reads_read_queued_thread_read_ep reads_read_page_read_thread reads_ep)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>auth \<in> {Notify, Receive, SyncSend}; labels_are_invisible aag l {pasObjectAbs aag nptr}; (pasSubject aag, auth, pasObjectAbs aag nptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag nptr} \<union> all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)))
theory Ipc_IF

lemma not_etcb_at_not_cdom_can_read:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "\<lbrakk> \<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s;
           tcb_at t s; valid_etcbs s; pas_refined aag s; pas_cur_domain aag s \<rbrakk>
           \<Longrightarrow> aag_can_read aag t" apply (clarsimp simp: valid_etcbs_def tcb_at_st_tcb_at etcb_at_def is_etcb_at_def
                        pas_refined_def tcb_domain_map_wellformed_aux_def) apply (erule_tac x="(t, cur_domain s)" in ballE) apply (force dest: domains_distinct[THEN pas_domains_distinct_inj]) apply (force intro: domtcbs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; tcb_at t s; valid_etcbs s; pas_refined aag s; pas_cur_domain aag s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>tcb_domain y = cur_domain s; \<forall>ptr. st_tcb_at (\<lambda>_. True) ptr s = (\<exists>y. ekheap s ptr = Some y); pas_cur_domain aag s; ekheap s t = Some y; pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>tcb_domain y = cur_domain s; \<forall>ptr. st_tcb_at (\<lambda>_. True) ptr s = (\<exists>y. ekheap s ptr = Some y); pas_cur_domain aag s; ekheap s t = Some y; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; case (t, cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> aag_can_read aag t
 2. \<And>y. \<lbrakk>tcb_domain y = cur_domain s; \<forall>ptr. st_tcb_at (\<lambda>_. True) ptr s = (\<exists>y. ekheap s ptr = Some y); pas_cur_domain aag s; ekheap s t = Some y; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (t, cur_domain s) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>tcb_domain y = cur_domain s; \<forall>ptr. st_tcb_at (\<lambda>_. True) ptr s = (\<exists>y. ekheap s ptr = Some y); pas_cur_domain aag s; ekheap s t = Some y; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (t, cur_domain s) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma tcb_at_ntfn_queue:
  "\<lbrakk> valid_objs s; t \<in> set q; ko_at (Notification ntfn) nptr s; ntfn_obj ntfn = WaitingNtfn q \<rbrakk>
     \<Longrightarrow> tcb_at t s" by (fastforce simp: obj_at_def valid_obj_def valid_ntfn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; t \<in> set q; ko_at (Notification ntfn) nptr s; ntfn_obj ntfn = WaitingNtfn q\<rbrakk> \<Longrightarrow> tcb_at t s
theory Ipc_IF

lemma invisible_ep_invisible_receiver:
  "\<lbrakk> labels_are_invisible aag l {pasObjectAbs aag epptr};
     (pasObjectAbs aag tcb, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag;
     (pasObjectAbs aag tcb, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<rbrakk>
     \<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag epptr} \<union> {pasObjectAbs aag tcb})" by (auto simp: labels_are_invisible_def aag_can_affect_label_def all_with_auth_to_def
           dest: reads_ep reads_read_queued_thread_read_ep)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag epptr}; (pasObjectAbs aag tcb, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasObjectAbs aag tcb, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag epptr} \<union> {pasObjectAbs aag tcb})
theory Ipc_IF

lemma no_fail_gts:
  "no_fail (tcb_at tcb) (get_thread_state tcb)" apply (clarsimp simp: get_thread_state_def thread_get_def) apply (rule no_fail_pre) apply wp by (clarsimp simp: get_tcb_def tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at tcb) (get_thread_state tcb) proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at tcb) (do tcb <- gets_the (get_tcb tcb);
return (tcb_state tcb)
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P (do tcb <- gets_the (get_tcb tcb);
return (tcb_state tcb)
od)
 2. \<And>s. tcb_at tcb s \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at tcb s \<Longrightarrow> ((\<lambda>s. get_tcb tcb s \<noteq> None) and (\<lambda>s. get_tcb tcb s \<noteq> None \<longrightarrow> True)) s
theory Ipc_IF

lemma sts_noop:
   "monadic_rewrite True True (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s))
                    (set_thread_state_ext tcb) (return ())" unfolding set_thread_state_ext_def when_def apply (monadic_rewrite_l monadic_rewrite_if_l_False \<open>wpsimp wp: gts_wp\<close>) apply (monadic_rewrite_symb_exec_l_drop)+ apply (rule monadic_rewrite_refl) by (auto simp: pred_tcb_at_def obj_at_def is_tcb_def get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) (set_thread_state_ext tcb) (return ()) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) (do ts <- get_thread_state tcb;
cur <- gets cur_thread;
action <- gets scheduler_action;
if \<not> runnable ts \<and> cur = tcb \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od) (return ()) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (do ts <- get_thread_state tcb;
cur <- gets cur_thread;
action <- gets scheduler_action;
return ()
od) (return ())
 2. \<And>s. (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) s \<Longrightarrow> ((\<lambda>s. \<forall>st. st_tcb_at ((=) st) tcb s \<longrightarrow> ((\<lambda>_. \<not> (\<not> runnable st \<and> cur_thread s = tcb \<and> scheduler_action s = resume_cur_thread)) and (\<lambda>_. True)) s) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (return ()) (return ())
 2. \<And>s. (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) s \<Longrightarrow> ((\<lambda>s. \<forall>st. st_tcb_at ((=) st) tcb s \<longrightarrow> ((\<lambda>_. \<not> (\<not> runnable st \<and> cur_thread s = tcb \<and> scheduler_action s = resume_cur_thread)) and (\<lambda>_. True)) s) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) s \<Longrightarrow> ((\<lambda>s. \<forall>st. st_tcb_at ((=) st) tcb s \<longrightarrow> ((\<lambda>_. \<not> (\<not> runnable st \<and> cur_thread s = tcb \<and> scheduler_action s = resume_cur_thread)) and (\<lambda>_. True)) s) and (\<lambda>_. True)) s
theory Ipc_IF

lemma gts_reads_respects:
  "reads_respects aag l (K (aag_can_read aag t \<or> aag_can_affect aag l t)) (get_thread_state t)" unfolding get_thread_state_def by (wp thread_get_reads_respects)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l t)) (get_thread_state t) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l t)) (thread_get tcb_state t)
theory Ipc_IF

lemma ev2_invisible_simple:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "\<lbrakk> labels_are_invisible aag l L; modifies_at_most aag L Q f \<rbrakk>
           \<Longrightarrow> reads_respects aag l Q (f :: (det_state, unit) nondet_monad)" apply (simp add: equiv_valid_def2) apply (rule equiv_valid_2_guard_imp) apply (rule ev2_invisible[OF domains_distinct]) by fastforce+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f\<rbrakk> \<Longrightarrow> reads_respects aag l Q f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) Q f proof (prove)
goal (3 subgoals):
 1. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) ?Q ?Q' f f
 2. \<And>s. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f; Q s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f; Q s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f\<rbrakk> \<Longrightarrow> labels_are_invisible aag l ?L4
 2. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f\<rbrakk> \<Longrightarrow> labels_are_invisible aag l ?L'4
 3. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f\<rbrakk> \<Longrightarrow> modifies_at_most aag ?L4 ?Q4 f
 4. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f\<rbrakk> \<Longrightarrow> modifies_at_most aag ?L'4 ?Q'4 f
 5. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f\<rbrakk> \<Longrightarrow> \<forall>s t. ?P4 s \<and> ?P'4 t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f t). rva = rvb)
 6. \<And>s. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f; Q s\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 7. \<And>s. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f; Q s\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s
theory Ipc_IF

lemma BlockedOnReceive_inj:
  "x = (case (BlockedOnReceive x pl) of BlockedOnReceive x pl \<Rightarrow> x)"
  "pl = (case (BlockedOnReceive x pl) of BlockedOnReceive x pl \<Rightarrow> pl)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = (case BlockedOnReceive x pl of BlockedOnReceive x pl \<Rightarrow> x) &&& pl = (case BlockedOnReceive x pl of BlockedOnReceive x pl \<Rightarrow> pl)
theory Ipc_IF

lemma receive_blockedD:
  "receive_blocked st \<Longrightarrow> \<exists>epptr pl. st = BlockedOnReceive epptr pl" by (cases st; simp add: receive_blocked_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. receive_blocked st \<Longrightarrow> \<exists>epptr pl. st = BlockedOnReceive epptr pl
theory Ipc_IF

lemma receive_signal_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag (l :: 'a subject_label)
     (valid_objs and pas_refined aag and (\<lambda>s. is_subject aag (cur_thread s))
                 and K ((\<forall>ntfnptr \<in> obj_refs_ac cap.
                           (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and>
                           is_subject aag thread)))
     (receive_signal thread cap is_blocking)" unfolding receive_signal_def fun_app_def do_nbrecv_failed_transfer_def by (wp set_simple_ko_reads_respects set_thread_state_reads_respects
         as_user_set_register_reads_respects' get_simple_ko_reads_respects hoare_vcg_all_lift
      | wpc
      | wp (once) hoare_drop_imps
      | force dest: reads_ep)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (valid_objs and pas_refined aag and (\<lambda>s. is_subject aag (cur_thread s)) and K (\<forall>ntfnptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> is_subject aag thread)) (receive_signal thread cap is_blocking) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (valid_objs and pas_refined aag and (\<lambda>s. is_subject aag (cur_thread s)) and K (\<forall>ntfnptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> is_subject aag thread)) (do ntfnptr <- case cap of NotificationCap ntfnptr badge rights \<Rightarrow> return ntfnptr | _ \<Rightarrow> fail;
ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification ntfnptr);
set_notification ntfnptr (ntfn_set_obj ntfn (WaitingNtfn [thread]))
od | False \<Rightarrow> do as_user thread (setRegister badge_register 0);
return ()
od | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification ntfnptr);
set_notification ntfnptr (ntfn_set_obj ntfn (WaitingNtfn (queue @ [thread])))
od | False \<Rightarrow> do as_user thread (setRegister badge_register 0);
return ()
od | ActiveNtfn badge \<Rightarrow> do as_user thread (setRegister badge_register badge);
set_notification ntfnptr (ntfn_set_obj ntfn IdleNtfn)
od
od)
theory Ipc_IF

lemma for_each_byte_of_word_def2:
  "for_each_byte_of_word P ptr \<equiv> (\<forall>x\<in>ptr_range ptr word_size_bits. P x)" by (simp add: for_each_byte_of_word_def ptr_range_def word_size_size_bits_word add_diff_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. for_each_byte_of_word P ptr \<equiv> \<forall>x\<in>ptr_range ptr word_size_bits. P x
theory Ipc_IF

lemma lookup_ipc_buffer_aag_can_read_or_affect:
  "\<lbrace>pas_refined aag and valid_objs and K (aag_can_read aag thread \<or> aag_can_affect aag l thread)\<rbrace>
   lookup_ipc_buffer is_receiver thread
   \<lbrace>\<lambda>rv s. aag_can_read_or_affect_ipc_buffer aag l rv\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_strengthen_post[OF lookup_ipc_buffer_has_read_auth]) apply (auto simp: ipc_buffer_has_read_auth_def aag_can_read_or_affect_ipc_buffer_def
             intro: reads_read_thread_read_pages
              simp: aag_can_affect_label_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and valid_objs and K (aag_can_read_or_affect aag l thread)\<rbrace> lookup_ipc_buffer is_receiver thread \<lbrace>\<lambda>rv s. aag_can_read_or_affect_ipc_buffer aag l rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. aag_can_read_or_affect aag l thread \<Longrightarrow> \<lbrace>pas_refined aag and valid_objs\<rbrace> lookup_ipc_buffer is_receiver thread \<lbrace>\<lambda>rv s. aag_can_read_or_affect_ipc_buffer aag l rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>aag_can_read_or_affect aag l thread; ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) rv\<rbrakk> \<Longrightarrow> aag_can_read_or_affect_ipc_buffer aag l rv proof (prove)
goal:
No subgoals!