theory Invocation_DP

lemma call_kernel_with_intent_allow_error_helper:
  assumes unify: "cdl_intent_op intent = Some intent_op \<and>
  cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra"
  and set_cap_hold: "\<lbrace>R\<rbrace>set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>"
  and mark_tcb_intent_error_hold: "\<lbrace>Ra\<rbrace>mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>r. R\<rbrace>"
                                  "\<lbrace>Perror\<rbrace>mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>r. Perror\<rbrace>"
  and corrupt_ipc_buffer_hold: "\<lbrace>Rb\<rbrace>corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<rbrace>"
                               "\<lbrace>Perror\<rbrace>corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Perror\<rbrace>"

  and perform_invocation_hold: "\<And>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>\<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 \<and>
                          cdl_intent_error (cdl_tcb_intent tcb) = False)
                       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 s\<rbrace>"
  and set_restart_cap_hold: "\<And>iv.
    \<lbrace>\<lambda>s. Ps iv s \<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>"

  and decode_invocation_allow_error:
      "\<And>c ref cs. \<lbrace> Pd cs c ref \<rbrace> decode_invocation c ref cs intent_op
       \<lbrace> Ps \<rbrace>, \<lbrace>\<lambda>r s. Perror s
          \<and> cdl_current_thread s = Some root_tcb_id
          \<and> cdl_current_domain s = minBound
          \<and> <(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)> s \<rbrace>
