theory CSpace_AI

lemma resolve_address_bits_real_cte_at:
  "\<lbrace> valid_objs and valid_cap (fst args) \<rbrace>
  resolve_address_bits args
  \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, -" unfolding resolve_address_bits_def proof (induct args rule: resolve_address_bits'.induct) case (1 z cap cref) show ?case apply (clarsimp simp add: validE_R_def validE_def valid_def split: sum.split) apply (subst (asm) resolve_address_bits'.simps) apply (cases cap) defer 6  (* cnode *)
           apply (auto simp: in_monad)[11] apply (rename_tac obj_ref nat list) apply (simp only: cap.simps) apply (case_tac "nat + length list = 0") apply (simp add: fail_def) apply (simp only: if_False) apply (simp only: K_bind_def in_bindE_R) apply (elim conjE exE) apply (simp only: split: if_split_asm) apply (clarsimp simp add: in_monad) apply (clarsimp simp add: valid_cap_def) apply (simp only: K_bind_def in_bindE_R) apply (elim conjE exE) apply (simp only: split: if_split_asm) apply (frule (8) "1.hyps") apply (clarsimp simp: in_monad validE_def validE_R_def valid_def) apply (frule in_inv_by_hoareD [OF get_cap_inv]) apply simp apply (frule (1) post_by_hoare [OF get_cap_valid]) apply (erule allE, erule impE, blast) apply (clarsimp simp: in_monad split: cap.splits) apply (drule (1) bspec, simp)+ apply (clarsimp simp: in_monad) apply (frule in_inv_by_hoareD [OF get_cap_inv]) apply (clarsimp simp add: valid_cap_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap (fst args)\<rbrace> resolve_address_bits args \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap (fst args)\<rbrace> resolve_address_bits' TYPE('a) args \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, - proof (state)
goal (1 subgoal):
 1. \<And>z cap cref. (\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc. \<lbrakk>cap = CNodeCap x61 x62 x63; x62 + length x63 \<noteq> 0; (Inr v, s') \<in> fst (whenE (\<not> x63 \<le> cref) (throwError $ GuardMismatch (length cref) x63) s); (Inr rv, st) \<in> fst (whenE (length cref < x62 + length x63) (throwError $ DepthMismatch (length cref) (x62 + length x63)) s'); (Inr rva, sta) \<in> fst ((returnOk $ take x62 (drop (length x63) cref)) st); (Inr rvb, stb) \<in> fst ((returnOk $ drop (x62 + length x63) cref) sta); rvb \<noteq> []; (Inr rvc, stc) \<in> fst ((liftE $ get_cap (x61, rva)) stb); is_cnode_cap rvc\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and (\<lambda>a. a \<turnstile> fst (rvc, rvb))\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, -) \<Longrightarrow> \<lbrace>valid_objs and (\<lambda>a. a \<turnstile> fst (cap, cref))\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, - proof (state)
this:
\<lbrakk>cap = CNodeCap ?x61.0 ?x62.0 ?x63.0; ?x62.0 + length ?x63.0 \<noteq> 0; (Inr ?v, ?s') \<in> fst (whenE (\<not> ?x63.0 \<le> cref) (throwError $ GuardMismatch (length cref) ?x63.0) ?s); (Inr ?rv, ?st) \<in> fst (whenE (length cref < ?x62.0 + length ?x63.0) (throwError $ DepthMismatch (length cref) (?x62.0 + length ?x63.0)) ?s'); (Inr ?rva, ?sta) \<in> fst ((returnOk $ take ?x62.0 (drop (length ?x63.0) cref)) ?st); (Inr ?rvb, ?stb) \<in> fst ((returnOk $ drop (?x62.0 + length ?x63.0) cref) ?sta); ?rvb \<noteq> []; (Inr ?rvc, ?stc) \<in> fst ((liftE $ get_cap (?x61.0, ?rva)) ?stb); is_cnode_cap ?rvc\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and (\<lambda>a. a \<turnstile> fst (?rvc, ?rvb))\<rbrace> resolve_address_bits' z (?rvc, ?rvb) \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, -

