theory CSpace_All

lemma lookupCapAndSlot_ccorres :
  "ccorres
   (lookup_failure_rel \<currency> (\<lambda>(c,s) (c',s'). ccap_relation c c' \<and> s'= Ptr s)) lookupCapAndSlot_xf
   (\<lambda>s. invs' s \<and> tcb_at' thread s)
   (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>cPtr = cPtr\<rbrace> ) []
  (lookupCapAndSlot thread cPtr)
  (Call lookupCapAndSlot_'proc)" apply (cinit lift: thread_' cPtr_') apply (ctac (no_vcg))
     \<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 csymbr  \<comment> \<open>call slot_C_update\<close> apply (simp add: Collect_const[symmetric] lookupSlot_raw_rel_def liftE_bindE
                 del: Collect_const) apply (rule ccorres_move_c_guard_cte) apply (rule_tac P="cte_at' rv" and P'=UNIV in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: Bex_def in_monad getSlotCap_def in_getCTE2 cte_wp_at_ctes_of) apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) apply (simp add: ccte_relation_ccap_relation typ_heap_simps')
    \<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 (rule ccorres_return_C_errorE, simp+)[1] apply vcg apply (wp | simp)+

  \<comment> \<open>last subgoal\<close> apply clarsimp apply (rule conjI, fastforce) apply clarsimp apply (case_tac err, simp+) [1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (lookup_failure_rel \<currency> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (\<lambda>s. invs' s \<and> tcb_at' thread s) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>cPtr = cPtr\<rbrace>) [] (lookupCapAndSlot thread cPtr) (Call lookupCapAndSlot_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?Q511 cPtra threada) (?Q'511 cPtra threada) [SKIP] (doE slot <- lookupSlotForThread thread cPtr;
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE) (\<acute>lu_ret___struct_lookupSlot_raw_ret_C :== CALL lookupSlot_'proc(threada,cPtra);;
(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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C \<acute>lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C \<acute>lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCapAndSlot_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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_')))))
 2. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q511 cPtra threada s \<and> s' \<in> ?Q'511 cPtra threada proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada rv lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?Q519 cPtra threada rv) (?Q'519 cPtra threada rv lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (doE cap <- liftE (getSlotCap rv);
returnOk (cap, rv)
odE) (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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCapAndSlot_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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>?Q519 cPtra threada\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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'519 cPtra threada 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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada rv lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?Q519 cPtr (tcb_ptr_to_ctcb_ptr thread) rv) (?Q'519 cPtr (tcb_ptr_to_ctcb_ptr thread) rv lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (doE cap <- liftE (getSlotCap rv);
returnOk (cap, rv)
odE) (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCapAndSlot_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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_')))
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>?Q519 cPtra threada\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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'519 cPtra threada 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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?Q519 cPtr (tcb_ptr_to_ctcb_ptr thread) rv) (?G'784 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C) [SKIP] (doE cap <- liftE (getSlotCap rv);
returnOk (cap, rv)
odE) (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCapAndSlot_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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>?Q519 cPtra threada\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> ?G'785 cPtra threada 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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?G'785 cPtr (tcb_ptr_to_ctcb_ptr thread) \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?G'784 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCapAndSlot_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?Q519 cPtr (tcb_ptr_to_ctcb_ptr thread) rv) (?G'843 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C) [SKIP] (doE cap <- liftE (getSlotCap rv);
returnOk (cap, rv)
odE) (Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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'']))) (lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C lu_ret___struct_lookupSlot_raw_ret_C) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCapAndSlot_ret_C)));;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_')
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>?Q519 cPtra threada\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> ?G'844 cPtra threada 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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?G'844 cPtr (tcb_ptr_to_ctcb_ptr thread) \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?G'843 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCapAndSlot_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?Q519 cPtr (tcb_ptr_to_ctcb_ptr thread) rv) (?G'843 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C) [SKIP] (do cap <- getSlotCap rv;
returnOk (cap, rv)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr rv} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. cte_Ptr rv) (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCapAndSlot_ret_C)));;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_')
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>?Q519 cPtra threada\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> ?G'844 cPtra threada 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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?G'844 cPtr (tcb_ptr_to_ctcb_ptr thread) \<equiv>\<^sup>? \<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?G'843 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCapAndSlot_ret_C_' s) proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?A902 cPtr (tcb_ptr_to_ctcb_ptr thread) rv) (?C'901 rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C) [SKIP] (do cap <- getSlotCap rv;
returnOk (cap, rv)
od) (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. cte_Ptr rv) (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCapAndSlot_ret_C));;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_')
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. ?A902 cPtra threada a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> ?C'900 cPtra threada 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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
\<lambda>rv lu_ret___struct_lookupSlot_raw_ret_C s. ?C'901 rv lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCapAndSlot_ret_C_' s) \<equiv>\<^sup>? ?C'900 cPtr (tcb_ptr_to_ctcb_ptr thread) proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. cte_wp_at' (\<lambda>_. True) rv \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. cte_Ptr rv) (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCapAndSlot_ret_C));;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_' {},{s. \<exists>(rv, \<sigma>')\<in>fst ((do cap <- getSlotCap rv;
returnOk (cap, rv)
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (lookup_failure_rel \<currency> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) rv (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_' s)}
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada rv lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C \<sigma>. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> {s. cte_wp_at' (\<lambda>_. True) rv \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rva, \<sigma>')\<in>fst ((do cap <- getSlotCap rv;
returnOk (cap, rv)
od) \<sigma>). (\<sigma>', s\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. cte_Ptr rv) (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCapAndSlot_ret_C)), ret__struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. cte_Ptr rv) (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCapAndSlot_ret_C)), global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (lookup_failure_rel \<currency> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) rva (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_' (s\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. cte_Ptr rv) (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCapAndSlot_ret_C)), ret__struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. cte_Ptr rv) (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C'']))) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) ret___struct_lookupCapAndSlot_ret_C)), global_exn_var_' := Return\<rparr>))}
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>rv lu_ret___struct_lookupSlot_raw_ret_C \<sigma> x cte. \<lbrakk>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; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> rv = Some cte\<rbrakk> \<Longrightarrow> ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C''])))
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>rv lu_ret___struct_lookupSlot_raw_ret_C \<sigma> x cte y'. \<lbrakk>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; ctes_of \<sigma> rv = Some cte; ctes_of \<sigma> rv = Some cte; ccte_relation cte y'; cslift x (cte_Ptr rv) = Some y'\<rbrakk> \<Longrightarrow> ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(cte_Ptr rv\<rightarrow>[''cap_C''])))
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (3 subgoals):
 1. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtra threada err) (?Q''519 cPtra threada 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_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'
FI;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 2. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 3. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (3 subgoals):
 1. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtr (tcb_ptr_to_ctcb_ptr thread) err) (?Q''519 cPtr (tcb_ptr_to_ctcb_ptr thread) err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_';;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c lookupSlot_raw_ret_C.slot_C rv'} (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_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_lookupCapAndSlot_ret_C);;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 2. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 3. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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''519 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtr (tcb_ptr_to_ctcb_ptr thread) err) (?P'934 cPtr (tcb_ptr_to_ctcb_ptr thread) err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_')
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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'933 cPtr (tcb_ptr_to_ctcb_ptr thread) err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_' {},UNIV
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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'934 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t) \<inter> ?R'933 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtr (tcb_ptr_to_ctcb_ptr thread) err) (?P'934 cPtr (tcb_ptr_to_ctcb_ptr thread) err rv' lu_ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
(\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_'))))
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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'933 cPtr (tcb_ptr_to_ctcb_ptr thread) err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_' {},UNIV
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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'934 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t) \<inter> ?R'933 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (4 subgoals):
 1. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C ret__struct_cap_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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> (\<lambda>(c, s) (c', s'). ccap_relation c c' \<and> s' = cte_Ptr s)) (liftxf errstate lookupCapAndSlot_ret_C.status_C (\<lambda>x. (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) ret__struct_lookupCapAndSlot_ret_C_') (?QE519 cPtr (tcb_ptr_to_ctcb_ptr thread) err) (?G'1238 err rv' lu_ret___struct_lookupSlot_raw_ret_C ret___struct_lookupCapAndSlot_ret_C ret__struct_cap_C) [SKIP] (throwError err) (return_C ret__struct_lookupCapAndSlot_ret_C_'_update (\<lambda>a. lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. ret__struct_cap_C) (lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') ret___struct_lookupCapAndSlot_ret_C))))
 2. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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'933 cPtr (tcb_ptr_to_ctcb_ptr thread) err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_' {},UNIV
 3. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>?QE519 cPtra threada\<rbrace>
 4. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. v) (lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s)))\<rparr> \<in> ?G'1239 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t) s v}}}}} \<inter> ?R'933 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))}