"
  and lookup_extra_caps_exec:
  "\<And>r. \<lbrace> Pd1 (fst r) (snd r) \<rbrace> lookup_extra_caps root_tcb_id  intent_extra
       \<lbrace> \<lambda>xa s. Pd xa (fst r) (snd r) s \<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>"
  and lookup_cap_and_slot_exec:
      "\<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>\<lambda>y s. False \<rbrace>"
  and upd_thread:
    "\<lbrace>P\<rbrace> update_thread root_tcb_id  (cdl_tcb_intent_update (\<lambda>x. intent))
     \<lbrace>\<lambda>rv s. Pd2 s\<rbrace>"
  and error_imp: "\<And>s. Pd2 s \<Longrightarrow> (cdl_current_thread s = Some root_tcb_id)
  \<and> cdl_current_domain s = minBound
  \<and> <(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap
    \<and>* (root_tcb_id) \<mapsto>f (Tcb tcb) \<and>* (\<lambda>s. True)> s
  \<and> Perror s"
  shows
  "\<lbrace>\<lambda>s. \<not> cdl_intent_error intent
  \<and> ((cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound) \<longrightarrow> P s)
  \<and> <(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap
  \<and>* (root_tcb_id) \<mapsto>f (Tcb tcb) \<and>* (\<lambda>s. True)> s
   \<rbrace>  call_kernel_with_intent intent check \<lbrace>\<lambda>r s. ((\<not> r \<or> check) \<longrightarrow> Q s)
     \<and> ((r \<and> \<not> check) \<longrightarrow> Perror s) \<rbrace>" using unify apply (simp add:call_kernel_with_intent_def) apply (wp thread_has_error_wp) apply (simp add:call_kernel_loop_def) apply (rule_tac P = "thread_ptr = root_tcb_id" in hoare_gen_asm) apply (rule_tac Q = "\<lambda>r s. (cdl_current_thread s = Some root_tcb_id
                                    \<and> cdl_current_domain s = minBound) \<longrightarrow>
                                       (\<not>tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and>
                                       (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)"
                        in hoare_strengthen_post[rotated]) apply (fastforce simp: error_imp) apply wp  (* fragile , do not know why *)
            apply (rule hoare_vcg_imp_lift[where P' = "\<lambda>s. cdl_current_thread s \<noteq> Some root_tcb_id
                                                          \<or> cdl_current_domain s \<noteq> minBound"]) apply (rule hoare_pre,(wp hoare_vcg_imp_lift|wpc|simp cong: if_cong)+)[1] apply (wp | wpc | simp)+ apply (rule hoare_pre_cont) apply (wp has_restart_cap_sep_wp[where cap = RunningCap])+ apply simp apply (rule_tac current_thread1=root_tcb_id and current_domain1=minBound in
                         hoare_strengthen_post[OF schedule_no_choice_wp]) apply (clarsimp, assumption) apply clarsimp apply (rule_tac Q =
               "\<lambda>r a. (\<not> tcb_has_error root_tcb_id a \<longrightarrow> (Q a
                            \<and> cdl_current_thread a = Some root_tcb_id
                            \<and> cdl_current_domain a = minBound
                            \<and> <(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)> a))
                            \<and> (tcb_has_error root_tcb_id a \<longrightarrow> (Perror a
                            \<and> cdl_current_thread a = Some root_tcb_id
                            \<and> cdl_current_domain a = minBound
                            \<and> <(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)> a))"
               in hoare_strengthen_post[rotated]) apply fastforce apply (rule whileLoop_wp[where
                I = "\<lambda>rv s. case rv of Inl _ \<Rightarrow>
                     (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 \<and>
                            cdl_intent_error (cdl_tcb_intent tcb) = False)
                            root_tcb_id s \<and>
                     cdl_current_thread s = Some root_tcb_id \<and>
                     cdl_current_domain s = minBound \<and> Pd2 s)
                | Inr rv \<Rightarrow> Q (Inr rv) s" and Q=Q for Q, rotated]) apply (case_tac r, simp_all)[1] apply (simp add: validE_def[symmetric]) apply (rule hoare_pre, wp) apply (simp add: validE_def, (wp | simp add: validE_def[symmetric])+) apply (wp handle_pending_interrupts_no_ntf_cap) apply (rule handle_event_syscall_allow_error
                       [where cur_thread = root_tcb_id
                          and intent_op = intent_op
                          and intent_cptr = intent_cptr
                          and intent_extra = intent_extra]) apply (wp set_cap_wp
                              set_cap_hold delete_cap_simple_wp[where cap = RestartCap])[1] apply (rule decode_invocation_allow_error) apply (rule lookup_extra_caps_exec) apply (rule lookup_cap_and_slot_exec) apply (unfold validE_R_def) apply (rule hoare_post_impErr) apply (rule lookup_cap_and_slot_exec) apply simp apply simp apply ((wp corrupt_ipc_buffer_sep_inv corrupt_ipc_buffer_active_tcbs
                          mark_tcb_intent_error_hold corrupt_ipc_buffer_hold | simp)+)[4] apply (rule hoare_post_impErr[OF perform_invocation_hold]) apply (fastforce simp:sep_state_projection_def sep_any_def sep_map_c_def sep_conj_def) apply simp apply (wp set_restart_cap_hold) apply (clarsimp dest!:error_imp) apply (sep_cancel, simp) apply (clarsimp split: sum.split_asm) apply (rule_tac P = "thread_ptr = root_tcb_id" in hoare_gen_asm) apply simp apply (wp upd_thread update_thread_wp)+ apply (clarsimp simp: sep_map_c_conj sep_map_f_conj object_at_def
                        object_project_def sep_state_projection_def
                  split:option.splits cdl_object.split) apply (case_tac z) apply (clarsimp dest!:arg_cong[where f= object_type],simp add:object_type_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrace> call_kernel_with_intent intent check \<lbrace>\<lambda>r s. (\<not> r \<or> check \<longrightarrow> Q s) \<and> (r \<and> \<not> check \<longrightarrow> Perror s)\<rbrace> proof (prove)
using this:
cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrace> call_kernel_with_intent intent check \<lbrace>\<lambda>r s. (\<not> r \<or> check \<longrightarrow> Q s) \<and> (r \<and> \<not> check \<longrightarrow> Perror s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrace> do thread_ptr <- gets_the cdl_current_thread;
y <- assert (thread_ptr = root_tcb_id);
domain <- gets cdl_current_domain;
y <- assert (domain = minBound);
y <- update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent));
y <- call_kernel_loop (SyscallEvent SysCall);
ntptr <- gets_the cdl_current_thread;
y <- assert (thread_ptr = ntptr);
ndomain <- gets cdl_current_domain;
y <- assert (minBound = ndomain);
has_error <- thread_has_error thread_ptr;
y <- when check (assert (\<not> has_error));
return has_error
od \<lbrace>\<lambda>r s. ((r \<longrightarrow> check) \<longrightarrow> Q s) \<and> (r \<and> \<not> check \<longrightarrow> Perror s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>thread_ptr y domain ya yb. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B8 thread_ptr y domain ya yb\<rbrace> call_kernel_loop (SyscallEvent SysCall) \<lbrace>\<lambda>yc s. cdl_current_thread s \<noteq> None \<longrightarrow> thread_ptr = the (cdl_current_thread s) \<longrightarrow> minBound = cdl_current_domain s \<longrightarrow> (if check then \<lambda>sa. \<not> tcb_has_error thread_ptr s \<longrightarrow> ((tcb_has_error thread_ptr s \<longrightarrow> check) \<longrightarrow> Q sa) \<and> (tcb_has_error thread_ptr s \<and> \<not> check \<longrightarrow> Perror sa) else (\<lambda>a. ((tcb_has_error thread_ptr s \<longrightarrow> check) \<longrightarrow> Q a) \<and> (tcb_has_error thread_ptr s \<and> \<not> check \<longrightarrow> Perror a))) s\<rbrace>
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>?B8 thread_ptr y domain ya\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (7 subgoals):
 1. \<And>thread_ptr domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B8 thread_ptr () domain () ()\<rbrace> do y <- whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError);
y <- schedule;
gets cdl_current_thread >>= case_option (return ()) (\<lambda>thread. do restart <- has_restart_cap thread;
when restart (set_cap (thread, tcb_pending_op_slot) RunningCap)
od)
od \<lbrace>\<lambda>yc s. (check \<longrightarrow> (\<exists>y. cdl_current_thread s = Some y) \<longrightarrow> thread_ptr = the (cdl_current_thread s) \<longrightarrow> minBound = cdl_current_domain s \<longrightarrow> \<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (\<not> check \<longrightarrow> (\<exists>y. cdl_current_thread s = Some y) \<longrightarrow> thread_ptr = the (cdl_current_thread s) \<longrightarrow> minBound = cdl_current_domain s \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s))\<rbrace>
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>?B8 thread_ptr y domain ya\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (7 subgoals):
 1. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> do y <- whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError);
