kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_IF

lemma do_ipc_transfer_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag l (pspace_aligned and valid_vspace_objs and valid_arch_state and
                         valid_objs and valid_mdb and pas_refined aag and
                         K ((grant \<longrightarrow> (is_subject aag sender \<and>
                                       is_subject aag receiver)) \<and>
                           aag_can_read_or_affect aag l sender \<and>
                           aag_can_read_or_affect aag l receiver
                           ))
     (do_ipc_transfer sender ep badge grant receiver)" unfolding do_ipc_transfer_def apply (wp do_normal_transfer_reads_respects lookup_ipc_buffer_reads_respects
            lookup_ipc_buffer_has_read_auth do_fault_transfer_reads_respects
            thread_get_reads_respects lookup_ipc_buffer_has_auth
            lookup_ipc_buffer_aligned
        | wpc
        | simp
        | wp (once) hoare_drop_imps
        | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K ((grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<and> aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect aag l receiver)) (do_ipc_transfer sender ep badge grant receiver) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K ((grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<and> aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect aag l receiver)) (do recv_buffer <- lookup_ipc_buffer True receiver;
fault <- thread_get tcb_fault sender;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False sender;
do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer
od | Some f \<Rightarrow> do_fault_transfer badge sender receiver recv_buffer
od) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma receive_endpoint_threads_blocked:
"\<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s;
  ko_at (Endpoint (RecvEP list)) ep s; x\<in>set list\<rbrakk> \<Longrightarrow>
  st_tcb_at (receive_blocked_on ep) x s" apply (rule ep_queued_st_tcb_at'') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (RecvEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> st_tcb_at (receive_blocked_on ep) x s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (RecvEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> ko_at (Endpoint ?ep) ?ptr s
 2. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (RecvEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> (x, ?rt) \<in> ep_q_refs_of ?ep
 3. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (RecvEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> valid_objs s
 4. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (RecvEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 5. \<And>pl pl'. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (RecvEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> ?rt = EPSend \<and> receive_blocked_on ep (BlockedOnSend ?ptr pl) \<or> ?rt = EPRecv \<and> receive_blocked_on ep (BlockedOnReceive ?ptr pl') proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma receive_blocked_threads_have_Receive_auth:
  "\<lbrakk>pas_refined aag s; valid_objs s; sym_refs (state_refs_of s);
    st_tcb_at (receive_blocked_on ep) x s\<rbrakk> \<Longrightarrow>
  (pasObjectAbs aag x,Receive,pasObjectAbs aag ep) \<in> pasPolicy aag" apply (drule_tac auth="Receive" 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 (receive_blocked_on ep) x s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, 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 (receive_blocked_on ep) x s\<rbrakk> \<Longrightarrow> (x, Receive, ?y) \<in> state_objs_to_policy s
 2. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); st_tcb_at (receive_blocked_on ep) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ?y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, 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 (receive_blocked_on ep) x s\<rbrakk> \<Longrightarrow> (?y, Receive) \<in> thread_st_auth s x
 2. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); st_tcb_at (receive_blocked_on ep) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ?y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, 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; receive_blocked_on ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> (?y, Receive) \<in> tcb_st_to_auth (tcb_state tcb)
 2. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); st_tcb_at (receive_blocked_on ep) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ?y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma receive_endpoint_reads_affects_queued:
  "\<lbrakk>(pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag;
        aag_can_read_label aag (pasObjectAbs 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 (RecvEP list)) epptr s; ep = RecvEP list;
        x \<in> set list\<rbrakk>
       \<Longrightarrow>
             aag_can_read_label aag (pasObjectAbs aag x) \<or>
             aag_can_affect aag l x" apply (frule receive_endpoint_threads_blocked, (simp | assumption)+) apply (drule receive_blocked_threads_have_Receive_auth, (simp | assumption)+) apply (auto dest: read_sync_ep_read_receivers) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; aag_can_read_or_affect aag l epptr; pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (RecvEP list)) epptr s; ep = RecvEP list; x \<in> set list\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; aag_can_read_or_affect aag l epptr; pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (RecvEP list)) epptr s; ep = RecvEP list; x \<in> set list; st_tcb_at (receive_blocked_on epptr) x s\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; aag_can_read_or_affect aag l epptr; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (RecvEP list)) epptr s; ep = RecvEP list; x \<in> set list; st_tcb_at (receive_blocked_on epptr) x s; (pasObjectAbs aag x, Receive, 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 handle_fault_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag (l :: 'a subject_label) (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)" unfolding handle_fault_def catch_def fun_app_def handle_double_fault_def apply (wp (once) hoare_drop_imps |
        wp set_thread_state_reads_respects send_fault_ipc_reads_respects | wpc | simp)+ apply (fastforce intro: reads_affects_equiv_get_tcb_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects 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) proof (prove)
