theory CSpace_RAB_C

lemma lookupSlotForThread_ccorres':
  "ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) lookupSlot_raw_xf
  (valid_pspace' and tcb_at' thread)
  ({s. capptr_' s = cptr} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) []
  (lookupSlotForThread thread cptr) (Call lookupSlot_'proc)" apply (cinit lift: capptr_' thread_'
           simp add: getThreadCSpaceRoot_def locateSlot_conv
                     returnOk_liftE[symmetric] split_def) apply (ctac pre: ccorres_liftE_Seq) apply (ctac (no_vcg) add: resolveAddressBits_ccorres) apply csymbr+ apply (ctac add: ccorres_return_CE) apply csymbr+ apply (ctac add: ccorres_return_C_errorE) apply wp+ apply vcg apply (rule conjI) apply (clarsimp simp: conj_comms word_size tcbSlots Kernel_C.tcbCTable_def) apply (rule conjI, fastforce) apply (erule tcb_at_cte_at') apply (clarsimp simp add: Collect_const_mem errstate_def tcbSlots
                            Kernel_C.tcbCTable_def word_size lookupSlot_raw_rel_def
                            word_sle_def
                 split del: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (valid_pspace' and tcb_at' thread) (\<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) [] (lookupSlotForThread thread cptr) (Call lookupSlot_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (?Q620 threada capptr) (?Q'620 threada capptr) [SKIP] (doE threadRoot <- liftE (getSlotCap (thread + 2 ^ cte_level_bits * tcbCTableSlot));
p <- CSpace_H.resolveAddressBits threadRoot cptr (size cptr);
returnOk (fst p)
odE) (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val threada && 0xFFFFFE00)) (sint Kernel_C.tcbCTable) False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))} (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val threada && 0xFFFFFE00)) (sint Kernel_C.tcbCTable) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])))));;
(\<acute>res_ret :== CALL resolveAddressBits_'proc(\<acute>threadRoot,capptr,SCAST(32 signed \<rightarrow> 32) (1 << unat 5));;
(\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<acute>res_ret) \<acute>ret___struct_lookupSlot_raw_ret_C;;
(\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<acute>res_ret) \<acute>ret___struct_lookupSlot_raw_ret_C;;
return_C ret__struct_lookupSlot_raw_ret_C_'_update ret___struct_lookupSlot_raw_ret_C_'))))
 2. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q620 threada capptr s \<and> s' \<in> ?Q'620 threada capptr proof (prove)
goal (4 subgoals):
 1. \<And>threada capptr rv threadRoot. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (?Q632 threada capptr rv) (?Q'632 threada capptr rv threadRoot) [SKIP] (doE p <- CSpace_H.resolveAddressBits rv cptr (size cptr);
returnOk (fst p)
odE) (\<acute>res_ret :== CALL resolveAddressBits_'proc(threadRoot,capptr,SCAST(32 signed \<rightarrow> 32) (1 << unat 5));;
(\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<acute>res_ret) \<acute>ret___struct_lookupSlot_raw_ret_C;;
(\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<acute>res_ret) \<acute>ret___struct_lookupSlot_raw_ret_C;;
return_C ret__struct_lookupSlot_raw_ret_C_'_update ret___struct_lookupSlot_raw_ret_C_')))
 2. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<lbrace>?R632 threada capptr\<rbrace> getSlotCap (thread + 2 ^ cte_level_bits * tcbCTableSlot) \<lbrace>?Q632 threada capptr\<rbrace>
 3. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'632 threada capptr) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> ?Q'632 threada capptr rv (threadRoot_' s)}
 4. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R632 threada capptr and tcb_at' (ctcb_ptr_to_tcb_ptr threada) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))))) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s \<and> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> ?R'632 threada capptr \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>threada capptr rv threadRoot rva res_ret. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot; (case rva of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C res_ret, bitsRemaining_C res_ret); resolveAddressBits_ret_C.status_C res_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (?Q726 threada capptr rv threadRoot rva) (?Q'726 threada capptr rv threadRoot rva res_ret) [SKIP] (returnOk (fst rva)) (\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C res_ret) \<acute>ret___struct_lookupSlot_raw_ret_C;;
(\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C res_ret) \<acute>ret___struct_lookupSlot_raw_ret_C;;
return_C ret__struct_lookupSlot_raw_ret_C_'_update ret___struct_lookupSlot_raw_ret_C_'))
 2. \<And>threada capptr rv threadRoot err rv' res_ret. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot; resolveAddressBits_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (resolveAddressBits_ret_C.status_C rv') res_ret\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (?QE726 threada capptr rv threadRoot err) (?Q''726 threada capptr rv threadRoot err rv' res_ret) [SKIP] (throwError err) (\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C rv') \<acute>ret___struct_lookupSlot_raw_ret_C;;
