theory CSpace1_R

lemma lookupSlotForThread_corres:
  "corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref))
        (valid_objs and pspace_aligned and tcb_at t)
        (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t)
        (lookup_slot_for_thread t (to_bl cptr))
        (lookupSlotForThread t cptr)" apply (unfold lookup_slot_for_thread_def lookupSlotForThread_def) apply (simp add: returnOk_bindE const_def) apply (simp add: getThreadCSpaceRoot) apply (fold returnOk_liftE) apply (simp add: returnOk_bindE) apply (rule corres_initial_splitE) apply (subst corres_liftE_rel_sum) apply (rule corres_guard_imp) apply (rule getSlotCap_tcb_corres) apply simp apply simp apply (subst bindE_returnOk[symmetric]) apply (rule corres_initial_splitE) apply (rule rab_corres') apply simp apply (simp add: word_size) apply simp apply (clarsimp simp: word_size) prefer 4 apply wp apply clarsimp apply (erule (1) objs_valid_tcb_ctable) prefer 4 apply wp apply clarsimp apply simp prefer 2 apply (rule hoare_vcg_precond_impE) apply (rule resolve_address_bits_cte_at [unfolded validE_R_def]) apply clarsimp prefer 2 apply (rule hoare_vcg_precond_impE) apply (rule resolveAddressBits_cte_at') apply (simp add: invs'_def valid_state'_def valid_pspace'_def) apply (simp add: returnOk_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (lookup_slot_for_thread t (to_bl cptr)) (lookupSlotForThread t cptr) proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (doE tcb <- liftE $ gets_the $ get_tcb t;
resolve_address_bits (tcb_ctable tcb, to_bl cptr)
odE) (doE threadRootSlot <- withoutFailure $ getThreadCSpaceRoot t;
threadRoot <- withoutFailure $ getSlotCap threadRootSlot;
bits <- returnOk (finiteBitSize $ fromCPtr cptr);
(s, uu_) <- CSpaceDecls_H.resolveAddressBits threadRoot cptr bits;
returnOk s
odE) proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (doE tcb <- liftE (gets_the (get_tcb t));
resolve_address_bits (tcb_ctable tcb, to_bl cptr)
odE) (doE threadRootSlot <- liftE (getThreadCSpaceRoot t);
threadRoot <- liftE (getSlotCap threadRootSlot);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot cptr (size cptr);
returnOk s
odE) proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (doE tcb <- liftE (gets_the (get_tcb t));
resolve_address_bits (tcb_ctable tcb, to_bl cptr)
odE) (doE threadRootSlot <- liftE (return t);
threadRoot <- liftE (getSlotCap threadRootSlot);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot cptr (size cptr);
returnOk s
odE) proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (doE tcb <- liftE (gets_the (get_tcb t));
resolve_address_bits (tcb_ctable tcb, to_bl cptr)
odE) (doE threadRootSlot <- returnOk t;
threadRoot <- liftE (getSlotCap threadRootSlot);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot cptr (size cptr);
returnOk s
odE) proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (doE tcb <- liftE (gets_the (get_tcb t));
resolve_address_bits (tcb_ctable tcb, to_bl cptr)
odE) (doE threadRoot <- liftE (getSlotCap t);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot cptr (size cptr);
returnOk s
odE) proof (prove)
goal (4 subgoals):
 1. corres (lfr \<oplus> ?r'1) (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (liftE (gets_the (get_tcb t))) (liftE (getSlotCap t))
 2. \<And>rv rv'. ?r'1 rv rv' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (?Q1 rv) (?Q'1 rv') (resolve_address_bits (tcb_ctable rv, to_bl cptr)) (doE (s, uu_) <- CSpace_H.resolveAddressBits rv' cptr (size cptr);
returnOk s
odE)
 3. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>?Q1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>?Q'1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. corres ?r'1 (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (gets_the (get_tcb t)) (getSlotCap t)
 2. \<And>rv rv'. ?r'1 rv rv' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (?Q1 rv) (?Q'1 rv') (resolve_address_bits (tcb_ctable rv, to_bl cptr)) (doE (s, uu_) <- CSpace_H.resolveAddressBits rv' cptr (size cptr);
returnOk s
odE)
 3. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>?Q1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>?Q'1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. corres ?r'1 ?Q9 ?Q'9 (gets_the (get_tcb t)) (getSlotCap t)
 2. \<And>s. (valid_objs and pspace_aligned and tcb_at t) s \<Longrightarrow> ?Q9 s
 3. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<Longrightarrow> ?Q'9 s
 4. \<And>rv rv'. ?r'1 rv rv' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (?Q1 rv) (?Q'1 rv') (resolve_address_bits (tcb_ctable rv, to_bl cptr)) (doE (s, uu_) <- CSpace_H.resolveAddressBits rv' cptr (size cptr);
