theory RAB_FN

lemma resolveAddressBitsFn_eq:
  "monadic_rewrite F E (\<lambda>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s))
        \<and> valid_objs' s \<and> cnode_caps_gsCNodes' s)
    (resolveAddressBits cap capptr bits)
    (gets (resolveAddressBitsFn cap capptr bits o only_cnode_caps o ctes_of))"
  (is "monadic_rewrite F E (?P cap) (?f cap bits) (?g cap capptr bits)") proof (induct cap capptr bits rule: resolveAddressBits.induct) case (1 cap cref depth) note objBits_defs[simp] show ?case apply (subst resolveAddressBits.simps, subst resolveAddressBitsFn.simps) apply (simp only: Let_def haskell_assertE_def K_bind_def) apply (rule monadic_rewrite_name_pre) apply (rule monadic_rewrite_guard_imp) apply (rule_tac P="(=) s" in monadic_rewrite_trans) 
      (* step 1, apply the induction hypothesis on the lhs *)
       apply (rule monadic_rewrite_named_if monadic_rewrite_named_bindE
                  monadic_rewrite_refl[THEN monadic_rewrite_guard_imp, where f="returnOk y" for y]
                  monadic_rewrite_refl[THEN monadic_rewrite_guard_imp, where f="x $ y" for x y]
                  monadic_rewrite_refl[THEN monadic_rewrite_guard_imp, where f="assertE P" for P s]
                  TrueI)+ apply (rule_tac g="case nextCap of CNodeCap a b c d
            \<Rightarrow> ?g nextCap cref bitsLeft
            | _ \<Rightarrow> returnOk (slot, bitsLeft)" in monadic_rewrite_guard_imp) apply (wpc | rule monadic_rewrite_refl "1.hyps"
           | simp only: capability.case haskell_assertE_def simp_thms)+ apply (clarsimp simp: in_monad locateSlot_conv getSlotCap_def
                      dest!: in_getCTE fst_stateAssertD) apply (fastforce elim: cte_wp_at_weakenE') apply (rule monadic_rewrite_refl[THEN monadic_rewrite_guard_imp], simp) 
     (* step 2, split and match based on the lhs structure *)
      apply (simp add: locateSlot_conv liftE_bindE unlessE_def whenE_def
                      if_to_top_of_bindE assertE_def stateAssert_def bind_assoc
                      assert_def if_to_top_of_bind getSlotCap_def
               split del: if_split cong: if_cong) apply (rule monadic_rewrite_if_l monadic_rewrite_symb_exec_l'[OF _ get_wp, rotated]
                 empty_fail_get no_fail_get impI
                 monadic_rewrite_refl get_wp
       | simp add: throwError_def returnOk_def locateSlotFun_def if_not_P
                   isCNodeCap_capUntypedPtr_capCNodePtr
             cong: if_cong split del: if_split)+ apply (rule monadic_rewrite_symb_exec_l'[OF _ getCTE_inv _ _ getCTE_cte_wp_at, rotated]) apply simp apply (rule impI, rule no_fail_getCTE) apply (simp add: monadic_rewrite_def simpler_gets_def return_def returnOk_def
                           only_cnode_caps_def cte_wp_at_ctes_of isCap_simps
                           locateSlotFun_def isCNodeCap_capUntypedPtr_capCNodePtr
                    split: capability.split) apply (rule monadic_rewrite_name_pre[where P="\<lambda>_. False" and f=fail]
                     monadic_rewrite_refl get_wp
           | simp add: throwError_def returnOk_def locateSlotFun_def if_not_P
                       isCNodeCap_capUntypedPtr_capCNodePtr
             cong: if_cong split del: if_split)+ 
  (* step 3, prove the non-failure conditions *)
   apply (clarsimp simp: isCap_simps) apply (frule(1) cte_wp_at_valid_objs_valid_cap') apply (clarsimp simp: cte_level_bits_def valid_cap_simps'
                        real_cte_at' isCap_simps) apply (clarsimp simp: cte_wp_at_ctes_of only_cnode_caps_def ball_Un
                        cnode_caps_gsCNodes_def ran_map_option o_def) apply (drule bspec, rule IntI, erule ranI, simp add: isCap_simps) apply (simp add: isCap_simps capAligned_def word_bits_def and_mask_less') done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits cap capptr bits) (gets (resolveAddressBitsFn cap capptr bits \<circ> only_cnode_caps \<circ> ctes_of)) proof (state)
goal (1 subgoal):
 1. \<And>a b c. (\<And>x v s s' rv st rva sta rvb stb rvba stc rvbb std rvbc ste rvbd stf rvc stg rvd sth rve sti x111 x112 x113 x114. \<lbrakk>x = a; isCNodeCap x; (Inr v, s') \<in> fst (returnOk (capCNodeBits x) s); (Inr rv, st) \<in> fst (returnOk (capCNodeGuardSize x) s'); (Inr rva, sta) \<in> fst (returnOk (v + rv) st); (Inr rvb, stb) \<in> fst (haskell_assertE (rva \<noteq> 0) [] sta); (Inr rvba, stc) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rva) && mask v) stb); (Inr rvbb, std) \<in> fst ((withoutFailure $ locateSlotCap x rvba) stc); (Inr rvbc, ste) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rv) && mask rv) std); (Inr rvbd, stf) \<in> fst ((unlessE (rv \<le> c \<and> rvbc = capCNodeGuard x) $ throw $ Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard x) rv) ste); (Inr rvc, stg) \<in> fst ((whenE (c < rva) $ throw $ Fault_H.lookup_failure.DepthMismatch c rva) stf); (Inr rvd, sth) \<in> fst (returnOk (c - rva) stg); rvd \<noteq> 0; (Inr rve, sti) \<in> fst ((withoutFailure $ getSlotCap rvbb) sth); rve = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (isCNodeCap rve \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = rve) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits rve b rvd) (gets (resolveAddressBitsFn rve b rvd \<circ> only_cnode_caps \<circ> ctes_of))) \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (isCNodeCap a \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = a) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits a b c) (gets (resolveAddressBitsFn a b c \<circ> only_cnode_caps \<circ> ctes_of)) proof (state)
this:
\<lbrakk>?x = cap; isCNodeCap ?x; (Inr ?v, ?s') \<in> fst (returnOk (capCNodeBits ?x) ?s); (Inr ?rv, ?st) \<in> fst (returnOk (capCNodeGuardSize ?x) ?s'); (Inr ?rva, ?sta) \<in> fst (returnOk (?v + ?rv) ?st); (Inr ?rvb, ?stb) \<in> fst (haskell_assertE (?rva \<noteq> 0) [] ?sta); (Inr ?rvba, ?stc) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - ?rva) && mask ?v) ?stb); (Inr ?rvbb, ?std) \<in> fst ((withoutFailure $ locateSlotCap ?x ?rvba) ?stc); (Inr ?rvbc, ?ste) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - ?rv) && mask ?rv) ?std); (Inr ?rvbd, ?stf) \<in> fst ((unlessE (?rv \<le> depth \<and> ?rvbc = capCNodeGuard ?x) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard ?x) ?rv) ?ste); (Inr ?rvc, ?stg) \<in> fst ((whenE (depth < ?rva) $ throw $ Fault_H.lookup_failure.DepthMismatch depth ?rva) ?stf); (Inr ?rvd, ?sth) \<in> fst (returnOk (depth - ?rva) ?stg); ?rvd \<noteq> 0; (Inr ?rve, ?sti) \<in> fst ((withoutFailure $ getSlotCap ?rvbb) ?sth); ?rve = capability.CNodeCap ?x111.0 ?x112.0 ?x113.0 ?x114.0\<rbrakk> \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (isCNodeCap ?rve \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = ?rve) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits ?rve cref ?rvd) (gets (resolveAddressBitsFn ?rve cref ?rvd \<circ> only_cnode_caps \<circ> ctes_of))