flex-flex pairs:
?G'1239 cPtr (tcb_ptr_to_ctcb_ptr thread) \<equiv>\<^sup>? \<lambda>err rv' lu_ret___struct_lookupSlot_raw_ret_C s. ?G'1238 err rv' lu_ret___struct_lookupSlot_raw_ret_C (ret___struct_lookupCapAndSlot_ret_C_' s) proof (prove)
goal (3 subgoals):
 1. \<And>cPtra threada err rv' lu_ret___struct_lookupSlot_raw_ret_C. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; 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'933 cPtr (tcb_ptr_to_ctcb_ptr thread) err rv' lu_ret___struct_lookupSlot_raw_ret_C) \<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C rv') \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
\<acute>ret___struct_lookupCapAndSlot_ret_C :== lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. \<acute>ret__struct_cap_C) \<acute>ret___struct_lookupCapAndSlot_ret_C;;
return_C ret__struct_lookupCapAndSlot_ret_C_'_update ret___struct_lookupCapAndSlot_ret_C_' {},UNIV
 2. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. v) (lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s)))\<rparr> \<in> {sa. lookupCapAndSlot_ret_C.status_C (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. v) (lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s)))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupCapAndSlot_ret_C.status_C (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. v) (lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s))))) (errstate sa)}}}}}} \<inter> ?R'933 cPtra threada err (ret__struct_lookupSlot_raw_ret_C_' t) (errstate t)))} proof (prove)
