theory Invocation_DP

lemma handle_event_syscall_no_decode_exception:
  assumes set_cap_hold: "\<lbrace>Rm \<rbrace>set_cap (cur_thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<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 cur_thread  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 cur_thread 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 cur_thread intent_cptr
       \<lbrace> \<lambda>rv s. \<not> ep_related_cap (fst rv) \<rbrace>, -"
  and mark_tcb_intent_error_hold: "\<lbrace> Ra \<rbrace>mark_tcb_intent_error cur_thread False \<lbrace>\<lambda>r. Rm\<rbrace>"
  and corrupt_ipc_buffer_hold: "\<lbrace> Rb \<rbrace>corrupt_ipc_buffer cur_thread 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. Rb s \<and> <(cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* sep_true > s\<rbrace>, \<lbrace>\<lambda>r. Inv'\<rbrace>"
  and set_restart_cap_hold: "\<And>iv. \<lbrace>Ps iv\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV iv\<rbrace>"
  shows "\<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread)
   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) cur_thread
   \<rbrace> handle_event (SyscallEvent SysCall)
   \<lbrace>\<lambda>r. Q\<rbrace>,\<lbrace>\<lambda>y. Inv'\<rbrace>" apply (simp add:handle_event_def handle_syscall_def handle_invocation_def) apply (rule liftE_wp_split_r)+ apply (rule syscall_valid_helper) apply (rule liftE_wp_split_r)+ apply (rule wp_no_exception_seq_r) apply (rule liftE_wp_no_exception) apply (rule whenE_wp) apply simp apply wp apply (rule_tac P = "y = cur_thread" in hoare_gen_asm) apply simp apply (rule set_cap_hold) apply (rule_tac P = "y = cur_thread" in hoare_gen_asm) apply simp apply (rule mark_tcb_intent_error_hold) apply (rule_tac P = "y = cur_thread" in hoare_gen_asm) apply simp apply (rule corrupt_ipc_buffer_hold) apply (wp has_restart_cap_sep_wp[where cap = RestartCap])[1] apply (rule_tac P = "y = cur_thread" in hoare_gen_asmEx) apply (simp add:conj_comms) apply (rule perform_invocation_hold) apply (rule_tac P = "y = cur_thread" in hoare_gen_asm) apply simp apply (wp hoare_vcg_conj_lift set_restart_cap_hold)[1] apply (rule_tac P = " \<not> ep_related_cap (fst yb)
       \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread"
       in hoare_gen_asmEx) apply (simp add:split_def) apply (rule decode_invocation_no_exception) apply (rule wp_no_exception_seq)+ apply (simp add:split_def) apply (rule wp_no_exception_seq) apply (simp add:returnOk_liftE) apply wp[1] apply (rule_tac P = " y = cur_thread \<and>
       cdl_intent_extras (cdl_tcb_intent ya) = intent_extra" in hoare_gen_asmEx) apply simp apply (rule hoare_post_impErr[OF no_exception_conj]) apply (rule_tac r = yb in lookup_extra_caps_exec) prefer 2 apply (elim conjE) apply (simp add:Fun.comp_def) apply wp[1] apply simp apply (rule_tac P = "(cdl_intent_cap (cdl_tcb_intent ya)) = intent_cptr
       \<and> y = cur_thread"
       in hoare_gen_asmEx) apply (rule hoare_post_impErr[OF no_exception_conj]) apply simp apply (rule lookup_cap_and_slot_exec) prefer 2 apply (elim conjE) apply simp apply simp apply wp apply simp apply (wp non_ep_cap get_thread_sep_wp get_thread_inv | simp)+ apply (clarsimp simp:object_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> doE thread_ptr <- liftE (gets_the cdl_current_thread);
thread <- liftE (get_thread thread_ptr);
syscall (doE (cap, cap_ref) <- lookup_cap_and_slot thread_ptr (cdl_intent_cap (cdl_tcb_intent thread));
extra_caps <- lookup_extra_caps thread_ptr (cdl_intent_extras (cdl_tcb_intent thread));
returnOk (cap, cap_ref, extra_caps)
odE) handle_fault (\<lambda>(cap, cap_ref, extra_caps). case cdl_intent_op (cdl_tcb_intent thread) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x) (do y <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) (\<lambda>inv. doE y <- liftE (set_cap (thread_ptr, tcb_pending_op_slot) RestartCap);
y <- perform_invocation True True inv;
restart <- liftE (has_restart_cap thread_ptr);
whenE restart (liftE (do y <- corrupt_ipc_buffer thread_ptr True;
y <- mark_tcb_intent_error thread_ptr False;
set_cap (thread_ptr, tcb_pending_op_slot) RunningCap
od))
odE)
odE \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> syscall (doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE) handle_fault (\<lambda>(cap, cap_ref, extra_caps). case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x) (do ya <- corrupt_ipc_buffer y True;
mark_tcb_intent_error y True
od) (\<lambda>inv. doE ya <- liftE (set_cap (y, tcb_pending_op_slot) RestartCap);
ya <- perform_invocation True True inv;
restart <- liftE (has_restart_cap y);
whenE restart (liftE (do ya <- corrupt_ipc_buffer y True;
ya <- mark_tcb_intent_error y False;
set_cap (y, tcb_pending_op_slot) RunningCap
od))
odE) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 3. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> doE ya <- liftE (set_cap (y, tcb_pending_op_slot) RestartCap);
ya <- perform_invocation True True xa;
restart <- liftE (has_restart_cap y);
whenE restart (liftE (do ya <- corrupt_ipc_buffer y True;
ya <- mark_tcb_intent_error y False;
set_cap (y, tcb_pending_op_slot) RunningCap
od))
odE \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 2. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> doE ya <- perform_invocation True True xa;
restart <- liftE (has_restart_cap y);
whenE restart (liftE (do ya <- corrupt_ipc_buffer y True;
ya <- mark_tcb_intent_error y False;
set_cap (y, tcb_pending_op_slot) RunningCap
od))
odE \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 2. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 3. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 6. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> doE restart <- liftE (has_restart_cap y);
whenE restart (liftE (do ya <- corrupt_ipc_buffer y True;
ya <- mark_tcb_intent_error y False;
set_cap (y, tcb_pending_op_slot) RunningCap
od))
odE \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 3. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 4. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 7. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa yb yc yd. \<lbrace>?P'16 y ya x xa yb yc yd\<rbrace> whenE yd (liftE (do ya <- corrupt_ipc_buffer y True;
ya <- mark_tcb_intent_error y False;
set_cap (y, tcb_pending_op_slot) RunningCap
od)) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>?P'16 y ya x xa yb yc\<rbrace>
 3. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 4. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 5. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 8. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa yb yc yd. yd \<Longrightarrow> \<lbrace>?Q19 y ya x xa yb yc yd\<rbrace> liftE (do ya <- corrupt_ipc_buffer y True;
ya <- mark_tcb_intent_error y False;
set_cap (y, tcb_pending_op_slot) RunningCap
od) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?Q19 y ya x xa yb yc yd else Q\<rbrace>
 3. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 4. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 5. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 8. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa yd. yd \<Longrightarrow> \<lbrace>?Q19 y ya x xa () () True\<rbrace> do ya <- corrupt_ipc_buffer y True;