goal (1 subgoal):
 1. \<And>a b c. (\<And>x v s s' rv st rva sta rvb stb rvba stc rvbb std rvbc ste rvbd stf rvc stg rvd sth rve sti x111 x112 x113 x114. \<lbrakk>x = a; isCNodeCap x; (Inr v, s') \<in> fst (returnOk (capCNodeBits x) s); (Inr rv, st) \<in> fst (returnOk (capCNodeGuardSize x) s'); (Inr rva, sta) \<in> fst (returnOk (v + rv) st); (Inr rvb, stb) \<in> fst (haskell_assertE (rva \<noteq> 0) [] sta); (Inr rvba, stc) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rva) && mask v) stb); (Inr rvbb, std) \<in> fst ((withoutFailure $ locateSlotCap x rvba) stc); (Inr rvbc, ste) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rv) && mask rv) std); (Inr rvbd, stf) \<in> fst ((unlessE (rv \<le> c \<and> rvbc = capCNodeGuard x) $ throw $ Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard x) rv) ste); (Inr rvc, stg) \<in> fst ((whenE (c < rva) $ throw $ Fault_H.lookup_failure.DepthMismatch c rva) stf); (Inr rvd, sth) \<in> fst (returnOk (c - rva) stg); rvd \<noteq> 0; (Inr rve, sti) \<in> fst ((withoutFailure $ getSlotCap rvbb) sth); rve = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (isCNodeCap rve \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = rve) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits rve b rvd) (gets (resolveAddressBitsFn rve b rvd \<circ> only_cnode_caps \<circ> ctes_of))) \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (isCNodeCap a \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = a) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits a b c) (gets (resolveAddressBitsFn a b c \<circ> only_cnode_caps \<circ> ctes_of)) proof (state)
this:
tcbBlockSizeBits \<equiv> 9
epSizeBits \<equiv> 4
ntfnSizeBits \<equiv> wordSizeCase 4 5
cteSizeBits \<equiv> wordSizeCase 4 5

goal (1 subgoal):
 1. \<And>a b c. (\<And>x v s s' rv st rva sta rvb stb rvba stc rvbb std rvbc ste rvbd stf rvc stg rvd sth rve sti x111 x112 x113 x114. \<lbrakk>x = a; isCNodeCap x; (Inr v, s') \<in> fst (returnOk (capCNodeBits x) s); (Inr rv, st) \<in> fst (returnOk (capCNodeGuardSize x) s'); (Inr rva, sta) \<in> fst (returnOk (v + rv) st); (Inr rvb, stb) \<in> fst (haskell_assertE (rva \<noteq> 0) [] sta); (Inr rvba, stc) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rva) && mask v) stb); (Inr rvbb, std) \<in> fst ((withoutFailure $ locateSlotCap x rvba) stc); (Inr rvbc, ste) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rv) && mask rv) std); (Inr rvbd, stf) \<in> fst ((unlessE (rv \<le> c \<and> rvbc = capCNodeGuard x) $ throw $ Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard x) rv) ste); (Inr rvc, stg) \<in> fst ((whenE (c < rva) $ throw $ Fault_H.lookup_failure.DepthMismatch c rva) stf); (Inr rvd, sth) \<in> fst (returnOk (c - rva) stg); rvd \<noteq> 0; (Inr rve, sti) \<in> fst ((withoutFailure $ getSlotCap rvbb) sth); rve = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (isCNodeCap rve \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = rve) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits rve b rvd) (gets (resolveAddressBitsFn rve b rvd \<circ> only_cnode_caps \<circ> ctes_of))) \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (isCNodeCap a \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = a) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits a b c) (gets (resolveAddressBitsFn a b c \<circ> only_cnode_caps \<circ> ctes_of)) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits cap cref depth) (gets (resolveAddressBitsFn cap cref depth \<circ> only_cnode_caps \<circ> ctes_of)) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (let nodeCap = cap 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~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap nodeCap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard nodeCap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard nodeCap) guardBits;
whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - 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) (gets ((\<lambda>caps. let nodeCap = cap in if isCNodeCap nodeCap then let radixBits = capCNodeBits nodeCap; guardBits = capCNodeGuardSize nodeCap; levelBits = radixBits + guardBits; offset = fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits; guard = fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits; bitsLeft = depth - levelBits; slot = locateSlotFun (capCNodePtr nodeCap) offset in if levelBits = 0 then Inr (0, 0) else if \<not> (guardBits \<le> depth \<and> guard = capCNodeGuard nodeCap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard nodeCap) guardBits else if depth < levelBits then Inl $ Fault_H.lookup_failure.DepthMismatch depth levelBits else if bitsLeft = 0 then Inr (slot, 0) else case caps slot of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref bitsLeft caps | Some capability.NullCap \<Rightarrow> Inr (slot, bitsLeft) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref bitsLeft caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref bitsLeft caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref bitsLeft caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref bitsLeft caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref bitsLeft caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref bitsLeft caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref bitsLeft caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref bitsLeft caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref bitsLeft caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref bitsLeft caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of)) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
y <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
y <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - 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) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E ((=) s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
y <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
y <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - 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) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of)) proof (prove)
goal (2 subgoals):
 1. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q2 s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
