theory CSpace_R

lemma rab_cap_to'':
  assumes P: "\<And>cap. isCNodeCap cap \<longrightarrow> P cap"
  shows
  "s \<turnstile> \<lbrace>\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace>
     resolveAddressBits cap cref depth
   \<lbrace>\<lambda>rv s. ex_cte_cap_wp_to' P (fst rv) s\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" proof (induct arbitrary: s rule: resolveAddressBits.induct) case (1 cap fn cref depth) show ?case apply (subst resolveAddressBits.simps) apply (simp add: Let_def split_def cap_case_CNodeCap[unfolded isCap_simps]
               split del: if_split cong: if_cong) apply (rule hoare_pre_spec_validE) apply ((elim exE | wp (once) spec_strengthen_postE[OF "1.hyps"])+,
              (rule refl conjI | simp add: in_monad split del: if_split del: cte_refs'.simps)+) apply (wp getSlotCap_cap_to2
                     | simp    add: assertE_def split_def whenE_def locateSlotCap_def
                        split del: if_split | simp add: imp_conjL[symmetric]
                     | wp (once) hoare_drop_imps)+ apply (clarsimp simp: P) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits cap cref depth \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (state)
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> sa \<turnstile> \<lbrace>\<lambda>s. isCNodeCap rve \<longrightarrow> (\<forall>r\<in>cte_refs' rve (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits rve b rvd \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. isCNodeCap a \<longrightarrow> (\<forall>r\<in>cte_refs' a (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits a b c \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<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 fn `~shiftR~` (cref - ?rva) && mask ?v) ?stb); (Inr ?rvbb, ?std) \<in> fst ((withoutFailure $ locateSlotCap ?x ?rvba) ?stc); (Inr ?rvbc, ?ste) \<in> fst (returnOk (fromCPtr fn `~shiftR~` (cref - ?rv) && mask ?rv) ?std); (Inr ?rvbd, ?stf) \<in> fst ((unlessE (?rv \<le> cref \<and> ?rvbc = capCNodeGuard ?x) $ throw $ Fault_H.lookup_failure.GuardMismatch cref (capCNodeGuard ?x) ?rv) ?ste); (Inr ?rvc, ?stg) \<in> fst ((whenE (cref < ?rva) $ throw $ Fault_H.lookup_failure.DepthMismatch cref ?rva) ?stf); (Inr ?rvd, ?sth) \<in> fst (returnOk (cref - ?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> ?sa \<turnstile> \<lbrace>\<lambda>s. isCNodeCap ?rve \<longrightarrow> (\<forall>r\<in>cte_refs' ?rve (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits ?rve fn ?rvd \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

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> sa \<turnstile> \<lbrace>\<lambda>s. isCNodeCap rve \<longrightarrow> (\<forall>r\<in>cte_refs' rve (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits rve b rvd \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. isCNodeCap a \<longrightarrow> (\<forall>r\<in>cte_refs' a (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits a b c \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. depth \<turnstile> \<lbrace>\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits cap fn cref \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. depth \<turnstile> \<lbrace>\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> 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 fn `~shiftR~` (cref - levelBits) && mask radixBits);
slot <- withoutFailure $ locateSlotCap nodeCap offset;
guard <- returnOk (fromCPtr fn `~shiftR~` (cref - guardBits) && mask guardBits);
unlessE (guardBits \<le> cref \<and> guard = capCNodeGuard nodeCap) $ throw $ Fault_H.lookup_failure.GuardMismatch cref (capCNodeGuard nodeCap) guardBits;
whenE (cref < levelBits) $ throw $ Fault_H.lookup_failure.DepthMismatch cref levelBits;
bitsLeft <- returnOk (cref - 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 fn bitsLeft | _ \<Rightarrow> returnOk (slot, bitsLeft)
odE
odE else throw Fault_H.lookup_failure.InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. depth \<turnstile> \<lbrace>\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> if isCNodeCap cap then doE y <- assertE (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap);
slot <- liftE (locateSlotCap cap ((fn >> cref - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)));
y <- unlessE (capCNodeGuardSize cap \<le> cref \<and> (fn >> cref - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) (throwError (Fault_H.lookup_failure.GuardMismatch cref (capCNodeGuard cap) (capCNodeGuardSize cap)));
y <- whenE (cref < capCNodeBits cap + capCNodeGuardSize cap) (throwError (Fault_H.lookup_failure.DepthMismatch cref (capCNodeBits cap + capCNodeGuardSize cap)));
if cref \<le> capCNodeBits cap + capCNodeGuardSize cap then returnOk (slot, 0) else doE nextCap <- liftE (getSlotCap slot);
if \<exists>v0 v1 v2 v3. nextCap = capability.CNodeCap v0 v1 v2 v3 then CSpace_H.resolveAddressBits nextCap fn (cref - (capCNodeBits cap + capCNodeGuardSize cap)) else returnOk (slot, cref - (capCNodeBits cap + capCNodeGuardSize cap))
odE
odE else throwError Fault_H.lookup_failure.InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. depth \<turnstile> \<lbrace>?P'10\<rbrace> if isCNodeCap cap then doE y <- assertE (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap);
slot <- liftE (locateSlotCap cap ((fn >> cref - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)));
y <- unlessE (capCNodeGuardSize cap \<le> cref \<and> (fn >> cref - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) (throwError (Fault_H.lookup_failure.GuardMismatch cref (capCNodeGuard cap) (capCNodeGuardSize cap)));
y <- whenE (cref < capCNodeBits cap + capCNodeGuardSize cap) (throwError (Fault_H.lookup_failure.DepthMismatch cref (capCNodeBits cap + capCNodeGuardSize cap)));
if cref \<le> capCNodeBits cap + capCNodeGuardSize cap then returnOk (slot, 0) else doE nextCap <- liftE (getSlotCap slot);
if \<exists>v0 v1 v2 v3. nextCap = capability.CNodeCap v0 v1 v2 v3 then CSpace_H.resolveAddressBits nextCap fn (cref - (capCNodeBits cap + capCNodeGuardSize cap)) else returnOk (slot, cref - (capCNodeBits cap + capCNodeGuardSize cap))
odE
odE else throwError Fault_H.lookup_failure.InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' depth). ex_cte_cap_wp_to' P r depth) \<Longrightarrow> ?P'10 depth proof (prove)
goal (8 subgoals):
 1. \<And>rva s''a s''b s''c rvd s''d. \<lbrakk>isCNodeCap cap; 0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap; (rva, s''a) \<in> fst (locateSlotCap cap ((fn >> cref - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)) depth); (fn >> cref - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<and> ((fn >> cref - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap \<longrightarrow> s''b = s''a); s''c = s''a; \<not> cref \<le> capCNodeBits cap + capCNodeGuardSize cap; (rvd, s''d) \<in> fst (getSlotCap rva s''a); \<forall>v0 v1 v2 v3. rvd \<noteq> capability.CNodeCap v0 v1 v2 v3\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?P'55 () depth rva s''a () s''a () s''a rvd\<rbrace> returnOk (rva, cref - (capCNodeBits cap + capCNodeGuardSize cap)) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>isCNodeCap cap; (Inr rv, s'') \<in> fst (assertE (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) depth); (Inr rva, s''a) \<in> fst (liftE (locateSlotCap cap ((fn >> cref - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s''); (Inr rvb, s''b) \<in> fst (unlessE (capCNodeGuardSize cap \<le> cref \<and> (fn >> cref - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) (throwError (Fault_H.lookup_failure.GuardMismatch cref (capCNodeGuard cap) (capCNodeGuardSize cap))) s''a); (Inr rvc, s''c) \<in> fst (whenE (cref < capCNodeBits cap + capCNodeGuardSize cap) (throwError (Fault_H.lookup_failure.DepthMismatch cref (capCNodeBits cap + capCNodeGuardSize cap))) s''b); \<not> cref \<le> capCNodeBits cap + capCNodeGuardSize cap\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?P'33 rv s'' rva s''a rvb s''b rvc\<rbrace> liftE (getSlotCap rva) \<lbrace>\<lambda>rvd s. ((\<exists>v0 v1 v2 v3. rvd = capability.CNodeCap v0 v1 v2 v3) \<longrightarrow> isCNodeCap rvd \<longrightarrow> (\<forall>r\<in>cte_refs' rvd (irq_node' s). ex_cte_cap_wp_to' P r s)) \<and> ((\<nexists>v0 v1 v2 v3. rvd = capability.CNodeCap v0 v1 v2 v3) \<longrightarrow> ?P'55 rv s'' rva s''a rvb s''b rvc s''c rvd s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>isCNodeCap cap; (Inr rv, s'') \<in> fst (assertE (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) depth); (Inr rva, s''a) \<in> fst (liftE (locateSlotCap cap ((fn >> cref - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s''); (Inr rvb, s''b) \<in> fst (unlessE (capCNodeGuardSize cap \<le> cref \<and> (fn >> cref - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) (throwError (Fault_H.lookup_failure.GuardMismatch cref (capCNodeGuard cap) (capCNodeGuardSize cap))) s''a)\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?B23 rv s'' rva s''a rvb\<rbrace> whenE (cref < capCNodeBits cap + capCNodeGuardSize cap) (throwError (Fault_H.lookup_failure.DepthMismatch cref (capCNodeBits cap + capCNodeGuardSize cap))) \<lbrace>\<lambda>rvc s. (cref \<le> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> True \<and> ex_cte_cap_wp_to' P (fst (rva, 0)) s) \<and> (\<not> cref \<le> capCNodeBits cap + capCNodeGuardSize cap \<longrightarrow> ?P'33 rv s'' rva s''a rvb s''b rvc s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>isCNodeCap cap; (Inr rv, s'') \<in> fst (assertE (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) depth); (Inr rva, s''a) \<in> fst (liftE (locateSlotCap cap ((fn >> cref - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B20 rv s'' rva\<rbrace> unlessE (capCNodeGuardSize cap \<le> cref \<and> (fn >> cref - capCNodeGuardSize cap) && mask (capCNodeGuardSize cap) = capCNodeGuard cap) (throwError (Fault_H.lookup_failure.GuardMismatch cref (capCNodeGuard cap) (capCNodeGuardSize cap))) \<lbrace>?B23 rv s'' rva s''a\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv s''. \<lbrakk>isCNodeCap cap; (Inr rv, s'') \<in> fst (assertE (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) depth)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B17 rv\<rbrace> liftE (locateSlotCap cap ((fn >> cref - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap))) \<lbrace>?B20 rv s''\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. isCNodeCap cap \<Longrightarrow> depth \<turnstile> \<lbrace>?P14\<rbrace> assertE (0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap) \<lbrace>?B17\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<not> isCNodeCap cap \<Longrightarrow> depth \<turnstile> \<lbrace>?P'14\<rbrace> throwError Fault_H.lookup_failure.InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' depth). ex_cte_cap_wp_to' P r depth) \<Longrightarrow> (isCNodeCap cap \<longrightarrow> ?P14 depth) \<and> (\<not> isCNodeCap cap \<longrightarrow> ?P'14 depth) proof (prove)
goal (1 subgoal):
 1. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' depth). ex_cte_cap_wp_to' P r depth) \<Longrightarrow> isCNodeCap cap \<longrightarrow> (0 < capCNodeBits cap \<longrightarrow> (\<forall>cap. (\<exists>v0 v1 v2 v3. cap = capability.CNodeCap v0 v1 v2 v3) \<and> isCNodeCap cap \<longrightarrow> P cap)) \<and> (0 < capCNodeGuardSize cap \<longrightarrow> (\<forall>cap. (\<exists>v0 v1 v2 v3. cap = capability.CNodeCap v0 v1 v2 v3) \<and> isCNodeCap cap \<longrightarrow> P cap)) proof (prove)
goal:
No subgoals! proof (state)
this:
depth \<turnstile> \<lbrace>\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits cap fn cref \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal:
No subgoals!