y <- schedule;
gets cdl_current_thread >>= case_option (return ()) (\<lambda>thread. do restart <- has_restart_cap thread;
when restart (set_cap (thread, tcb_pending_op_slot) RunningCap)
od)
od \<lbrace>\<lambda>yc s. (check \<longrightarrow> (\<exists>y. cdl_current_thread s = Some y) \<longrightarrow> thread_ptr = the (cdl_current_thread s) \<longrightarrow> minBound = cdl_current_domain s \<longrightarrow> \<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (\<not> check \<longrightarrow> (\<exists>y. cdl_current_thread s = Some y) \<longrightarrow> thread_ptr = the (cdl_current_thread s) \<longrightarrow> minBound = cdl_current_domain s \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s))\<rbrace>
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (8 subgoals):
 1. \<And>thread_ptr domain rv s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id; cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)\<rbrakk> \<Longrightarrow> (check \<longrightarrow> (\<exists>y. cdl_current_thread s = Some y) \<longrightarrow> thread_ptr = the (cdl_current_thread s) \<longrightarrow> minBound = cdl_current_domain s \<longrightarrow> \<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (\<not> check \<longrightarrow> (\<exists>y. cdl_current_thread s = Some y) \<longrightarrow> thread_ptr = the (cdl_current_thread s) \<longrightarrow> minBound = cdl_current_domain s \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s))
 2. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> do y <- whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError);
y <- schedule;
gets cdl_current_thread >>= case_option (return ()) (\<lambda>thread. do restart <- has_restart_cap thread;
when restart (set_cap (thread, tcb_pending_op_slot) RunningCap)
od)
od \<lbrace>\<lambda>r s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)\<rbrace>
 3. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 4. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 5. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 6. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 7. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<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; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (7 subgoals):
 1. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> do y <- whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError);