goal (2 subgoals):
 1. \<And>cPtra threada. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<lbrace>?R519 cPtra threada\<rbrace> lookupSlotForThread thread cPtr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr a))\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and tcb_at' thread and ?R519 cPtra threada) s \<and> s' \<in> {s. capptr_'_update (\<lambda>_. cPtra) (thread_'_update (\<lambda>_. threada) s) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cPtr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. lookupSlot_raw_ret_C.slot_C (ret__struct_lookupSlot_raw_ret_C_' t)) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ret___struct_lookupCapAndSlot_ret_C_' s))\<rparr> \<in> UNIV \<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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_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_lookupCapAndSlot_ret_C_' := lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. v) (lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s)))\<rparr> \<in> {sa. lookupCapAndSlot_ret_C.status_C (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. v) (lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s)))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupCapAndSlot_ret_C.status_C (lookupCapAndSlot_ret_C.cap_C_update (\<lambda>_. v) (lookupCapAndSlot_ret_C.slot_C_update (\<lambda>_. NULL) (lookupCapAndSlot_ret_C.status_C_update (\<lambda>_. lookupSlot_raw_ret_C.status_C (ret__struct_lookupSlot_raw_ret_C_' t)) (ret___struct_lookupCapAndSlot_ret_C_' s))))) (errstate sa)}}}}}} \<inter> \<lbrace>True\<rbrace>))} proof (prove)
goal (1 subgoal):
 1. \<And>cPtra threada s s'. \<lbrakk>cPtra = cPtr; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; invs' s \<and> tcb_at' thread s\<rbrakk> \<Longrightarrow> valid_objs' s \<and> (\<forall>t. 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>)))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; tcb_at' thread s\<rbrakk> \<Longrightarrow> valid_objs' s \<and> (\<forall>t. 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>)))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; tcb_at' thread s\<rbrakk> \<Longrightarrow> \<forall>t. 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>))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' t err v. \<lbrakk>(s, s') \<in> rf_sr; invs' s; tcb_at' thread 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); 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!