returnOk s
odE)
 5. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>?Q1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 6. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>?Q'1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s. (valid_objs and pspace_aligned and tcb_at t) s \<Longrightarrow> (tcb_at t and valid_objs and pspace_aligned) s
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<Longrightarrow> (pspace_distinct' and pspace_aligned') s
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (?Q1 rv) (?Q'1 rv') (resolve_address_bits (tcb_ctable rv, to_bl cptr)) (doE (s, uu_) <- CSpace_H.resolveAddressBits rv' cptr (size cptr);
returnOk s
odE)
 4. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>?Q1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>?Q'1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<Longrightarrow> (pspace_distinct' and pspace_aligned') s
 2. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (?Q1 rv) (?Q'1 rv') (resolve_address_bits (tcb_ctable rv, to_bl cptr)) (doE (s, uu_) <- CSpace_H.resolveAddressBits rv' cptr (size cptr);
returnOk s
odE)
 3. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>?Q1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>?Q'1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (?Q1 rv) (?Q'1 rv') (resolve_address_bits (tcb_ctable rv, to_bl cptr)) (doE (s, uu_) <- CSpace_H.resolveAddressBits rv' cptr (size cptr);
returnOk s
odE)
 2. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>?Q1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>?Q'1\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cref, bits) cref'. cref' = cte_map cref)) (?Q16 rv rv) (?Q'17 rv' rv') (resolve_address_bits (tcb_ctable rv, to_bl cptr) >>=E returnOk) (doE (s, uu_) <- CSpace_H.resolveAddressBits rv' cptr (size cptr);
returnOk s
odE)
 2. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>\<lambda>rv. ?Q16 rv rv\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. ?Q'17 rv' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> corres (lfr \<oplus> ?r'19 rv rv') (?Q16 rv rv) (?Q'17 rv' rv') (resolve_address_bits (tcb_ctable rv, to_bl cptr)) (CSpace_H.resolveAddressBits rv' cptr (size cptr))
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; ?r'19 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>?Q16 rv rv\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>?Q'17 rv' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>\<lambda>rv. ?Q16 rv rv\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 6. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. ?Q'17 rv' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> cap_relation (fst (tcb_ctable rv, to_bl cptr)) rv'
 2. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> drop (32 - size cptr) (to_bl cptr) = snd (tcb_ctable rv, to_bl cptr)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> size cptr = length (snd (tcb_ctable rv, to_bl cptr))
 4. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 5. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 6. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 7. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 8. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> drop (32 - size cptr) (to_bl cptr) = snd (tcb_ctable rv, to_bl cptr)
 2. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> size cptr = length (snd (tcb_ctable rv, to_bl cptr))
 3. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 6. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 7. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> size cptr = length (snd (tcb_ctable rv, to_bl cptr))
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 6. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> size cptr = 32
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 6. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 2. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrace>valid_objs and pspace_aligned and tcb_at t\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s. (valid_objs and pspace_aligned and tcb_at t) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable (the (get_tcb t s)), to_bl cptr))) s
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s y. \<lbrakk>valid_objs s; pspace_aligned s; tcb_at t s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable y
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 2. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\<rbrace> liftE (getSlotCap t) \<lbrace>\<lambda>rv'. valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<Longrightarrow> (valid_objs' and pspace_distinct' and pspace_aligned') s \<and> valid_objs' s
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 2. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 2. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>?Q59 rv rv'\<rbrace> resolve_address_bits (tcb_ctable rv, to_bl cptr) \<lbrace>?Q19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 2. \<And>rv rv' s. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))) s\<rbrakk> \<Longrightarrow> ?Q59 rv rv' s
 3. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (?Q19 rv rv' rva) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 4. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' s. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (tcb_ctable rv, to_bl cptr))) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (fst (tcb_ctable rv, to_bl cptr))) s
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (cte_wp_at (\<lambda>_. True) (fst rva)) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 3. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (cte_wp_at (\<lambda>_. True) (fst rva)) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s)
 2. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (cte_wp_at (\<lambda>_. True) (fst rva)) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. cap_relation (tcb_ctable rv) rv' \<Longrightarrow> \<lbrace>?Q63 rv rv'\<rbrace> CSpace_H.resolveAddressBits rv' cptr (size cptr) \<lbrace>?Q'19 rv rv'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 2. \<And>rv rv' s. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv') s\<rbrakk> \<Longrightarrow> ?Q63 rv rv' s
 3. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (cte_wp_at (\<lambda>_. True) (fst rva)) (?Q'19 rv rv' rv'a) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s) proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' s. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' rv') s\<rbrakk> \<Longrightarrow> (valid_objs' and valid_cap' rv') s
 2. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (cte_wp_at (\<lambda>_. True) (fst rva)) (cte_wp_at' (\<lambda>_. True) (fst rv'a)) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' rva rv'a. \<lbrakk>cap_relation (tcb_ctable rv) rv'; (case rva of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits') rv'a\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref)) (cte_wp_at (\<lambda>_. True) (fst rva)) (cte_wp_at' (\<lambda>_. True) (fst rv'a)) (returnOk rva) (case rv'a of (s, uu_) \<Rightarrow> returnOk s) proof (prove)
goal:
No subgoals!