y <- schedule;
gets cdl_current_thread >>= case_option (return ()) (\<lambda>thread. do restart <- has_restart_cap thread;
when restart (set_cap (thread, tcb_pending_op_slot) RunningCap)
od)
od \<lbrace>\<lambda>r s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)\<rbrace>
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (10 subgoals):
 1. \<And>thread_ptr domain x xa xb. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B143 thread_ptr domain x xa xb\<rbrace> case xb of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart (set_cap (thread, tcb_pending_op_slot) RunningCap)
od \<lbrace>\<lambda>r s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)\<rbrace>
 2. \<And>thread_ptr domain x xa. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread_ptr domain x xa\<rbrace> gets cdl_current_thread \<lbrace>?B143 thread_ptr domain x xa\<rbrace>
 3. \<And>thread_ptr domain x. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread_ptr domain x\<rbrace> schedule \<lbrace>?B142 thread_ptr domain x\<rbrace>
 4. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>?B141 thread_ptr domain\<rbrace>
 5. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 6. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 7. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 8. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 9. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 10. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (10 subgoals):
 1. \<And>thread_ptr domain x xa xb. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B143 thread_ptr domain x xa xb\<rbrace> case xb of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart (set_cap (thread, tcb_pending_op_slot) RunningCap)
od \<lbrace>\<lambda>r s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)\<rbrace>
 2. \<And>thread_ptr domain x xa. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread_ptr domain x xa\<rbrace> gets cdl_current_thread \<lbrace>?B143 thread_ptr domain x xa\<rbrace>
 3. \<And>thread_ptr domain x. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread_ptr domain x\<rbrace> schedule \<lbrace>?B142 thread_ptr domain x\<rbrace>
 4. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>?B141 thread_ptr domain\<rbrace>
 5. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 6. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 7. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 8. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 9. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 10. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (11 subgoals):
 1. \<And>thread_ptr domain x xa xb. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound\<rbrace> case xb of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart (set_cap (thread, tcb_pending_op_slot) RunningCap)
od \<lbrace>\<lambda>r s. \<not> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound)\<rbrace>
 2. \<And>thread_ptr domain x xa xb. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?Q'145 thread_ptr domain x xa xb\<rbrace> case xb of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart (set_cap (thread, tcb_pending_op_slot) RunningCap)
