theory CSpace_AI

lemma rab_cte_cap_to':
  "s \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst args) \<longrightarrow> (\<forall>r\<in>cte_refs (fst args) (interrupt_irq_node s). ex_cte_cap_wp_to P r s))
               \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace>
    resolve_address_bits args
   \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" unfolding resolve_address_bits_def proof (induct args arbitrary: s rule: resolve_address_bits'.induct) case (1 z cap cref s') have P:
    "\<And>P' Q args adm s.
      \<lbrakk> s \<turnstile> \<lbrace>P'\<rbrace> resolve_address_bits' z args \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>;
        \<And>rv s. ex_cte_cap_wp_to P (fst rv) s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow>
        s \<turnstile> \<lbrace>P'\<rbrace> resolve_address_bits' z args \<lbrace>Q\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" unfolding spec_validE_def apply (fold validE_R_def) apply (erule hoare_post_imp_R) apply simp done show ?case apply (subst resolve_address_bits'.simps) apply (cases cap, simp_all split del: if_split) defer 6  (* CNode *)
             apply (wp+)[11] apply (simp add: split_def cong: if_cong split del: if_split) apply (rule hoare_pre_spec_validE) apply (wp P [OF "1.hyps"], (simp add: in_monad | rule conjI refl)+) apply (wp | simp | rule get_cap_wp)+ apply (fastforce simp: ex_cte_cap_wp_to_def elim!: cte_wp_at_weakenE) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst args) \<longrightarrow> (\<forall>r\<in>cte_refs (fst args) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits args \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst args) \<longrightarrow> (\<forall>r\<in>cte_refs (fst args) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' TYPE('a) args \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. 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>\<lambda>s. (is_cnode_cap (fst (rvc, rvb)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (rvc, rvb)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (cap, cref)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. 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>\<lambda>s. (is_cnode_cap (fst (?rvc, ?rvb)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (?rvc, ?rvb)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' z (?rvc, ?rvb) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. 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>\<lambda>s. (is_cnode_cap (fst (rvc, rvb)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (rvc, rvb)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (cap, cref)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P' Q args adm s. \<lbrakk>s \<turnstile> \<lbrace>P'\<rbrace> resolve_address_bits' z args \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<And>rv s. ex_cte_cap_wp_to P (fst rv) s \<Longrightarrow> Q rv s\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P'\<rbrace> resolve_address_bits' z args \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P' Q args adm s. \<lbrakk>\<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> resolve_address_bits' z args \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<And>rv s. ex_cte_cap_wp_to P (fst rv) s \<Longrightarrow> Q rv s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> resolve_address_bits' z args \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P' Q args adm s. \<lbrakk>\<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> resolve_address_bits' z args \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, -; \<And>rv s. ex_cte_cap_wp_to P (fst rv) s \<Longrightarrow> Q rv s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> resolve_address_bits' z args \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>P' Q args adm s rv sa. \<lbrakk>\<And>rv s. ex_cte_cap_wp_to P (fst rv) s \<Longrightarrow> Q rv s; ex_cte_cap_wp_to P (fst rv) sa\<rbrakk> \<Longrightarrow> Q rv sa proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?s \<turnstile> \<lbrace>?P'\<rbrace> resolve_address_bits' z ?args \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<And>rv s. ex_cte_cap_wp_to P (fst rv) s \<Longrightarrow> ?Q rv s\<rbrakk> \<Longrightarrow> ?s \<turnstile> \<lbrace>?P'\<rbrace> resolve_address_bits' z ?args \<lbrace>?Q\<rbrace>, \<lbrace>\<lambda>_ _. 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>\<lambda>s. (is_cnode_cap (fst (rvc, rvb)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (rvc, rvb)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (cap, cref)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (cap, cref)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (cap, cref)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<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. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (\<forall>y. length y = x62 \<longrightarrow> ex_cte_cap_wp_to P (x61, y) s) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> if x62 = 0 \<and> x63 = [] then fail else doE whenE (\<not> x63 \<le> cref) (throwError $ GuardMismatch (length cref) x63);
whenE (length cref < x62 + length x63) (throwError $ DepthMismatch (length cref) (x62 + length x63));
offset <- returnOk $ take x62 (drop (length x63) cref);
rest <- returnOk $ drop (x62 + length x63) cref;
if rest = [] then returnOk ((x61, offset), []) else doE next_cap <- liftE $ get_cap (x61, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((x61, offset), rest)
odE
odE \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. cap = DomainCap \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. cap = DomainCap \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. cap = IRQControlCap \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. cap = DomainCap \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. cap = IRQControlCap \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap\<rbrace> throwError InvalidRoot \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (\<forall>y. length y = x62 \<longrightarrow> ex_cte_cap_wp_to P (x61, y) s) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> if x62 = 0 \<and> x63 = [] then fail else doE whenE (\<not> x63 \<le> cref) (throwError $ GuardMismatch (length cref) x63);
whenE (length cref < x62 + length x63) (throwError $ DepthMismatch (length cref) (x62 + length x63));
offset <- returnOk $ take x62 (drop (length x63) cref);
rest <- returnOk $ drop (x62 + length x63) cref;
if rest = [] then returnOk ((x61, offset), []) else doE next_cap <- liftE $ get_cap (x61, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((x61, offset), rest)
odE
odE \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (\<forall>y. length y = x62 \<longrightarrow> ex_cte_cap_wp_to P (x61, y) s) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<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. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> s' \<turnstile> \<lbrace>?P'138 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. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x61 x62 x63. \<lbrakk>cap = CNodeCap x61 x62 x63; (\<forall>y. length y = x62 \<longrightarrow> ex_cte_cap_wp_to P (x61, y) s') \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrakk> \<Longrightarrow> ?P'138 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'167 x61 x62 x63 () s' () s' rvb\<rbrace> returnOk ((x61, take x62 (drop (length x63) cref)), drop (x62 + length x63) cref) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. 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'154 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> (is_cnode_cap (fst (rvb, drop (x62 + length x63) cref)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (rvb, drop (x62 + length x63) cref)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)) \<and> (\<not> is_cnode_cap rvb \<longrightarrow> ?P'167 x61 x62 x63 rv s'' rva s''a rvb s)\<rbrace>, \<lbrace>\<lambda>_ _. 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>?B148 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> ex_cte_cap_wp_to P (fst ((x61, drop (length x63) cref), [])) s) \<and> (\<not> length cref \<le> x62 + length x63 \<longrightarrow> ?P'154 x61 x62 x63 rv s'' rva s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x61 x62 x63. \<lbrakk>cap = CNodeCap x61 x62 x63; \<not> (x62 = 0 \<and> x63 = [])\<rbrakk> \<Longrightarrow> s' \<turnstile> \<lbrace>?P'142 x61 x62 x63\<rbrace> whenE (\<not> x63 \<le> cref) (throwError (GuardMismatch (length cref) x63)) \<lbrace>?B148 x61 x62 x63\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>x61 x62 x63. \<lbrakk>cap = CNodeCap x61 x62 x63; (\<forall>y. length y = x62 \<longrightarrow> ex_cte_cap_wp_to P (x61, y) s') \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrakk> \<Longrightarrow> (x62 = 0 \<and> x63 = [] \<longrightarrow> True \<and> True) \<and> (\<not> (x62 = 0 \<and> x63 = []) \<longrightarrow> ?P'142 x61 x62 x63 s') proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x63. \<lbrakk>cap = CNodeCap x61 x62 x63; (\<forall>y. length y = x62 \<longrightarrow> ex_cte_cap_wp_to P (x61, y) s') \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrakk> \<Longrightarrow> (0 < x62 \<longrightarrow> x63 \<le> cref \<longrightarrow> \<not> length cref < x62 + length x63 \<longrightarrow> length cref \<noteq> x62 + length x63 \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) (x61, take x62 (drop (length x63) cref)) s' \<longrightarrow> is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s'). ex_cte_cap_wp_to P r s'))) \<and> (x63 \<noteq> [] \<longrightarrow> x63 \<le> cref \<longrightarrow> \<not> length cref < x62 + length x63 \<longrightarrow> length cref \<noteq> x62 + length x63 \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) (x61, take x62 (drop (length x63) cref)) s' \<longrightarrow> is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s'). ex_cte_cap_wp_to P r s'))) proof (prove)
goal:
No subgoals! proof (state)
this:
s' \<turnstile> \<lbrace>\<lambda>s. (is_cnode_cap (fst (cap, cref)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (cap, cref)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal:
No subgoals!