(\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C rv') \<acute>ret___struct_lookupSlot_raw_ret_C;;
return_C ret__struct_lookupSlot_raw_ret_C_'_update ret___struct_lookupSlot_raw_ret_C_'))
 3. \<And>threada capptr rv threadRoot. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot\<rbrakk> \<Longrightarrow> \<lbrace>?R728 threada capptr rv\<rbrace> CSpace_H.resolveAddressBits rv cptr (size cptr) \<lbrace>?Q726 threada capptr rv threadRoot\<rbrace>, \<lbrace>?QE726 threada capptr rv threadRoot\<rbrace>
 4. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<lbrace>?R632 threada capptr\<rbrace> getSlotCap (thread + 2 ^ cte_level_bits * tcbCTableSlot) \<lbrace>\<lambda>rv. valid_pspace' and valid_cap' rv and K (size cptr \<le> 32) and ?R728 threada capptr rv\<rbrace>
 5. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'632 threada capptr) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. n_bits_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) (capptr_'_update (\<lambda>_. capptr) (nodeCap_'_update (\<lambda>_. threadRoot_' s) sa)) \<in> \<lbrace>ccap_relation rv \<acute>nodeCap\<rbrace> \<inter> \<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>unat \<acute>n_bits = size cptr\<rbrace>} \<inter> {sa. \<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. (case rva of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (sa\<lparr>globals := globals t\<rparr>) \<in> ?Q'726 threada capptr rv (threadRoot_' s) rva (ret__struct_resolveAddressBits_ret_C_' t))) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (sa\<lparr>globals := globals t\<rparr>) \<in> ?Q''726 threada capptr rv (threadRoot_' s) err (ret__struct_resolveAddressBits_ret_C_' t) (errstate t)))}}
 6. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R632 threada capptr and tcb_at' (ctcb_ptr_to_tcb_ptr threada) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))))) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s \<and> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> ?R'632 threada capptr \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>threada capptr rv threadRoot rva res_ret ret___struct_lookupSlot_raw_ret_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot; (case rva of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C res_ret, bitsRemaining_C res_ret); resolveAddressBits_ret_C.status_C res_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (?Q726 threada capptr rv threadRoot rva) (?G'876 threada capptr rv threadRoot rva res_ret ret___struct_lookupSlot_raw_ret_C) [SKIP] (returnOk (fst rva)) (return_C ret__struct_lookupSlot_raw_ret_C_'_update (\<lambda>s. lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C res_ret) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C res_ret) ret___struct_lookupSlot_raw_ret_C)))
 2. \<And>threada capptr rv threadRoot err rv' res_ret. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot; resolveAddressBits_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (resolveAddressBits_ret_C.status_C rv') res_ret\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (?QE726 threada capptr rv threadRoot err) (?Q''726 threada capptr rv threadRoot err rv' res_ret) [SKIP] (throwError err) (\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C rv') \<acute>ret___struct_lookupSlot_raw_ret_C;;