od \<lbrace>\<lambda>rv s. (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)\<rbrace>
 3. \<And>thread_ptr domain x xa. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread_ptr domain x xa\<rbrace> gets cdl_current_thread \<lbrace>\<lambda>xb s. (cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> ?Q'145 thread_ptr domain x xa xb s\<rbrace>
 4. \<And>thread_ptr domain x. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread_ptr domain x\<rbrace> schedule \<lbrace>?B142 thread_ptr domain x\<rbrace>
 5. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>?B141 thread_ptr domain\<rbrace>
 6. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 7. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 8. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 9. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 10. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>thread_ptr domain x xa xb. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?Q'145 thread_ptr domain x xa xb\<rbrace> case xb of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart (set_cap (thread, tcb_pending_op_slot) RunningCap)
od \<lbrace>\<lambda>rv s. (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)\<rbrace>
 2. \<And>thread_ptr domain x xa. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread_ptr domain x xa\<rbrace> gets cdl_current_thread \<lbrace>\<lambda>xb s. (cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> ?Q'145 thread_ptr domain x xa xb s\<rbrace>
 3. \<And>thread_ptr domain x. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread_ptr domain x\<rbrace> schedule \<lbrace>?B142 thread_ptr domain x\<rbrace>
 4. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>?B141 thread_ptr domain\<rbrace>
 5. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 6. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 7. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 8. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 9. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 10. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (11 subgoals):
 1. \<And>thread_ptr domain x xb x2 xc. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id; xb = Some x2; xc\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 root_tcb_id domain x () (Some x2) x2 True\<rbrace> set_cap (x2, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>rv s. (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)\<rbrace>
 2. \<And>thread_ptr domain x xa xb x2. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id; xb = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R199 thread_ptr domain x xa xb x2\<rbrace> has_restart_cap x2 \<lbrace>\<lambda>xc. if xc then ?Q206 thread_ptr domain x xa xb x2 xc else (\<lambda>s. (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s))\<rbrace>
 3. \<And>thread_ptr domain x xa. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread_ptr domain x xa\<rbrace> gets cdl_current_thread \<lbrace>\<lambda>xb s. (cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> (xb = None \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)) \<and> (\<forall>xc. xb = Some xc \<longrightarrow> ?R199 thread_ptr domain x xa xb xc s)\<rbrace>
 4. \<And>thread_ptr domain x. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread_ptr domain x\<rbrace> schedule \<lbrace>?B142 thread_ptr domain x\<rbrace>
 5. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>?B141 thread_ptr domain\<rbrace>
 6. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 7. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 8. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 9. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 10. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>thread_ptr domain x xa xb x2. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id; xb = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R199 thread_ptr domain x xa xb x2\<rbrace> has_restart_cap x2 \<lbrace>\<lambda>xc. if xc then \<lambda>a. False else (\<lambda>s. (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s))\<rbrace>
 2. \<And>thread_ptr domain x xa. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread_ptr domain x xa\<rbrace> gets cdl_current_thread \<lbrace>\<lambda>xb s. (cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> (xb = None \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)) \<and> (\<forall>xc. xb = Some xc \<longrightarrow> ?R199 thread_ptr domain x xa xb xc s)\<rbrace>
 3. \<And>thread_ptr domain x. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread_ptr domain x\<rbrace> schedule \<lbrace>?B142 thread_ptr domain x\<rbrace>
 4. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>?B141 thread_ptr domain\<rbrace>
 5. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 6. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 7. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 8. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 9. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 10. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (8 subgoals):
 1. \<And>thread_ptr domain x. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread_ptr domain x\<rbrace> schedule \<lbrace>\<lambda>xa s. (cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> (cdl_current_thread s = None \<longrightarrow> (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s)) \<and> (\<forall>x. cdl_current_thread s = Some x \<longrightarrow> cdl.lift ((x, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (if RunningCap = RestartCap then \<lambda>a. False else (\<lambda>s. (\<not> tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Q s) \<and> (tcb_has_error (the (cdl_current_thread s)) s \<longrightarrow> Perror s))) s)\<rbrace>
 2. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>?B141 thread_ptr domain\<rbrace>
 3. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 4. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 5. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 6. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 7. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<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; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (8 subgoals):
 1. \<And>thread_ptr domain x. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?B141 root_tcb_id domain x\<rbrace> schedule \<lbrace>\<lambda>xa s. cdl_current_thread s = Some root_tcb_id \<longrightarrow> cdl_current_domain s = minBound \<longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s)\<rbrace>
 2. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>?B141 thread_ptr domain\<rbrace>
 3. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 4. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 5. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 6. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 7. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<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; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (8 subgoals):
 1. \<And>thread_ptr domain x rv s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id; cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P217 root_tcb_id domain x s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<longrightarrow> cdl_current_domain s = minBound \<longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s)
 2. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>\<lambda>a b. cdl_current_thread b = Some thread_ptr \<and> cdl_current_domain b = minBound \<and> ?P217 thread_ptr domain a b\<rbrace>
 3. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 4. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 5. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 6. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 7. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<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; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (7 subgoals):
 1. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 thread_ptr () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>\<lambda>a b. cdl_current_thread b = Some thread_ptr \<and> cdl_current_domain b = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) b \<and> (\<not> tcb_has_error thread_ptr b \<longrightarrow> Q b) \<and> (tcb_has_error thread_ptr b \<longrightarrow> Perror b)\<rbrace>
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (7 subgoals):
 1. \<And>domain. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 root_tcb_id () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>\<lambda>a b. cdl_current_thread b = Some root_tcb_id \<and> cdl_current_domain b = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) b \<and> (\<not> tcb_has_error root_tcb_id b \<longrightarrow> Q b) \<and> (tcb_has_error root_tcb_id b \<longrightarrow> Perror b)\<rbrace>
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (8 subgoals):
 1. \<And>domain rv s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)\<rbrakk> \<Longrightarrow> 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 RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s)
 2. \<And>domain. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 root_tcb_id () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>\<lambda>r a. (\<not> tcb_has_error root_tcb_id a \<longrightarrow> Q a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error root_tcb_id a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)\<rbrace>
 3. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 4. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 5. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 6. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 7. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<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; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (7 subgoals):
 1. \<And>domain. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 root_tcb_id () domain () ()\<rbrace> whileLoop (\<lambda>r s. isLeft r)
  (\<lambda>r. handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od)) (Inl PreemptError) \<lbrace>\<lambda>r a. (\<not> tcb_has_error root_tcb_id a \<longrightarrow> Q a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error root_tcb_id a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)\<rbrace>
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. ?P'36 thread_ptr y domain ya a and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (8 subgoals):
 1. \<And>domain r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s); isRight r\<rbrakk> \<Longrightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)
 2. \<And>domain r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrace> handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od) \<lbrace>\<lambda>rv s. case rv of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)\<rbrace>
 3. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 4. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 5. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 6. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 7. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<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; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (7 subgoals):
 1. \<And>domain r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrace> handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od) \<lbrace>\<lambda>rv s. case rv of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)\<rbrace>
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (7 subgoals):
 1. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrace> handle_event (SyscallEvent SysCall) <handle> (\<lambda>_. do y <- handle_pending_interrupts;
throwError PreemptError
od) \<lbrace>\<lambda>rv s. (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)\<rbrace>, \<lbrace>\<lambda>x 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s\<rbrace>
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (9 subgoals):
 1. \<And>r x. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?F297 r x\<rbrace> do y <- handle_pending_interrupts;
