theory Invocation_DP

lemma handle_event_syscall_allow_error:
  assumes set_cap_hold: "\<lbrace>Rm \<rbrace>set_cap (cur_thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r. Q\<rbrace>"

  and decode_invocation_allow_error:
      "\<And>c ref cs. \<lbrace> Pd cs c ref \<rbrace> decode_invocation c ref cs intent_op
       \<lbrace> Ps \<rbrace>, \<lbrace>\<lambda>r. Perror\<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>"
             "\<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>"
  and corrupt_ipc_buffer_hold: "\<lbrace> Rb \<rbrace>corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>r. Ra\<rbrace>"
             "\<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<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>"
  and error_imp: "\<And>s. Pd2 s \<Longrightarrow>  cdl_current_thread s = Some cur_thread \<and> Perror s"
  shows "\<lbrace> Pd2
   and tcb_at'
     (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and>
            cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and>
            cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and>
            cdl_intent_error (cdl_tcb_intent tcb) = False) cur_thread
   \<rbrace> handle_event (SyscallEvent SysCall)
   \<lbrace>\<lambda>r s.  (\<not> tcb_has_error cur_thread s \<longrightarrow> Q s)
  \<and> (tcb_has_error cur_thread s \<longrightarrow> Perror s)\<rbrace>,\<lbrace>\<lambda>y. Inv\<rbrace>" apply (simp add:handle_event_def handle_syscall_def
    handle_invocation_def when_def) apply (rule liftE_wp_split_r)+ apply (rule_tac P = "y = cur_thread" in hoare_gen_asmEx) apply simp apply (rule_tac P = "cdl_intent_op (cdl_tcb_intent ya) = Some intent_op
       \<and> (cdl_intent_cap (cdl_tcb_intent ya)) = intent_cptr
       \<and>  cdl_intent_extras (cdl_tcb_intent ya) = intent_extra"
       in hoare_gen_asmEx) apply simp apply (rule syscall_valid_helper_allow_error) 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 (wp set_cap_hold tcb_has_error_set_cap) apply (rule_tac P = "y = cur_thread" in hoare_gen_asm) apply (simp add:tcb_pending_op_slot_def tcb_ipcbuffer_slot_def) apply (wp mark_tcb_intent_error_hold mark_tcb_intent_error_no_error') 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 simp apply (rule_tac P = " \<not> ep_related_cap (fst r)
       \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op"
       in hoare_gen_asmEx) apply (simp add:split_def) apply (rule decode_invocation_allow_error) 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 simp apply (rule_tac P = "
       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 = r in lookup_extra_caps_exec) prefer 2 apply (elim conjE) apply (simp add:Fun.comp_def) apply wp[1] apply simp apply simp apply (rule lookup_cap_and_slot_exec) apply (wp mark_tcb_intent_error_hold
        corrupt_ipc_buffer_hold |
        simp add:error_imp)+ apply (wp non_ep_cap get_thread_sep_wp get_thread_inv | simp)+ apply (clarsimp simp:object_at_def tcb_has_error_def error_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> cdl_intent_error (cdl_tcb_intent tcb) = False) cur_thread\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>r s. (\<not> tcb_has_error cur_thread s \<longrightarrow> Q s) \<and> (tcb_has_error cur_thread s \<longrightarrow> Perror s)\<rbrace>, \<lbrace>\<lambda>y. Inv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) 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 s. (\<not> tcb_has_error cur_thread s \<longrightarrow> Q s) \<and> (tcb_has_error cur_thread s \<longrightarrow> Perror s)\<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 s. (\<not> tcb_has_error cur_thread s \<longrightarrow> Q s) \<and> (tcb_has_error cur_thread s \<longrightarrow> Perror s)\<rbrace>, \<lbrace>\<lambda>y. Inv\<rbrace>
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>?P'3 y\<rbrace>
 3. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y ya. y = cur_thread \<Longrightarrow> \<lbrace>?P'6 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 s. (\<not> tcb_has_error cur_thread s \<longrightarrow> Q s) \<and> (tcb_has_error cur_thread s \<longrightarrow> Perror s)\<rbrace>, \<lbrace>\<lambda>y. Inv\<rbrace>
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?P'6 y ya and K (y = cur_thread)\<rbrace>
 3. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y ya. y = cur_thread \<Longrightarrow> \<lbrace>?P'6 cur_thread ya\<rbrace> syscall (doE (cap, cap_ref) <- lookup_cap_and_slot cur_thread (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps cur_thread (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 y <- corrupt_ipc_buffer cur_thread True;
