theory TCB_DP

lemma call_kernel_with_intent_no_fault_helper':
   "\<lbrakk>cdl_intent_op intent = Some intent_op \<and>
 cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra;
 \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>;
 \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>;
 \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>;
 \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv
      \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and>
              cdl_current_domain s = minBound \<and>
              <(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)> s \<and> Rb s\<rbrace>,
      \<lbrace>E\<rbrace>;
 \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>;
 \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>;
 \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra
     \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>;
 \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr
 \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>;
 \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -;
 \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s.  \<not> ep_related_cap cap \<and> tcb_at' (\<lambda>tcb. True) root_tcb_id s \<and>
        ((cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound) \<longrightarrow> P s) \<rbrace>
   call_kernel_with_intent intent False \<lbrace>\<lambda>r. Q\<rbrace>" apply (wp call_kernel_with_intent_no_fault_helper) apply (clarsimp | assumption | safe | wp | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>; \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>E\<rbrace>; \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>; \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>; \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>; \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -; \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> ep_related_cap cap \<and> tcb_at' (\<lambda>tcb. True) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrace> call_kernel_with_intent intent False \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>iv. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>; \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>E\<rbrace>; \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>; \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>; \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>; \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -; \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?PIV1 iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>\<lambda>r s. tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = cdl_intent_cap intent \<and> cdl_intent_extras (cdl_tcb_intent tcb) = cdl_intent_extras intent) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> no_pending s \<and> ?Pd2.1 s\<rbrace>
 2. \<And>iv. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>; \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>E\<rbrace>; \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>; \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>; \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>; \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -; \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Ps1 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. ?PIV1 iv\<rbrace>
 3. \<And>c ref cs. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>; \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>E\<rbrace>; \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>; \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>; \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>; \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -; \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Pd1 cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>?Ps1\<rbrace>, \<lbrace>\<lambda>xa s. False\<rbrace>
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>; \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>E\<rbrace>; \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>; \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>; \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>; \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -; \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Pd1.1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. ?Pd1 xa (fst r) (snd r)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 5. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>; \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>E\<rbrace>; \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>; \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>; \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>; \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -; \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.1\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. ?Pd1.1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>; \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>E\<rbrace>; \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>; \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>; \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>; \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -; \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.1\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -
 7. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>; \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>E\<rbrace>; \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>; \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>; \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>; \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -; \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P1\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. ?Pd2.1\<rbrace>
 8. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<lbrace>R\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>Ra\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>Rb\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>; \<And>E iv. \<lbrace>PIV iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> Rb s\<rbrace>, \<lbrace>E\<rbrace>; \<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>; \<And>E c ref cs. \<lbrace>Pd cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>Ps\<rbrace>, \<lbrace>E\<rbrace>; \<And>E r. \<lbrace>Pd1 (fst r) (snd r)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst r) (snd r)\<rbrace>, \<lbrace>E\<rbrace>; \<And>E. \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>r s. Pd1 (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -; \<lbrace>P\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>rv. Pd2\<rbrace>; \<not> ep_related_cap cap \<and> tcb_at' (\<lambda>tcb. True) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> tcb_at' (\<lambda>tcb. True) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P1 s) proof (prove)
goal:
No subgoals!