goal (1 subgoal):
 1. reads_respects 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)) (do _ <- gets_the (get_tcb thread);
do x <- send_fault_ipc thread fault;
case x of Inl e \<Rightarrow> set_thread_state thread Inactive | Inr b \<Rightarrow> return b
od;
return ()
od) 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> \<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb thread s = get_tcb thread t proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma handle_fault_reply_reads_respects:
  "reads_respects aag l (K (aag_can_read aag thread)) (handle_fault_reply fault thread x y)" apply (case_tac fault) apply (wp as_user_reads_respects thread_get_reads_respects
               thread_get_wp' handle_arch_fault_reply_reads_respects[simplified K_def]
            | simp add: det_zipWithM_x det_setRegister)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag thread)) (handle_fault_reply fault thread x y) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. fault = CapFault x11 x12 x13 \<Longrightarrow> reads_respects aag l (K (aag_can_read aag thread)) (handle_fault_reply fault thread x y)
 2. \<And>x2. fault = UnknownSyscallException x2 \<Longrightarrow> reads_respects aag l (K (aag_can_read aag thread)) (handle_fault_reply fault thread x y)
 3. \<And>x31 x32. fault = UserException x31 x32 \<Longrightarrow> reads_respects aag l (K (aag_can_read aag thread)) (handle_fault_reply fault thread x y)
 4. \<And>x4. fault = ArchFault x4 \<Longrightarrow> reads_respects aag l (K (aag_can_read aag thread)) (handle_fault_reply fault thread x y) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma lookup_ipc_buffer_has_read_auth':
  "\<lbrace>pas_refined aag and valid_objs and K (is_subject aag thread)\<rbrace>
   lookup_ipc_buffer is_receiver thread
   \<lbrace>\<lambda>rv s. ipc_buffer_has_read_auth aag (pasSubject aag) rv\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_strengthen_post[OF lookup_ipc_buffer_has_read_auth]) apply (drule sym, simp) done

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

lemma reply_from_kernel_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag l (K (is_subject aag thread)) (reply_from_kernel thread x)" unfolding reply_from_kernel_def fun_app_def by (wp set_message_info_reads_respects set_mrs_reads_respects
         as_user_reads_respects lookup_ipc_buffer_reads_respects
      | simp add: split_def det_setRegister)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag thread)) (reply_from_kernel thread x) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag thread)) (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)
theory Ipc_IF