mark_tcb_intent_error cur_thread True
od) (\<lambda>inv. doE y <- liftE (set_cap (cur_thread, tcb_pending_op_slot) RestartCap);
y <- perform_invocation True True inv;
restart <- liftE (has_restart_cap cur_thread);
whenE restart (liftE (do y <- corrupt_ipc_buffer cur_thread True;
y <- mark_tcb_intent_error cur_thread False;
set_cap (cur_thread, tcb_pending_op_slot) RunningCap
od))
odE) \<lbrace>\<lambda>r s. (\<not> tcb_has_error cur_thread s \<longrightarrow> Q s) \<and> (tcb_has_error cur_thread s \<longrightarrow> Perror s)\<rbrace>, \<lbrace>\<lambda>y. Inv\<rbrace>
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?P'6 y ya and K (y = cur_thread)\<rbrace>
 3. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 cur_thread ya\<rbrace> syscall (doE (cap, cap_ref) <- lookup_cap_and_slot cur_thread (cdl_intent_cap (cdl_tcb_intent ya));
extra_caps <- lookup_extra_caps cur_thread (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 y <- corrupt_ipc_buffer cur_thread True;
mark_tcb_intent_error cur_thread True
od) (\<lambda>inv. doE y <- liftE (set_cap (cur_thread, tcb_pending_op_slot) RestartCap);
y <- perform_invocation True True inv;
restart <- liftE (has_restart_cap cur_thread);
whenE restart (liftE (do y <- corrupt_ipc_buffer cur_thread True;
y <- mark_tcb_intent_error cur_thread False;
set_cap (cur_thread, tcb_pending_op_slot) RunningCap
od))
odE) \<lbrace>\<lambda>r s. (\<not> tcb_has_error cur_thread s \<longrightarrow> Q s) \<and> (tcb_has_error cur_thread s \<longrightarrow> Perror s)\<rbrace>, \<lbrace>\<lambda>y. Inv\<rbrace>
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?P'9 y ya and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 3. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 cur_thread ya\<rbrace> syscall (doE (cap, cap_ref) <- lookup_cap_and_slot cur_thread intent_cptr;
extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE) handle_fault (\<lambda>(cap, cap_ref, extra_caps). decode_invocation cap cap_ref extra_caps intent_op) (do y <- corrupt_ipc_buffer cur_thread True;
mark_tcb_intent_error cur_thread True
od) (\<lambda>inv. doE y <- liftE (set_cap (cur_thread, tcb_pending_op_slot) RestartCap);
y <- perform_invocation True True inv;
restart <- liftE (has_restart_cap cur_thread);
whenE restart (liftE (do y <- corrupt_ipc_buffer cur_thread True;
y <- mark_tcb_intent_error cur_thread False;
set_cap (cur_thread, tcb_pending_op_slot) RunningCap
od))
odE) \<lbrace>\<lambda>r s. (\<not> tcb_has_error cur_thread s \<longrightarrow> Q s) \<and> (tcb_has_error cur_thread s \<longrightarrow> Perror s)\<rbrace>, \<lbrace>\<lambda>y. Inv\<rbrace>
 2. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?P'9 y ya and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 3. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> doE y <- liftE (set_cap (cur_thread, tcb_pending_op_slot) RestartCap);
