theory Invocation_DP

lemma call_kernel_with_intent_no_fault_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>"
  and corrupt_ipc_buffer_hold: "\<lbrace>Rb\<rbrace>corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>r. Ra\<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)
                       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_no_exception:
      "\<And>c ref cs. \<lbrace> Pd cs c ref \<rbrace> decode_invocation c ref cs intent_op
       \<lbrace> Ps \<rbrace>, \<lbrace>\<lambda>xa s. False\<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  non_ep_cap:
      "\<lbrace> Pd2 \<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr
       \<lbrace> \<lambda>rv s. \<not> ep_related_cap (fst rv) \<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>"

  shows
  "\<lbrace>\<lambda>s. tcb_at' \<top> root_tcb_id s \<and>
    (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrace>
   call_kernel_with_intent intent False \<lbrace>\<lambda>r. Q\<rbrace>" using unify apply (simp add:call_kernel_with_intent_def) apply wp apply (rule_tac P = "thread_ptr = root_tcb_id" in hoare_gen_asm) apply (simp add:call_kernel_loop_def) apply (rule_tac Q = "\<lambda>r s. cdl_current_thread s = Some root_tcb_id
                               \<and> cdl_current_domain s = minBound \<longrightarrow> Q s
               " in hoare_strengthen_post[rotated]) apply fastforce apply clarsimp apply wp apply (rule hoare_vcg_imp_lift) apply (wpc|wp hoare_vcg_imp_lift|simp cong: if_cong)+ apply (rule hoare_pre_cont) apply (wp has_restart_cap_sep_wp[where cap = RunningCap])[1] apply wp apply (rule_tac Q = "\<lambda>r s. cdl_current_thread s = Some root_tcb_id
                              \<and> cdl_current_domain s = minBound \<longrightarrow> (Q s
                              \<and>  <(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)> s)"
                in hoare_strengthen_post) apply (rule schedule_no_choice_wp) 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)
                            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_no_decode_exception
                   [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_all_scheduable_tcbs
                         set_cap_hold delete_cap_simple_wp[where cap = RestartCap])[1] apply (rule decode_invocation_no_exception) apply (rule lookup_extra_caps_exec) apply (rule lookup_cap_and_slot_exec) apply (rule non_ep_cap) apply ((wp corrupt_ipc_buffer_sep_inv corrupt_ipc_buffer_active_tcbs
                 mark_tcb_intent_error_hold corrupt_ipc_buffer_hold | simp)+)[2] 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 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 auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (\<lambda>tcb. True) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrace> call_kernel_with_intent intent False \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
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. tcb_at' (\<lambda>tcb. True) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrace> call_kernel_with_intent intent False \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (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. object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P 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);
thread_has_error thread_ptr
od \<lbrace>\<lambda>r. Q\<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>?B6 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> Q 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>?B6 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (7 subgoals):
 1. \<And>thread_ptr y domain ya yb. \<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'17 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> Q 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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'17 root_tcb_id () 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. (\<exists>y. cdl_current_thread s = Some y) \<longrightarrow> root_tcb_id = the (cdl_current_thread s) \<longrightarrow> minBound = cdl_current_domain s \<longrightarrow> Q 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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> Q s\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_current_thread s = Some y) \<longrightarrow> root_tcb_id = the (cdl_current_thread s) \<longrightarrow> minBound = cdl_current_domain s \<longrightarrow> Q 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'17 root_tcb_id () 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> Q 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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'17 root_tcb_id () 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> Q 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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'17 root_tcb_id () 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> Q 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (10 subgoals):
 1. \<And>domain y x xa. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B58 domain y x xa\<rbrace> case xa 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> Q s\<rbrace>
 2. \<And>domain y x. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B57 domain y x\<rbrace> gets cdl_current_thread \<lbrace>?B58 domain y x\<rbrace>
 3. \<And>domain y. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B56 domain y\<rbrace> schedule \<lbrace>?B57 domain y\<rbrace>
 4. \<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'17 (ds_id 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>?B56 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (11 subgoals):
 1. \<And>domain y x xa. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?P'60 domain y x xa\<rbrace> case xa 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>domain y x xa. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?Q'60 domain y x xa\<rbrace> case xa 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. Q\<rbrace>
 3. \<And>domain y x. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B57 domain y x\<rbrace> gets cdl_current_thread \<lbrace>\<lambda>xa s. ?P'60 domain y x xa s \<or> ?Q'60 domain y x xa s\<rbrace>
 4. \<And>domain y. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B56 domain y\<rbrace> schedule \<lbrace>?B57 domain y\<rbrace>
 5. \<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'17 (ds_id 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>?B56 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>domain y xa x2 xb. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; xa = Some x2; xb\<rbrakk> \<Longrightarrow> \<lbrace>?Q115 domain y () (Some x2) x2 True\<rbrace> set_cap (x2, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<And>domain y x xa x2. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R108 domain y x xa x2\<rbrace> has_restart_cap x2 \<lbrace>\<lambda>xb. if xb then ?Q115 domain y x xa x2 xb else Q\<rbrace>
 3. \<And>domain y x. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B57 domain y x\<rbrace> gets cdl_current_thread \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> \<not> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound)) \<and> (\<forall>x. xa = Some x \<longrightarrow> cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> (xa = None \<longrightarrow> Q s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R108 domain y x xa xb s)\<rbrace>
 4. \<And>domain y. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B56 domain y\<rbrace> schedule \<lbrace>?B57 domain y\<rbrace>
 5. \<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'17 (ds_id 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>?B56 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>domain y x xa x2. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R108 domain y x xa x2\<rbrace> has_restart_cap x2 \<lbrace>\<lambda>xb. if xb then \<lambda>a. False else Q\<rbrace>
 2. \<And>domain y x. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B57 domain y x\<rbrace> gets cdl_current_thread \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> \<not> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound)) \<and> (\<forall>x. xa = Some x \<longrightarrow> cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> (xa = None \<longrightarrow> Q s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R108 domain y x xa xb s)\<rbrace>
 3. \<And>domain y. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B56 domain y\<rbrace> schedule \<lbrace>?B57 domain y\<rbrace>
 4. \<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'17 (ds_id 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>?B56 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (9 subgoals):
 1. \<And>domain y x. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B57 domain y x\<rbrace> gets cdl_current_thread \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> \<not> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound)) \<and> (\<forall>x. xa = Some x \<longrightarrow> cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> (xa = None \<longrightarrow> Q s) \<and> (\<forall>x. xa = 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 Q) s)\<rbrace>
 2. \<And>domain y. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B56 domain y\<rbrace> schedule \<lbrace>?B57 domain y\<rbrace>
 3. \<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'17 (ds_id 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>?B56 domain\<rbrace>
 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (8 subgoals):
 1. \<And>domain y. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B56 domain y\<rbrace> schedule \<lbrace>\<lambda>x s. (cdl_current_thread s = None \<longrightarrow> \<not> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound)) \<and> (\<forall>x. cdl_current_thread s = Some x \<longrightarrow> cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> (cdl_current_thread s = None \<longrightarrow> Q 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 Q) s)\<rbrace>
 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'17 (ds_id 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>?B56 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (9 subgoals):
 1. \<And>domain y. \<lbrakk>cdl_intent_op intent = Some intent_op; intent_cptr = cdl_intent_cap intent; intent_extra = cdl_intent_extras intent\<rbrakk> \<Longrightarrow> \<lbrace>?B56 domain y\<rbrace> schedule \<lbrace>\<lambda>r s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 2. \<And>domain y 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 \<longrightarrow> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> (cdl_current_thread s = None \<longrightarrow> \<not> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound)) \<and> (\<forall>x. cdl_current_thread s = Some x \<longrightarrow> cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> (cdl_current_thread s = None \<longrightarrow> Q 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 Q) s)
 3. \<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'17 (ds_id 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>?B56 domain\<rbrace>
 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (8 subgoals):
 1. \<And>domain y 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 \<longrightarrow> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> (cdl_current_thread s = None \<longrightarrow> \<not> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound)) \<and> (\<forall>x. cdl_current_thread s = Some x \<longrightarrow> cdl_current_thread s \<noteq> Some root_tcb_id \<or> cdl_current_domain s \<noteq> minBound) \<or> (cdl_current_thread s = None \<longrightarrow> Q 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 Q) 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'17 (ds_id 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>y s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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'17 (ds_id 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>y s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. ?P'17 thread_ptr y domain ya yb 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s; isRight r\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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) 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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>?F214 r x\<rbrace> do y <- handle_pending_interrupts;
throwError PreemptError
od \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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) 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>?Q210 r\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>?F214 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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ?Q210 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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>?F214 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) 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>?Q210 r\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>?F214 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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ?Q210 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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>?Q210 r\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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) 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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ?Q210 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s 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>?Rm243 r\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<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>?Pd243 r cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>?Ps243 r\<rbrace>, \<lbrace>\<lambda>xa s. False\<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.243 r (fst rv) (snd rv)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. ?Pd243 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.243 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. ?Pd1.243 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.243 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>?Ra243 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv. ?Rm243 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>?Rb243 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra243 r\<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>?PIV243 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb243 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) 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>?Ps243 r iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV243 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; (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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and ?Pd2.243 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) root_tcb_id) s
A total of 16 subgoals... proof (prove)
goal (15 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>?Pd243 r cs c ref\<rbrace> decode_invocation c ref cs intent_op \<lbrace>?Ps243 r\<rbrace>, \<lbrace>\<lambda>xa s. False\<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.243 r (fst rv) (snd rv)\<rbrace> lookup_extra_caps root_tcb_id intent_extra \<lbrace>\<lambda>xa. ?Pd243 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.243 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. ?Pd1.243 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.243 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>?Ra243 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> R s \<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>?Rb243 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra243 r\<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>?PIV243 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb243 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) 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>?Ps243 r iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV243 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; (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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and ?Pd2.243 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) 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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 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.243 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.243 r\<rbrace> lookup_cap_and_slot root_tcb_id intent_cptr \<lbrace>\<lambda>rv s. ?Pd1.243 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.243 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>?Ra243 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> R s \<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>?Rb243 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra243 r\<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>?PIV243 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb243 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) 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. ?PIV243 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; (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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and ?Pd2.243 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) 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 thread_ptr y domain\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 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.243 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.243 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>?Ra243 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> R s \<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>?Rb243 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra243 r\<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>?PIV243 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb243 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) 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. ?PIV243 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; (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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and ?Pd2.243 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) root_tcb_id) s
 8. \<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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) and K (thread_ptr = root_tcb_id)\<rbrace>
 9. \<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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 thread_ptr y domain\<rbrace>
 10. \<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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 thread_ptr y\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 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>?Ra243 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> R s \<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>?Rb243 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra243 r\<rbrace>
 4. \<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>?PIV243 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb243 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) 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>
 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>Ps iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. ?PIV243 r iv\<rbrace>
 6. \<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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and 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) root_tcb_id) s
 7. \<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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) a) and K (thread_ptr = root_tcb_id)\<rbrace>
 8. \<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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 thread_ptr y domain\<rbrace>
 9. \<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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 thread_ptr y\<rbrace>
 10. \<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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 thread_ptr\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 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>?Ra243 r\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> R s \<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>?Rb243 r\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>rv. ?Ra243 r\<rbrace>
 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>?PIV243 r iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. ?Rb243 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) 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>
 4. \<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. ?PIV243 r iv\<rbrace>
 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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and 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) 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<rbrace>