(\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C rv') \<acute>ret___struct_lookupSlot_raw_ret_C;;
return_C ret__struct_lookupSlot_raw_ret_C_'_update ret___struct_lookupSlot_raw_ret_C_'))
 3. \<And>threada capptr rv threadRoot. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot\<rbrakk> \<Longrightarrow> \<lbrace>?R728 threada capptr rv\<rbrace> CSpace_H.resolveAddressBits rv cptr (size cptr) \<lbrace>?Q726 threada capptr rv threadRoot\<rbrace>, \<lbrace>?QE726 threada capptr rv threadRoot\<rbrace>
 4. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<lbrace>?R632 threada capptr\<rbrace> getSlotCap (thread + 2 ^ cte_level_bits * tcbCTableSlot) \<lbrace>\<lambda>rv. valid_pspace' and valid_cap' rv and K (size cptr \<le> 32) and ?R728 threada capptr rv\<rbrace>
 5. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'632 threada capptr) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. n_bits_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) (capptr_'_update (\<lambda>_. capptr) (nodeCap_'_update (\<lambda>_. threadRoot_' s) sa)) \<in> \<lbrace>ccap_relation rv \<acute>nodeCap\<rbrace> \<inter> \<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>unat \<acute>n_bits = size cptr\<rbrace>} \<inter> {sa. \<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. (case rva of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (sa\<lparr>globals := globals t\<rparr>) \<in> {sa. sa \<in> {sb. sb\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' sa)\<rparr> \<in> {sb. sb\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' sa))\<rparr> \<in> ?G'876 threada capptr rv (threadRoot_' s) rva (ret__struct_resolveAddressBits_ret_C_' t) (ret___struct_lookupSlot_raw_ret_C_' sa)}}})) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (sa\<lparr>globals := globals t\<rparr>) \<in> ?Q''726 threada capptr rv (threadRoot_' s) err (ret__struct_resolveAddressBits_ret_C_' t) (errstate t)))}}
 6. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R632 threada capptr and tcb_at' (ctcb_ptr_to_tcb_ptr threada) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))))) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s \<and> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> ?R'632 threada capptr \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>threada capptr rv threadRoot err rv' res_ret. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot; resolveAddressBits_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (resolveAddressBits_ret_C.status_C rv') res_ret\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (?QE726 threada capptr rv threadRoot err) (?Q''726 threada capptr rv threadRoot err rv' res_ret) [SKIP] (throwError err) (\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C rv') \<acute>ret___struct_lookupSlot_raw_ret_C;;
