theory CNode_AC

lemma resolve_address_bits_authorised_aux:
  "s \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap, cref))
                               \<longrightarrow> (\<forall>x \<in> obj_refs_ac (fst (cap, cref)). is_subject aag x))\<rbrace>
       resolve_address_bits (cap, cref)
       \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv. \<top>\<rbrace>" unfolding resolve_address_bits_def proof (induct arbitrary: s rule: resolve_address_bits'.induct) case (1 z cap' cref' s') have P: "\<And>s f P Q. s \<turnstile> \<lbrace>P\<rbrace> throwError f \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv s. True\<rbrace>" by wp+ show ?case apply (subst resolve_address_bits'.simps) apply (cases cap', simp_all add: P split del: if_split) apply (rule hoare_pre_spec_validE) apply (wp "1.hyps", (assumption | simp add: in_monad | rule conjI)+) apply (wp get_cap_wp)+ apply (auto simp: cte_wp_at_caps_of_state is_cap_simps cap_auth_conferred_def
                dest: caps_of_state_pasObjectAbs_eq) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap, cref)). is_subject aag x))\<rbrace> resolve_address_bits (cap, cref) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap, cref)). is_subject aag x))\<rbrace> resolve_address_bits' TYPE(det_ext) (cap, cref) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>z cap cref s. (\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc sa. \<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> sa \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (rvc, rvb)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (rvc, rvb)). is_subject aag x))\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap, cref)). is_subject aag x))\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> 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> ?sa \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (?rvc, ?rvb)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (?rvc, ?rvb)). is_subject aag x))\<rbrace> resolve_address_bits' z (?rvc, ?rvb) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>

goal (1 subgoal):
 1. \<And>z cap cref s. (\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc sa. \<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> sa \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (rvc, rvb)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (rvc, rvb)). is_subject aag x))\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap, cref)). is_subject aag x))\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s f P Q. s \<turnstile> \<lbrace>P\<rbrace> throwError f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv s. True\<rbrace> proof (state)
this:
?s \<turnstile> \<lbrace>?P\<rbrace> throwError ?f \<lbrace>?Q\<rbrace>, \<lbrace>\<lambda>rv s. True\<rbrace>