throwError PreemptError
od \<lbrace>\<lambda>rv s. (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)\<rbrace>, \<lbrace>\<lambda>x 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s\<rbrace>
 2. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Q293 r\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>rv s. (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)\<rbrace>, \<lbrace>?F297 r\<rbrace>
 3. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> ?Q293 r s
 4. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 5. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 6. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 7. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 8. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 9. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (9 subgoals):
 1. \<And>r x. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?F297 r x\<rbrace> handle_pending_interrupts \<lbrace>\<lambda>a b. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id b \<and> cdl_current_thread b = Some root_tcb_id \<and> cdl_current_domain b = minBound \<and> Pd2 b\<rbrace>
 2. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Q293 r\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>rv s. (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)\<rbrace>, \<lbrace>?F297 r\<rbrace>
 3. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> ?Q293 r s
 4. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 5. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 6. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 7. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 8. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 9. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (8 subgoals):
 1. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Q293 r\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>rv s. (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)\<rbrace>, \<lbrace>\<lambda>x. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 2. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> ?Q293 r s
 3. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 4. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 5. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 6. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 7. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<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; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (19 subgoals):
 1. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rm326 r\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>rv s. Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 2. \<And>r c ref cs. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd326 r cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>?Ps326 r\<rbrace>, \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 3. \<And>r rv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd1.326 r (fst rv) (snd rv)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. ?Pd326 r xa (fst rv) (snd rv)\<rbrace>, \<lbrace>\<lambda>rv s. False\<rbrace>
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.326 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. ?Pd1.326 r (fst rv) (snd rv) s \<and> \<not> ep_related_cap (fst rv)\<rbrace>, \<lbrace>\<lambda>x s. False\<rbrace>
 5. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.326 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -
 6. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv. ?Rm326 r\<rbrace>
 7. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 8. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 9. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 10. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