(\<acute>ret___struct_lookupSlot_raw_ret_C :== lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C rv') \<acute>ret___struct_lookupSlot_raw_ret_C;;
return_C ret__struct_lookupSlot_raw_ret_C_'_update ret___struct_lookupSlot_raw_ret_C_'))
 2. \<And>threada capptr rv threadRoot. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot\<rbrakk> \<Longrightarrow> \<lbrace>?R728 threada capptr rv\<rbrace> CSpace_H.resolveAddressBits rv cptr (size cptr) \<lbrace>\<lambda>rva _. True\<rbrace>, \<lbrace>?QE726 threada capptr rv threadRoot\<rbrace>
 3. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<lbrace>?R632 threada capptr\<rbrace> getSlotCap (thread + 2 ^ cte_level_bits * tcbCTableSlot) \<lbrace>\<lambda>rv. valid_pspace' and valid_cap' rv and K (size cptr \<le> 32) and ?R728 threada capptr rv\<rbrace>
 4. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'632 threada capptr) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. n_bits_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) (capptr_'_update (\<lambda>_. capptr) (nodeCap_'_update (\<lambda>_. threadRoot_' s) sa)) \<in> \<lbrace>ccap_relation rv \<acute>nodeCap\<rbrace> \<inter> \<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>unat \<acute>n_bits = size cptr\<rbrace>} \<inter> {sa. \<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (sa\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr> \<in> \<lbrace>lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) \<^bsup>s\<^esup>ret___struct_lookupSlot_raw_ret_C)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookupSlot_raw_rel (fst rv) (lookupSlot_raw_ret_C.slot_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) \<^bsup>s\<^esup>ret___struct_lookupSlot_raw_ret_C)))\<rbrace>}}})) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (sa\<lparr>globals := globals t\<rparr>) \<in> ?Q''726 threada capptr rv (threadRoot_' s) err (ret__struct_resolveAddressBits_ret_C_' t) (errstate t)))}}
 5. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R632 threada capptr and tcb_at' (ctcb_ptr_to_tcb_ptr threada) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))))) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s \<and> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> ?R'632 threada capptr \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>threada capptr rv threadRoot err rv' res_ret ret___struct_lookupSlot_raw_ret_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot; resolveAddressBits_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err (resolveAddressBits_ret_C.status_C rv') res_ret\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (?QE726 threada capptr rv threadRoot err) (?G'991 threada capptr rv threadRoot err rv' res_ret ret___struct_lookupSlot_raw_ret_C) [SKIP] (throwError err) (return_C ret__struct_lookupSlot_raw_ret_C_'_update (\<lambda>s. lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C rv') (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C rv') ret___struct_lookupSlot_raw_ret_C)))
 2. \<And>threada capptr rv threadRoot. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot\<rbrakk> \<Longrightarrow> \<lbrace>?R728 threada capptr rv\<rbrace> CSpace_H.resolveAddressBits rv cptr (size cptr) \<lbrace>\<lambda>rva _. True\<rbrace>, \<lbrace>?QE726 threada capptr rv threadRoot\<rbrace>
 3. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<lbrace>?R632 threada capptr\<rbrace> getSlotCap (thread + 2 ^ cte_level_bits * tcbCTableSlot) \<lbrace>\<lambda>rv. valid_pspace' and valid_cap' rv and K (size cptr \<le> 32) and ?R728 threada capptr rv\<rbrace>
 4. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'632 threada capptr) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. n_bits_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) (capptr_'_update (\<lambda>_. capptr) (nodeCap_'_update (\<lambda>_. threadRoot_' s) sa)) \<in> \<lbrace>ccap_relation rv \<acute>nodeCap\<rbrace> \<inter> \<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>unat \<acute>n_bits = size cptr\<rbrace>} \<inter> {sa. \<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (sa\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr> \<in> \<lbrace>lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) \<^bsup>s\<^esup>ret___struct_lookupSlot_raw_ret_C)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookupSlot_raw_rel (fst rv) (lookupSlot_raw_ret_C.slot_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) \<^bsup>s\<^esup>ret___struct_lookupSlot_raw_ret_C)))\<rbrace>}}})) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (sa\<lparr>globals := globals t\<rparr>) \<in> {sa. sa \<in> {sb. sb\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' sa)\<rparr> \<in> {sb. sb\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' sa))\<rparr> \<in> ?G'991 threada capptr rv (threadRoot_' s) err (ret__struct_resolveAddressBits_ret_C_' t) (errstate t) (ret___struct_lookupSlot_raw_ret_C_' sa)}}}))}}
 5. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R632 threada capptr and tcb_at' (ctcb_ptr_to_tcb_ptr threada) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))))) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s \<and> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> ?R'632 threada capptr \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>threada capptr rv threadRoot. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; ccap_relation rv threadRoot\<rbrakk> \<Longrightarrow> \<lbrace>?R728 threada capptr rv\<rbrace> CSpace_H.resolveAddressBits rv cptr (size cptr) \<lbrace>\<lambda>rva _. True\<rbrace>, \<lbrace>\<lambda>err _. True\<rbrace>
 2. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<lbrace>?R632 threada capptr\<rbrace> getSlotCap (thread + 2 ^ cte_level_bits * tcbCTableSlot) \<lbrace>\<lambda>rv. valid_pspace' and valid_cap' rv and K (size cptr \<le> 32) and ?R728 threada capptr rv\<rbrace>
 3. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'632 threada capptr) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. n_bits_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) (capptr_'_update (\<lambda>_. capptr) (nodeCap_'_update (\<lambda>_. threadRoot_' s) sa)) \<in> \<lbrace>ccap_relation rv \<acute>nodeCap\<rbrace> \<inter> \<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>unat \<acute>n_bits = size cptr\<rbrace>} \<inter> {s. \<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr> \<in> \<lbrace>lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) \<^bsup>s\<^esup>ret___struct_lookupSlot_raw_ret_C)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookupSlot_raw_rel (fst rv) (lookupSlot_raw_ret_C.slot_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) \<^bsup>s\<^esup>ret___struct_lookupSlot_raw_ret_C)))\<rbrace>}}})) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr> \<in> {sa. lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))) (errstate sa)}}}}))}}
 4. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R632 threada capptr and tcb_at' (ctcb_ptr_to_tcb_ptr threada) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))))) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s \<and> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> ?R'632 threada capptr \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>threada capptr. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'632 threada capptr) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. n_bits_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) (capptr_'_update (\<lambda>_. capptr) (nodeCap_'_update (\<lambda>_. threadRoot_' s) sa)) \<in> \<lbrace>ccap_relation rv \<acute>nodeCap\<rbrace> \<inter> \<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>unat \<acute>n_bits = size cptr\<rbrace>} \<inter> {s. \<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr> \<in> \<lbrace>lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) \<^bsup>s\<^esup>ret___struct_lookupSlot_raw_ret_C)) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookupSlot_raw_rel (fst rv) (lookupSlot_raw_ret_C.slot_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C \<^bsup>t\<^esup>ret__struct_resolveAddressBits_ret_C) \<^bsup>s\<^esup>ret___struct_lookupSlot_raw_ret_C)))\<rbrace>}}})) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> res_ret_'_update (\<lambda>_. ret__struct_resolveAddressBits_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. s \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)\<rparr> \<in> {sa. sa\<lparr>ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr> \<in> {sa. lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))) (errstate sa)}}}}))}}
 2. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. valid_pspace' s \<and> valid_objs' s \<and> K (size cptr \<le> 32) s \<and> True \<and> True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))))) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s \<and> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> ?R'632 threada capptr \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. valid_pspace' s \<and> valid_objs' s \<and> K (size cptr \<le> 32) s \<and> True \<and> True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))))) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s \<and> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> {s. \<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<longrightarrow> ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<and> capptr = cptr \<and> unat (SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) = size cptr \<and> (\<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookupSlot_raw_rel (fst rv) (lookupSlot_raw_ret_C.slot_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))))) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))) (errstate (s\<lparr>threadRoot_' := h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])), globals := globals t, res_ret_' := ret__struct_resolveAddressBits_ret_C_' t, ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr>)))))} \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. valid_pspace' s \<and> valid_objs' s \<and> K (size cptr \<le> 32) s \<and> True \<and> True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))))) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s
 2. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> {s. \<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<longrightarrow> ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<and> capptr = cptr \<and> unat (SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) = size cptr \<and> (\<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookupSlot_raw_rel (fst rv) (lookupSlot_raw_ret_C.slot_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))))) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))) (errstate (s\<lparr>threadRoot_' := h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])), globals := globals t, res_ret_' := ret__struct_resolveAddressBits_ret_C_' t, ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr>)))))} \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' thread s\<rbrakk> \<Longrightarrow> valid_objs' s \<and> cte_wp_at' (\<lambda>_. True) thread s
 2. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> {s. \<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<longrightarrow> ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<and> capptr = cptr \<and> unat (SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) = size cptr \<and> (\<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookupSlot_raw_rel (fst rv) (lookupSlot_raw_ret_C.slot_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))))) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))) (errstate (s\<lparr>threadRoot_' := h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])), globals := globals t, res_ret_' := ret__struct_resolveAddressBits_ret_C_' t, ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr>)))))} \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; tcb_at' thread s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) thread s
 2. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> {s. \<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<longrightarrow> ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<and> capptr = cptr \<and> unat (SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) = size cptr \<and> (\<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookupSlot_raw_rel (fst rv) (lookupSlot_raw_ret_C.slot_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))))) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))) (errstate (s\<lparr>threadRoot_' := h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])), globals := globals t, res_ret_' := ret__struct_resolveAddressBits_ret_C_' t, ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr>)))))} \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>threada capptr s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; capptr = cptr; (s, s') \<in> rf_sr; (valid_pspace' and tcb_at' thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> \<lbrace>cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (thread + 2 ^ cte_level_bits * tcbCTableSlot)\<rbrace> \<inter> {s. \<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<longrightarrow> ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C'']))) \<and> capptr = cptr \<and> unat (SCAST(32 signed \<rightarrow> 32) (1 << unat 5)) = size cptr \<and> (\<forall>t. (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (cte, bits) \<Rightarrow> \<lambda>(cte', bits'). cte' = cte_Ptr cte \<and> bits = unat bits' \<and> bits' \<le> 0x20) (resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t), bitsRemaining_C (ret__struct_resolveAddressBits_ret_C_' t)) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookupSlot_raw_rel (fst rv) (lookupSlot_raw_ret_C.slot_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))))) \<and> (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. lookup_failure_rel err (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (errstate t) \<longrightarrow> lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel err (lookupSlot_raw_ret_C.status_C (lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s)))) (errstate (s\<lparr>threadRoot_' := h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val threada && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCTable * word_of_nat (size_of TYPE(cte_C)))\<rightarrow>[''cap_C''])), globals := globals t, res_ret_' := ret__struct_resolveAddressBits_ret_C_' t, ret___struct_lookupSlot_raw_ret_C_' := lookupSlot_raw_ret_C.slot_C_update (\<lambda>_. resolveAddressBits_ret_C.slot_C (ret__struct_resolveAddressBits_ret_C_' t)) (lookupSlot_raw_ret_C.status_C_update (\<lambda>_. resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' t)) (ret___struct_lookupSlot_raw_ret_C_' s))\<rparr>)))))} \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>0 \<le> sint Kernel_C.tcbCTable \<and> (case False of True \<Rightarrow> sint Kernel_C.tcbCTable + 1 | False \<Rightarrow> sint Kernel_C.tcbCTable) \<le> uint tcbCNodeEntries\<rbrace> proof (prove)
goal:
No subgoals!