A total of 11 subgoals... 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>?PIV243 r 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> Rb s \<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) 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. ?PIV243 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; (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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and 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) 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (10 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> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Rb s \<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) 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) 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; (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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and 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) 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (9 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) 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) 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; (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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and 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) 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (8 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; (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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and 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) 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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) 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> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> Q s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s) \<and> isLeft r\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdl_current_thread s = Some root_tcb_id) and 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) 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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>?B5 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>?B5 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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'327 thread_ptr y domain ya\<rbrace> update_thread thread_ptr (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb. (\<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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a | Inr rv \<Rightarrow> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Q a \<and> cdl.lift ((root_tcb_id, 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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>\<lambda>ya. ?P'327 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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'327 root_tcb_id () domain ()\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. intent)) \<lbrace>\<lambda>yb a. 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) root_tcb_id a \<and> cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> Pd2 a\<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>?B4 thread_ptr y domain\<rbrace> assert (domain = minBound) \<lbrace>\<lambda>ya. ?P'327 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>?B3 thread_ptr y\<rbrace> gets cdl_current_domain \<lbrace>?B4 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>?B2 thread_ptr\<rbrace> assert (thread_ptr = root_tcb_id) \<lbrace>?B3 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>?Q1\<rbrace> gets_the cdl_current_thread \<lbrace>?B2\<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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P s)\<rbrakk> \<Longrightarrow> ?Q1 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; object_at (\<lambda>obj. \<exists>tcb. obj = Tcb tcb) root_tcb_id s \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> P 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) 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:
No subgoals!