A total of 19 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>r c ref cs. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd326 r cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>?Ps326 r\<rbrace>, \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 2. \<And>r rv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd1.326 r (fst rv) (snd rv)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. ?Pd326 r xa (fst rv) (snd rv)\<rbrace>, \<lbrace>\<lambda>rv s. False\<rbrace>
 3. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.326 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. ?Pd1.326 r (fst rv) (snd rv) s \<and> \<not> ep_related_cap (fst rv)\<rbrace>, \<lbrace>\<lambda>x s. False\<rbrace>
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.326 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -
 5. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. R s \<and> 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 - \<and>* (\<lambda>s. True)) s\<rbrace>
 6. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 7. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 8. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 9. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 10. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ps326 r iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>r rv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd1.326 r (fst rv) (snd rv)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. Pd xa (fst rv) (snd rv)\<rbrace>, \<lbrace>\<lambda>rv s. False\<rbrace>
 2. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.326 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. ?Pd1.326 r (fst rv) (snd rv) s \<and> \<not> ep_related_cap (fst rv)\<rbrace>, \<lbrace>\<lambda>x s. False\<rbrace>
 3. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.326 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. R s \<and> 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 - \<and>* (\<lambda>s. True)) s\<rbrace>
 5. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 6. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 7. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 8. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 9. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
 10. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; ?Pd2.326 r s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.326 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. Pd1 (fst rv) (snd rv) s \<and> \<not> ep_related_cap (fst rv)\<rbrace>, \<lbrace>\<lambda>x s. False\<rbrace>
 2. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Pd2.326 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -
 3. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. R s \<and> 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 - \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 5. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 6. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 7. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 8. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
 9. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; ?Pd2.326 r s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 10. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (?Pd2.326 r and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, -
 2. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. R s \<and> 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 - \<and>* (\<lambda>s. True)) s\<rbrace>
 3. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 5. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 6. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 7. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
 8. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 9. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 10. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. R s \<and> 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 - \<and>* (\<lambda>s. True)) s\<rbrace>
 3. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 5. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 6. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 7. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
 8. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 9. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 10. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
A total of 15 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Pd2\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>?Q352 r\<rbrace>, \<lbrace>?E352 r\<rbrace>
 2. \<And>r rv s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; ?Q352 r rv s\<rbrakk> \<Longrightarrow> \<not> ep_related_cap (fst rv)
 3. \<And>r e s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; ?E352 r e s\<rbrakk> \<Longrightarrow> True
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. R s \<and> 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 - \<and>* (\<lambda>s. True)) s\<rbrace>
 5. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 6. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 7. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 8. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 9. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
 10. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>r rv s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd1 (fst rv) (snd rv) s \<and> \<not> ep_related_cap (fst rv)\<rbrakk> \<Longrightarrow> \<not> ep_related_cap (fst rv)
 2. \<And>r e s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; False\<rbrakk> \<Longrightarrow> True
 3. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. R s \<and> 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 - \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 5. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 6. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 7. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 8. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
 9. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 10. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>r e s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; False\<rbrakk> \<Longrightarrow> True
 2. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. R s \<and> 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 - \<and>* (\<lambda>s. True)) s\<rbrace>
 3. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 5. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 6. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 7. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
 8. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 9. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 10. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Ra326 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. R s \<and> 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 - \<and>* (\<lambda>s. True)) s\<rbrace>
 2. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>rv s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 3. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Rb326 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra326 r\<rbrace>
 4. \<And>r. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>ya s. Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 5. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb326 r s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 6. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
 7. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 8. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 9. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 10. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
