theory Move_C

lemma empty_fail_resolveAddressBits:
  "empty_fail (resolveAddressBits cap cptr bits)" proof - note empty_fail_cond[simp] show ?thesis apply (rule empty_fail_use_cutMon) apply (induct rule: resolveAddressBits.induct) apply (subst resolveAddressBits.simps) apply (unfold Let_def cnode_cap_case_if fun_app_def
                K_bind_def haskell_assertE_def split_def) apply (intro empty_fail_cutMon_intros) apply (clarsimp simp: empty_fail_drop_cutMon locateSlot_conv returnOk_liftE[symmetric]
                        isCap_simps)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (CSpace_H.resolveAddressBits cap cptr bits) proof (state)
goal (1 subgoal):
 1. empty_fail (CSpace_H.resolveAddressBits cap cptr bits) proof (state)
this:
empty_fail ?f \<Longrightarrow> empty_fail (K_bind ?f ?x)
empty_fail (?f ?x) \<Longrightarrow> empty_fail (?f $ ?x)
\<lbrakk>?P \<Longrightarrow> empty_fail ?f; \<not> ?P \<Longrightarrow> empty_fail ?g\<rbrakk> \<Longrightarrow> empty_fail (if ?P then ?f else ?g)
\<lbrakk>?P \<Longrightarrow> empty_fail (?f ?x); \<not> ?P \<Longrightarrow> empty_fail (?g ?x)\<rbrakk> \<Longrightarrow> empty_fail ((if ?P then ?f else ?g) ?x)
?S \<noteq> {} \<Longrightarrow> empty_fail (select ?S)
(fst ?S = {} \<Longrightarrow> snd ?S) \<Longrightarrow> empty_fail (select_f ?S)
\<lbrakk>empty_fail ?a; \<And>x. empty_fail (?b x)\<rbrakk> \<Longrightarrow> empty_fail (?a >>= ?b)
(\<And>x. empty_fail (?f x)) \<Longrightarrow> empty_fail (lift ?f ?x)
empty_fail ?f \<Longrightarrow> empty_fail (liftE ?f)
\<lbrakk>empty_fail ?f; \<And>rv. empty_fail (?g rv)\<rbrakk> \<Longrightarrow> empty_fail (?f >>=E ?g)
(\<And>x. x \<in> set ?xs \<Longrightarrow> empty_fail (?m x)) \<Longrightarrow> empty_fail (mapM ?m ?xs)
(?P \<Longrightarrow> empty_fail ?f) \<Longrightarrow> empty_fail (whenE ?P ?f)
(\<not> ?P \<Longrightarrow> empty_fail ?f) \<Longrightarrow> empty_fail (unlessE ?P ?f)
\<lbrakk>empty_fail ?f; \<And>x. empty_fail (?g x)\<rbrakk> \<Longrightarrow> empty_fail (?f <catch> ?g)
(?P \<Longrightarrow> empty_fail ?x) \<Longrightarrow> empty_fail (when ?P ?x)
(\<not> ?P \<Longrightarrow> empty_fail ?f) \<Longrightarrow> empty_fail (unless ?P ?f)
empty_fail ?m \<Longrightarrow> empty_fail (liftM ?f ?m)
empty_fail ?m \<Longrightarrow> empty_fail (liftME ?f ?m)
\<lbrakk>empty_fail ?L; \<And>r. empty_fail (?R r)\<rbrakk> \<Longrightarrow> empty_fail (?L <handle> ?R)
\<lbrakk>empty_fail ?f; \<And>e. empty_fail (?handler e)\<rbrakk> \<Longrightarrow> empty_fail (?f <handle2> ?handler)
(\<And>m. m \<in> set ?ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence ?ms)
(\<And>m. m \<in> set ?ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence_x ?ms)
(\<And>m. m \<in> set ?ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE ?ms)
(\<And>m. m \<in> set ?ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE_x ?ms)
(\<And>m. m \<in> ?f ` set ?ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapM_x ?f ?ms)
(\<And>m. m \<in> ?f ` set ?xs \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapME ?f ?xs)
(\<And>m'. m' \<in> ?f ` set ?xs \<Longrightarrow> empty_fail m') \<Longrightarrow> empty_fail (mapME_x ?f ?xs)
(\<And>m. m \<in> set ?ms \<Longrightarrow> empty_fail (?P m)) \<Longrightarrow> empty_fail (filterM ?P ?ms)
(\<And>x y. empty_fail (?f x y)) \<Longrightarrow> empty_fail (zipWithM_x ?f ?xs ?ys)
(\<And>x y. empty_fail (?f x y)) \<Longrightarrow> empty_fail (zipWithM ?f ?xs ?ys)
\<forall>x. empty_fail (?f x) \<Longrightarrow> empty_fail (maybeM ?f ?t)
\<lbrakk>empty_fail ?P; empty_fail ?a; empty_fail ?b\<rbrakk> \<Longrightarrow> empty_fail (ifM ?P ?a ?b)
\<lbrakk>empty_fail ?P; empty_fail ?a; empty_fail ?b\<rbrakk> \<Longrightarrow> empty_fail (ifME ?P ?a ?b)
\<lbrakk>empty_fail ?P; empty_fail ?f\<rbrakk> \<Longrightarrow> empty_fail (whenM ?P ?f)
\<lbrakk>empty_fail ?A; empty_fail ?B\<rbrakk> \<Longrightarrow> empty_fail (andM ?A ?B)
\<lbrakk>empty_fail ?A; empty_fail ?B\<rbrakk> \<Longrightarrow> empty_fail (orM ?A ?B)
empty_fail ?A \<Longrightarrow> empty_fail (notM ?A)
(\<And>r. empty_fail (?B r)) \<Longrightarrow> empty_fail (whileLoop ?C
  ?B ?r)
(\<And>r. empty_fail (?B r)) \<Longrightarrow> empty_fail (whileLoopE ?C
  ?B ?r)
\<lbrakk>empty_fail ?C; empty_fail ?B\<rbrakk> \<Longrightarrow> empty_fail (whileM ?C ?B)

goal (1 subgoal):
 1. empty_fail (CSpace_H.resolveAddressBits cap cptr bits) proof (prove)
goal (1 subgoal):
 1. empty_fail (CSpace_H.resolveAddressBits cap cptr bits) proof (prove)
goal (1 subgoal):
 1. \<And>s. empty_fail (cutMon ((=) s) (CSpace_H.resolveAddressBits cap cptr bits)) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s. (\<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 sa. \<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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd))) \<Longrightarrow> empty_fail (cutMon ((=) s) (CSpace_H.resolveAddressBits a b c)) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s. (\<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 sa. \<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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd))) \<Longrightarrow> empty_fail (cutMon ((=) s) (let nodeCap = a 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 b `~shiftR~` (c - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap nodeCap offset;
guard <- returnOk (fromCPtr b `~shiftR~` (c - guardBits) && mask guardBits);
unlessE (guardBits \<le> c \<and> guard = capCNodeGuard nodeCap) $ throw $ Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard nodeCap) guardBits;
whenE (c < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch c levelBits;
bitsLeft <- returnOk (c - 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 b bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (1 subgoal):
 1. \<And>a b c s. (\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd))) \<Longrightarrow> empty_fail (cutMon ((=) s) (if isCNodeCap a then doE radixBits <- returnOk (capCNodeBits a);
guardBits <- returnOk (capCNodeGuardSize a);
levelBits <- returnOk (radixBits + guardBits);
y <- assertE (levelBits \<noteq> 0);
offset <- returnOk (fromCPtr b `~shiftR~` (c - levelBits) && mask radixBits);
slot <- withoutFailure (locateSlotCap a offset);
guard <- returnOk (fromCPtr b `~shiftR~` (c - guardBits) && mask guardBits);
y <- unlessE (guardBits \<le> c \<and> guard = capCNodeGuard a) (throw (Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard a) guardBits));
y <- whenE (c < levelBits) (throw (Fault_H.lookup_failure.DepthMismatch c levelBits));
bitsLeft <- returnOk (c - levelBits);
if bitsLeft = 0 then returnOk (slot, 0) else doE nextCap <- withoutFailure (getSlotCap slot);
if isCNodeCap nextCap then CSpace_H.resolveAddressBits nextCap b bitsLeft else returnOk (slot, bitsLeft)
odE
odE else throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (15 subgoals):
 1. \<And>a b c s. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) s) (returnOk (capCNodeBits a)))
 2. \<And>a b c s rv sa. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a; (Inr rv, sa) \<in> fst (returnOk (capCNodeBits a) s)\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) sa) (returnOk (capCNodeGuardSize a)))
 3. \<And>a b c s rv sa rva sb. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a; (Inr rv, sa) \<in> fst (returnOk (capCNodeBits a) s); (Inr rva, sb) \<in> fst (returnOk (capCNodeGuardSize a) sa)\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) sb) (returnOk (rv + rva)))
 4. \<And>a b c s rv sa rva sb rvb sc. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a; (Inr rv, sa) \<in> fst (returnOk (capCNodeBits a) s); (Inr rva, sb) \<in> fst (returnOk (capCNodeGuardSize a) sa); (Inr rvb, sc) \<in> fst (returnOk (rv + rva) sb)\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) sc) (assertE (rvb \<noteq> 0)))
 5. \<And>a b c s rv sa rva sb rvb sc rvc sd. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a; (Inr rv, sa) \<in> fst (returnOk (capCNodeBits a) s); (Inr rva, sb) \<in> fst (returnOk (capCNodeGuardSize a) sa); (Inr rvb, sc) \<in> fst (returnOk (rv + rva) sb); (Inr rvc, sd) \<in> fst (assertE (rvb \<noteq> 0) sc)\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) sd) (returnOk (fromCPtr b `~shiftR~` (c - rvb) && mask rv)))
 6. \<And>a b c s rv sa rva sb rvb sc rvc sd rvd se. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a; (Inr rv, sa) \<in> fst (returnOk (capCNodeBits a) s); (Inr rva, sb) \<in> fst (returnOk (capCNodeGuardSize a) sa); (Inr rvb, sc) \<in> fst (returnOk (rv + rva) sb); (Inr rvc, sd) \<in> fst (assertE (rvb \<noteq> 0) sc); (Inr rvd, se) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rvb) && mask rv) sd)\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) se) (withoutFailure (locateSlotCap a rvd)))
 7. \<And>a b c s rv sa rva sb rvb sc rvc sd rvd se rve sf. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a; (Inr rv, sa) \<in> fst (returnOk (capCNodeBits a) s); (Inr rva, sb) \<in> fst (returnOk (capCNodeGuardSize a) sa); (Inr rvb, sc) \<in> fst (returnOk (rv + rva) sb); (Inr rvc, sd) \<in> fst (assertE (rvb \<noteq> 0) sc); (Inr rvd, se) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rvb) && mask rv) sd); (Inr rve, sf) \<in> fst (withoutFailure (locateSlotCap a rvd) se)\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) sf) (returnOk (fromCPtr b `~shiftR~` (c - rva) && mask rva)))
 8. \<And>a b c s rv sa rva sb rvb sc rvc sd rvd se rve sf rvf sg. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a; (Inr rv, sa) \<in> fst (returnOk (capCNodeBits a) s); (Inr rva, sb) \<in> fst (returnOk (capCNodeGuardSize a) sa); (Inr rvb, sc) \<in> fst (returnOk (rv + rva) sb); (Inr rvc, sd) \<in> fst (assertE (rvb \<noteq> 0) sc); (Inr rvd, se) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rvb) && mask rv) sd); (Inr rve, sf) \<in> fst (withoutFailure (locateSlotCap a rvd) se); (Inr rvf, sg) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rva) && mask rva) sf)\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) sg) (unlessE (rva \<le> c \<and> rvf = capCNodeGuard a) (throw (Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard a) rva))))
 9. \<And>a b c s rv sa rva sb rvb sc rvc sd rvd se rve sf rvf sg rvg sh. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a; (Inr rv, sa) \<in> fst (returnOk (capCNodeBits a) s); (Inr rva, sb) \<in> fst (returnOk (capCNodeGuardSize a) sa); (Inr rvb, sc) \<in> fst (returnOk (rv + rva) sb); (Inr rvc, sd) \<in> fst (assertE (rvb \<noteq> 0) sc); (Inr rvd, se) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rvb) && mask rv) sd); (Inr rve, sf) \<in> fst (withoutFailure (locateSlotCap a rvd) se); (Inr rvf, sg) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rva) && mask rva) sf); (Inr rvg, sh) \<in> fst (unlessE (rva \<le> c \<and> rvf = capCNodeGuard a) (throw (Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard a) rva)) sg)\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) sh) (whenE (c < rvb) (throw (Fault_H.lookup_failure.DepthMismatch c rvb))))
 10. \<And>a b c s rv sa rva sb rvb sc rvc sd rvd se rve sf rvf sg rvg sh rvh si. \<lbrakk>\<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 sa. \<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 (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> empty_fail (cutMon ((=) sa) (CSpace_H.resolveAddressBits rve b rvd)); isCNodeCap a; (Inr rv, sa) \<in> fst (returnOk (capCNodeBits a) s); (Inr rva, sb) \<in> fst (returnOk (capCNodeGuardSize a) sa); (Inr rvb, sc) \<in> fst (returnOk (rv + rva) sb); (Inr rvc, sd) \<in> fst (assertE (rvb \<noteq> 0) sc); (Inr rvd, se) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rvb) && mask rv) sd); (Inr rve, sf) \<in> fst (withoutFailure (locateSlotCap a rvd) se); (Inr rvf, sg) \<in> fst (returnOk (fromCPtr b `~shiftR~` (c - rva) && mask rva) sf); (Inr rvg, sh) \<in> fst (unlessE (rva \<le> c \<and> rvf = capCNodeGuard a) (throw (Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard a) rva)) sg); (Inr rvh, si) \<in> fst (whenE (c < rvb) (throw (Fault_H.lookup_failure.DepthMismatch c rvb)) sh)\<rbrakk> \<Longrightarrow> empty_fail (cutMon ((=) si) (returnOk (c - rvb)))
A total of 15 subgoals... proof (prove)
goal:
No subgoals! proof (state)
this:
empty_fail (CSpace_H.resolveAddressBits cap cptr bits)

goal:
No subgoals!