theory CSpace1_R

lemma rab_corres':
  "\<lbrakk> cap_relation (fst a) c'; drop (32-bits) (to_bl cref') = snd a;
     bits = length (snd a) \<rbrakk> \<Longrightarrow>
  corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits').
                   cte' = cte_map cte \<and> length bits = bits'))
          (valid_objs and pspace_aligned and valid_cap (fst a))
          (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c')
          (resolve_address_bits a)
          (resolveAddressBits c' cref' bits)" unfolding resolve_address_bits_def proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) case (1 z cap cref) show ?case proof (cases "isCNodeCap c'") case True with "1.prems" obtain ptr guard' guard cbits where caps:
      "cap = cap.CNodeCap ptr cbits guard"
      "c' = CNodeCap ptr cbits (of_bl guard) (length guard)" apply (cases cap, simp_all add: isCap_defs) apply auto done with "1.prems" have IH: "\<And>vd vc c' f' cref' bits.
      \<lbrakk> cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref;
        vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap;
       cap_relation vd c'; bits = length vc; is_cnode_cap vd;
       drop (32 - bits) (to_bl cref') = vc \<rbrakk>
      \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits').
                   cte' = cte_map cte \<and> length bits = bits'))
    (valid_objs and pspace_aligned and (\<lambda>s. s \<turnstile> fst (vd,vc)))
    (valid_objs' and pspace_distinct' and pspace_aligned' and (\<lambda>s. s \<turnstile>' c'))
    (resolve_address_bits' z (vd, vc))
    (CSpace_H.resolveAddressBits c' cref' bits)" apply - apply (rule "1.hyps" [of _ cbits guard, OF caps(1)]) prefer 7 apply (clarsimp simp: in_monad) apply (rule get_cap_success) by (auto simp: in_monad intro!: get_cap_success)  (* takes time *)
     note if_split [split del] { assume "cbits + length guard = 0 \<or> cbits = 0 \<and> guard = []" hence ?thesis apply (simp add: caps isCap_defs
                         resolveAddressBits.simps resolve_address_bits'.simps) apply (rule corres_fail) apply (clarsimp simp: valid_cap_def) done } moreover { assume "cbits + length guard \<noteq> 0 \<and> \<not>(cbits = 0 \<and> guard = [])" hence [simp]: "((cbits + length guard = 0) = False) \<and>
                     ((cbits = 0 \<and> guard = []) = False) \<and>
                    (0 < cbits \<or> guard \<noteq> []) " by simp note drop_append[simp del] from "1.prems" have ?thesis apply - apply (subst resolveAddressBits.simps) apply (subst resolve_address_bits'.simps) apply (simp add: Let_def unlessE_whenE) apply (simp add: caps isCap_defs Let_def whenE_bindE_throwError_to_if) apply (subst cnode_cap_case_if) apply (corresKsimp search: getSlotCap_corres IH
                              wp: get_cap_wp getSlotCap_valid no_fail_stateAssert
                            simp: locateSlot_conv) apply (simp add: drop_postfix_eq) apply clarsimp apply (prop_tac "is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits") apply (erule valid_CNodeCapE; fastforce simp: cte_level_bits_def) subgoal premises prems for s s' x apply (insert prems) apply (rule context_conjI) apply (simp add: guard_mask_shift[OF \<open>to_bl _ = _\<close>, where guard=guard,symmetric]) apply (simp add: caps lookup_failure_map_def) apply (rule conjI) apply (clarsimp split: if_splits) apply (intro conjI impI allI;clarsimp?) apply (subst \<open>to_bl _ = _\<close>[symmetric]) apply (drule postfix_dropD) apply clarsimp apply (prop_tac "32 + (cbits + length guard) - length cref =
                             (cbits + length guard) + (32 - length cref)") apply (drule len_drop_lemma, simp, arith) apply simp apply (subst drop_drop [symmetric]) subgoal by simp apply (erule (2) valid_CNodeCapE) apply (rule cap_table_at_cte_at[OF _ refl]) apply (simp add: obj_at_def is_cap_table_def well_formed_cnode_n_def) apply (frule (2) cte_wp_valid_cap) apply (rule context_conjI) apply (intro conjI impI allI;clarsimp?) apply (erule (2) valid_CNodeCapE) apply (erule (3) cte_map_shift') apply simp apply (erule (1) cte_map_shift; assumption?) subgoal by simp apply (clarsimp simp: cte_level_bits_def) apply (rule conjI) apply (clarsimp simp: valid_cap_def cap_table_at_gsCNodes isCap_simps) apply (rule and_mask_less_size, simp add: word_bits_def word_size cte_level_bits_def) apply (clarsimp split: if_splits) done done } ultimately show ?thesis by fast next case False with "1.prems" show ?thesis by (cases cap)
         (auto simp: resolve_address_bits'.simps resolveAddressBits.simps
                     isCap_defs lookup_failure_map_def) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation (fst a) c'; drop (32 - bits) (to_bl cref') = snd a; bits = length (snd a)\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (fst a)) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits a) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation (fst a) c'; drop (32 - bits) (to_bl cref') = snd a; bits = length (snd a)\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (fst a)) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' TYPE(det_ext) a) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