y <- perform_invocation True True xa;
restart <- liftE (has_restart_cap cur_thread);
whenE restart (liftE (do y <- corrupt_ipc_buffer cur_thread True;
y <- mark_tcb_intent_error cur_thread False;
set_cap (cur_thread, tcb_pending_op_slot) RunningCap
od))
odE \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 6. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 8. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> doE y <- perform_invocation True True xa;
restart <- liftE (has_restart_cap cur_thread);
whenE restart (liftE (do y <- corrupt_ipc_buffer cur_thread True;
y <- mark_tcb_intent_error cur_thread False;
set_cap (cur_thread, tcb_pending_op_slot) RunningCap
od))
odE \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 3. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 7. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 9. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> doE restart <- liftE (has_restart_cap cur_thread);
whenE restart (liftE (do y <- corrupt_ipc_buffer cur_thread True;
y <- mark_tcb_intent_error cur_thread False;
set_cap (cur_thread, tcb_pending_op_slot) RunningCap
od))
odE \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 3. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 4. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 8. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 9. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 10. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>y ya x xa r ra rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 y ya x xa r ra rb\<rbrace> whenE rb (liftE (do y <- corrupt_ipc_buffer cur_thread True;
y <- mark_tcb_intent_error cur_thread False;
set_cap (cur_thread, tcb_pending_op_slot) RunningCap
od)) \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>?P'28 y ya x xa r ra\<rbrace>
 3. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 4. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 5. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 9. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 10. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>y ya x xa r ra rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 y ya x xa r ra rb\<rbrace> liftE (do y <- corrupt_ipc_buffer cur_thread True;
y <- mark_tcb_intent_error cur_thread False;
set_cap (cur_thread, tcb_pending_op_slot) RunningCap
od) \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 3. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 4. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 5. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 9. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 10. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>y ya x xa rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 cur_thread ya x xa () () True\<rbrace> do y <- corrupt_ipc_buffer cur_thread True;
y <- mark_tcb_intent_error cur_thread False;
set_cap (cur_thread, tcb_pending_op_slot) RunningCap
od \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 2. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 3. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 4. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 5. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 9. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 10. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>y ya x xa rb xb xc. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?B38 y ya x xa rb xb xc\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r s. Q s \<and> \<not> tcb_has_error cur_thread s\<rbrace>
 2. \<And>y ya x xa rb xb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?B36 y ya x xa rb xb\<rbrace> mark_tcb_intent_error cur_thread False \<lbrace>?B38 y ya x xa rb xb\<rbrace>
 3. \<And>y ya x xa rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 cur_thread ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>?B36 y ya x xa rb\<rbrace>
 4. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 5. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 6. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 7. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 9. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 10. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>y ya x xa rb xb xc. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'40 y ya x xa rb xb xc\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r s. Q s \<and> \<not> tcb_has_error cur_thread s\<rbrace>
 2. \<And>y ya x xa rb xb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?B36 y ya x xa rb xb\<rbrace> mark_tcb_intent_error cur_thread False \<lbrace>\<lambda>xc. ?P'40 y ya x xa rb xb xc and K (y = cur_thread)\<rbrace>
 3. \<And>y ya x xa rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 cur_thread ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>?B36 y ya x xa rb\<rbrace>
 4. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 5. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 6. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 7. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 9. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 10. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>y ya x xa rb. \<lbrakk>cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'40 cur_thread ya x xa True () ()\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>r s. Q s \<and> \<not> tcb_has_error cur_thread s\<rbrace>
 2. \<And>y ya x xa rb xb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?B36 y ya x xa rb xb\<rbrace> mark_tcb_intent_error cur_thread False \<lbrace>\<lambda>xc. ?P'40 y ya x xa rb xb xc and K (y = cur_thread)\<rbrace>
 3. \<And>y ya x xa rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 cur_thread ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>?B36 y ya x xa rb\<rbrace>
 4. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 5. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 6. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 7. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 9. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 10. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>y ya x xa rb xb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?B36 y ya x xa rb xb\<rbrace> mark_tcb_intent_error cur_thread False \<lbrace>\<lambda>xc. (\<lambda>a. Rm a \<and> ((\<lambda>s. \<not> tcb_has_error y s) and K (snd (y, tcb_pending_op_slot) \<noteq> tcb_ipcbuffer_slot)) a) and K (y = cur_thread)\<rbrace>
 2. \<And>y ya x xa rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 cur_thread ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>?B36 y ya x xa rb\<rbrace>
 3. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 4. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 5. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 6. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 9. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 10. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>y ya x xa rb xb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'49 y ya x xa rb xb\<rbrace> mark_tcb_intent_error cur_thread False \<lbrace>\<lambda>xc. (\<lambda>a. Rm a \<and> ((\<lambda>s. \<not> tcb_has_error y s) and K (snd (y, tcb_pending_op_slot) \<noteq> tcb_ipcbuffer_slot)) a) and K (y = cur_thread)\<rbrace>
 2. \<And>y ya x xa rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 cur_thread ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>xb. ?P'49 y ya x xa rb xb and K (y = cur_thread)\<rbrace>
 3. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 4. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 5. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 6. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 9. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 10. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>y ya x xa rb. \<lbrakk>cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'49 cur_thread ya x xa True ()\<rbrace> mark_tcb_intent_error cur_thread False \<lbrace>\<lambda>xc a. Rm a \<and> \<not> tcb_has_error cur_thread a\<rbrace>
 2. \<And>y ya x xa rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 cur_thread ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>xb. ?P'49 y ya x xa rb xb and K (y = cur_thread)\<rbrace>
 3. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 4. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 5. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 6. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 9. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 10. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>y ya x xa rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 cur_thread ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>xb. (\<lambda>a. Ra a \<and> True) and K (y = cur_thread)\<rbrace>
 2. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 3. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 4. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 5. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 9. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 10. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>y ya x xa rb. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; rb\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 cur_thread ya x xa () () (ds_id True)\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>xb. Ra\<rbrace>
 2. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>rb. if rb then ?Q31 y ya x xa r ra rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 3. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 4. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 5. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 8. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 9. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 10. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>y ya x xa r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 y ya x xa r ra\<rbrace> has_restart_cap cur_thread \<lbrace>\<lambda>r. if r then Rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)\<rbrace>
 2. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>?P'25 y ya x xa r\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 3. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 4. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 8. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 9. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 10. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>\<lambda>r s. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> (if RestartCap = RestartCap then Rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)) s\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>?P'22 y ya x xa\<rbrace>
 3. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 7. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 9. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya x xa r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'61 y ya x xa r\<rbrace> perform_invocation True True xa \<lbrace>\<lambda>r s. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> (if RestartCap = RestartCap then Rb else Q and (\<lambda>s. \<not> tcb_has_error cur_thread s)) s\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. ?P'61 y ya x xa r and K (y = cur_thread)\<rbrace>
 3. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 7. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 9. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya x xa. \<lbrakk>cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'61 cur_thread ya x xa ()\<rbrace> perform_invocation True True xa \<lbrace>\<lambda>r s. Rb s \<and> cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. ?P'61 y ya x xa r and K (y = cur_thread)\<rbrace>
 3. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 7. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 9. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qa12 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV xa and K (y = cur_thread)\<rbrace>
 2. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>?Qa12 y ya r\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 6. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 8. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'65 y ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV xa and K (y = cur_thread)\<rbrace>
 2. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>\<lambda>xa. ?P'65 y ya r xa and K (y = cur_thread)\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 6. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 8. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya x xa. \<lbrakk>cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; y = cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?P'65 cur_thread ya x xa\<rbrace> set_cap (cur_thread, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>r. PIV xa\<rbrace>
 2. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>\<lambda>xa. ?P'65 y ya r xa and K (y = cur_thread)\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 6. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 8. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 y ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>\<lambda>xa. Ps xa and K (y = cur_thread)\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Qi12 cur_thread ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>Ps\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>?Qi12 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; \<not> ep_related_cap (fst r) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op\<rbrakk> \<Longrightarrow> \<lbrace>?P'71 cur_thread ya r\<rbrace> case r of (cap, a) \<Rightarrow> case a of (cap_ref, extra_caps) \<Rightarrow> decode_invocation cap cap_ref extra_caps intent_op \<lbrace>Ps\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>\<lambda>a. ?P'71 y ya a and K (\<not> ep_related_cap (fst a) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; \<not> ep_related_cap (fst r) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op\<rbrakk> \<Longrightarrow> \<lbrace>?P'71 cur_thread ya r\<rbrace> decode_invocation (fst r) (fst (snd r)) (snd (snd r)) intent_op \<lbrace>Ps\<rbrace>, \<lbrace>\<lambda>ret. Perror\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>\<lambda>a. ?P'71 y ya a and K (\<not> ep_related_cap (fst a) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> doE a <- lookup_cap_and_slot cur_thread intent_cptr;
case a of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE
odE \<lbrace>\<lambda>a. Pd (snd (snd a)) (fst a) (fst (snd a)) and K (\<not> ep_related_cap (fst a) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 4. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 6. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'74 y ya r\<rbrace> case r of (cap, cap_ref) \<Rightarrow> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (cap, cap_ref, extra_caps)
odE \<lbrace>\<lambda>a. Pd (snd (snd a)) (fst a) (fst (snd a)) and K (\<not> ep_related_cap (fst a) \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>?P'74 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'74 cur_thread ya r\<rbrace> doE extra_caps <- lookup_extra_caps cur_thread intent_extra;
returnOk (fst r, snd r, extra_caps)
odE \<lbrace>\<lambda>a b. Pd (snd (snd a)) (fst a) (fst (snd a)) b \<and> \<not> ep_related_cap (fst a)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>?P'74 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'78 y ya r ra\<rbrace> returnOk (fst r, snd r, ra) \<lbrace>\<lambda>a b. Pd (snd (snd a)) (fst a) (fst (snd a)) b \<and> \<not> ep_related_cap (fst a)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'74 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?P'78 y ya r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>?P'74 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 6. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 8. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya r ra. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'78 cur_thread ya r ra\<rbrace> return (fst r, snd r, ra) \<lbrace>\<lambda>a b. Pd (snd (snd a)) (fst a) (fst (snd a)) b \<and> \<not> ep_related_cap (fst a)\<rbrace>
 2. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'74 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?P'78 y ya r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>?P'74 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 6. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 8. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'74 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>\<lambda>ra a. Pd (snd (snd (fst r, snd r, ra))) (fst (fst r, snd r, ra)) (fst (snd (fst r, snd r, ra))) a \<and> \<not> ep_related_cap (fst (fst r, snd r, ra))\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>?P'74 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'74 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>\<lambda>ra a. Pd ra (fst r) (snd r) a \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>?P'74 y ya\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'87 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>\<lambda>ra a. Pd ra (fst r) (snd r) a \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r. ?P'87 y ya r and K (cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'87 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>\<lambda>ra a. Pd ra (fst r) (snd r) a \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r. ?P'87 y ya r and K (cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P95 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q90 y ya r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'93 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q'90 y ya r\<rbrace>, -
 3. \<And>y ya r rv s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Q90 y ya r rv s \<and> ?Q'90 y ya r rv s\<rbrakk> \<Longrightarrow> Pd rv (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)
 4. \<And>y ya r e s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r. ?P95 y ya r and ?P'93 y ya r and K (cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 7. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 8. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 9. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 10. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'93 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q'90 y ya r\<rbrace>, -
 2. \<And>y ya r rv s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; Pd rv (fst r) (snd r) s \<and> ?Q'90 y ya r rv s\<rbrakk> \<Longrightarrow> Pd rv (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)
 3. \<And>y ya r e s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r. Pd1 (fst r) (snd r) and ?P'93 y ya r and K (cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 7. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 9. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya r rv s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; Pd rv (fst r) (snd r) s \<and> ?Q'90 y ya r rv s\<rbrakk> \<Longrightarrow> Pd rv (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)
 2. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'93 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q'90 y ya r\<rbrace>, -
 3. \<And>y ya r e s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r. Pd1 (fst r) (snd r) and ?P'93 y ya r and K (cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 7. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 9. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y ya r rv s. \<lbrakk>y = cur_thread; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op; cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; Pd rv (fst r) (snd r) s; ?Q'90 y ya r rv s\<rbrakk> \<Longrightarrow> Pd rv (fst r) (snd r) s \<and> \<not> ep_related_cap (fst r)
 2. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'93 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>?Q'90 y ya r\<rbrace>, -
 3. \<And>y ya r e s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r. Pd1 (fst r) (snd r) and ?P'93 y ya r and K (cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 6. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 7. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 8. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 9. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya r. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?P'93 cur_thread ya r\<rbrace> lookup_extra_caps cur_thread intent_extra \<lbrace>\<lambda>a b. \<not> ep_related_cap (fst r)\<rbrace>, -
 2. \<And>y ya r e s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r. Pd1 (fst r) (snd r) and ?P'93 y ya r and K (cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 5. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 6. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 7. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 8. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya r e s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr; cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; False\<rbrakk> \<Longrightarrow> False
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r. Pd1 (fst r) (snd r) and (\<lambda>a. \<not> ep_related_cap (fst r)) and K (cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 4. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 5. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 6. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 7. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r. Pd1 (fst r) (snd r) and (\<lambda>a. \<not> ep_related_cap (fst r)) and K (cdl_intent_extras (cdl_tcb_intent ya) = intent_extra)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 4. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 6. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>?Pre14 cur_thread ya\<rbrace> lookup_cap_and_slot cur_thread intent_cptr \<lbrace>\<lambda>r a. Pd1 (fst r) (snd r) a \<and> \<not> ep_related_cap (fst r)\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 3. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 4. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; ?Pre14 cur_thread ya s\<rbrakk> \<Longrightarrow> Perror s
 5. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. ?Pre14 y ya and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 6. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> mark_tcb_intent_error cur_thread True \<lbrace>\<lambda>rv. Perror\<rbrace>
 2. \<And>y ya. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra\<rbrakk> \<Longrightarrow> \<lbrace>Perror\<rbrace> corrupt_ipc_buffer cur_thread True \<lbrace>\<lambda>ya. Perror\<rbrace>
 3. \<And>y ya s. \<lbrakk>y = cur_thread; cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra; Pd2 s\<rbrakk> \<Longrightarrow> Perror s
 4. \<And>y. \<lbrace>?P' y\<rbrace> get_thread y \<lbrace>\<lambda>ya. Pd2 and (\<lambda>s. \<not> tcb_has_error y s) and K (cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra) and K (y = cur_thread)\<rbrace>
 5. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) 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 s. Pd2 s \<and> \<not> tcb_has_error y s \<and> cdl_intent_op (cdl_tcb_intent ya) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent ya) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent ya) = intent_extra \<and> y = cur_thread\<rbrace>
 2. \<lbrace>Pd2 and tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some intent_op \<and> cdl_intent_cap (cdl_tcb_intent tcb) = intent_cptr \<and> cdl_intent_extras (cdl_tcb_intent tcb) = intent_extra \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread\<rbrace> gets_the cdl_current_thread \<lbrace>?P'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. 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 \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) cur_thread s \<Longrightarrow> (\<exists>y. cdl_current_thread s = Some y) \<longrightarrow> \<not> tcb_has_error (the (cdl_current_thread s)) 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 \<and> the (cdl_current_thread s) = cur_thread) (the (cdl_current_thread s)) s proof (prove)
goal:
No subgoals!