y <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
y <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - 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) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 2. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E ((=) s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
y <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
y <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - 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) (?g5 s)
 2. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (?g5 s) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 3. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (3 subgoals):
 1. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E ((=) s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
y <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
y <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - 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) (?g5 s)
 2. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (?g5 s) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 3. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (4 subgoals):
 1. \<And>s radixBits s' guardBits s'a levelBits s'b y s'c offset s'd slot s'e guard s'f ya s'g yb s'h bitsLeft s'i nextCap s'j. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; (Inr radixBits, s') \<in> fst (returnOk (capCNodeBits cap) s); (Inr guardBits, s'a) \<in> fst (returnOk (capCNodeGuardSize cap) s'); (Inr levelBits, s'b) \<in> fst (returnOk (radixBits + guardBits) s'a); (Inr y, s'c) \<in> fst (assertE (levelBits \<noteq> 0) s'b); (Inr offset, s'd) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits) s'c); (Inr slot, s'e) \<in> fst ((withoutFailure $ locateSlotCap cap offset) s'd); (Inr guard, s'f) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits) s'e); (Inr ya, s'g) \<in> fst ((unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits) s'f); (Inr yb, s'h) \<in> fst ((whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits) s'g); (Inr bitsLeft, s'i) \<in> fst (returnOk (depth - levelBits) s'h); bitsLeft \<noteq> 0; (Inr nextCap, s'j) \<in> fst ((withoutFailure $ getSlotCap slot) s'i)\<rbrakk> \<Longrightarrow> monadic_rewrite F E ((=) s'j) (case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap cref bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)) (?g'130 s radixBits guardBits levelBits y offset slot guard ya yb bitsLeft nextCap)
 2. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E ((=) s) (throw Fault_H.lookup_failure.InvalidRoot) (?d6 s)
 3. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
