theory CSpace_All

lemma lookupCap_ccorres':
  "ccorres (lookup_failure_rel \<currency> ccap_relation) lookupCap_xf
   (valid_pspace' and tcb_at' a)
   (UNIV \<inter> {s. cPtr_' s = b} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr a}) []
  (lookupCap a b) (Call lookupCap_'proc)" apply (cinit lift: cPtr_' thread_' simp: lookupCapAndSlot_def liftME_def bindE_assoc) apply (ctac (no_vcg) add: lookupSlotForThread_ccorres')
     \<comment> \<open>case where lu_ret.status is EXCEPTION_NONE\<close> apply (simp  add: split_beta cong:call_ignore_cong) apply csymbr  \<comment> \<open>call status_C_update\<close> apply (simp add: Collect_const[symmetric] lookupSlot_raw_rel_def liftE_def
                 del: Collect_const) apply (rule ccorres_move_c_guard_cte) apply (ctac ) apply (rule ccorres_return_CE [unfolded returnOk_def, simplified], simp+)[1] apply wp apply vcg
    \<comment> \<open>case where lu_ret.status is *not* EXCEPTION_NONE\<close> apply simp apply (rule ccorres_split_throws) apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr \<comment> \<open>call cap_null_cap_new_'proc\<close> apply csymbr apply (rule ccorres_return_C_errorE, simp+)[1] apply vcg apply (wp | simp)+

  \<comment> \<open>last subgoal\<close> apply (clarsimp simp: valid_pspace_valid_objs') apply (intro impI conjI allI) apply (simp add: lookupSlot_raw_rel_def) apply (rule_tac y="ret___struct_lookupCap_ret_C_' s" for s
                    in arg_cong, fastforce) apply simp apply (case_tac err, simp+) [1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (valid_pspace' and tcb_at' a) (UNIV \<inter> \<lbrace>\<acute>cPtr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>) [] (lookupCap a b) (Call lookupCap_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?Q446 thread cPtr) (?Q'446 thread cPtr) [SKIP] (doE x <- lookupSlotForThread a b;
liftE (getSlotCap x)
odE) (\<acute>lu_ret___struct_lookupSlot_raw_ret_C :== CALL lookupSlot_'proc(thread,cPtr);;
(IF lookupSlot_raw_ret_C.status_C \<acute>lu_ret___struct_lookupSlot_raw_ret_C \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C \<acute>lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C (lu_ret___struct_lookupSlot_raw_ret_C_' s)} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C \<acute>lu_ret___struct_lookupSlot_raw_ret_C\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'))))
 2. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q446 thread cPtr s \<and> s' \<in> ?Q'446 thread cPtr proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C); lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?Q454 thread cPtr rv) (?Q'454 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (liftE (getSlotCap rv)) (IF lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 thread cPtr err) (?Q''454 thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (IF lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>?Q454 thread cPtr\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q'454 thread cPtr rv (ret__struct_lookupSlot_raw_ret_C_' t))) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C); lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?Q454 (tcb_ptr_to_ctcb_ptr a) b rv) (?Q'454 (tcb_ptr_to_ctcb_ptr a) b rv lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (liftE (getSlotCap rv)) (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'))
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 thread cPtr err) (?Q''454 thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (IF lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>?Q454 thread cPtr\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q'454 thread cPtr rv (ret__struct_lookupSlot_raw_ret_C_' t))) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C); lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?Q454 (tcb_ptr_to_ctcb_ptr a) b rv) (?G'682 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) [SKIP] (liftE (getSlotCap rv)) (Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCap_ret_C));;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 thread cPtr err) (?Q''454 thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (IF lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>?Q454 thread cPtr\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> ?G'683 thread cPtr rv (ret__struct_lookupSlot_raw_ret_C_' t) s}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?G'683 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?G'682 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C = cte_Ptr rv; lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?Q454 (tcb_ptr_to_ctcb_ptr a) b rv) (?G'682 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) [SKIP] (do r <- getSlotCap rv;
return (Inr r)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr rv} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCap_ret_C));;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 thread cPtr err) (?Q''454 thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (IF lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>?Q454 thread cPtr\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> ?G'683 thread cPtr rv (ret__struct_lookupSlot_raw_ret_C_' t) s}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?G'683 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?G'682 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C = cte_Ptr rv; lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?A741 (tcb_ptr_to_ctcb_ptr a) b rv) (?C'740 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) [SKIP] (do r <- getSlotCap rv;
return (Inr r)
od) (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 thread cPtr err) (?Q''454 thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (IF lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. ?A741 thread cPtr a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> ?C'739 thread cPtr rv (ret__struct_lookupSlot_raw_ret_C_' t) s \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
\<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?C'740 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) \<equiv>\<^sup>? ?C'739 (tcb_ptr_to_ctcb_ptr a) b proof (prove)
goal (6 subgoals):
 1. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_Ca rva ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C = cte_Ptr rv; lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; ccap_relation rva ret___struct_lookupCap_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?Q748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_Ca rva) (?Q'748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_Ca rva ret___struct_lookupCap_ret_C) [SKIP] (return (Inr rva)) (return_C ret__struct_lookupCap_ret_C_'_update (\<lambda>a. lookupCap_ret_C.cap_C_update (\<lambda>_. ret___struct_lookupCap_ret_C) (?oldv748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_Ca)))
 2. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C = cte_Ptr rv; lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> \<lbrace>?R758 (tcb_ptr_to_ctcb_ptr a) b rv\<rbrace> getSlotCap rv \<lbrace>?Q748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C\<rbrace>
 3. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C = cte_Ptr rv; lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'756 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCap_ret_C) {s. ret___struct_lookupCap_ret_C_' s = lookupCap_ret_C.cap_C_update (\<lambda>_. (lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) (?oldv748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) \<and> (\<forall>rva. ccap_relation rva ((lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) \<longrightarrow> s \<in> ?Q'748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C rva ((lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s))}
 4. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 thread cPtr err) (?Q''454 thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (IF lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 5. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R758 thread cPtr a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 6. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> ?R'754 thread cPtr rv (ret__struct_lookupSlot_raw_ret_C_' t) s \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
\<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?R'756 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) \<equiv>\<^sup>? ?R'754 (tcb_ptr_to_ctcb_ptr a) b proof (prove)
goal (5 subgoals):
 1. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C = cte_Ptr rv; lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> \<lbrace>?R758 (tcb_ptr_to_ctcb_ptr a) b rv\<rbrace> getSlotCap rv \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C = cte_Ptr rv; lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'756 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCap_ret_C) {s. ret___struct_lookupCap_ret_C_' s = lookupCap_ret_C.cap_C_update (\<lambda>_. (lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) (?oldv748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) \<and> (\<forall>rva. ccap_relation rva ((lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) \<longrightarrow> s \<in> \<lbrace>lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>_. (lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) (?oldv748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. (lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) (?oldv748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C)))\<rbrace>)}
 3. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 thread cPtr err) (?Q''454 thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (IF lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 4. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R758 thread cPtr a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 5. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> ?R'754 thread cPtr rv (ret__struct_lookupSlot_raw_ret_C_' t) s \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
\<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?R'756 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) \<equiv>\<^sup>? ?R'754 (tcb_ptr_to_ctcb_ptr a) b proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C = cte_Ptr rv; lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'756 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCap_ret_C) {s. ret___struct_lookupCap_ret_C_' s = lookupCap_ret_C.cap_C_update (\<lambda>_. (lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) (?oldv748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) \<and> (\<forall>rva. ccap_relation rva ((lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) \<longrightarrow> s \<in> \<lbrace>lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>_. (lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) (?oldv748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. (lookupCap_ret_C.cap_C \<circ> ret___struct_lookupCap_ret_C_') s) (?oldv748 thread cPtr rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C)))\<rbrace>)}
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 thread cPtr err) (?Q''454 thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (IF lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> ?R'754 thread cPtr rv (ret__struct_lookupSlot_raw_ret_C_' t) s \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
\<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?R'756 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) \<equiv>\<^sup>? ?R'754 (tcb_ptr_to_ctcb_ptr a) b proof (prove)
goal (3 subgoals):
 1. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 thread cPtr err) (?Q''454 thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (IF lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'
FI;;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 2. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 3. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> \<lbrace>lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C) = lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv838 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s) \<and> (\<forall>rva. ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) \<longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv837 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv836 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s))))\<rbrace> \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (3 subgoals):
 1. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 (tcb_ptr_to_ctcb_ptr a) b err) (?Q''454 (tcb_ptr_to_ctcb_ptr a) b err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_';;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCap_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(lookupSlot_raw_ret_C.slot_C rv'\<rightarrow>[''cap_C'']))) \<acute>ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 2. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 3. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> \<lbrace>lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C) = lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv838 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s) \<and> (\<forall>rva. ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) \<longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv837 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv836 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s))))\<rbrace> \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?Q''454 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 (tcb_ptr_to_ctcb_ptr a) b err) (?P'842 (tcb_ptr_to_ctcb_ptr a) b err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'841 (tcb_ptr_to_ctcb_ptr a) b err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_' {},UNIV
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> \<lbrace>lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C) = lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv838 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s) \<and> (\<forall>rva. ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) \<longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv837 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv836 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s))))\<rbrace> \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?P'842 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t) \<inter> ?R'841 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 (tcb_ptr_to_ctcb_ptr a) b err) (?P'842 (tcb_ptr_to_ctcb_ptr a) b err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')))
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'841 (tcb_ptr_to_ctcb_ptr a) b err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_' {},UNIV
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> \<lbrace>lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C) = lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv838 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s) \<and> (\<forall>rva. ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) \<longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv837 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv836 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s))))\<rbrace> \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> ?P'842 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t) \<inter> ?R'841 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 (tcb_ptr_to_ctcb_ptr a) b err) (?G'914 err rv' lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C) [SKIP] (throwError err) (\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
(\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_'))
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'841 (tcb_ptr_to_ctcb_ptr a) b err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_' {},UNIV
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> \<lbrace>lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C) = lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv838 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s) \<and> (\<forall>rva. ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) \<longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv837 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv836 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s))))\<rbrace> \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> ?G'915 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t) s}} \<inter> ?R'841 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?G'915 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>err rv' lu_ret___struct_lookupSlot_raw_ret_C s. ?G'914 err rv' lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C ret__struct_cap_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 (tcb_ptr_to_ctcb_ptr a) b err) (?G'1005 err rv' lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C ret__struct_cap_C) [SKIP] (throwError err) (\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. ret__struct_cap_C) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') ret___struct_lookupCap_ret_C);;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_')
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'841 (tcb_ptr_to_ctcb_ptr a) b err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_' {},UNIV
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> \<lbrace>lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C) = lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv838 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s) \<and> (\<forall>rva. ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) \<longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv837 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv836 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s))))\<rbrace> \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> {sa. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> ?G'1006 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t) s v}}} \<inter> ?R'841 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?G'1006 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>err rv' lu_ret___struct_lookupSlot_raw_ret_C s. ?G'1005 err rv' lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C ret__struct_cap_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (?QE454 (tcb_ptr_to_ctcb_ptr a) b err) (?G'1077 err rv' lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCap_ret_C ret__struct_cap_C) [SKIP] (throwError err) (return_C ret__struct_lookupCap_ret_C_'_update (\<lambda>a. lookupCap_ret_C.cap_C_update (\<lambda>_. ret__struct_cap_C) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') ret___struct_lookupCap_ret_C)))
 2. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'841 (tcb_ptr_to_ctcb_ptr a) b err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_' {},UNIV
 3. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE454 thread cPtr\<rbrace>
 4. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> \<lbrace>lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C) = lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv838 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s) \<and> (\<forall>rva. ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) \<longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv837 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv836 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s))))\<rbrace> \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> {sa. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.cap_C_update (\<lambda>_. v) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s))\<rparr> \<in> ?G'1078 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t) s v}}}} \<inter> ?R'841 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?G'1078 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>err rv' lu_ret___struct_lookupSlot_raw_ret_C s. ?G'1077 err rv' lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (3 subgoals):
 1. \<And>thread cPtr err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; lookupSlot_raw_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C rv') lu_ret___struct_lookupSlot_raw_ret_C\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'841 (tcb_ptr_to_ctcb_ptr a) b err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCap_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCap_ret_C :== lookupCap_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCap_ret_C;;
