theory CSpace1_R

lemma resolveAddressBits_real_cte_at':
  "\<lbrace> valid_objs' and valid_cap' cap \<rbrace>
  resolveAddressBits cap addr depth
  \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -" proof (induct rule: resolveAddressBits.induct) case (1 cap addr depth) show ?case apply (clarsimp simp: validE_def validE_R_def valid_def split: sum.split) apply (subst (asm) resolveAddressBits.simps) apply (simp only: Let_def split: if_split_asm) prefer 2 apply (simp add: in_monad) apply (simp only: in_bindE_R K_bind_def) apply (elim exE conjE) apply (simp only: split: if_split_asm) apply (clarsimp simp: in_monad locateSlot_conv stateAssert_def) apply (cases cap) apply (simp_all add: isCap_defs)[12] apply (clarsimp simp add: valid_cap'_def objBits_simps' cte_level_bits_def
                        split: option.split_asm) apply (simp only: in_bindE_R K_bind_def) apply (elim exE conjE) apply (simp only: cap_case_CNodeCap split: if_split_asm) apply (drule_tac cap=nextCap in isCapDs(4), elim exE) apply (simp only: in_bindE_R K_bind_def) apply (frule (12) 1 [OF refl], (assumption | rule refl)+) apply (clarsimp simp: in_monad locateSlot_conv objBits_simps stateAssert_def) apply (cases cap) apply (simp_all add: isCap_defs)[12] apply (frule in_inv_by_hoareD [OF getSlotCap_inv]) apply simp apply (frule (1) post_by_hoare [OF getSlotCap_valid_cap]) apply (simp add: valid_def validE_def validE_R_def) apply (erule allE, erule impE, blast) apply (drule (1) bspec) apply simp apply (clarsimp simp: in_monad locateSlot_conv objBits_simps stateAssert_def) apply (cases cap) apply (simp_all add: isCap_defs)[12] apply (frule in_inv_by_hoareD [OF getSlotCap_inv]) apply (clarsimp simp: valid_cap'_def cte_level_bits_def objBits_defs) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> CSpace_H.resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, - 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> \<lbrace>valid_objs' and valid_cap' rve\<rbrace> CSpace_H.resolveAddressBits rve b rvd \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -) \<Longrightarrow> \<lbrace>valid_objs' and valid_cap' a\<rbrace> CSpace_H.resolveAddressBits a b c \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, - 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 addr `~shiftR~` (depth - ?rva) && mask ?v) ?stb); (Inr ?rvbb, ?std) \<in> fst ((withoutFailure $ locateSlotCap ?x ?rvba) ?stc); (Inr ?rvbc, ?ste) \<in> fst (returnOk (fromCPtr addr `~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> \<lbrace>valid_objs' and valid_cap' ?rve\<rbrace> CSpace_H.resolveAddressBits ?rve addr ?rvd \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -

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> \<lbrace>valid_objs' and valid_cap' rve\<rbrace> CSpace_H.resolveAddressBits rve b rvd \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -) \<Longrightarrow> \<lbrace>valid_objs' and valid_cap' a\<rbrace> CSpace_H.resolveAddressBits a b c \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> CSpace_H.resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba. \<lbrakk>(Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits cap addr depth s); valid_objs' s; valid_cap' cap s\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba. \<lbrakk>(Inr (aa, ba), b) \<in> fst ((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 addr `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap nodeCap offset;
guard <- returnOk (fromCPtr addr `~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 addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else throw Fault_H.lookup_failure.InvalidRoot) s); valid_objs' s; valid_cap' cap s\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; (Inr (aa, ba), b) \<in> fst ((doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
haskell_assertE (levelBits \<noteq> 0) [];
offset <- returnOk (fromCPtr addr `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr addr `~shiftR~` (depth - guardBits) && mask guardBits);
unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) 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 addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE) s)\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba. \<lbrakk>valid_objs' s; valid_cap' cap s; \<not> isCNodeCap cap; (Inr (aa, ba), b) \<in> fst (throw Fault_H.lookup_failure.InvalidRoot s)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba. \<lbrakk>valid_objs' s; valid_cap' cap s; \<not> isCNodeCap cap; (Inr (aa, ba), b) \<in> fst (throw Fault_H.lookup_failure.InvalidRoot s)\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; (Inr (aa, ba), b) \<in> fst ((doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
haskell_assertE (levelBits \<noteq> 0) [];
offset <- returnOk (fromCPtr addr `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr addr `~shiftR~` (depth - guardBits) && mask guardBits);
unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) 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 addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE) s)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; (Inr (aa, ba), b) \<in> fst ((doE radixBits <- returnOk (capCNodeBits cap);
guardBits <- returnOk (capCNodeGuardSize cap);
levelBits <- returnOk (radixBits + guardBits);
haskell_assertE (levelBits \<noteq> 0) [];
offset <- returnOk (fromCPtr addr `~shiftR~` (depth - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap cap offset;
guard <- returnOk (fromCPtr addr `~shiftR~` (depth - guardBits) && mask guardBits);
unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) 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 addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE) s)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; \<exists>s'' radixBits. (Inr radixBits, s'') \<in> fst (returnOk (capCNodeBits cap) s) \<and> (\<exists>s''a guardBits. (Inr guardBits, s''a) \<in> fst (returnOk (capCNodeGuardSize cap) s'') \<and> (\<exists>s'' levelBits. (Inr levelBits, s'') \<in> fst (returnOk (radixBits + guardBits) s''a) \<and> (\<exists>s''a y. (Inr y, s''a) \<in> fst (haskell_assertE (levelBits \<noteq> 0) [] s'') \<and> (\<exists>s'' offset. (Inr offset, s'') \<in> fst (returnOk (fromCPtr addr `~shiftR~` (depth - levelBits) && mask radixBits) s''a) \<and> (\<exists>s''a slot. (Inr slot, s''a) \<in> fst ((withoutFailure $ locateSlotCap cap offset) s'') \<and> (\<exists>s'' guard. (Inr guard, s'') \<in> fst (returnOk (fromCPtr addr `~shiftR~` (depth - guardBits) && mask guardBits) s''a) \<and> (\<exists>s''a y. (Inr y, s''a) \<in> fst ((unlessE (guardBits \<le> depth \<and> guard = capCNodeGuard cap) $ throw $ Fault_H.lookup_failure.GuardMismatch depth (capCNodeGuard cap) guardBits) s'') \<and> (\<exists>s'' y. (Inr y, s'') \<in> fst ((whenE (depth < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch depth levelBits) s''a) \<and> (\<exists>s''a bitsLeft. (Inr bitsLeft, s''a) \<in> fst (returnOk (depth - levelBits) s'') \<and> (Inr (aa, ba), b) \<in> fst ((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 addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE) s''a))))))))))\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); (Inr (aa, ba), b) \<in> fst ((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 addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE) s''i)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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 0, s''i) \<in> fst (returnOk (depth - levelBits) s''h); bitsLeft = 0; (Inr (aa, ba), b) \<in> fst (returnOk (slot, 0) s''i)\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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 (aa, ba), b) \<in> fst ((doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE) s''i)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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 (aa, ba), b) \<in> fst ((doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE) s''i)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (13 subgoals):
 1. \<And>s x1. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 2. \<And>s. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.NullCap\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 3. \<And>s x31 x32 x33 x34. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 4. \<And>s x4. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 5. \<And>s x51 x52 x53 x54 x55 x56. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 6. \<And>s. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.DomainCap\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 7. \<And>s x71 x72 x73. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 8. \<And>s x8. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 9. \<And>s x91 x92 x93. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
 10. \<And>s x101 x102 x103 x104. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> addr && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; (addr >> capCNodeBits cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; depth = capCNodeBits cap + capCNodeGuardSize cap; cap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * (addr && mask (capCNodeBits cap))) s
