theory RAB_FN

lemma resolveAddressBitsFn_real_cte_at':
  "resolveAddressBitsFn cap addr depth (only_cnode_caps (ctes_of s)) = Inr rv
    \<Longrightarrow> (isCNodeCap cap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)
    \<Longrightarrow> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)
    \<Longrightarrow> valid_objs' s \<Longrightarrow> valid_cap' cap s
    \<Longrightarrow> real_cte_at' (fst rv) s" using monadic_rewrite_refine_validE_R[where F=False and P''=\<top>,
    OF resolveAddressBitsFn_eq resolveAddressBits_real_cte_at'] apply (clarsimp simp: valid_def validE_R_def validE_def simpler_gets_def) apply (cases rv, clarsimp) apply metis done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>resolveAddressBitsFn cap addr depth (only_cnode_caps (ctes_of s)) = Inr rv; isCNodeCap cap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s; cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); valid_objs' s; valid_cap' cap s\<rbrakk> \<Longrightarrow> real_cte_at' (fst rv) s proof (prove)
using this:
False \<longrightarrow> no_fail (\<lambda>_. True) (CSpace_H.resolveAddressBits ?cap2 ?addr2 ?depth2) \<Longrightarrow> \<lbrace>(\<lambda>s. (isCNodeCap ?cap2 \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = ?cap2) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) and (valid_objs' and valid_cap' ?cap2) and (\<lambda>_. True)\<rbrace> gets (resolveAddressBitsFn ?cap2 ?addr2 ?depth2 \<circ> only_cnode_caps \<circ> ctes_of) \<lbrace>\<lambda>rv. real_cte_at' (fst rv)\<rbrace>, -

goal (1 subgoal):
 1. \<lbrakk>resolveAddressBitsFn cap addr depth (only_cnode_caps (ctes_of s)) = Inr rv; isCNodeCap cap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s; cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); valid_objs' s; valid_cap' cap s\<rbrakk> \<Longrightarrow> real_cte_at' (fst rv) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>resolveAddressBitsFn cap addr depth (only_cnode_caps (ctes_of s)) = Inr rv; isCNodeCap cap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s; cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); valid_objs' s; valid_cap' cap s; \<And>cap addr depth. \<forall>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<and> valid_objs' s \<and> valid_cap' cap s \<longrightarrow> (\<forall>a. (\<exists>b. resolveAddressBitsFn cap addr depth (only_cnode_caps (ctes_of s)) = Inr (a, b)) \<longrightarrow> real_cte_at' a s)\<rbrakk> \<Longrightarrow> real_cte_at' (fst rv) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>resolveAddressBitsFn cap addr depth (only_cnode_caps (ctes_of s)) = Inr (a, b); isCNodeCap cap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s; cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s); valid_objs' s; valid_cap' cap s; \<And>cap addr depth. \<forall>s. (isCNodeCap cap \<longrightarrow> (\<exists>slot. cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s)) \<and> valid_objs' s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) \<and> valid_objs' s \<and> valid_cap' cap s \<longrightarrow> (\<forall>a. (\<exists>b. resolveAddressBitsFn cap addr depth (only_cnode_caps (ctes_of s)) = Inr (a, b)) \<longrightarrow> real_cte_at' a s); rv = (a, b)\<rbrakk> \<Longrightarrow> real_cte_at' a s proof (prove)
goal:
No subgoals!