ya <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
yb <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else (withoutFailure $ getSlotCap slot) >>=E ?g'130 s radixBits guardBits levelBits y offset slot guard ya yb bitsLeft
odE else ?d6 s) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 4. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (5 subgoals):
 1. \<And>s radixBits s' guardBits s'a levelBits s'b y s'c offset s'd slot s'e guard s'f ya s'g yb s'h bitsLeft s'i nextCap s'j. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; (Inr radixBits, s') \<in> fst (returnOk (capCNodeBits cap) s); (Inr guardBits, s'a) \<in> fst (returnOk (capCNodeGuardSize cap) s'); (Inr levelBits, s'b) \<in> fst (returnOk (radixBits + guardBits) s'a); (Inr y, s'c) \<in> fst (assertE (levelBits \<noteq> 0) s'b); (Inr offset, s'd) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits) s'c); (Inr slot, s'e) \<in> fst ((withoutFailure $ locateSlotCap cap offset) s'd); (Inr guard, s'f) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits) s'e); (Inr ya, s'g) \<in> fst ((unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits) s'f); (Inr yb, s'h) \<in> fst ((whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits) s'g); (Inr bitsLeft, s'i) \<in> fst (returnOk (depth - levelBits) s'h); bitsLeft \<noteq> 0; (Inr nextCap, s'j) \<in> fst ((withoutFailure $ getSlotCap slot) s'i)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?Q139 s radixBits s' guardBits s'a levelBits s'b y s'c offset s'd slot s'e guard s'f ya s'g yb s'h bitsLeft s'i nextCap s'j) (case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap cref bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)) (case nextCap of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn nextCap cref bitsLeft \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (slot, bitsLeft))
 2. \<And>s radixBits s' guardBits s'a levelBits s'b y s'c offset s'd slot s'e guard s'f ya s'g yb s'h bitsLeft s'i nextCap s'j sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; (Inr radixBits, s') \<in> fst (returnOk (capCNodeBits cap) s); (Inr guardBits, s'a) \<in> fst (returnOk (capCNodeGuardSize cap) s'); (Inr levelBits, s'b) \<in> fst (returnOk (radixBits + guardBits) s'a); (Inr y, s'c) \<in> fst (assertE (levelBits \<noteq> 0) s'b); (Inr offset, s'd) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits) s'c); (Inr slot, s'e) \<in> fst ((withoutFailure $ locateSlotCap cap offset) s'd); (Inr guard, s'f) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits) s'e); (Inr ya, s'g) \<in> fst ((unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits) s'f); (Inr yb, s'h) \<in> fst ((whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits) s'g); (Inr bitsLeft, s'i) \<in> fst (returnOk (depth - levelBits) s'h); bitsLeft \<noteq> 0; (Inr nextCap, s'j) \<in> fst ((withoutFailure $ getSlotCap slot) s'i); s'j = sa\<rbrakk> \<Longrightarrow> ?Q139 s radixBits s' guardBits s'a levelBits s'b y s'c offset s'd slot s'e guard s'f ya s'g yb s'h bitsLeft s'i nextCap s'j sa
 3. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E ((=) s) (throw Fault_H.lookup_failure.InvalidRoot) (?d6 s)
 4. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
ya <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
yb <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn nextCap cref bitsLeft \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else ?d6 s) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 5. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (4 subgoals):
 1. \<And>s radixBits s' guardBits s'a levelBits s'b y s'c offset s'd slot s'e guard s'f ya s'g yb s'h bitsLeft s'i nextCap s'j sa. \<lbrakk>(\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; (Inr radixBits, s') \<in> fst (returnOk (capCNodeBits cap) s); (Inr guardBits, s'a) \<in> fst (returnOk (capCNodeGuardSize cap) s'); (Inr levelBits, s'b) \<in> fst (returnOk (radixBits + guardBits) s'a); (Inr y, s'c) \<in> fst (assertE (levelBits \<noteq> 0) s'b); (Inr offset, s'd) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits) s'c); (Inr slot, s'e) \<in> fst ((withoutFailure $ locateSlotCap cap offset) s'd); (Inr guard, s'f) \<in> fst (returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits) s'e); (Inr ya, s'g) \<in> fst ((unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits) s'f); (Inr yb, s'h) \<in> fst ((whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits) s'g); (Inr bitsLeft, s'i) \<in> fst (returnOk (depth - levelBits) s'h); bitsLeft \<noteq> 0; (Inr nextCap, sa) \<in> fst ((withoutFailure $ getSlotCap slot) s'i); s'j = sa\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. nextCap = capability.CNodeCap x xa xb xc \<longrightarrow> (isCNodeCap nextCap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = nextCap) slot sa)) \<and> valid_objs' sa \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of sa)) (gsCNodes sa)
 2. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E ((=) s) (throw Fault_H.lookup_failure.InvalidRoot) (?d6 s)
 3. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