A total of 13 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>s x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> addr && mask x112 < 2 ^ n; (addr >> x112) && mask x114 = x113; depth = x112 + x114; cap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> real_cte_at' (x111 + 2 ^ cte_level_bits * (addr && mask x112)) s
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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 (aa, ba), b) \<in> fst ((doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE) s''i)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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 (aa, ba), b) \<in> fst ((doE nextCap <- withoutFailure $ getSlotCap slot;
case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE) s''i)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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; \<exists>s'' nextCap. (Inr nextCap, s'') \<in> fst ((withoutFailure $ getSlotCap slot) s''i) \<and> (Inr (aa, ba), b) \<in> fst ((case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)) s'')\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); (Inr (aa, ba), b) \<in> fst ((case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap addr bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits nextCap addr bitsLeft s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap ptr bits grd gsize. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits nextCap addr bitsLeft s''j); nextCap = capability.CNodeCap ptr bits grd gsize\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap ptr bits grd gsize. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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 (capability.CNodeCap ptr bits grd gsize), s''j) \<in> fst ((withoutFailure $ getSlotCap slot) s''i); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr bitsLeft s''j); nextCap = capability.CNodeCap ptr bits grd gsize\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap ptr bits grd gsize. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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 (capability.CNodeCap ptr bits grd gsize), s''j) \<in> fst ((withoutFailure $ getSlotCap slot) s''i); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr bitsLeft s''j); nextCap = capability.CNodeCap ptr bits grd gsize; \<lbrace>valid_objs' and valid_cap' (capability.CNodeCap ptr bits grd gsize)\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr bitsLeft \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s''j ptr bits grd gsize. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (13 subgoals):
 1. \<And>s b aa ba s''j ptr bits grd gsize x1. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s''j ptr bits grd gsize. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.NullCap\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 3. \<And>s b aa ba s''j ptr bits grd gsize x31 x32 x33 x34. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 4. \<And>s b aa ba s''j ptr bits grd gsize x4. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 5. \<And>s b aa ba s''j ptr bits grd gsize x51 x52 x53 x54 x55 x56. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 6. \<And>s b aa ba s''j ptr bits grd gsize. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.DomainCap\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 7. \<And>s b aa ba s''j ptr bits grd gsize x71 x72 x73. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 8. \<And>s b aa ba s''j ptr bits grd gsize x8. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 9. \<And>s b aa ba s''j ptr bits grd gsize x91 x92 x93. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 10. \<And>s b aa ba s''j ptr bits grd gsize x101 x102 x103 x104. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> real_cte_at' aa b
