theory EmptyFail_AI

lemma resolve_address_bits_spec_empty_fail:
  notes spec_empty_fail_bindE'[wp_split]
  shows "spec_empty_fail (resolve_address_bits slot) s" unfolding resolve_address_bits_def proof (induct arbitrary: s rule: resolve_address_bits'.induct) case (1 z cap cref s') show ?case apply (simp add: resolve_address_bits'.simps) apply (case_tac cap,
              (wp | simp | intro impI conjI | rule "1.hyps" | rule drop_spec_empty_fail
                  | simp add: whenE_def in_monad | force)+) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (resolve_address_bits slot) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (resolve_address_bits' TYPE('a) slot) s proof (state)
goal (1 subgoal):
 1. \<And>z cap cref x. (\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc x. \<lbrakk>cap = CNodeCap x61 x62 x63; x62 + length x63 \<noteq> 0; (Inr v, s') \<in> fst (whenE (\<not> x63 \<le> cref) (throwError $ GuardMismatch (length cref) x63) s); (Inr rv, st) \<in> fst (whenE (length cref < x62 + length x63) (throwError $ DepthMismatch (length cref) (x62 + length x63)) s'); (Inr rva, sta) \<in> fst ((returnOk $ take x62 (drop (length x63) cref)) st); (Inr rvb, stb) \<in> fst ((returnOk $ drop (x62 + length x63) cref) sta); rvb \<noteq> []; (Inr rvc, stc) \<in> fst ((liftE $ get_cap (x61, rva)) stb); is_cnode_cap rvc\<rbrakk> \<Longrightarrow> spec_empty_fail (resolve_address_bits' z (rvc, rvb)) x) \<Longrightarrow> spec_empty_fail (resolve_address_bits' z (cap, cref)) x proof (state)
this:
\<lbrakk>cap = CNodeCap ?x61.0 ?x62.0 ?x63.0; ?x62.0 + length ?x63.0 \<noteq> 0; (Inr ?v, ?s') \<in> fst (whenE (\<not> ?x63.0 \<le> cref) (throwError $ GuardMismatch (length cref) ?x63.0) ?s); (Inr ?rv, ?st) \<in> fst (whenE (length cref < ?x62.0 + length ?x63.0) (throwError $ DepthMismatch (length cref) (?x62.0 + length ?x63.0)) ?s'); (Inr ?rva, ?sta) \<in> fst ((returnOk $ take ?x62.0 (drop (length ?x63.0) cref)) ?st); (Inr ?rvb, ?stb) \<in> fst ((returnOk $ drop (?x62.0 + length ?x63.0) cref) ?sta); ?rvb \<noteq> []; (Inr ?rvc, ?stc) \<in> fst ((liftE $ get_cap (?x61.0, ?rva)) ?stb); is_cnode_cap ?rvc\<rbrakk> \<Longrightarrow> spec_empty_fail (resolve_address_bits' z (?rvc, ?rvb)) ?sa

goal (1 subgoal):
 1. \<And>z cap cref x. (\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc x. \<lbrakk>cap = CNodeCap x61 x62 x63; x62 + length x63 \<noteq> 0; (Inr v, s') \<in> fst (whenE (\<not> x63 \<le> cref) (throwError $ GuardMismatch (length cref) x63) s); (Inr rv, st) \<in> fst (whenE (length cref < x62 + length x63) (throwError $ DepthMismatch (length cref) (x62 + length x63)) s'); (Inr rva, sta) \<in> fst ((returnOk $ take x62 (drop (length x63) cref)) st); (Inr rvb, stb) \<in> fst ((returnOk $ drop (x62 + length x63) cref) sta); rvb \<noteq> []; (Inr rvc, stc) \<in> fst ((liftE $ get_cap (x61, rva)) stb); is_cnode_cap rvc\<rbrakk> \<Longrightarrow> spec_empty_fail (resolve_address_bits' z (rvc, rvb)) x) \<Longrightarrow> spec_empty_fail (resolve_address_bits' z (cap, cref)) x proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (resolve_address_bits' z (cap, cref)) s' proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s' proof (prove)
goal:
No subgoals! proof (state)
this:
spec_empty_fail (resolve_address_bits' z (cap, cref)) s'

goal:
No subgoals!