theory Syscall_S

lemma bisim_rab:
  "bisim (dc \<oplus> (=)) \<top> (\<lambda>s. separate_cnode_cap (caps_of_state s) cap \<and> valid_cap cap s)
                       (doE
                            _ \<leftarrow> whenE (length cref < word_bits) (throwError undefined);
                            case cap of
                                 CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then
                                                             returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref)
                                                          else
                                                             (throwError undefined)
                                | _ \<Rightarrow> throwError undefined
                        odE)
                      (resolve_address_bits (cap, cref))" using resolve_address_bits'.simps[simp] unfolding resolve_address_bits_def apply (cases "length cref < word_bits") apply (auto intro!: bisim_underlyingI
               elim!: separate_cnode_capE
               simp: whenE_def in_monad Bex_def in_bindE word_bits_def in_get_cap_cte_wp_at cte_wp_at_caps_of_state
               simp del: add_is_0 split: if_split_asm)[1] apply simp apply (rule bisim_underlyingI) apply (clarsimp ) apply (erule separate_cnode_capE) apply (fastforce simp: word_bits_def in_monad ) apply (case_tac "\<not> guard \<le> cref") apply (clarsimp simp: in_monad Bex_def) apply (drule (2) valid_sep_cap_not_cnode [where cref = cref]) apply simp apply (fastforce simp: in_monad Bex_def in_bindE word_bits_def in_get_cap_cte_wp_at cte_wp_at_caps_of_state whenE_def
               simp del: add_is_0 split: if_split_asm) apply clarsimp apply (erule separate_cnode_capE) apply (fastforce simp: word_bits_def in_monad) apply (drule (2) valid_sep_cap_not_cnode [where cref = cref]) apply simp apply (fastforce simp: in_monad Bex_def in_bindE word_bits_def in_get_cap_cte_wp_at cte_wp_at_caps_of_state whenE_def
              simp del: add_is_0 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>s. separate_cnode_cap (caps_of_state s) cap \<and> s \<turnstile> cap) (doE _ <- whenE (length cref < word_bits) (throwError undefined);
case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined
odE) (resolve_address_bits (cap, cref)) proof (prove)
using this:
resolve_address_bits' ?z (?cap, ?cref) = (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)

goal (1 subgoal):
 1. bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>s. separate_cnode_cap (caps_of_state s) cap \<and> s \<turnstile> cap) (doE _ <- whenE (length cref < word_bits) (throwError undefined);
case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined
odE) (resolve_address_bits (cap, cref)) proof (prove)
using this:
resolve_address_bits' ?z (?cap, ?cref) = (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)

goal (1 subgoal):
 1. bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>s. separate_cnode_cap (caps_of_state s) cap \<and> s \<turnstile> cap) (doE _ <- whenE (length cref < word_bits) (throwError undefined);
case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined
odE) (resolve_address_bits' TYPE('a) (cap, cref)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>z cap cref. resolve_address_bits' z (cap, cref) = (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); length cref < word_bits\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>s. separate_cnode_cap (caps_of_state s) cap \<and> s \<turnstile> cap) (doE _ <- whenE (length cref < word_bits) (throwError undefined);
case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined
odE) (resolve_address_bits' TYPE('a) (cap, cref))
 2. \<lbrakk>\<And>z cap cref. resolve_address_bits' z (cap, cref) = (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); \<not> length cref < word_bits\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>s. separate_cnode_cap (caps_of_state s) cap \<and> s \<turnstile> cap) (doE _ <- whenE (length cref < word_bits) (throwError undefined);