A total of 13 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s''j ptr bits grd gsize x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> (addr >> depth - (x112 + x114)) && mask x112 < 2 ^ n; \<not> depth \<le> x112 + x114; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - x114) && mask x114 = x113; cap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s''j ptr bits grd gsize x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> (addr >> depth - (x112 + x114)) && mask x112 < 2 ^ n; \<not> depth \<le> x112 + x114; (capability.CNodeCap ptr bits grd gsize, s''j) \<in> fst (getSlotCap (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) s''j); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - x114) && mask x114 = x113; cap = capability.CNodeCap x111 x112 x113 x114; s''j = s\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s''j ptr bits grd gsize x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> (addr >> depth - (x112 + x114)) && mask x112 < 2 ^ n; \<not> depth \<le> x112 + x114; (capability.CNodeCap ptr bits grd gsize, s) \<in> fst (getSlotCap (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) s); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - x114) && mask x114 = x113; cap = capability.CNodeCap x111 x112 x113 x114; s''j = s\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s''j ptr bits grd gsize x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> (addr >> depth - (x112 + x114)) && mask x112 < 2 ^ n; \<not> depth \<le> x112 + x114; (capability.CNodeCap ptr bits grd gsize, s) \<in> fst (getSlotCap (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) s); \<lbrace>\<lambda>a. valid_objs' a \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) a\<rbrace> CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -; (addr >> depth - x114) && mask x114 = x113; cap = capability.CNodeCap x111 x112 x113 x114; s''j = s; (valid_cap' (capability.CNodeCap ptr bits grd gsize) and cte_wp_at' (\<lambda>_. True) (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112))) s\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s''j ptr bits grd gsize x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> (addr >> depth - (x112 + x114)) && mask x112 < 2 ^ n; \<not> depth \<le> x112 + x114; (capability.CNodeCap ptr bits grd gsize, s) \<in> fst (getSlotCap (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) s); \<forall>s. valid_objs' s \<and> valid_cap' (capability.CNodeCap ptr bits grd gsize) s \<longrightarrow> (\<forall>x\<in>fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) s). case x of (r, s') \<Rightarrow> \<forall>a. (\<exists>b. r = Inr (a, b)) \<longrightarrow> real_cte_at' a s'); (addr >> depth - x114) && mask x114 = x113; cap = capability.CNodeCap x111 x112 x113 x114; s''j = s; valid_cap' (capability.CNodeCap ptr bits grd gsize) s \<and> cte_wp_at' (\<lambda>_. True) (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s''j ptr bits grd gsize x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> (addr >> depth - (x112 + x114)) && mask x112 < 2 ^ n; \<not> depth \<le> x112 + x114; (capability.CNodeCap ptr bits grd gsize, s) \<in> fst (getSlotCap (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) s); (addr >> depth - x114) && mask x114 = x113; cap = capability.CNodeCap x111 x112 x113 x114; s''j = s; valid_cap' (capability.CNodeCap ptr bits grd gsize) s \<and> cte_wp_at' (\<lambda>_. True) (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s; \<forall>x\<in>fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) s). case x of (r, s') \<Rightarrow> \<forall>a. (\<exists>b. r = Inr (a, b)) \<longrightarrow> real_cte_at' a s'\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba s''j ptr bits grd gsize x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> (addr >> depth - (x112 + x114)) && mask x112 < 2 ^ n; \<not> depth \<le> x112 + x114; (capability.CNodeCap ptr bits grd gsize, s) \<in> fst (getSlotCap (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s); (Inr (aa, ba), b) \<in> fst (CSpace_H.resolveAddressBits (capability.CNodeCap ptr bits grd gsize) addr (depth - (x112 + x114)) s); (addr >> depth - x114) && mask x114 = x113; cap = capability.CNodeCap x111 x112 x113 x114; s''j = s; valid_cap' (capability.CNodeCap ptr bits grd gsize) s \<and> cte_wp_at' (\<lambda>_. True) (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s; case (Inr (aa, ba), b) of (r, s') \<Rightarrow> \<forall>a. (\<exists>b. r = Inr (a, b)) \<longrightarrow> real_cte_at' a s'\<rbrakk> \<Longrightarrow> real_cte_at' aa b
 2. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba s'' radixBits s''a guardBits s''b levelBits s''c y s''d offset s''e slot s''f guard s''g ya s''h yb s''i bitsLeft s''j nextCap. \<lbrakk>valid_objs' s; valid_cap' cap 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 (haskell_assertE (levelBits \<noteq> 0) [] s''b); (Inr offset, s''d) \<in> fst (returnOk (fromCPtr addr `~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 addr `~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); \<not> isCNodeCap nextCap; (Inr (aa, ba), b) \<in> fst (returnOk (slot, bitsLeft) s''j)\<rbrakk> \<Longrightarrow> real_cte_at' aa b proof (prove)
goal (1 subgoal):
 1. \<And>s b nextCap. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b proof (prove)
goal (12 subgoals):
 1. \<And>s b nextCap x1. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
 2. \<And>s b nextCap. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.NullCap\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
 3. \<And>s b nextCap x31 x32 x33 x34. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
 4. \<And>s b nextCap x4. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
 5. \<And>s b nextCap x51 x52 x53 x54 x55 x56. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
 6. \<And>s b nextCap. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.DomainCap\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
 7. \<And>s b nextCap x71 x72 x73. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
 8. \<And>s b nextCap x8. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
 9. \<And>s b nextCap x91 x92 x93. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
 10. \<And>s b nextCap x101 x102 x103 x104. \<lbrakk>valid_objs' s; valid_cap' cap s; isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize 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> (addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap) < 2 ^ n) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB; \<not> depth \<le> capCNodeBits cap + capCNodeGuardSize cap; (nextCap, b) \<in> fst (getSlotCap (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s); \<not> isCNodeCap nextCap; (addr >> depth - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap; cap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> real_cte_at' (global.capUntypedPtr cap + 2 ^ cte_level_bits * ((addr >> depth - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) b
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s b nextCap x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> (addr >> depth - (x112 + x114)) && mask x112 < 2 ^ n; \<not> depth \<le> x112 + x114; (nextCap, b) \<in> fst (getSlotCap (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s); \<not> (case nextCap of capability.CNodeCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False); (addr >> depth - x114) && mask x114 = x113; cap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> real_cte_at' (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) b proof (prove)
goal (1 subgoal):
 1. \<And>s b nextCap x111 x112 x113 x114. \<lbrakk>valid_objs' s; valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; 0 < x112 \<or> 0 < x114; case gsCNodes s x111 of None \<Rightarrow> False | Some n \<Rightarrow> n = x112 \<and> (addr >> depth - (x112 + x114)) && mask x112 < 2 ^ n; \<not> depth \<le> x112 + x114; (nextCap, b) \<in> fst (getSlotCap (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) s); \<not> (case nextCap of capability.CNodeCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False); (addr >> depth - x114) && mask x114 = x113; cap = capability.CNodeCap x111 x112 x113 x114; b = s\<rbrakk> \<Longrightarrow> real_cte_at' (x111 + 2 ^ cte_level_bits * ((addr >> depth - (x112 + x114)) && mask x112)) b proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>valid_objs' and valid_cap' cap\<rbrace> CSpace_H.resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -

goal:
No subgoals!