ya <- mark_tcb_intent_error y False;
set_cap (y, tcb_pending_op_slot) RunningCap
od \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?Q19 y ya x xa yb yc yd else Q\<rbrace>
 3. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 4. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 5. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 8. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>y ya x xa yd yb xb. yd \<Longrightarrow> \<lbrace>?B24 y ya x xa yd yb xb\<rbrace> set_cap (y, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>y ya x xa yd yb. yd \<Longrightarrow> \<lbrace>?B22 y ya x xa yd yb\<rbrace> mark_tcb_intent_error y False \<lbrace>?B24 y ya x xa yd yb\<rbrace>
 3. \<And>y ya x xa yd. yd \<Longrightarrow> \<lbrace>?Q19 y ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer y True \<lbrace>?B22 y ya x xa yd\<rbrace>
 4. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?Q19 y ya x xa yb yc yd else Q\<rbrace>
 5. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 6. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 7. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 8. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 9. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 10. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>y ya x xa yd yb xb. \<lbrakk>yd; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'26 y ya x xa yd yb xb\<rbrace> set_cap (y, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>y ya x xa yd yb. yd \<Longrightarrow> \<lbrace>?B22 y ya x xa yd yb\<rbrace> mark_tcb_intent_error y False \<lbrace>\<lambda>xb. ?P'26 y ya x xa yd yb xb and K (y = cur_thread)\<rbrace>
 3. \<And>y ya x xa yd. yd \<Longrightarrow> \<lbrace>?Q19 y ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer y True \<lbrace>?B22 y ya x xa yd\<rbrace>
 4. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?Q19 y ya x xa yb yc yd else Q\<rbrace>
 5. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 6. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 7. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 8. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 9. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 10. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>y ya x xa yd. \<lbrakk>yd; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'26 cur_thread ya x xa True () ()\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>y ya x xa yd yb. yd \<Longrightarrow> \<lbrace>?B22 y ya x xa yd yb\<rbrace> mark_tcb_intent_error y False \<lbrace>\<lambda>xb. ?P'26 y ya x xa yd yb xb and K (y = cur_thread)\<rbrace>
 3. \<And>y ya x xa yd. yd \<Longrightarrow> \<lbrace>?Q19 y ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer y True \<lbrace>?B22 y ya x xa yd\<rbrace>
 4. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?Q19 y ya x xa yb yc yd else Q\<rbrace>
 5. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 6. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 7. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 8. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 9. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 10. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya x xa yd yb. yd \<Longrightarrow> \<lbrace>?B22 y ya x xa yd yb\<rbrace> mark_tcb_intent_error y False \<lbrace>\<lambda>xb. Rm and K (y = cur_thread)\<rbrace>
 2. \<And>y ya x xa yd. yd \<Longrightarrow> \<lbrace>?Q19 y ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer y True \<lbrace>?B22 y ya x xa yd\<rbrace>
 3. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?Q19 y ya x xa yb yc yd else Q\<rbrace>
 4. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 5. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 6. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 9. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya x xa yd yb. \<lbrakk>yd; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'27 y ya x xa yd yb\<rbrace> mark_tcb_intent_error y False \<lbrace>\<lambda>xb. Rm and K (y = cur_thread)\<rbrace>
 2. \<And>y ya x xa yd. yd \<Longrightarrow> \<lbrace>?Q19 y ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer y True \<lbrace>\<lambda>yb. ?P'27 y ya x xa yd yb and K (y = cur_thread)\<rbrace>
 3. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?Q19 y ya x xa yb yc yd else Q\<rbrace>
 4. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 5. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 6. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 9. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya x xa yd. \<lbrakk>yd; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'27 cur_thread ya x xa True ()\<rbrace> mark_tcb_intent_error cur_thread False \<lbrace>\<lambda>xb. Rm\<rbrace>
 2. \<And>y ya x xa yd. yd \<Longrightarrow> \<lbrace>?Q19 y ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer y True \<lbrace>\<lambda>yb. ?P'27 y ya x xa yd yb and K (y = cur_thread)\<rbrace>
 3. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?Q19 y ya x xa yb yc yd else Q\<rbrace>
 4. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 5. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 6. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 9. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa yd. yd \<Longrightarrow> \<lbrace>?Q19 y ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer y True \<lbrace>\<lambda>yb. Ra and K (y = cur_thread)\<rbrace>
 2. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?Q19 y ya x xa yb yc yd else Q\<rbrace>
 3. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 4. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 5. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 8. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa yd. \<lbrakk>yd; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'30 y ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer y True \<lbrace>\<lambda>yb. Ra and K (y = cur_thread)\<rbrace>
 2. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?P'30 y ya x xa yb yc yd and K (y = cur_thread) else Q\<rbrace>
 3. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 4. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 5. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 8. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa yd. \<lbrakk>yd; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'30 cur_thread ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>yb. Ra\<rbrace>
 2. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>yd. if yd then ?P'30 y ya x xa yb yc yd and K (y = cur_thread) else Q\<rbrace>
 3. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 4. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 5. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 8. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya x xa yb yc. \<lbrace>?P'13 y ya x xa yb yc\<rbrace> has_restart_cap y \<lbrace>\<lambda>ya. if ya then Rb and K (y = cur_thread) else Q\<rbrace>
 2. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>?P'13 y ya x xa yb\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 3. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 4. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 7. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y ya x xa yb. \<lbrace>?P'10 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>\<lambda>ya s. cdl.lift ((y, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> (if RestartCap = RestartCap then Rb and K (y = cur_thread) else Q) s\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 2. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>?P'10 y ya x xa\<rbrace>
 3. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 6. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y ya x xa yb. y = cur_thread \<Longrightarrow> \<lbrace>?P'35 y ya x xa yb\<rbrace> perform_invocation True True xa \<lbrace>\<lambda>ya s. cdl.lift ((y, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> (if RestartCap = RestartCap then Rb and K (y = cur_thread) else Q) s\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 2. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>yb. ?P'35 y ya x xa yb and K (y = cur_thread)\<rbrace>
 3. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 6. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y ya x xa. y = cur_thread \<Longrightarrow> \<lbrace>?P'35 cur_thread ya x xa ()\<rbrace> perform_invocation True True xa \<lbrace>\<lambda>y s. Rb s \<and> cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>y. Inv'\<rbrace>
 2. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>yb. ?P'35 y ya x xa yb and K (y = cur_thread)\<rbrace>
 3. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 6. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya x xa. \<lbrace>?Qa6 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>ya. PIV xa and K (y = cur_thread)\<rbrace>
 2. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>?Qa6 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya x xa. y = cur_thread \<Longrightarrow> \<lbrace>?P'39 y ya x xa\<rbrace> set_cap (y, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>ya. PIV xa and K (y = cur_thread)\<rbrace>
 2. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>\<lambda>xa. ?P'39 y ya yb xa and K (y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya x xa. y = cur_thread \<Longrightarrow> \<lbrace>?P'39 cur_thread ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>y. PIV xa\<rbrace>
 2. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>\<lambda>xa. ?P'39 y ya yb xa and K (y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y ya yb. \<lbrace>?Qi6 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>\<lambda>xa. Ps xa and K (y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>?Qi6 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y ya yb. \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread \<Longrightarrow> \<lbrace>?P'43 y ya yb\<rbrace> case yb of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (cdl_tcb_intent ya) of None \<Rightarrow> if ep_related_cap cap then decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> decode_invocation cap cap_ref extra_caps x \<lbrace>\<lambda>xa. Ps xa and K (y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>\<lambda>yb. ?P'43 y ya yb and K (\<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ya yb. \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<Longrightarrow> \<lbrace>?P'43 cur_thread ya yb\<rbrace> decode_invocation (fst yb) (fst (snd yb)) (snd (snd yb)) intent_op \<lbrace>Ps\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>\<lambda>yb. ?P'43 y ya yb and K (\<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> doE (cap, cap_ref) <- lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>\<lambda>yb. Pd (snd (snd yb)) (fst yb) (fst (snd yb)) and K (\<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 3. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y ya yb. \<lbrace>?P'47 y ya yb\<rbrace> case yb of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>\<lambda>yb. Pd (snd (snd yb)) (fst yb) (fst (snd yb)) and K (\<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?P'47 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y ya yb. \<lbrace>?P'47 y ya yb\<rbrace> doE extra_caps <- lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya));
returnOk (fst yb, snd yb, extra_caps)
odE \<lbrace>\<lambda>yb. Pd (snd (snd yb)) (fst yb) (fst (snd yb)) and (\<lambda>yc. \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?P'47 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya yb yc. \<lbrace>?P'50 y ya yb yc\<rbrace> returnOk (fst yb, snd yb, yc) \<lbrace>\<lambda>yb. Pd (snd (snd yb)) (fst yb) (fst (snd yb)) and (\<lambda>yc. \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya yb. \<lbrace>?P'47 y ya yb\<rbrace> lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya)) \<lbrace>?P'50 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?P'47 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya yb yc. \<lbrace>?P'50 y ya yb yc\<rbrace> return (fst yb, snd yb, yc) \<lbrace>\<lambda>yb. Pd (snd (snd yb)) (fst yb) (fst (snd yb)) and (\<lambda>yc. \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread)\<rbrace>
 2. \<And>y ya yb. \<lbrace>?P'47 y ya yb\<rbrace> lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya)) \<lbrace>?P'50 y ya yb\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?P'47 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y ya yb. \<lbrace>?P'47 y ya yb\<rbrace> lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya)) \<lbrace>\<lambda>yc. Pd (snd (snd (fst yb, snd yb, yc))) (fst (fst yb, snd yb, yc)) (fst (snd (fst yb, snd yb, yc))) and (\<lambda>yd. \<not> ep_related_cap (fst (fst yb, snd yb, yc)) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?P'47 y ya\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y ya yb. y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<Longrightarrow> \<lbrace>?P'56 y ya yb\<rbrace> lookup_extra_caps y (cdl_intent_extras (cdl_tcb_intent ya)) \<lbrace>\<lambda>yc. Pd (snd (snd (fst yb, snd yb, yc))) (fst (fst yb, snd yb, yc)) (fst (snd (fst yb, snd yb, yc))) and (\<lambda>yd. \<not> ep_related_cap (fst (fst yb, snd yb, yc)) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> y = cur_thread)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. ?P'56 y ya yb and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ya yb. cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<Longrightarrow> \<lbrace>?P'56 cur_thread ya yb\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>\<lambda>y a. Pd y (fst yb) (snd yb) a \<and> \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. ?P'56 y ya yb and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>ya yb. cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<Longrightarrow> \<lbrace>?P62 cur_thread ya yb\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q58 ya yb\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>ya yb. cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<Longrightarrow> \<lbrace>?P'61 cur_thread ya yb\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q'58 ya yb\<rbrace>, -
 3. \<And>ya yb rv s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Q58 ya yb rv s \<and> ?Q'58 ya yb rv s\<rbrakk> \<Longrightarrow> Pd rv (fst yb) (snd yb) s \<and> \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op
 4. \<And>ya yb e s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 5. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. ?P62 y ya yb and ?P'61 y ya yb and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 7. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ya yb. cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<Longrightarrow> \<lbrace>?P'61 cur_thread ya yb\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q'58 ya yb\<rbrace>, -
 2. \<And>ya yb rv s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; Pd rv (fst yb) (snd yb) s \<and> ?Q'58 ya yb rv s\<rbrakk> \<Longrightarrow> Pd rv (fst yb) (snd yb) s \<and> \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op
 3. \<And>ya yb e s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 4. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. Pd1 (fst yb) (snd yb) and ?P'61 y ya yb and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 6. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ya yb rv s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; Pd rv (fst yb) (snd yb) s \<and> ?Q'58 ya yb rv s\<rbrakk> \<Longrightarrow> Pd rv (fst yb) (snd yb) s \<and> \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op
 2. \<And>ya yb. cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<Longrightarrow> \<lbrace>?P'61 cur_thread ya yb\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q'58 ya yb\<rbrace>, -
 3. \<And>ya yb e s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 4. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. Pd1 (fst yb) (snd yb) and ?P'61 y ya yb and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 6. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ya yb rv s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; Pd rv (fst yb) (snd yb) s; ?Q'58 ya yb rv s\<rbrakk> \<Longrightarrow> Pd rv (fst yb) (snd yb) s \<and> \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op
 2. \<And>ya yb. cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<Longrightarrow> \<lbrace>?P'61 cur_thread ya yb\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q'58 ya yb\<rbrace>, -
 3. \<And>ya yb e s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 4. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. Pd1 (fst yb) (snd yb) and ?P'61 y ya yb and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 6. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ya yb. cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<Longrightarrow> \<lbrace>?P'61 cur_thread ya yb\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>\<lambda>rv s. \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op\<rbrace>, -
 2. \<And>ya yb e s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 3. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. Pd1 (fst yb) (snd yb) and ?P'61 y ya yb and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ya yb e s. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 2. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. Pd1 (fst yb) (snd yb) and (\<lambda>a. \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op) and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrace>?P'3 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. Pd1 (fst yb) (snd yb) and (\<lambda>a. \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op) and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 3. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread \<Longrightarrow> \<lbrace>?P'76 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>yb. Pd1 (fst yb) (snd yb) and (\<lambda>a. \<not> ep_related_cap (fst yb) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op) and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?P'76 y ya and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 3. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread \<Longrightarrow> \<lbrace>?P78 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?Q78 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread \<Longrightarrow> \<lbrace>?P'78 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?Q'78 y ya\<rbrace>, -
 3. \<And>y ya rv s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; ?Q78 y ya rv s \<and> ?Q'78 y ya rv s\<rbrakk> \<Longrightarrow> (Pd1 (fst rv) (snd rv) and (\<lambda>a. \<not> ep_related_cap (fst rv) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op) and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)) s
 4. \<And>y ya e s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; False\<rbrakk> \<Longrightarrow> False
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?P78 y ya and ?P'78 y ya and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 6. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<Longrightarrow> \<lbrace>?P78 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>?Q78 cur_thread ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread \<Longrightarrow> \<lbrace>?P'78 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?Q'78 y ya\<rbrace>, -
 3. \<And>y ya rv s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; ?Q78 y ya rv s \<and> ?Q'78 y ya rv s\<rbrakk> \<Longrightarrow> (Pd1 (fst rv) (snd rv) and (\<lambda>a. \<not> ep_related_cap (fst rv) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op) and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)) s
 4. \<And>y ya e s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; False\<rbrakk> \<Longrightarrow> False
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?P78 y ya and ?P'78 y ya and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 6. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread \<Longrightarrow> \<lbrace>?P'78 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?Q'78 y ya\<rbrace>, -
 2. \<And>y ya rv s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; (Pd1 (fst rv) (snd rv) s \<and> \<not> ep_related_cap (fst rv)) \<and> ?Q'78 y ya rv s\<rbrakk> \<Longrightarrow> (Pd1 (fst rv) (snd rv) and (\<lambda>a. \<not> ep_related_cap (fst rv) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op) and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)) s
 3. \<And>y ya e s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; False\<rbrakk> \<Longrightarrow> False
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. Pd2 and ?P'78 y ya and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya rv s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; (Pd1 (fst rv) (snd rv) s \<and> \<not> ep_related_cap (fst rv)) \<and> ?Q'78 y ya rv s\<rbrakk> \<Longrightarrow> (Pd1 (fst rv) (snd rv) and (\<lambda>a. \<not> ep_related_cap (fst rv) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op) and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)) s
 2. \<And>y ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread \<Longrightarrow> \<lbrace>?P'78 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?Q'78 y ya\<rbrace>, -
 3. \<And>y ya e s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; False\<rbrakk> \<Longrightarrow> False
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. Pd2 and ?P'78 y ya and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya rv s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; y = cur_thread; ?Q'78 y ya rv s; Pd1 (fst rv) (snd rv) s; \<not> ep_related_cap (fst rv)\<rbrakk> \<Longrightarrow> (Pd1 (fst rv) (snd rv) and (\<lambda>a. \<not> ep_related_cap (fst rv) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op) and K (y = cur_thread \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)) s
 2. \<And>y ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread \<Longrightarrow> \<lbrace>?P'78 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>?Q'78 y ya\<rbrace>, -
 3. \<And>y ya e s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; False\<rbrakk> \<Longrightarrow> False
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. Pd2 and ?P'78 y ya and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 5. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread \<Longrightarrow> \<lbrace>?P'78 y ya\<rbrace> lookup_cap_and_slot y (cdl_intent_cap (cdl_tcb_intent ya)) \<lbrace>\<lambda>a b. cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrace>, -
 2. \<And>y ya e s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; False\<rbrakk> \<Longrightarrow> False
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. Pd2 and ?P'78 y ya and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ya. cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<Longrightarrow> \<lbrace>?P'78 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>a b. cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrace>, -
 2. \<And>y ya e s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; False\<rbrakk> \<Longrightarrow> False
 3. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. Pd2 and ?P'78 y ya and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 4. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y ya e s. \<lbrakk>cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread; False\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. Pd2 and (\<lambda>a. cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 3. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. Pd2 and (\<lambda>a. cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> y = cur_thread)\<rbrace>
 2. \<lbrace>(\<lambda>s. cdl_current_thread s = Some cur_thread) 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) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl_current_thread s = Some cur_thread \<and> Pd2 s \<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) cur_thread s \<Longrightarrow> tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra) cur_thread s \<and> tcb_at' (\<lambda>tcb. cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr) cur_thread s proof (prove)
goal:
No subgoals!