goal (1 subgoal):
 1. \<And>z cap cref c' cref' bits. \<lbrakk>\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc c' cref' bits. \<lbrakk>cap = cap.CNodeCap x61 x62 x63; x62 + length x63 \<noteq> 0; (Inr v, s') \<in> fst (whenE (\<not> x63 \<le> cref) (throwError $ ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) x63) s); (Inr rv, st) \<in> fst (whenE (length cref < x62 + length x63) (throwError $ ExceptionTypes_A.lookup_failure.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; cap_relation (fst (rvc, rvb)) c'; drop (32 - bits) (to_bl cref') = snd (rvc, rvb); bits = length (snd (rvc, rvb))\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (fst (rvc, rvb))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (rvc, rvb)) (CSpace_H.resolveAddressBits c' cref' bits); cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref))\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
\<lbrakk>cap = 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 $ ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) ?x63.0) ?s); (Inr ?rv, ?st) \<in> fst (whenE (length cref < ?x62.0 + length ?x63.0) (throwError $ ExceptionTypes_A.lookup_failure.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; cap_relation (fst (?rvc, ?rvb)) ?c'; drop (32 - ?bits) (to_bl ?cref') = snd (?rvc, ?rvb); ?bits = length (snd (?rvc, ?rvb))\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (?rvc, ?rvb))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' ?c') (resolve_address_bits' z (?rvc, ?rvb)) (CSpace_H.resolveAddressBits ?c' ?cref' ?bits)
cap_relation (fst (cap, cref)) c'
drop (32 - bits) (to_bl cref') = snd (cap, cref)
bits = length (snd (cap, cref))

goal (1 subgoal):
 1. \<And>z cap cref c' cref' bits. \<lbrakk>\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc c' cref' bits. \<lbrakk>cap = cap.CNodeCap x61 x62 x63; x62 + length x63 \<noteq> 0; (Inr v, s') \<in> fst (whenE (\<not> x63 \<le> cref) (throwError $ ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) x63) s); (Inr rv, st) \<in> fst (whenE (length cref < x62 + length x63) (throwError $ ExceptionTypes_A.lookup_failure.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; cap_relation (fst (rvc, rvb)) c'; drop (32 - bits) (to_bl cref') = snd (rvc, rvb); bits = length (snd (rvc, rvb))\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (fst (rvc, rvb))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (rvc, rvb)) (CSpace_H.resolveAddressBits c' cref' bits); cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref))\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
isCNodeCap c'

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (chain)
picking this:
cap_relation (fst (cap, cref)) c'
drop (32 - bits) (to_bl cref') = snd (cap, cref)
bits = length (snd (cap, cref))
isCNodeCap c' proof (prove)
using this:
cap_relation (fst (cap, cref)) c'
drop (32 - bits) (to_bl cref') = snd (cap, cref)
bits = length (snd (cap, cref))
isCNodeCap c'

goal (1 subgoal):
 1. (\<And>ptr cbits guard. \<lbrakk>cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; drop (32 - length cref) (to_bl cref') = cref; case c' of capability.CNodeCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False; cap = cap.ArchObjectCap x12; bits = length cref\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
cap = cap.CNodeCap ptr cbits guard
c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (chain)
picking this:
cap_relation (fst (cap, cref)) c'
drop (32 - bits) (to_bl cref') = snd (cap, cref)
bits = length (snd (cap, cref))
cap = cap.CNodeCap ptr cbits guard
c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard) proof (prove)
using this:
cap_relation (fst (cap, cref)) c'
drop (32 - bits) (to_bl cref') = snd (cap, cref)
bits = length (snd (cap, cref))
cap = cap.CNodeCap ptr cbits guard
c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)

goal (1 subgoal):
 1. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>s. s \<turnstile> fst (vd, vc))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (vd, vc)) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
goal (1 subgoal):
 1. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>s. s \<turnstile> fst (vd, vc))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (vd, vc)) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
goal (11 subgoals):
 1. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> cbits + length guard \<noteq> 0
 2. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?v5 vd vc c' f' cref' bits), ?s'5 vd vc c' f' cref' bits) \<in> fst (whenE (\<not> guard \<le> cref) (throwError $ ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard) (?s5 vd vc c' f' cref' bits))
 3. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?rv5 vd vc c' f' cref' bits), ?st5 vd vc c' f' cref' bits) \<in> fst (whenE (length cref < cbits + length guard) (throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard)) (?s'5 vd vc c' f' cref' bits))
 4. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?rva5 vd vc c' f' cref' bits), ?sta5 vd vc c' f' cref' bits) \<in> fst ((returnOk $ take cbits (drop (length guard) cref)) (?st5 vd vc c' f' cref' bits))
 5. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr vc, ?stb5 vd vc c' f' cref' bits) \<in> fst ((returnOk $ drop (cbits + length guard) cref) (?sta5 vd vc c' f' cref' bits))
 6. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> vc \<noteq> []
 7. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr vd, ?stc5 vd vc c' f' cref' bits) \<in> fst ((liftE $ get_cap (ptr, ?rva5 vd vc c' f' cref' bits)) (?stb5 vd vc c' f' cref' bits))
 8. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> is_cnode_cap vd
 9. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> cap_relation (fst (vd, vc)) c'
 10. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> drop (32 - bits) (to_bl cref') = snd (vd, vc)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr vd, ?stc5 vd vc c' f' cref' bits) \<in> fst ((liftE $ get_cap (ptr, ?rva5 vd vc c' f' cref' bits)) (?stb5 vd vc c' f' cref' bits))
 2. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> cbits + length guard \<noteq> 0
 3. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?v5 vd vc c' f' cref' bits), ?s'5 vd vc c' f' cref' bits) \<in> fst (whenE (\<not> guard \<le> cref) (throwError $ ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard) (?s5 vd vc c' f' cref' bits))
 4. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?rv5 vd vc c' f' cref' bits), ?st5 vd vc c' f' cref' bits) \<in> fst (whenE (length cref < cbits + length guard) (throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard)) (?s'5 vd vc c' f' cref' bits))
 5. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?rva5 vd vc c' f' cref' bits), ?sta5 vd vc c' f' cref' bits) \<in> fst ((returnOk $ take cbits (drop (length guard) cref)) (?st5 vd vc c' f' cref' bits))
 6. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr vc, ?stb5 vd vc c' f' cref' bits) \<in> fst ((returnOk $ drop (cbits + length guard) cref) (?sta5 vd vc c' f' cref' bits))
 7. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> vc \<noteq> []
 8. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> is_cnode_cap vd
 9. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> cap_relation (fst (vd, vc)) c'
 10. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> drop (32 - bits) (to_bl cref') = snd (vd, vc)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>vd c' f' cref'. \<lbrakk>0 < cbits \<or> guard \<noteq> []; \<not> length cref < cbits + length guard; guard \<le> cref; length cref \<noteq> cbits + length guard; vd \<noteq> cap.NullCap; cap_relation vd c'; is_cnode_cap vd; drop (32 + (cbits + length guard) - length cref) (to_bl cref') = drop (cbits + length guard) cref; drop (32 - length cref) (to_bl cref') = cref; bits = length cref; cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (vd, ?stc5 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard))) \<in> fst (get_cap (ptr, ?rva5 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard))) (?stb5 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard))))
 2. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> cbits + length guard \<noteq> 0
 3. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?v5 vd vc c' f' cref' bits), ?s'5 vd vc c' f' cref' bits) \<in> fst (whenE (\<not> guard \<le> cref) (throwError $ ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard) (?s5 vd vc c' f' cref' bits))
 4. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?rv5 vd vc c' f' cref' bits), ?st5 vd vc c' f' cref' bits) \<in> fst (whenE (length cref < cbits + length guard) (throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard)) (?s'5 vd vc c' f' cref' bits))
 5. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?rva5 vd vc c' f' cref' bits), ?sta5 vd vc c' f' cref' bits) \<in> fst ((returnOk $ take cbits (drop (length guard) cref)) (?st5 vd vc c' f' cref' bits))
 6. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr vc, ?stb5 vd vc c' f' cref' bits) \<in> fst ((returnOk $ drop (cbits + length guard) cref) (?sta5 vd vc c' f' cref' bits))
 7. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> vc \<noteq> []
 8. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> is_cnode_cap vd
 9. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> cap_relation (fst (vd, vc)) c'
 10. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> drop (32 - bits) (to_bl cref') = snd (vd, vc)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> cbits + length guard \<noteq> 0
 2. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?v5 vd vc c' f' cref' bits), ?s'5 vd vc c' f' cref' bits) \<in> fst (whenE (\<not> guard \<le> cref) (throwError $ ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard) (?s5 vd vc c' f' cref' bits))
 3. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?rv5 vd vc c' f' cref' bits), ?st5 vd vc c' f' cref' bits) \<in> fst (whenE (length cref < cbits + length guard) (throwError $ ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard)) (?s'5 vd vc c' f' cref' bits))
 4. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr (?rva5 vd vc c' f' cref' bits), ?sta5 vd vc c' f' cref' bits) \<in> fst ((returnOk $ take cbits (drop (length guard) cref)) (?st5 vd vc c' f' cref' bits))
 5. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> (Inr vc, ?s22 vd vc c' f' cref' bits\<lparr>kheap := [ptr \<mapsto> CNode (length (?offset29 vd vc c' f' cref' bits)) (\<lambda>x. if length x = length (?offset28 vd vc c' f' cref' bits) then Some vd else None)]\<rparr>) \<in> fst ((returnOk $ drop (cbits + length guard) cref) (?sta5 vd vc c' f' cref' bits))
 6. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> vc \<noteq> []
 7. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> is_cnode_cap vd
 8. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> cap_relation (fst (vd, vc)) c'
 9. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> drop (32 - bits) (to_bl cref') = snd (vd, vc)
 10. \<And>vd vc c' f' cref' bits. \<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap; cap_relation vd c'; bits = length vc; is_cnode_cap vd; drop (32 - bits) (to_bl cref') = vc; cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref)); cap = cap.CNodeCap ptr cbits guard; c' = capability.CNodeCap ptr cbits (of_bl guard) (length guard)\<rbrakk> \<Longrightarrow> bits = length (snd (vd, vc))
flex-flex pairs:
\<lambda>vd c' f' cref'. ?offset31 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard)) \<equiv>\<^sup>? \<lambda>vd c' f' cref'. ?rva5 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard))
\<lambda>vd c' f' cref'. ?offset30 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard)) \<equiv>\<^sup>? \<lambda>vd c' f' cref'. ?rva5 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard))
\<lambda>vd c' f' cref'. ?s25 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard)) \<equiv>\<^sup>? \<lambda>vd c' f' cref'. ?s22 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard))
\<lambda>vd c' f' cref'. ?offset29 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard)) \<equiv>\<^sup>? \<lambda>vd c' f' cref'. ?rva5 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard))
\<lambda>vd c' f' cref'. ?offset28 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard)) \<equiv>\<^sup>? \<lambda>vd c' f' cref'. ?rva5 vd (drop (cbits + length guard) cref) c' f' cref' (length cref - (cbits + length guard)) proof (state)
this:
\<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; ?vc1 = drop (cbits + length guard) cref; ?vc1 \<noteq> []; ?vd1 \<noteq> cap.NullCap; cap_relation ?vd1 ?c'1; ?bits1 = length ?vc1; is_cnode_cap ?vd1; drop (32 - ?bits1) (to_bl ?cref'1) = ?vc1\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>s. s \<turnstile> fst (?vd1, ?vc1))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' ?c'1) (resolve_address_bits' z (?vd1, ?vc1)) (CSpace_H.resolveAddressBits ?c'1 ?cref'1 ?bits1)

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
\<lbrakk>cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref; ?vc1 = drop (cbits + length guard) cref; ?vc1 \<noteq> []; ?vd1 \<noteq> cap.NullCap; cap_relation ?vd1 ?c'1; ?bits1 = length ?vc1; is_cnode_cap ?vd1; drop (32 - ?bits1) (to_bl ?cref'1) = ?vc1\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>s. s \<turnstile> fst (?vd1, ?vc1))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' ?c'1) (resolve_address_bits' z (?vd1, ?vc1)) (CSpace_H.resolveAddressBits ?c'1 ?cref'1 ?bits1)

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
?P (if ?Q then ?x else ?y) = ((?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y))

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
?P (if ?Q then ?x else ?y) = ((?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y))

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
cbits + length guard = 0 \<or> cbits = 0 \<and> guard = []

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
using this:
cbits + length guard = 0 \<or> cbits = 0 \<and> guard = []

goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
goal (1 subgoal):
 1. cbits = 0 \<and> guard = [] \<Longrightarrow> corres ((\<lambda>a aa. aa = lookup_failure_map a) \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (\<lambda>a. valid_objs a \<and> pspace_aligned a \<and> a \<turnstile> cap.CNodeCap ptr 0 []) (\<lambda>a. valid_objs' a \<and> pspace_distinct' a \<and> pspace_aligned' a \<and> valid_cap' (capability.CNodeCap ptr 0 0 0) a) fail fail proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>cbits = 0 \<and> guard = []; (s, s') \<in> state_relation; valid_objs s \<and> pspace_aligned s \<and> s \<turnstile> cap.CNodeCap ptr 0 []; valid_objs' s' \<and> pspace_distinct' s' \<and> pspace_aligned' s' \<and> valid_cap' (capability.CNodeCap ptr 0 0 0) s'; True\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
cbits + length guard = 0 \<or> cbits = 0 \<and> guard = [] \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
cbits + length guard = 0 \<or> cbits = 0 \<and> guard = [] \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
cbits + length guard = 0 \<or> cbits = 0 \<and> guard = [] \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
cbits + length guard \<noteq> 0 \<and> \<not> (cbits = 0 \<and> guard = [])

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
using this:
cbits + length guard \<noteq> 0 \<and> \<not> (cbits = 0 \<and> guard = [])

goal (1 subgoal):
 1. (cbits + length guard = 0) = False \<and> (cbits = 0 \<and> guard = []) = False \<and> (0 < cbits \<or> guard \<noteq> []) proof (state)
this:
(cbits + length guard = 0) = False \<and> (cbits = 0 \<and> guard = []) = False \<and> (0 < cbits \<or> guard \<noteq> [])

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
drop ?n (?xs @ ?ys) = drop ?n ?xs @ drop (?n - length ?xs) ?ys

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (chain)
picking this:
cap_relation (fst (cap, cref)) c'
drop (32 - bits) (to_bl cref') = snd (cap, cref)
bits = length (snd (cap, cref)) proof (prove)
using this:
cap_relation (fst (cap, cref)) c'
drop (32 - bits) (to_bl cref') = snd (cap, cref)
bits = length (snd (cap, cref))

goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref))\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref))\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (let nodeCap = c' in if isCNodeCap nodeCap then doE radixBits <- returnOk (capCNodeBits nodeCap);
guardBits <- returnOk (capCNodeGuardSize nodeCap);
levelBits <- returnOk (radixBits + guardBits);
haskell_assertE (levelBits \<noteq> 0) [];
offset <- returnOk (fromCPtr cref' `~shiftR~` (bits - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap nodeCap offset;
guard <- returnOk (fromCPtr cref' `~shiftR~` (bits - guardBits) && mask guardBits);
unlessE (guardBits \<le> bits \<and> guard = capCNodeGuard nodeCap) $ throw $ Fault_H.lookup_failure.GuardMismatch bits (capCNodeGuard nodeCap) guardBits;
whenE (bits < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch bits levelBits;
bitsLeft <- returnOk (bits - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap cref' bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else throw Fault_H.lookup_failure.InvalidRoot) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation (fst (cap, cref)) c'; drop (32 - bits) (to_bl cref') = snd (cap, cref); bits = length (snd (cap, cref))\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (case cap of cap.CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ ExceptionTypes_A.lookup_failure.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 ExceptionTypes_A.lookup_failure.InvalidRoot) (let nodeCap = c' in if isCNodeCap nodeCap then doE radixBits <- returnOk (capCNodeBits nodeCap);
guardBits <- returnOk (capCNodeGuardSize nodeCap);
levelBits <- returnOk (radixBits + guardBits);
haskell_assertE (levelBits \<noteq> 0) [];
offset <- returnOk (fromCPtr cref' `~shiftR~` (bits - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap nodeCap offset;
guard <- returnOk (fromCPtr cref' `~shiftR~` (bits - guardBits) && mask guardBits);
unlessE (guardBits \<le> bits \<and> guard = capCNodeGuard nodeCap) $ throw $ Fault_H.lookup_failure.GuardMismatch bits (capCNodeGuard nodeCap) guardBits;
whenE (bits < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch bits levelBits;
bitsLeft <- returnOk (bits - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap cref' bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else throw Fault_H.lookup_failure.InvalidRoot) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap c'; drop (32 - length cref) (to_bl cref') = cref; bits = length cref\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap cap) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (case cap of cap.CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ ExceptionTypes_A.lookup_failure.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 ExceptionTypes_A.lookup_failure.InvalidRoot) (if is_cnode_cap cap then doE y <- assertE (0 < capCNodeBits c' \<or> 0 < capCNodeGuardSize c');
slot <- liftE (locateSlotCap c' ((cref' >> length cref - (capCNodeBits c' + capCNodeGuardSize c')) && mask (capCNodeBits c')));
y <- whenE (capCNodeGuardSize c' \<le> length cref \<longrightarrow> (cref' >> length cref - capCNodeGuardSize c') && mask (capCNodeGuardSize c') \<noteq> capCNodeGuard c') (throwError (Fault_H.lookup_failure.GuardMismatch (length cref) (capCNodeGuard c') (capCNodeGuardSize c')));
y <- whenE (length cref < capCNodeBits c' + capCNodeGuardSize c') (throwError (Fault_H.lookup_failure.DepthMismatch (length cref) (capCNodeBits c' + capCNodeGuardSize c')));
if length cref \<le> capCNodeBits c' + capCNodeGuardSize c' then returnOk (slot, 0) else doE nextCap <- liftE (getSlotCap slot);
case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap cref' (length cref - (capCNodeBits c' + capCNodeGuardSize c')) | _ \<Rightarrow> returnOk (slot, length cref - (capCNodeBits c' + capCNodeGuardSize c'))
odE
odE else throwError Fault_H.lookup_failure.InvalidRoot) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drop (32 - length cref) (to_bl cref') = cref; bits = length cref\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (cap.CNodeCap ptr cbits guard)) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard))) (if \<not> guard \<le> cref then throwError (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard) else if length cref < cbits + length guard then throwError (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard)) else if length cref = cbits + length guard then returnOk ((ptr, drop (length guard) cref), []) else doE next_cap <- liftE (get_cap (ptr, take cbits (drop (length guard) cref)));
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, drop (cbits + length guard) cref) else returnOk ((ptr, take cbits (drop (length guard) cref)), drop (cbits + length guard) cref)
odE) (doE slot <- liftE (locateSlotCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) ((cref' >> length cref - (cbits + length guard)) && mask cbits));
if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then throwError (Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard)) else if length cref < cbits + length guard then throwError (Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard)) else if length cref = cbits + length guard then returnOk (slot, 0) else doE nextCap <- liftE (getSlotCap slot);
case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap cref' (length cref - (capCNodeBits c' + capCNodeGuardSize c')) | _ \<Rightarrow> returnOk (slot, length cref - (capCNodeBits c' + capCNodeGuardSize c'))
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drop (32 - length cref) (to_bl cref') = cref; bits = length cref\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits'). cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and valid_cap (cap.CNodeCap ptr cbits guard)) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard))) (if \<not> guard \<le> cref then throwError (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard) else if length cref < cbits + length guard then throwError (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard)) else if length cref = cbits + length guard then returnOk ((ptr, drop (length guard) cref), []) else doE next_cap <- liftE (get_cap (ptr, take cbits (drop (length guard) cref)));
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, drop (cbits + length guard) cref) else returnOk ((ptr, take cbits (drop (length guard) cref)), drop (cbits + length guard) cref)
odE) (doE slot <- liftE (locateSlotCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) ((cref' >> length cref - (cbits + length guard)) && mask cbits));
if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then throwError (Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard)) else if length cref < cbits + length guard then throwError (Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard)) else if length cref = cbits + length guard then returnOk (slot, 0) else doE nextCap <- liftE (getSlotCap slot);
if isCNodeCap nextCap then CSpace_H.resolveAddressBits nextCap cref' (length cref - (capCNodeBits c' + capCNodeGuardSize c')) else returnOk (slot, length cref - (capCNodeBits c' + capCNodeGuardSize c'))
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>drop (32 - length cref) (to_bl cref') = cref; bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'\<rbrakk> \<Longrightarrow> (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard) \<and> (\<not> guard \<le> cref \<longrightarrow> Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard)) \<and> (if \<not> guard \<le> cref then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> length cref - (capCNodeBits c' + capCNodeGuardSize c') = length cref - (cbits + length guard) \<and> drop (32 - (length cref - (capCNodeBits c' + capCNodeGuardSize c'))) (to_bl cref') = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> (length cref < cbits + length guard \<longrightarrow> Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard))) \<and> (\<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) \<and> length cref - (cbits + length guard) = length cref - (capCNodeBits c' + capCNodeGuardSize c'))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<exists>zs. to_bl cref' = zs @ cref; bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'\<rbrakk> \<Longrightarrow> (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard) \<and> (\<not> guard \<le> cref \<longrightarrow> Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard)) \<and> (if \<not> guard \<le> cref then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> length cref - (capCNodeBits c' + capCNodeGuardSize c') = length cref - (cbits + length guard) \<and> drop (32 - (length cref - (capCNodeBits c' + capCNodeGuardSize c'))) (to_bl cref') = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> (length cref < cbits + length guard \<longrightarrow> Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard))) \<and> (\<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) \<and> length cref - (cbits + length guard) = length cref - (capCNodeBits c' + capCNodeGuardSize c'))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' zs. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = zs @ cref\<rbrakk> \<Longrightarrow> (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard) \<and> (\<not> guard \<le> cref \<longrightarrow> Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard)) \<and> (if \<not> guard \<le> cref then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> length cref - (capCNodeBits c' + capCNodeGuardSize c') = length cref - (cbits + length guard) \<and> drop (32 - (length cref - (capCNodeBits c' + capCNodeGuardSize c'))) (zs @ cref) = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> (length cref < cbits + length guard \<longrightarrow> Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard))) \<and> (\<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) \<and> length cref - (cbits + length guard) = length cref - (capCNodeBits c' + capCNodeGuardSize c'))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' zs. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = zs @ cref\<rbrakk> \<Longrightarrow> is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits
 2. \<And>s s' zs. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = zs @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard) \<and> (\<not> guard \<le> cref \<longrightarrow> Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard)) \<and> (if \<not> guard \<le> cref then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> length cref - (capCNodeBits c' + capCNodeGuardSize c') = length cref - (cbits + length guard) \<and> drop (32 - (length cref - (capCNodeBits c' + capCNodeGuardSize c'))) (zs @ cref) = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> (length cref < cbits + length guard \<longrightarrow> Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard))) \<and> (\<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) \<and> length cref - (cbits + length guard) = length cref - (capCNodeBits c' + capCNodeGuardSize c'))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' zs. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = zs @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard) \<and> (\<not> guard \<le> cref \<longrightarrow> Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard)) \<and> (if \<not> guard \<le> cref then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> length cref - (capCNodeBits c' + capCNodeGuardSize c') = length cref - (cbits + length guard) \<and> drop (32 - (length cref - (capCNodeBits c' + capCNodeGuardSize c'))) (zs @ cref) = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> (length cref < cbits + length guard \<longrightarrow> Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard))) \<and> (\<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) \<and> length cref - (cbits + length guard) = length cref - (capCNodeBits c' + capCNodeGuardSize c'))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard) \<and> (\<not> guard \<le> cref \<longrightarrow> Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard)) \<and> (if \<not> guard \<le> cref then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> length cref - (capCNodeBits c' + capCNodeGuardSize c') = length cref - (cbits + length guard) \<and> drop (32 - (length cref - (capCNodeBits c' + capCNodeGuardSize c'))) (x @ cref) = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> (length cref < cbits + length guard \<longrightarrow> Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard))) \<and> (\<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) \<and> length cref - (cbits + length guard) = length cref - (capCNodeBits c' + capCNodeGuardSize c'))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard) \<and> (\<not> guard \<le> cref \<longrightarrow> Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard)) \<and> (if \<not> guard \<le> cref then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> length cref - (capCNodeBits c' + capCNodeGuardSize c') = length cref - (cbits + length guard) \<and> drop (32 - (length cref - (capCNodeBits c' + capCNodeGuardSize c'))) (x @ cref) = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> (length cref < cbits + length guard \<longrightarrow> Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard))) \<and> (\<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) \<and> length cref - (cbits + length guard) = length cref - (capCNodeBits c' + capCNodeGuardSize c'))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (\<not> guard \<le> cref \<longrightarrow> Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard)) \<and> (if \<not> guard \<le> cref then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> length cref - (capCNodeBits c' + capCNodeGuardSize c') = length cref - (cbits + length guard) \<and> drop (32 - (length cref - (capCNodeBits c' + capCNodeGuardSize c'))) (x @ cref) = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> (length cref < cbits + length guard \<longrightarrow> Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard))) \<and> (\<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) \<and> length cref - (cbits + length guard) = length cref - (capCNodeBits c' + capCNodeGuardSize c'))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (\<not> guard \<le> cref \<longrightarrow> Fault_H.lookup_failure.GuardMismatch (length cref) (of_bl guard) (length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.GuardMismatch (length cref) guard)) \<and> (if \<not> guard \<le> cref then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> length cref - (capCNodeBits c' + capCNodeGuardSize c') = length cref - (cbits + length guard) \<and> drop (32 - (length cref - (capCNodeBits c' + capCNodeGuardSize c'))) (x @ cref) = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> (length cref < cbits + length guard \<longrightarrow> Fault_H.lookup_failure.DepthMismatch (length cref) (cbits + length guard) = lookup_failure_map (ExceptionTypes_A.lookup_failure.DepthMismatch (length cref) (cbits + length guard))) \<and> (\<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)) \<and> length cref - (cbits + length guard) = length cref - (capCNodeBits c' + capCNodeGuardSize c'))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> drop (32 + (cbits + length guard) - length cref) (x @ cref) = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s \<and> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>a. True else if length cref < cbits + length guard then \<lambda>a. True else if length cref = cbits + length guard then \<lambda>a. True else (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> guard \<le> cref \<and> cap \<noteq> cap.NullCap \<and> drop (32 + (cbits + length guard) - length cref) (x @ cref) = drop (cbits + length guard) cref) and cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> (if is_cnode_cap cap then valid_objs and pspace_aligned and valid_cap cap else (\<lambda>a. True)) s)) s
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> Ex (cap_relation cap) \<longrightarrow> is_cnode_cap cap \<longrightarrow> cap \<noteq> cap.NullCap \<and> drop (32 + (cbits + length guard) - length cref) (x @ cref) = drop (cbits + length guard) cref) \<and> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s \<longrightarrow> s \<turnstile> cap)
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (4 subgoals):
 1. \<And>cap xa. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap; cap_relation cap xa\<rbrakk> \<Longrightarrow> drop (32 + (cbits + length guard) - length cref) (x @ cref) = drop (cbits + length guard) cref
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 3. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 4. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (4 subgoals):
 1. \<And>cap xa. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap; cap_relation cap xa\<rbrakk> \<Longrightarrow> drop (32 + (cbits + length guard) - length cref) (to_bl cref') = drop (cbits + length guard) cref
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 3. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 4. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap; cap_relation cap x; drop (length (to_bl cref') - length cref) (to_bl cref') = cref\<rbrakk> \<Longrightarrow> drop (32 + (cbits + length guard) - length cref) (to_bl cref') = drop (cbits + length guard) cref
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 3. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 4. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap; cap_relation cap x; drop (32 - length cref) (to_bl cref') = cref\<rbrakk> \<Longrightarrow> drop (32 + (cbits + length guard) - length cref) (to_bl cref') = drop (cbits + length guard) cref
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 3. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 4. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (5 subgoals):
 1. \<And>cap x. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap; cap_relation cap x; drop (32 - length cref) (to_bl cref') = cref\<rbrakk> \<Longrightarrow> 32 + (cbits + length guard) - length cref = cbits + length guard + (32 - length cref)
 2. \<And>cap x. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap; cap_relation cap x; drop (32 - length cref) (to_bl cref') = cref; 32 + (cbits + length guard) - length cref = cbits + length guard + (32 - length cref)\<rbrakk> \<Longrightarrow> drop (32 + (cbits + length guard) - length cref) (to_bl cref') = drop (cbits + length guard) cref
 3. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 4. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 5. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap; cap_relation cap x; drop (32 - length cref) (to_bl cref') = cref; 32 + (cbits + length guard) - length cref = cbits + length guard + (32 - length cref)\<rbrakk> \<Longrightarrow> drop (32 + (cbits + length guard) - length cref) (to_bl cref') = drop (cbits + length guard) cref
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 3. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 4. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap; cap_relation cap x; drop (32 - length cref) (to_bl cref') = cref; 32 + (cbits + length guard) - length cref = cbits + length guard + (32 - length cref)\<rbrakk> \<Longrightarrow> drop (cbits + length guard + (32 - length cref)) (to_bl cref') = drop (cbits + length guard) cref
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 3. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 4. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap; cap_relation cap x; drop (32 - length cref) (to_bl cref') = cref; 32 + (cbits + length guard) - length cref = cbits + length guard + (32 - length cref)\<rbrakk> \<Longrightarrow> drop (cbits + length guard) (drop (32 - length cref) (to_bl cref')) = drop (cbits + length guard) cref
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 3. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 4. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; cte_wp_at ((=) cap_) (ptr, take cbits (drop (length guard) cref)) s; is_cnode_cap cap_; cap_relation cap_ x_; drop (32 - length cref) (to_bl cref') = cref; 32 + (cbits + length guard) - length cref = cbits + length guard + (32 - length cref)\<rbrakk> \<Longrightarrow> drop (cbits + length guard) (drop (32 - length cref) (to_bl cref')) = drop (cbits + length guard) cref proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 2. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 3. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (3 subgoals):
 1. \<And>cs. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; 0 < cbits; kheap s ptr = Some (CNode cbits cs); \<forall>cap\<in>ran cs. s \<turnstile> cap; dom cs = {x. length x = cbits}; is_aligned ptr (cte_level_bits + cbits); cbits < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, take cbits (drop (length guard) cref)) s
 2. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 3. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (3 subgoals):
 1. \<And>cs. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; 0 < cbits; kheap s ptr = Some (CNode cbits cs); \<forall>cap\<in>ran cs. s \<turnstile> cap; dom cs = {x. length x = cbits}; is_aligned ptr (cte_level_bits + cbits); cbits < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> cap_table_at (length (take cbits (drop (length guard) cref))) ptr s
 2. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 3. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; guard \<le> cref; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; length cref \<noteq> cbits + length guard; \<not> length cref < cbits + length guard; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; is_cnode_cap cap; cte_wp_at ((=) cap) (ptr, take cbits (drop (length guard) cref)) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> (guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))) \<and> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard)\<rbrakk> \<Longrightarrow> guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))\<rbrakk> \<Longrightarrow> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bits = cbits + length guard; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (cref' >> cbits) && mask (length guard) = of_bl guard; guard \<le> cref; length cref = cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; guard \<le> cref; \<not> length cref < cbits + length guard; length cref \<noteq> cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))
 3. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))\<rbrakk> \<Longrightarrow> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (3 subgoals):
 1. \<And>cs. \<lbrakk>bits = cbits + length guard; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (cref' >> cbits) && mask (length guard) = of_bl guard; guard \<le> cref; length cref = cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; 0 < cbits; kheap s ptr = Some (CNode cbits cs); \<forall>cap\<in>ran cs. s \<turnstile> cap; dom cs = {x. length x = cbits}; is_aligned ptr (cte_level_bits + cbits); cbits < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; guard \<le> cref; \<not> length cref < cbits + length guard; length cref \<noteq> cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))
 3. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))\<rbrakk> \<Longrightarrow> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (3 subgoals):
 1. \<And>cs. \<lbrakk>bits = cbits + length guard; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; (cref' >> cbits) && mask (length guard) = of_bl guard; guard \<le> cref; length cref = cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits; 0 < cbits; kheap s ptr = Some (CNode cbits cs); \<forall>cap\<in>ran cs. s \<turnstile> cap; dom cs = {x. length x = cbits}; is_aligned ptr (cte_level_bits + cbits); cbits < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> cbits \<le> word_bits - cte_level_bits
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; guard \<le> cref; \<not> length cref < cbits + length guard; length cref \<noteq> cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))
 3. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))\<rbrakk> \<Longrightarrow> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; guard \<le> cref; \<not> length cref < cbits + length guard; length cref \<noteq> cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))\<rbrakk> \<Longrightarrow> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; guard \<le> cref; \<not> length cref < cbits + length guard; length cref \<noteq> cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> cbits + length guard \<le> length cref
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))\<rbrakk> \<Longrightarrow> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; (cref' >> length cref - length guard) && mask (length guard) = of_bl guard; guard \<le> cref; \<not> length cref < cbits + length guard; length cref \<noteq> cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> cbits + length guard \<le> length cref proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> word_bits - cte_level_bits; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))\<rbrakk> \<Longrightarrow> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 2 ^ cte_level_bits * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 0x10 * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))); is_aligned ptr (4 + cbits); cbits \<le> word_bits - 4\<rbrakk> \<Longrightarrow> ((isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB) \<and> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 0x10 * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))); is_aligned ptr (4 + cbits); cbits \<le> word_bits - 4\<rbrakk> \<Longrightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<noteq> ZombieTCB) \<and> (case gsCNodes s' ptr of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = cbits \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> n = zombieCTEBits (capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)))) \<and> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ n) \<or> isThreadCap (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<or> isZombie (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) \<and> capZombieType (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) = ZombieTCB
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 0x10 * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))); is_aligned ptr (4 + cbits); cbits \<le> word_bits - 4\<rbrakk> \<Longrightarrow> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 0x10 * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))); is_aligned ptr (4 + cbits); cbits \<le> word_bits - 4; cap_aligned (cap.CNodeCap ptr cbits guard); cap_table_at cbits ptr s; 0 < cbits; length guard \<le> word_bits\<rbrakk> \<Longrightarrow> (cref' >> length cref - (cbits + length guard)) && mask cbits < 2 ^ cbits
 2. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 0x10 * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))); is_aligned ptr (4 + cbits); cbits \<le> word_bits - 4\<rbrakk> \<Longrightarrow> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits = length cref; (s, s') \<in> state_relation; valid_objs s; valid_objs' s'; pspace_aligned s; s \<turnstile> cap.CNodeCap ptr cbits guard; pspace_distinct' s'; pspace_aligned' s'; valid_cap' (capability.CNodeCap ptr cbits (of_bl guard) (length guard)) s'; to_bl cref' = x @ cref; (\<not> guard \<le> cref) = (length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard); guard \<le> cref \<longrightarrow> \<not> length cref < cbits + length guard \<longrightarrow> (length cref = cbits + length guard \<longrightarrow> ptr + 0x10 * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)) \<and> (length cref \<noteq> cbits + length guard \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref))); is_aligned ptr (4 + cbits); cbits \<le> word_bits - 4\<rbrakk> \<Longrightarrow> (if length guard \<le> length cref \<longrightarrow> (cref' >> length cref - length guard) && mask (length guard) \<noteq> of_bl guard then \<lambda>_. True else if length cref < cbits + length guard then \<lambda>_. True else if length cref = cbits + length guard then \<lambda>_. True else (\<lambda>s'. valid_objs' s' \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s' \<longrightarrow> (\<forall>cap. valid_cap' cap s' \<longrightarrow> (\<forall>rv. cap_relation rv cap \<longrightarrow> \<not> is_cnode_cap rv \<longrightarrow> ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = cte_map (ptr, take cbits (drop (length guard) cref)))))) and (pspace_distinct' and pspace_aligned') and (\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) (ptr + 0x10 * ((cref' >> length cref - (cbits + length guard)) && mask cbits)) s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> (if isCNodeCap cap then valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' cap else (\<lambda>a. True)) s)))) s' proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals! proof (state)
this:
corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
cbits + length guard \<noteq> 0 \<and> \<not> (cbits = 0 \<and> guard = []) \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal (2 subgoals):
 1. isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
 2. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (chain)
picking this:
cbits + length guard = 0 \<or> cbits = 0 \<and> guard = [] \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
cbits + length guard \<noteq> 0 \<and> \<not> (cbits = 0 \<and> guard = []) \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (prove)
using this:
cbits + length guard = 0 \<or> cbits = 0 \<and> guard = [] \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)
cbits + length guard \<noteq> 0 \<and> \<not> (cbits = 0 \<and> guard = []) \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal (1 subgoal):
 1. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
goal (1 subgoal):
 1. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
\<not> isCNodeCap c'

goal (1 subgoal):
 1. \<not> isCNodeCap c' \<Longrightarrow> corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (chain)
picking this:
cap_relation (fst (cap, cref)) c'
drop (32 - bits) (to_bl cref') = snd (cap, cref)
bits = length (snd (cap, cref))
\<not> isCNodeCap c' proof (prove)
using this:
cap_relation (fst (cap, cref)) c'
drop (32 - bits) (to_bl cref') = snd (cap, cref)
bits = length (snd (cap, cref))
\<not> isCNodeCap c'

goal (1 subgoal):
 1. corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits) proof (state)
this:
corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal:
No subgoals! proof (state)
this:
corres (lfr \<oplus> (\<lambda>a. case a of (cte, bits) \<Rightarrow> \<lambda>a. case a of (cte', bits') \<Rightarrow> cte' = cte_map cte \<and> length bits = bits')) (valid_objs and pspace_aligned and (\<lambda>a. a \<turnstile> fst (cap, cref))) (valid_objs' and pspace_distinct' and pspace_aligned' and valid_cap' c') (resolve_address_bits' z (cap, cref)) (CSpace_H.resolveAddressBits c' cref' bits)

goal:
No subgoals!