return_C ret__struct_lookupCap_ret_C_'_update ret___struct_lookupCap_ret_C_' {},UNIV
 2. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> \<lbrace>lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C) = lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv838 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s) \<and> (\<forall>rva. ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) \<longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv837 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv836 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s))))\<rbrace> \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> {sa. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.cap_C_update (\<lambda>_. v) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s))\<rparr> \<in> {sa. lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>_. v) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>_. v) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s)))) (errstate sa)}}}}} \<inter> ?R'841 thread cPtr err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (2 subgoals):
 1. \<And>thread cPtr. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b\<rbrakk> \<Longrightarrow> \<lbrace>?R454 thread cPtr\<rbrace> lookupSlotForThread a b \<lbrace>\<lambda>a. (\<lambda>a. True) and (\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' a) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a and ?R454 thread cPtr) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtr) (thread_'_update (\<lambda>_. thread) s) \<in> \<lbrace>\<acute>capptr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>} \<inter> {s. \<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> \<lbrace>cte_Ptr rv = cte_Ptr rv\<rbrace> \<inter> \<lbrace>lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C) = lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv838 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s) \<and> (\<forall>rva. ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) \<longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv837 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> ccap_relation rva (lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>v. lookupCap_ret_C.cap_C (lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<^bsup>s\<^esup>ret___struct_lookupCap_ret_C))) (?oldv836 thread cPtr rv \<^bsup>t\<^esup>ret__struct_lookupSlot_raw_ret_C s))))\<rbrace> \<inter> \<lbrace>True\<rbrace>}})) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr> \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s)\<rparr> \<in> {sa. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCap_ret_C_' := lookupCap_ret_C.cap_C_update (\<lambda>_. v) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s))\<rparr> \<in> {sa. lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>_. v) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupCap_ret_C.status_C (lookupCap_ret_C.cap_C_update (\<lambda>_. v) (lookupCap_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCap_ret_C_' s)))) (errstate sa)}}}}} \<inter> \<lbrace>True\<rbrace>))}
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (1 subgoal):
 1. \<And>thread cPtr s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr a; cPtr = b; (s, s') \<in> rf_sr; valid_pspace' s \<and> tcb_at' a s\<rbrakk> \<Longrightarrow> valid_objs' s \<and> (\<forall>t. (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s')) = lookupCap_ret_C.cap_C_update (\<lambda>v. h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (?oldv838 (tcb_ptr_to_ctcb_ptr a) b rv (ret__struct_lookupSlot_raw_ret_C_' t) (s'\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr>)) \<and> ((\<exists>rva. ccap_relation rva (h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C''])))) \<longrightarrow> lookupCap_ret_C.status_C (?oldv837 (tcb_ptr_to_ctcb_ptr a) b rv (ret__struct_lookupSlot_raw_ret_C_' t) (s'\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr>)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> (\<exists>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) \<longrightarrow> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate (s'\<lparr>globals := globals t\<rparr>)))))
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (1 subgoal):
 1. \<And>s s' t. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s\<rbrakk> \<Longrightarrow> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) \<longrightarrow> lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s')) = lookupCap_ret_C.cap_C_update (\<lambda>v. h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (?oldv838 (tcb_ptr_to_ctcb_ptr a) b rv (ret__struct_lookupSlot_raw_ret_C_' t) (s'\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr>)) \<and> ((\<exists>rva. ccap_relation rva (h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C''])))) \<longrightarrow> lookupCap_ret_C.status_C (?oldv837 (tcb_ptr_to_ctcb_ptr a) b rv (ret__struct_lookupSlot_raw_ret_C_' t) (s'\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr>)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) \<and> (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t) \<longrightarrow> (\<exists>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) \<longrightarrow> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate (s'\<lparr>globals := globals t\<rparr>))))
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (3 subgoals):
 1. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s; lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t))\<rbrakk> \<Longrightarrow> lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s')) = lookupCap_ret_C.cap_C_update (\<lambda>v. h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (?oldv838 (tcb_ptr_to_ctcb_ptr a) b rv (ret__struct_lookupSlot_raw_ret_C_' t) (s'\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr>))
 2. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s; lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)); \<exists>rva. ccap_relation rva (h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C''])))\<rbrakk> \<Longrightarrow> lookupCap_ret_C.status_C (?oldv837 (tcb_ptr_to_ctcb_ptr a) b rv (ret__struct_lookupSlot_raw_ret_C_' t) (s'\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr>)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE
 3. \<And>s s' t err. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s; lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t); \<exists>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate (s'\<lparr>globals := globals t\<rparr>))
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (3 subgoals):
 1. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s; lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t) = cte_Ptr rv\<rbrakk> \<Longrightarrow> lookupCap_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' s')) = lookupCap_ret_C.cap_C_update (\<lambda>v. h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (?oldv838 (tcb_ptr_to_ctcb_ptr a) b rv (ret__struct_lookupSlot_raw_ret_C_' t) (s'\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr>))
 2. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s; lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)); \<exists>rva. ccap_relation rva (h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C''])))\<rbrakk> \<Longrightarrow> lookupCap_ret_C.status_C (?oldv837 (tcb_ptr_to_ctcb_ptr a) b rv (ret__struct_lookupSlot_raw_ret_C_' t) (s'\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr>)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE
 3. \<And>s s' t err. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s; lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t); \<exists>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate (s'\<lparr>globals := globals t\<rparr>))
flex-flex pairs:
?oldv838 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv837 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s)
?oldv836 (tcb_ptr_to_ctcb_ptr a) b \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?oldv835 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCap_ret_C_' s) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t rv. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s; lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookupSlot_raw_rel rv (lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)); \<exists>rva. ccap_relation rva (h_val (hrs_mem (t_hrs_' (globals t))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C''])))\<rbrakk> \<Longrightarrow> lookupCap_ret_C.status_C (lookupCap_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCap_ret_C_' (s'\<lparr>globals := globals t, lu_ret___struct_lookupSlot_raw_ret_C_' := ret__struct_lookupSlot_raw_ret_C_' t\<rparr>))) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE
 2. \<And>s s' t err. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s; lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t); \<exists>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate (s'\<lparr>globals := globals t\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s s' t err. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' a s; lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate t); \<exists>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (errstate (s'\<lparr>globals := globals t\<rparr>)) proof (prove)
goal:
No subgoals!