A total of 14 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?PIV326 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. (Rb s \<and> 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 - \<and>* (\<lambda>s. True)) s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>rv. (\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending\<rbrace>
 2. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV326 r iv\<rbrace>
 3. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 4. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 5. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 6. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 7. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 8. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 9. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 10. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (11 subgoals):
 1. \<And>r iv rv s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; 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\<rbrakk> \<Longrightarrow> (Rb s \<and> 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 - \<and>* (\<lambda>s. True)) s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s
 2. \<And>r iv e s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) 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 s\<rbrakk> \<Longrightarrow> ((\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending) s
 3. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. PIV iv\<rbrace>
 4. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 5. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 6. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 7. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 8. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 9. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 10. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>r iv e s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) 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 s\<rbrakk> \<Longrightarrow> ((\<lambda>a. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a) and no_pending) s
 2. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. PIV iv\<rbrace>
 3. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 4. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 5. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 6. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 7. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 8. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 9. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 10. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (9 subgoals):
 1. \<And>r iv. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. PIV iv\<rbrace>
 2. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 3. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 4. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 5. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 6. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 7. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 8. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 9. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (8 subgoals):
 1. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; Pd2 s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s
 2. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 3. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 4. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 5. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 6. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 7. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<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; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s; Perror s\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s
 2. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 3. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 4. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 5. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 6. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 7. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<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; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (7 subgoals):
 1. \<And>r s. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; (case r of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Pd2 s | Inr rv \<Rightarrow> (\<not> tcb_has_error root_tcb_id s \<longrightarrow> Q s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s) \<and> (tcb_has_error root_tcb_id s \<longrightarrow> Perror s \<and> 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 RunningCap \<and>* (\<lambda>s. True)) s)) \<and> isLeft r\<rbrakk> \<Longrightarrow> (Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) root_tcb_id) s
 2. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 4. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 5. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 6. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 7. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (6 subgoals):
 1. \<And>thread_ptr y domain ya. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B7 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 2. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B7 thread_ptr y domain\<rbrace>
 3. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 4. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 5. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 6. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (6 subgoals):
 1. \<And>thread_ptr y domain ya. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'459 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a. (\<lambda>a. case Inl PreemptError of Inl x \<Rightarrow> 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 \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) thread_ptr a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> (\<not> tcb_has_error thread_ptr a \<longrightarrow> Q a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) \<and> (tcb_has_error thread_ptr a \<longrightarrow> Perror a \<and> cdl_current_thread a = Some thread_ptr \<and> cdl_current_domain a = minBound \<and> cdl.lift ((thread_ptr, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a)) and K (thread_ptr = root_tcb_id)\<rbrace>
 2. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>\<lambda>ya. ?P'459 thread_ptr y domain ya and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 4. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 5. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 6. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (6 subgoals):
 1. \<And>thread_ptr domain. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; thread_ptr = root_tcb_id\<rbrakk> \<Longrightarrow> \<lbrace>?P'459 root_tcb_id () domain ()\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>a b. tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id b \<and> cdl_current_thread b = Some root_tcb_id \<and> cdl_current_domain b = minBound \<and> Pd2 b\<rbrace>
 2. \<And>thread_ptr y domain. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B6 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>\<lambda>ya. ?P'459 thread_ptr y domain ya and K (thread_ptr = root_tcb_id)\<rbrace>
 3. \<And>thread_ptr y. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B5 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B6 thread_ptr y\<rbrace>
 4. \<And>thread_ptr. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?B4 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B5 thread_ptr\<rbrace>
 5. cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets_the cdl_current_thread \<lbrace>?B4\<rbrace>
 6. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl_intent_op intent = Some intent_op \<and> cdl_intent_cap intent = intent_cptr \<and> cdl_intent_extras intent = intent_extra; \<not> cdl_intent_error intent \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None \<longrightarrow> the (cdl_current_thread s) = root_tcb_id \<longrightarrow> cdl_current_domain s = minBound \<longrightarrow> ((\<lambda>a. tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent (tcb\<lparr>cdl_tcb_intent := intent\<rparr>)) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent (tcb\<lparr>cdl_tcb_intent := intent\<rparr>)) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent (tcb\<lparr>cdl_tcb_intent := intent\<rparr>)) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent (tcb\<lparr>cdl_tcb_intent := intent\<rparr>))) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> P a) and K (the (cdl_current_thread s) = root_tcb_id)) s proof (prove)
goal (1 subgoal):
 1. \<And>s z. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb proof (prove)
goal (10 subgoals):
 1. \<And>s z. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = Endpoint\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb
 2. \<And>s z. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = Notification\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb
 3. \<And>s z x3. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = Tcb x3\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb
 4. \<And>s z x4. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = CNode x4\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb
 5. \<And>s z x5. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb
 6. \<And>s z x6. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = PageTable x6\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb
 7. \<And>s z x7. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb
 8. \<And>s z x8. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = Frame x8\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb
 9. \<And>s z. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = Untyped\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb
 10. \<And>s z x10. \<lbrakk>cdl_intent_op intent = Some intent_op; \<not> cdl_intent_error intent; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; P s; object_slots (object_clean z) tcb_pending_op_slot = Some RunningCap; cdl_objects s root_tcb_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean (Tcb tcb)); cdl_current_thread s = Some root_tcb_id; cdl_current_domain s = minBound; z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb proof (prove)
goal:
No subgoals!