goal (1 subgoal):
 1. \<And>z cap cref s. (\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc sa. \<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> sa \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (rvc, rvb)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (rvc, rvb)). is_subject aag x))\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap, cref)). is_subject aag x))\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap', cref')) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap', cref')). is_subject aag x))\<rbrace> resolve_address_bits' z (cap', cref') \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap', cref')) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap', cref')). is_subject aag x))\<rbrace> 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 \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x63. cap' = CNodeCap x61 x62 x63 \<Longrightarrow> s' \<turnstile> \<lbrace>pas_refined aag and (\<lambda>y. is_subject aag x61)\<rbrace> if x62 = 0 \<and> x63 = [] then fail else doE y <- whenE (\<not> x63 \<le> cref') (throwError (GuardMismatch (length cref') x63));
y <- whenE (length cref' < x62 + length x63) (throwError (DepthMismatch (length cref') (x62 + length x63)));
if length cref' \<le> x62 + length x63 then returnOk ((x61, drop (length x63) cref'), []) else doE next_cap <- liftE (get_cap (x61, take x62 (drop (length x63) cref')));
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, drop (x62 + length x63) cref') else returnOk ((x61, take x62 (drop (length x63) cref')), drop (x62 + length x63) cref')
odE
odE \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63. cap' = CNodeCap x61 x62 x63 \<Longrightarrow> s' \<turnstile> \<lbrace>?P'28 x61 x62 x63\<rbrace> if x62 = 0 \<and> x63 = [] then fail else doE y <- whenE (\<not> x63 \<le> cref') (throwError (GuardMismatch (length cref') x63));
y <- whenE (length cref' < x62 + length x63) (throwError (DepthMismatch (length cref') (x62 + length x63)));
if length cref' \<le> x62 + length x63 then returnOk ((x61, drop (length x63) cref'), []) else doE next_cap <- liftE (get_cap (x61, take x62 (drop (length x63) cref')));
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, drop (x62 + length x63) cref') else returnOk ((x61, take x62 (drop (length x63) cref')), drop (x62 + length x63) cref')
odE
odE \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>x61 x62 x63. \<lbrakk>cap' = CNodeCap x61 x62 x63; (pas_refined aag and (\<lambda>y. is_subject aag x61)) s'\<rbrakk> \<Longrightarrow> ?P'28 x61 x62 x63 s' proof (prove)
goal (5 subgoals):
 1. \<And>x61 x62 x63 s'' s''a rvb s''b. \<lbrakk>cap' = CNodeCap x61 x62 x63; 0 < x62 \<or> x63 \<noteq> []; x63 \<le> cref' \<and> (x63 \<le> cref' \<longrightarrow> s'' = s'); s''a = s'; \<not> length cref' \<le> x62 + length x63; (rvb, s''b) \<in> fst (get_cap (x61, take x62 (drop (length x63) cref')) s'); \<not> is_cnode_cap rvb\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P'56 x61 x62 x63 () s' () s' rvb\<rbrace> returnOk ((x61, take x62 (drop (length x63) cref')), drop (x62 + length x63) cref') \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>x61 x62 x63 rv s'' rva s''a. \<lbrakk>cap' = CNodeCap x61 x62 x63; \<not> (x62 = 0 \<and> x63 = []); (Inr rv, s'') \<in> fst (whenE (\<not> x63 \<le> cref') (throwError (GuardMismatch (length cref') x63)) s'); (Inr rva, s''a) \<in> fst (whenE (length cref' < x62 + length x63) (throwError (DepthMismatch (length cref') (x62 + length x63))) s''); \<not> length cref' \<le> x62 + length x63\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?P'44 x61 x62 x63 rv s'' rva\<rbrace> liftE (get_cap (x61, take x62 (drop (length x63) cref'))) \<lbrace>\<lambda>rvb s. (is_cnode_cap rvb \<longrightarrow> (pas_refined aag and K (is_cnode_cap (fst (rvb, drop (x62 + length x63) cref')) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (rvb, drop (x62 + length x63) cref')). is_subject aag x))) s) \<and> (\<not> is_cnode_cap rvb \<longrightarrow> ?P'56 x61 x62 x63 rv s'' rva s''a rvb s)\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>x61 x62 x63 rv s''. \<lbrakk>cap' = CNodeCap x61 x62 x63; \<not> (x62 = 0 \<and> x63 = []); (Inr rv, s'') \<in> fst (whenE (\<not> x63 \<le> cref') (throwError (GuardMismatch (length cref') x63)) s')\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B38 x61 x62 x63 rv\<rbrace> whenE (length cref' < x62 + length x63) (throwError (DepthMismatch (length cref') (x62 + length x63))) \<lbrace>\<lambda>rva s. (length cref' \<le> x62 + length x63 \<longrightarrow> True \<and> is_subject aag (fst (fst ((x61, drop (length x63) cref'), [])))) \<and> (\<not> length cref' \<le> x62 + length x63 \<longrightarrow> ?P'44 x61 x62 x63 rv s'' rva s)\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>x61 x62 x63. \<lbrakk>cap' = CNodeCap x61 x62 x63; \<not> (x62 = 0 \<and> x63 = [])\<rbrakk> \<Longrightarrow> s' \<turnstile> \<lbrace>?P'32 x61 x62 x63\<rbrace> whenE (\<not> x63 \<le> cref') (throwError (GuardMismatch (length cref') x63)) \<lbrace>?B38 x61 x62 x63\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>x61 x62 x63. \<lbrakk>cap' = CNodeCap x61 x62 x63; (pas_refined aag and (\<lambda>y. is_subject aag x61)) s'\<rbrakk> \<Longrightarrow> (x62 = 0 \<and> x63 = [] \<longrightarrow> True \<and> True) \<and> (\<not> (x62 = 0 \<and> x63 = []) \<longrightarrow> ?P'32 x61 x62 x63 s') proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x63. \<lbrakk>cap' = CNodeCap x61 x62 x63; (pas_refined aag and (\<lambda>y. is_subject aag x61)) s'\<rbrakk> \<Longrightarrow> (x62 = 0 \<and> x63 = [] \<longrightarrow> True \<and> True) \<and> (\<not> (x62 = 0 \<and> x63 = []) \<longrightarrow> (\<not> x63 \<le> cref' \<longrightarrow> True \<and> True) \<and> (\<not> \<not> x63 \<le> cref' \<longrightarrow> (length cref' < x62 + length x63 \<longrightarrow> True \<and> True) \<and> (\<not> length cref' < x62 + length x63 \<longrightarrow> (length cref' \<le> x62 + length x63 \<longrightarrow> True \<and> is_subject aag (fst (fst ((x61, drop (length x63) cref'), [])))) \<and> (\<not> length cref' \<le> x62 + length x63 \<longrightarrow> True \<and> (\<forall>cap. cte_wp_at ((=) cap) (x61, take x62 (drop (length x63) cref')) s' \<longrightarrow> (is_cnode_cap cap \<longrightarrow> (pas_refined aag and K (is_cnode_cap (fst (cap, drop (x62 + length x63) cref')) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap, drop (x62 + length x63) cref')). is_subject aag x))) s') \<and> (\<not> is_cnode_cap cap \<longrightarrow> True \<and> is_subject aag (fst (fst ((x61, take x62 (drop (length x63) cref')), drop (x62 + length x63) cref'))))))))) proof (prove)
goal:
No subgoals! proof (state)
this:
s' \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap', cref')) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (fst (cap', cref')). is_subject aag x))\<rbrace> resolve_address_bits' z (cap', cref') \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>

goal:
No subgoals!