ya <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
yb <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn nextCap cref bitsLeft \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else ?d6 s) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 4. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (4 subgoals):
 1. \<And>s cte x xa xb xc slot. \<lbrakk>isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s; (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; valid_objs' s; cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); cte_wp_at' ((=) cte) (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s; cteCap cte = capability.CNodeCap x xa xb xc; isCNodeCap (capability.CNodeCap x xa xb xc)\<rbrakk> \<Longrightarrow> \<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x xa xb xc) slot s
 2. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E ((=) s) (throw Fault_H.lookup_failure.InvalidRoot) (?d6 s)
 3. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
ya <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
yb <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn nextCap cref bitsLeft \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else ?d6 s) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 4. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E ((=) s) (throw Fault_H.lookup_failure.InvalidRoot) (?d6 s)
 2. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
ya <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
yb <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn nextCap cref bitsLeft \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else ?d6 s) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 3. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
ya <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
yb <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn nextCap cref bitsLeft \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else throw Fault_H.lookup_failure.InvalidRoot) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 2. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (if isCNodeCap cap then doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr cref `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr cref `~shiftR~` (depth - guardBits) && mask guardBits);
ya <- unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits;
yb <- whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits;
bitsLeft <- returnOk (depth - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn nextCap cref bitsLeft \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else throw Fault_H.lookup_failure.InvalidRoot) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap + capCNodeGuardSize cap = 0 then Inr (0, 0) else if \<not> (capCNodeGuardSize cap \<le> depth \<and> fromCPtr cref `~shiftR~` (depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) then Inl $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl $ Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap) else if depth - (capCNodeBits cap + capCNodeGuardSize cap) = 0 then Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 2. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<Longrightarrow> monadic_rewrite F E (?Q5 s) (if isCNodeCap cap then if 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap then do x <- get;
if (case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB then if capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap then if depth < capCNodeBits cap + capCNodeGuardSize cap then throwError (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then returnOk (global.capUntypedPtr cap + 2 ^ cte_level_bits * (cref && mask (capCNodeBits cap)), 0) else do cte <- getCTE (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)));
case cteCap cte of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn (cteCap cte) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap))
od else throwError (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else fail
od else fail else throwError Fault_H.lookup_failure.InvalidRoot) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 2. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and ?Q5 s) sa proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>(\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; \<not> depth < capCNodeBits cap + capCNodeGuardSize cap; depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R340 s x) (do cte <- getCTE (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)));
case cteCap cte of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn (cteCap cte) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap))
od) (gets ((\<lambda>caps. case caps (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps) \<circ> only_cnode_caps \<circ> ctes_of))
 2. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R317 s x) (throwError (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap))) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 3. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; \<not> ((case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R314 s x) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 4. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; \<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R299 s) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 5. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R296 s) (throwError Fault_H.lookup_failure.InvalidRoot) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 6. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and (\<lambda>sa. (isCNodeCap cap \<longrightarrow> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap \<longrightarrow> ((\<lambda>sa. ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB \<longrightarrow> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> (depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (\<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> (depth = capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> ?R340 s sa sa))) \<and> (\<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) \<longrightarrow> ?R317 s sa sa)) \<and> (\<not> ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) \<longrightarrow> ?R314 s sa sa)) and (\<lambda>_. True)) sa) \<and> (\<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) \<longrightarrow> ?R299 s sa)) \<and> (\<not> isCNodeCap cap \<longrightarrow> ?R296 s sa))) sa proof (prove)
goal (8 subgoals):
 1. \<And>s x. \<lbrakk>(\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; \<not> depth < capCNodeBits cap + capCNodeGuardSize cap; depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap\<rbrakk> \<Longrightarrow> empty_fail (getCTE (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))))
 2. \<And>s x. \<lbrakk>(\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; \<not> depth < capCNodeBits cap + capCNodeGuardSize cap; depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap\<rbrakk> \<Longrightarrow> \<not> F \<longrightarrow> no_fail (?P'371 s x) (getCTE (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))))
 3. \<And>s x cte. \<lbrakk>(\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; \<not> depth < capCNodeBits cap + capCNodeGuardSize cap; depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E (cte_wp_at' (\<lambda>c. c = cte) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)))) (case cteCap cte of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn (cteCap cte) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap))) (gets ((\<lambda>caps. case caps (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps) \<circ> only_cnode_caps \<circ> ctes_of))
 4. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R317 s x) (throwError (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap))) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 5. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; \<not> ((case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R314 s x) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 6. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; \<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R299 s) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 7. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R296 s) (throwError Fault_H.lookup_failure.InvalidRoot) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 8. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and (\<lambda>sa. (isCNodeCap cap \<longrightarrow> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap \<longrightarrow> ((\<lambda>sa. ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB \<longrightarrow> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> (depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (\<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> (depth = capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> ((\<lambda>_. True) and ?P'371 s sa) sa))) \<and> (\<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) \<longrightarrow> ?R317 s sa sa)) \<and> (\<not> ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) \<longrightarrow> ?R314 s sa sa)) and (\<lambda>_. True)) sa) \<and> (\<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) \<longrightarrow> ?R299 s sa)) \<and> (\<not> isCNodeCap cap \<longrightarrow> ?R296 s sa))) sa proof (prove)
goal (7 subgoals):
 1. \<And>s x. \<lbrakk>(\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; \<not> depth < capCNodeBits cap + capCNodeGuardSize cap; depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap\<rbrakk> \<Longrightarrow> \<not> F \<longrightarrow> no_fail (?P'371 s x) (getCTE (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))))
 2. \<And>s x cte. \<lbrakk>(\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; \<not> depth < capCNodeBits cap + capCNodeGuardSize cap; depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E (cte_wp_at' (\<lambda>c. c = cte) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)))) (case cteCap cte of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn (cteCap cte) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap))) (gets ((\<lambda>caps. case caps (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps) \<circ> only_cnode_caps \<circ> ctes_of))
 3. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R317 s x) (throwError (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap))) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 4. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; \<not> ((case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R314 s x) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 5. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; \<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R299 s) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 6. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R296 s) (throwError Fault_H.lookup_failure.InvalidRoot) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 7. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and (\<lambda>sa. (isCNodeCap cap \<longrightarrow> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap \<longrightarrow> ((\<lambda>sa. ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB \<longrightarrow> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> (depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (\<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> (depth = capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> ((\<lambda>_. True) and ?P'371 s sa) sa))) \<and> (\<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) \<longrightarrow> ?R317 s sa sa)) \<and> (\<not> ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) \<longrightarrow> ?R314 s sa sa)) and (\<lambda>_. True)) sa) \<and> (\<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) \<longrightarrow> ?R299 s sa)) \<and> (\<not> isCNodeCap cap \<longrightarrow> ?R296 s sa))) sa proof (prove)
goal (6 subgoals):
 1. \<And>s x cte. \<lbrakk>(\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; \<not> depth < capCNodeBits cap + capCNodeGuardSize cap; depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E (cte_wp_at' (\<lambda>c. c = cte) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)))) (case cteCap cte of capability.CNodeCap a b c d \<Rightarrow> gets (resolveAddressBitsFn (cteCap cte) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<circ> only_cnode_caps \<circ> ctes_of) | _ \<Rightarrow> returnOk (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap))) (gets ((\<lambda>caps. case caps (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps) \<circ> only_cnode_caps \<circ> ctes_of))
 2. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R317 s x) (throwError (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap))) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 3. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; \<not> ((case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R314 s x) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 4. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; \<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R299 s) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 5. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R296 s) (throwError Fault_H.lookup_failure.InvalidRoot) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 6. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and (\<lambda>sa. (isCNodeCap cap \<longrightarrow> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap \<longrightarrow> ((\<lambda>sa. ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB \<longrightarrow> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> (depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (\<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> (depth = capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> ((\<lambda>_. True) and cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)))) sa))) \<and> (\<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) \<longrightarrow> ?R317 s sa sa)) \<and> (\<not> ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) \<longrightarrow> ?R314 s sa sa)) and (\<lambda>_. True)) sa) \<and> (\<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) \<longrightarrow> ?R299 s sa)) \<and> (\<not> isCNodeCap cap \<longrightarrow> ?R296 s sa))) sa proof (prove)
goal (5 subgoals):
 1. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R317 s x) (throwError (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap))) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 2. \<And>s x. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; \<not> ((case gsCNodes x (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R314 s x) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 3. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); isCNodeCap cap; \<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap)\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R299 s) fail (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 4. \<And>s. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); \<not> isCNodeCap cap\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?R296 s) (throwError Fault_H.lookup_failure.InvalidRoot) (gets ((\<lambda>caps. if isCNodeCap cap then if capCNodeBits cap = 0 \<and> capCNodeGuardSize cap = 0 then Inr (0, 0) else if capCNodeGuardSize cap \<le> depth \<longrightarrow> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) \<noteq> capCNodeGuard cap then Inl (Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) (capCNodeGuardSize cap)) else if depth < capCNodeBits cap + capCNodeGuardSize cap then Inl (Fault_H.lookup_failure.DepthMismatch depth (capCNodeBits cap + capCNodeGuardSize cap)) else if depth = capCNodeBits cap + capCNodeGuardSize cap then Inr (locateSlotFun (capCNodePtr cap) (cref && mask (capCNodeBits cap)), 0) else case caps (locateSlotFun (capCNodePtr cap) ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) of None \<Rightarrow> Inr (0, 0) | Some (capability.ThreadCap word) \<Rightarrow> resolveAddressBitsFn (capability.ThreadCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.NullCap \<Rightarrow> Inr (locateSlotFun (capCNodePtr cap) (fromCPtr cref `~shiftR~` (depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)), depth - (capCNodeBits cap + capCNodeGuardSize cap)) | Some (capability.NotificationCap word1 word2 bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.NotificationCap word1 word2 bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.IRQHandlerCap word) \<Rightarrow> resolveAddressBitsFn (capability.IRQHandlerCap word) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) \<Rightarrow> resolveAddressBitsFn (capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.DomainCap \<Rightarrow> resolveAddressBitsFn capability.DomainCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.Zombie word zombie_type nat) \<Rightarrow> resolveAddressBitsFn (capability.Zombie word zombie_type nat) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ArchObjectCap arch_capability) \<Rightarrow> resolveAddressBitsFn (capability.ArchObjectCap arch_capability) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.ReplyCap word bool1 bool2) \<Rightarrow> resolveAddressBitsFn (capability.ReplyCap word bool1 bool2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.UntypedCap bool word nat1 nat2) \<Rightarrow> resolveAddressBitsFn (capability.UntypedCap bool word nat1 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some (capability.CNodeCap word1 nat1 word2 nat2) \<Rightarrow> resolveAddressBitsFn (capability.CNodeCap word1 nat1 word2 nat2) cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps | Some capability.IRQControlCap \<Rightarrow> resolveAddressBitsFn capability.IRQControlCap cref (depth - (capCNodeBits cap + capCNodeGuardSize cap)) caps else Inl Fault_H.lookup_failure.InvalidRoot) \<circ> only_cnode_caps \<circ> ctes_of))
 5. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); s = sa\<rbrakk> \<Longrightarrow> ((=) s and (\<lambda>sa. (isCNodeCap cap \<longrightarrow> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap \<longrightarrow> ((\<lambda>sa. ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB \<longrightarrow> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> (depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (\<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> (depth = capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True) \<and> (depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> ((\<lambda>_. True) and cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)))) sa))) \<and> (\<not> (capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) \<longrightarrow> ?R317 s sa sa)) \<and> (\<not> ((case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) \<longrightarrow> ?R314 s sa sa)) and (\<lambda>_. True)) sa) \<and> (\<not> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) \<longrightarrow> ?R299 s sa)) \<and> (\<not> isCNodeCap cap \<longrightarrow> ?R296 s sa))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot sa)) \<and> valid_objs' sa \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of sa)) (gsCNodes sa); s = sa\<rbrakk> \<Longrightarrow> isCNodeCap cap \<longrightarrow> (0 < capCNodeBits cap \<longrightarrow> ((case gsCNodes sa (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> (isThreadCap cap \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> (isZombie cap \<and> capZombieType cap = ZombieTCB \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> ((case gsCNodes sa (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB)) \<and> (0 < capCNodeGuardSize cap \<longrightarrow> ((case gsCNodes sa (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> (isThreadCap cap \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> (isZombie cap \<and> capZombieType cap = ZombieTCB \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> ((case gsCNodes sa (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB)) \<and> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot sa)) \<and> valid_objs' sa \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of sa)) (gsCNodes sa); s = sa\<rbrakk> \<Longrightarrow> isCNodeCap cap \<longrightarrow> (0 < capCNodeBits cap \<longrightarrow> ((case gsCNodes sa (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> (isThreadCap cap \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> (isZombie cap \<and> capZombieType cap = ZombieTCB \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> ((case gsCNodes sa (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB)) \<and> (0 < capCNodeGuardSize cap \<longrightarrow> ((case gsCNodes sa (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> (isThreadCap cap \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> (isZombie cap \<and> capZombieType cap = ZombieTCB \<longrightarrow> capCNodeGuardSize cap \<le> depth \<and> (cref >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> \<not> depth < capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> depth \<noteq> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cte_level_bits * ((cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) sa) \<and> ((case gsCNodes sa (capCNodePtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> (cref >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB)) \<and> (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) proof (prove)
goal (1 subgoal):
 1. \<And>sa v0 v1 v2 v3 slot. \<lbrakk>valid_objs' sa; cnode_caps_gsCNodes (only_cnode_caps (ctes_of sa)) (gsCNodes sa); cap = capability.CNodeCap v0 v1 v2 v3; cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap v0 v1 v2 v3) slot sa\<rbrakk> \<Longrightarrow> (0 < v1 \<longrightarrow> ((case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n) \<longrightarrow> v3 \<le> depth \<and> (cref >> depth - v3) && mask v3 = v2 \<longrightarrow> \<not> depth < v1 + v3 \<longrightarrow> depth \<noteq> v1 + v3 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (v0 + 2 ^ cte_level_bits * ((cref >> depth - (v1 + v3)) && mask v1)) sa) \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n)) \<and> (0 < v3 \<longrightarrow> ((case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n) \<longrightarrow> v3 \<le> depth \<and> (cref >> depth - v3) && mask v3 = v2 \<longrightarrow> \<not> depth < v1 + v3 \<longrightarrow> depth \<noteq> v1 + v3 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (v0 + 2 ^ cte_level_bits * ((cref >> depth - (v1 + v3)) && mask v1)) sa) \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n)) \<and> (0 < v1 \<or> 0 < v3) proof (prove)
goal (1 subgoal):
 1. \<And>sa v0 v1 v2 v3 slot. \<lbrakk>valid_objs' sa; cnode_caps_gsCNodes (only_cnode_caps (ctes_of sa)) (gsCNodes sa); cap = capability.CNodeCap v0 v1 v2 v3; cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap v0 v1 v2 v3) slot sa; \<exists>cte. cteCap cte = capability.CNodeCap v0 v1 v2 v3 \<and> valid_cap' (cteCap cte) sa\<rbrakk> \<Longrightarrow> (0 < v1 \<longrightarrow> ((case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n) \<longrightarrow> v3 \<le> depth \<and> (cref >> depth - v3) && mask v3 = v2 \<longrightarrow> \<not> depth < v1 + v3 \<longrightarrow> depth \<noteq> v1 + v3 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (v0 + 2 ^ cte_level_bits * ((cref >> depth - (v1 + v3)) && mask v1)) sa) \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n)) \<and> (0 < v3 \<longrightarrow> ((case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n) \<longrightarrow> v3 \<le> depth \<and> (cref >> depth - v3) && mask v3 = v2 \<longrightarrow> \<not> depth < v1 + v3 \<longrightarrow> depth \<noteq> v1 + v3 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (v0 + 2 ^ cte_level_bits * ((cref >> depth - (v1 + v3)) && mask v1)) sa) \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n)) \<and> (0 < v1 \<or> 0 < v3) proof (prove)
goal (1 subgoal):
 1. \<And>sa v0 v1 v2 v3 slot cte. \<lbrakk>valid_objs' sa; cnode_caps_gsCNodes (only_cnode_caps (ctes_of sa)) (gsCNodes sa); cap = capability.CNodeCap v0 v1 v2 v3; cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap v0 v1 v2 v3) slot sa; cteCap cte = capability.CNodeCap v0 v1 v2 v3; capAligned (capability.CNodeCap v0 v1 v2 v3); 0 < v1; v1 + v3 \<le> word_bits; v2 && mask v3 = v2; \<forall>addr. real_cte_at' (v0 + 0x10 * (addr && mask v1)) sa\<rbrakk> \<Longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n) \<and> (0 < v3 \<longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n)) proof (prove)
goal (1 subgoal):
 1. \<And>sa v0 v1 v2 v3 slot cte ctea. \<lbrakk>valid_objs' sa; \<forall>cap\<in>ran (ctes_of sa) \<inter> {x. isCNodeCap (cteCap x)}. gsCNodes sa (capCNodePtr (cteCap cap)) = Some (capCNodeBits (cteCap cap)); cap = capability.CNodeCap v0 v1 v2 v3; cteCap cte = capability.CNodeCap v0 v1 v2 v3; capAligned (capability.CNodeCap v0 v1 v2 v3); 0 < v1; v1 + v3 \<le> word_bits; v2 && mask v3 = v2; \<forall>addr. real_cte_at' (v0 + 0x10 * (addr && mask v1)) sa; ctes_of sa slot = Some ctea; cteCap ctea = capability.CNodeCap v0 v1 v2 v3\<rbrakk> \<Longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n) \<and> (0 < v3 \<longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n)) proof (prove)
goal (1 subgoal):
 1. \<And>sa v0 v1 v2 v3 slot cte ctea. \<lbrakk>valid_objs' sa; cap = capability.CNodeCap v0 v1 v2 v3; cteCap cte = capability.CNodeCap v0 v1 v2 v3; capAligned (capability.CNodeCap v0 v1 v2 v3); 0 < v1; v1 + v3 \<le> word_bits; v2 && mask v3 = v2; \<forall>addr. real_cte_at' (v0 + 0x10 * (addr && mask v1)) sa; ctes_of sa slot = Some ctea; cteCap ctea = capability.CNodeCap v0 v1 v2 v3; gsCNodes sa (capCNodePtr (cteCap ctea)) = Some (capCNodeBits (cteCap ctea))\<rbrakk> \<Longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n) \<and> (0 < v3 \<longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> (cref >> depth - (v1 + v3)) && mask v1 < 2 ^ n)) proof (prove)
goal:
No subgoals! proof (state)
this:
monadic_rewrite F E (\<lambda>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) (CSpace_H.resolveAddressBits cap cref depth) (gets (resolveAddressBitsFn cap cref depth \<circ> only_cnode_caps \<circ> ctes_of))

goal:
No subgoals!