theory EmptyFail_H

lemma resolveAddressBits_spec_empty_fail:
  notes spec_empty_fail_bindE'[wp_split]
  shows
  "spec_empty_fail (CSpace_H.resolveAddressBits a b c) s" proof (induct arbitrary: s rule: resolveAddressBits.induct) case (1 a b c s) show ?case apply (simp add: resolveAddressBits.simps) apply (wp | simp | wpc | intro impI conjI | rule drop_spec_empty_fail)+ apply (rule use_spec_empty_fail) apply (rule 1 | simp add: in_monad | rule drop_spec_empty_fail | force)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (CSpace_H.resolveAddressBits a b c) s proof (state)
goal (1 subgoal):
 1. \<And>a b c x. (\<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 xa. \<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> spec_empty_fail (CSpace_H.resolveAddressBits rve b rvd) xa) \<Longrightarrow> spec_empty_fail (CSpace_H.resolveAddressBits a b c) x proof (state)
this:
\<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.0 ?x112.0 ?x113.0 ?x114.0\<rbrakk> \<Longrightarrow> spec_empty_fail (CSpace_H.resolveAddressBits ?rve b ?rvd) ?sa

goal (1 subgoal):
 1. \<And>a b c x. (\<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 xa. \<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> spec_empty_fail (CSpace_H.resolveAddressBits rve b rvd) xa) \<Longrightarrow> spec_empty_fail (CSpace_H.resolveAddressBits a b c) x proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (CSpace_H.resolveAddressBits a b c) s proof (prove)
goal (1 subgoal):
 1. (isCNodeCap a \<longrightarrow> spec_empty_fail (doE y <- assertE (0 < capCNodeBits a \<or> 0 < capCNodeGuardSize a);
slot <- liftE (locateSlotCap a ((b >> c - (capCNodeBits a + capCNodeGuardSize a)) && mask (capCNodeBits a)));
y <- unlessE (capCNodeGuardSize a \<le> c \<and> (b >> c - capCNodeGuardSize a) && mask (capCNodeGuardSize a) = capCNodeGuard a) (throwError (Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard a) (capCNodeGuardSize a)));
y <- whenE (c < capCNodeBits a + capCNodeGuardSize a) (throwError (Fault_H.lookup_failure.DepthMismatch c (capCNodeBits a + capCNodeGuardSize a)));
if c \<le> capCNodeBits a + capCNodeGuardSize a then returnOk (slot, 0) else doE nextCap <- liftE (getSlotCap slot);
case nextCap of capability.CNodeCap x xa xb xc \<Rightarrow> CSpace_H.resolveAddressBits nextCap b (c - (capCNodeBits a + capCNodeGuardSize a)) | _ \<Rightarrow> returnOk (slot, c - (capCNodeBits a + capCNodeGuardSize a))
odE
odE) s) \<and> (\<not> isCNodeCap a \<longrightarrow> spec_empty_fail (throwError Fault_H.lookup_failure.InvalidRoot) s) proof (prove)
goal (3 subgoals):
 1. \<And>s' xa s'a s'b s'c x s'd x111 x112 x113 x114. \<lbrakk>isCNodeCap a; (Inr (), s') \<in> fst (assertE (0 < capCNodeBits a \<or> 0 < capCNodeGuardSize a) s); (xa, s'a) \<in> fst (locateSlotCap a ((b >> c - (capCNodeBits a + capCNodeGuardSize a)) && mask (capCNodeBits a)) s'); (Inr (), s'b) \<in> fst (unlessE ((b >> c - capCNodeGuardSize a) && mask (capCNodeGuardSize a) = capCNodeGuard a) (throwError (Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard a) (capCNodeGuardSize a))) s'a); (Inr (), s'c) \<in> fst (whenE False (throwError (Fault_H.lookup_failure.DepthMismatch c (capCNodeBits a + capCNodeGuardSize a))) s'b); \<not> c \<le> capCNodeBits a + capCNodeGuardSize a; (capability.CNodeCap x111 x112 x113 x114, s'd) \<in> fst (getSlotCap xa s'c); x = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> empty_fail (CSpace_H.resolveAddressBits (capability.CNodeCap x111 x112 x113 x114) b (c - (capCNodeBits a + capCNodeGuardSize a)))
 2. \<And>s' xa s'a s'b s'c x s'd. \<lbrakk>isCNodeCap a; (Inr (), s') \<in> fst (assertE (0 < capCNodeBits a \<or> 0 < capCNodeGuardSize a) s); (xa, s'a) \<in> fst (locateSlotCap a ((b >> c - (capCNodeBits a + capCNodeGuardSize a)) && mask (capCNodeBits a)) s'); (Inr (), s'b) \<in> fst (unlessE ((b >> c - capCNodeGuardSize a) && mask (capCNodeGuardSize a) = capCNodeGuard a) (throwError (Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard a) (capCNodeGuardSize a))) s'a); (Inr (), s'c) \<in> fst (whenE False (throwError (Fault_H.lookup_failure.DepthMismatch c (capCNodeBits a + capCNodeGuardSize a))) s'b); \<not> c \<le> capCNodeBits a + capCNodeGuardSize a; (x, s'd) \<in> fst (getSlotCap xa s'c); x = capability.IRQControlCap\<rbrakk> \<Longrightarrow> empty_fail (returnOk (xa, c - (capCNodeBits a + capCNodeGuardSize a)))
 3. \<not> isCNodeCap a \<Longrightarrow> spec_empty_fail (throwError Fault_H.lookup_failure.InvalidRoot) s proof (prove)