goal (1 subgoal):
 1. \<And>z cap cref. (\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc. \<lbrakk>cap = CNodeCap x61 x62 x63; x62 + length x63 \<noteq> 0; (Inr v, s') \<in> fst (whenE (\<not> x63 \<le> cref) (throwError $ GuardMismatch (length cref) x63) s); (Inr rv, st) \<in> fst (whenE (length cref < x62 + length x63) (throwError $ DepthMismatch (length cref) (x62 + length x63)) s'); (Inr rva, sta) \<in> fst ((returnOk $ take x62 (drop (length x63) cref)) st); (Inr rvb, stb) \<in> fst ((returnOk $ drop (x62 + length x63) cref) sta); rvb \<noteq> []; (Inr rvc, stc) \<in> fst ((liftE $ get_cap (x61, rva)) stb); is_cnode_cap rvc\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and (\<lambda>a. a \<turnstile> fst (rvc, rvb))\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, -) \<Longrightarrow> \<lbrace>valid_objs and (\<lambda>a. a \<turnstile> fst (cap, cref))\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>a. a \<turnstile> fst (cap, cref))\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (cap, cref) s); valid_objs s; s \<turnstile> cap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (12 subgoals):
 1. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb x21 x22 x23 x24. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 3. \<And>s b aa ba bb x31 x32 x33. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 4. \<And>s b aa ba bb x41 x42 x43. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 5. \<And>s b aa ba bb x51 x52 x53. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 6. \<And>s b aa ba bb x61 x62 x63. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 7. \<And>s b aa ba bb x7. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 8. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = DomainCap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 9. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 10. \<And>s b aa ba bb x10. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb x21 x22 x23 x24. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 3. \<And>s b aa ba bb x31 x32 x33. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 4. \<And>s b aa ba bb x41 x42 x43. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 5. \<And>s b aa ba bb x51 x52 x53. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 6. \<And>s b aa ba bb x7. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 7. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = DomainCap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 8. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 9. \<And>s b aa ba bb x10. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 10. \<And>s b aa ba bb x111 x112 x113. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb x21 x22 x23 x24. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 3. \<And>s b aa ba bb x31 x32 x33. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 4. \<And>s b aa ba bb x41 x42 x43. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 5. \<And>s b aa ba bb x51 x52 x53. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 6. \<And>s b aa ba bb x7. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 7. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = DomainCap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 8. \<And>s b aa ba bb. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 9. \<And>s b aa ba bb x10. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 10. \<And>s b aa ba bb x111 x112 x113. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb x61 x62 x63. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); valid_objs s; s \<turnstile> cap; cap = CNodeCap obj_ref nat list\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((if nat + length list = 0 then fail else doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((if nat + length list = 0 then fail else doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list = 0\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((if nat + length list = 0 then fail else doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((if nat + length list = 0 then fail else doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list. \<lbrakk>(Inr ((aa, ba), bb), b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list. \<lbrakk>\<exists>s'' y. (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s) \<and> (\<exists>s''a y. (Inr y, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'') \<and> (\<exists>s'' offset. (Inr offset, s'') \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a) \<and> (\<exists>s''a rest. (Inr rest, s''a) \<in> fst ((returnOk $ drop (nat + length list) cref) s'') \<and> (Inr ((aa, ba), bb), b) \<in> fst ((if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''a)))); valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); (Inr ((aa, ba), bb), b) \<in> fst ((if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr [], s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest = []; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), []) s''c)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr ((aa, ba), bb), b) \<in> fst ((doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s aa nat list. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap aa nat list; cap = CNodeCap aa nat list; 0 < nat \<or> list \<noteq> []; list \<le> cref; length cref = nat + length list\<rbrakk> \<Longrightarrow> cap_table_at nat aa s
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr ((aa, ba), bb), b) \<in> fst ((doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr ((aa, ba), bb), b) \<in> fst ((doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; \<exists>s'' next_cap. (Inr next_cap, s'') \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c) \<and> (Inr ((aa, ba), bb), b) \<in> fst ((if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)) s'')\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); (Inr ((aa, ba), bb), b) \<in> fst ((if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d); \<lbrace>valid_objs and (\<lambda>a. a \<turnstile> fst (next_cap, rest))\<rbrace> resolve_address_bits' z (next_cap, rest) \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, -\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, s''d) \<in> fst (get_cap (obj_ref, take nat (drop (length list) cref)) s); is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s''d); \<forall>s. valid_objs s \<and> s \<turnstile> next_cap \<longrightarrow> (\<forall>x\<in>fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s). case x of (r, s') \<Rightarrow> \<forall>a b. (\<exists>ba. r = Inr ((a, b), ba)) \<longrightarrow> cap_table_at (length b) a s'); list \<le> cref\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, s''d) \<in> fst (get_cap (obj_ref, take nat (drop (length list) cref)) s); is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s''d); \<forall>s. valid_objs s \<and> s \<turnstile> next_cap \<longrightarrow> (\<forall>x\<in>fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s). case x of (r, s') \<Rightarrow> \<forall>a b. (\<exists>ba. r = Inr ((a, b), ba)) \<longrightarrow> cap_table_at (length b) a s'); list \<le> cref; s''d = s\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, s) \<in> fst (get_cap (obj_ref, take nat (drop (length list) cref)) s); is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s); \<forall>s. valid_objs s \<and> s \<turnstile> next_cap \<longrightarrow> (\<forall>x\<in>fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s). case x of (r, s') \<Rightarrow> \<forall>a b. (\<exists>ba. r = Inr ((a, b), ba)) \<longrightarrow> cap_table_at (length b) a s'); list \<le> cref; s''d = s\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, s) \<in> fst (get_cap (obj_ref, take nat (drop (length list) cref)) s); is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s); \<forall>s. valid_objs s \<and> s \<turnstile> next_cap \<longrightarrow> (\<forall>x\<in>fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s). case x of (r, s') \<Rightarrow> \<forall>a b. (\<exists>ba. r = Inr ((a, b), ba)) \<longrightarrow> cap_table_at (length b) a s'); list \<le> cref; s''d = s; s \<turnstile> next_cap\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, s) \<in> fst (get_cap (obj_ref, take nat (drop (length list) cref)) s); is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s); list \<le> cref; s''d = s; s \<turnstile> next_cap; \<forall>x\<in>fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s). case x of (r, s') \<Rightarrow> \<forall>a b. (\<exists>ba. r = Inr ((a, b), ba)) \<longrightarrow> cap_table_at (length b) a s'\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba bb obj_ref nat list next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, s) \<in> fst (get_cap (obj_ref, take nat (drop (length list) cref)) s); is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s); list \<le> cref; s \<turnstile> next_cap; \<forall>x\<in>fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s). case x of (r, s') \<Rightarrow> \<forall>a b. (\<exists>ba. r = Inr ((a, b), ba)) \<longrightarrow> cap_table_at (length b) a s'\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b
 2. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba bb obj_ref nat list s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap obj_ref nat list; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> cap_table_at (length ba) aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa nat list next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap aa nat list; cap = CNodeCap aa nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, b) \<in> fst (get_cap (aa, take nat (drop (length list) cref)) s); \<not> is_cnode_cap next_cap; list \<le> cref\<rbrakk> \<Longrightarrow> cap_table_at nat aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa nat list next_cap. \<lbrakk>valid_objs s; s \<turnstile> CNodeCap aa nat list; cap = CNodeCap aa nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, b) \<in> fst (get_cap (aa, take nat (drop (length list) cref)) s); \<not> is_cnode_cap next_cap; list \<le> cref; b = s\<rbrakk> \<Longrightarrow> cap_table_at nat aa b proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>valid_objs and (\<lambda>a. a \<turnstile> fst (cap, cref))\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, -

goal:
No subgoals!