lemma setup_caller_cap_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state and valid_global_objs\<rbrace>
   setup_caller_cap sender receiver grant
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding setup_caller_cap_def apply (wp cap_insert_globals_equiv'' set_thread_state_globals_equiv) apply (simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and valid_global_objs\<rbrace> setup_caller_cap sender receiver grant \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and valid_global_objs\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. (globals_equiv s and valid_arch_state and valid_global_objs) sa \<Longrightarrow> (globals_equiv s and valid_arch_state) sa \<and> valid_global_objs sa \<and> valid_arch_state sa proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma set_extra_badge_globals_equiv:
  "set_extra_badge buffer badge n \<lbrace>globals_equiv s\<rbrace>" unfolding set_extra_badge_def by (wp store_word_offs_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> set_extra_badge buffer badge n \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> store_word_offs buffer (buffer_cptr_index + n) badge \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory Ipc_IF

lemma transfer_caps_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
   transfer_caps info caps endpoint receiver recv_buffer
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding transfer_caps_def by (wp transfer_caps_loop_globals_equiv | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> transfer_caps info caps endpoint receiver recv_buffer \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> do dest_slots <- get_receive_slots receiver recv_buffer;
mi' <- return $ MI (mi_length info) 0 0 (mi_label info);
case recv_buffer of None \<Rightarrow> return mi' | Some receive_buffer \<Rightarrow> transfer_caps_loop endpoint receive_buffer 0 caps dest_slots mi'
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Ipc_IF

lemma set_collection: "a = {x. x\<in>a}" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a = {x. x \<in> a}
theory Ipc_IF

lemma valid_ep_send_enqueue:
  "\<lbrakk> ko_at (Endpoint (SendEP (t # ts))) a s; valid_objs s \<rbrakk>
     \<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> SendEP (b # bs)) s" unfolding valid_objs_def valid_obj_def valid_ep_def obj_at_def apply (drule bspec) apply (auto split: list.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Endpoint (SendEP (t # ts))) a s; valid_objs s\<rbrakk> \<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> SendEP (b # bs)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>ko. kheap s a = Some ko \<and> Endpoint (SendEP (t # ts)) = ko; \<forall>ptr\<in>dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint IdleEP \<Rightarrow> True | Endpoint (SendEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | Endpoint (RecvEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s)\<rbrakk> \<Longrightarrow> case case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> SendEP (b # bs) of IdleEP \<Rightarrow> True | SendEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | RecvEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts proof (prove)
goal (2 subgoals):
 1. \<exists>ko. kheap s a = Some ko \<and> Endpoint (SendEP (t # ts)) = ko \<Longrightarrow> ?ptr \<in> (dom $ kheap s)
 2. \<lbrakk>\<exists>ko. kheap s a = Some ko \<and> Endpoint (SendEP (t # ts)) = ko; \<exists>obj. kheap s ?ptr = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ?ptr t s | Endpoint IdleEP \<Rightarrow> True | Endpoint (SendEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | Endpoint (RecvEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s)\<rbrakk> \<Longrightarrow> case case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> SendEP (b # bs) of IdleEP \<Rightarrow> True | SendEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | RecvEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma case_list_cons_cong:
  "(case xxs of [] \<Rightarrow> f | x # xs \<Rightarrow> g xxs) =
   (case xxs of [] \<Rightarrow> f | x # xs \<Rightarrow> g (x # xs))" by (simp split: list.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case xxs of [] \<Rightarrow> f | x # xs \<Rightarrow> g xxs) = (case xxs of [] \<Rightarrow> f | x # xs \<Rightarrow> g (x # xs))
theory Ipc_IF

lemma valid_ntfn_dequeue:
  "\<lbrakk> ko_at (Notification ntfn) ntfnptr s;
     ntfn_obj ntfn = (WaitingNtfn (t # ts)); valid_objs s; ts \<noteq> [] \<rbrakk>
     \<Longrightarrow> valid_ntfn ntfn s" unfolding valid_objs_def valid_obj_def valid_ntfn_def obj_at_def apply (drule bspec) apply (auto split: list.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn (t # ts); valid_objs s; ts \<noteq> []\<rbrakk> \<Longrightarrow> valid_ntfn ntfn s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>ko. kheap s ntfnptr = Some ko \<and> Notification ntfn = ko; ntfn_obj ntfn = WaitingNtfn (t # ts); \<forall>ptr\<in>dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> (case ntfn_obj p of WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts \<and> (case ntfn_bound_tcb p of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> valid_bound_tcb (ntfn_bound_tcb p) s | ArchObj ao \<Rightarrow> arch_valid_obj ao s); ts \<noteq> []\<rbrakk> \<Longrightarrow> (case ntfn_obj ntfn of WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> valid_bound_tcb (ntfn_bound_tcb ntfn) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<exists>ko. kheap s ntfnptr = Some ko \<and> Notification ntfn = ko; ntfn_obj ntfn = WaitingNtfn (t # ts); ts \<noteq> []\<rbrakk> \<Longrightarrow> ?ptr \<in> (dom $ kheap s)
 2. \<lbrakk>\<exists>ko. kheap s ntfnptr = Some ko \<and> Notification ntfn = ko; ntfn_obj ntfn = WaitingNtfn (t # ts); ts \<noteq> []; \<exists>obj. kheap s ?ptr = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ?ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> (case ntfn_obj p of WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts \<and> (case ntfn_bound_tcb p of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> valid_bound_tcb (ntfn_bound_tcb p) s | ArchObj ao \<Rightarrow> arch_valid_obj ao s)\<rbrakk> \<Longrightarrow> (case ntfn_obj ntfn of WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> valid_bound_tcb (ntfn_bound_tcb ntfn) s proof (prove)
goal:
No subgoals!