goal (3 subgoals):
 1. \<And>s' xa s'a s'b s'c x s'd x111 x112 x113 x114 s. \<lbrakk>isCNodeCap a; (Inr (), s') \<in> fst (assertE (0 < capCNodeBits a \<or> 0 < capCNodeGuardSize a) s); (xa, s'a) \<in> fst (locateSlotCap a ((b >> c - (capCNodeBits a + capCNodeGuardSize a)) && mask (capCNodeBits a)) s'); (Inr (), s'b) \<in> fst (unlessE ((b >> c - capCNodeGuardSize a) && mask (capCNodeGuardSize a) = capCNodeGuard a) (throwError (Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard a) (capCNodeGuardSize a))) s'a); (Inr (), s'c) \<in> fst (whenE False (throwError (Fault_H.lookup_failure.DepthMismatch c (capCNodeBits a + capCNodeGuardSize a))) s'b); \<not> c \<le> capCNodeBits a + capCNodeGuardSize a; (capability.CNodeCap x111 x112 x113 x114, s'd) \<in> fst (getSlotCap xa s'c); x = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> spec_empty_fail (CSpace_H.resolveAddressBits (capability.CNodeCap x111 x112 x113 x114) b (c - (capCNodeBits a + capCNodeGuardSize a))) s
 2. \<And>s' xa s'a s'b s'c x s'd. \<lbrakk>isCNodeCap a; (Inr (), s') \<in> fst (assertE (0 < capCNodeBits a \<or> 0 < capCNodeGuardSize a) s); (xa, s'a) \<in> fst (locateSlotCap a ((b >> c - (capCNodeBits a + capCNodeGuardSize a)) && mask (capCNodeBits a)) s'); (Inr (), s'b) \<in> fst (unlessE ((b >> c - capCNodeGuardSize a) && mask (capCNodeGuardSize a) = capCNodeGuard a) (throwError (Fault_H.lookup_failure.GuardMismatch c (capCNodeGuard a) (capCNodeGuardSize a))) s'a); (Inr (), s'c) \<in> fst (whenE False (throwError (Fault_H.lookup_failure.DepthMismatch c (capCNodeBits a + capCNodeGuardSize a))) s'b); \<not> c \<le> capCNodeBits a + capCNodeGuardSize a; (x, s'd) \<in> fst (getSlotCap xa s'c); x = capability.IRQControlCap\<rbrakk> \<Longrightarrow> empty_fail (returnOk (xa, c - (capCNodeBits a + capCNodeGuardSize a)))
 3. \<not> isCNodeCap a \<Longrightarrow> spec_empty_fail (throwError Fault_H.lookup_failure.InvalidRoot) s proof (prove)
goal:
No subgoals! proof (state)
this:
spec_empty_fail (CSpace_H.resolveAddressBits a b c) s

goal:
No subgoals!