case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined
odE) (resolve_address_bits' TYPE('a) (cap, cref)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>z cap cref. resolve_address_bits' z (cap, cref) = (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); \<not> length cref < word_bits\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>s. separate_cnode_cap (caps_of_state s) cap \<and> s \<turnstile> cap) (doE _ <- whenE (length cref < word_bits) (throwError undefined);
case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined
odE) (resolve_address_bits' TYPE('a) (cap, cref)) proof (prove)
goal (1 subgoal):
 1. \<not> length cref < word_bits \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>s. separate_cnode_cap (caps_of_state s) cap \<and> s \<turnstile> cap) (case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) (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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s)\<rbrakk> \<Longrightarrow> \<exists>(r', t')\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). (dc \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s s' r' t'. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); separate_cnode_cap (caps_of_state s') cap; s' \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>x\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). case x of (r', t') \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s s' r' t'. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (3 subgoals):
 1. \<And>s' r t. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); s' \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> \<exists>x\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). case x of (r', t') \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s' r t p bits guard. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); s' \<turnstile> cap; cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'\<rbrakk> \<Longrightarrow> \<exists>x\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). case x of (r', t') \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 3. \<And>s s' r' t'. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t p bits guard. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); s' \<turnstile> cap; cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'\<rbrakk> \<Longrightarrow> \<exists>x\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). case x of (r', t') \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s s' r' t'. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (3 subgoals):
 1. \<And>s' r t p bits guard. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); s' \<turnstile> cap; cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'; \<not> guard \<le> cref\<rbrakk> \<Longrightarrow> \<exists>x\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). case x of (r', t') \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s' r t p bits guard. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); s' \<turnstile> cap; cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'; \<not> \<not> guard \<le> cref\<rbrakk> \<Longrightarrow> \<exists>x\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). case x of (r', t') \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 3. \<And>s s' r' t'. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t p bits guard. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); s' \<turnstile> cap; cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'; \<not> \<not> guard \<le> cref\<rbrakk> \<Longrightarrow> \<exists>x\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). case x of (r', t') \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s s' r' t'. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (3 subgoals):
 1. \<And>s' r t p bits guard. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'; \<not> \<not> guard \<le> cref\<rbrakk> \<Longrightarrow> bits \<le> length cref - length guard
 2. \<And>s' r t p bits guard. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'; \<not> \<not> guard \<le> cref; \<exists>cap'. caps_of_state s' (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap'\<rbrakk> \<Longrightarrow> \<exists>x\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). case x of (r', t') \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 3. \<And>s s' r' t'. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t p bits guard. \<lbrakk>\<not> length cref < word_bits; (r, t) \<in> fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'); cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'; \<not> \<not> guard \<le> cref; \<exists>cap'. caps_of_state s' (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap'\<rbrakk> \<Longrightarrow> \<exists>x\<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'). case x of (r', t') \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s s' r' t'. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>\<not> length cref < word_bits; s = s'; True; separate_cnode_cap (caps_of_state s') cap \<and> s' \<turnstile> cap; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t'. \<lbrakk>\<not> length cref < word_bits; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'); separate_cnode_cap (caps_of_state s') cap; s' \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'). case x of (r, t) \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r' t'. \<lbrakk>\<not> length cref < word_bits; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'); s' \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'). case x of (r, t) \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s' r' t' p bits guard. \<lbrakk>\<not> length cref < word_bits; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'); s' \<turnstile> cap; cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'). case x of (r, t) \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' p bits guard. \<lbrakk>\<not> length cref < word_bits; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'); s' \<turnstile> cap; cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'). case x of (r, t) \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r' t' p bits guard. \<lbrakk>\<not> length cref < word_bits; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'); cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'\<rbrakk> \<Longrightarrow> bits \<le> length cref - length guard
 2. \<And>s' r' t' p bits guard. \<lbrakk>\<not> length cref < word_bits; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'); cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'; \<exists>cap'. caps_of_state s' (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'). case x of (r, t) \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' p bits guard. \<lbrakk>\<not> length cref < word_bits; (r', t') \<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' TYPE('a) (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s'); cap = CNodeCap p bits guard; bits + length guard = word_bits; \<forall>off cap'. caps_of_state s' (p, off) = Some cap' \<longrightarrow> separate_cap cap'; \<exists>cap'. caps_of_state s' (p, take bits (drop (length guard) cref)) = Some cap' \<and> \<not> is_cnode_cap cap'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case cap of CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) else throwError undefined | _ \<Rightarrow> throwError undefined) s'). case x of (r, t) \<Rightarrow> (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal:
No subgoals!