theory Fastpath_Equiv

lemma cnode_caps_gsCNodes_from_sr:
  "\<lbrakk> valid_objs s; (s, s') \<in> state_relation \<rbrakk> \<Longrightarrow> cnode_caps_gsCNodes' s'" apply (clarsimp simp: cnode_caps_gsCNodes_def only_cnode_caps_def
                        o_def ran_map_option) apply (safe, simp_all) apply (clarsimp elim!: ranE) apply (frule(1) pspace_relation_cte_wp_atI[rotated]) apply clarsimp apply (clarsimp simp: is_cap_simps) apply (frule(1) cte_wp_at_valid_objs_valid_cap) apply (clarsimp simp: valid_cap_simps cap_table_at_gsCNodes_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s')) (gsCNodes s') proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>valid_objs s; (s, s') \<in> state_relation; cap \<in> cteCap ` (ran (ctes_of s') \<inter> {x. isCNodeCap (cteCap x)}) \<or> cap \<in> (\<lambda>x. capability.NullCap) ` (ran (ctes_of s') \<inter> {x. \<not> isCNodeCap (cteCap x)}); isCNodeCap cap\<rbrakk> \<Longrightarrow> gsCNodes s' (capCNodePtr cap) = Some (capCNodeBits cap) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_objs s; (s, s') \<in> state_relation; x \<in> ran (ctes_of s'); isCNodeCap (cteCap x)\<rbrakk> \<Longrightarrow> gsCNodes s' (capCNodePtr (cteCap x)) = Some (capCNodeBits (cteCap x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>valid_objs s; (s, s') \<in> state_relation; isCNodeCap (cteCap x); ctes_of s' xa = Some x\<rbrakk> \<Longrightarrow> gsCNodes s' (capCNodePtr (cteCap x)) = Some (capCNodeBits (cteCap x)) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>valid_objs s; (s, s') \<in> state_relation; isCNodeCap (cteCap x); ctes_of s' xa = Some x\<rbrakk> \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')
 2. \<And>x xa. \<lbrakk>valid_objs s; (s, s') \<in> state_relation; isCNodeCap (cteCap x); ctes_of s' xa = Some x; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap x) \<and> xa = cte_map slot\<rbrakk> \<Longrightarrow> gsCNodes s' (capCNodePtr (cteCap x)) = Some (capCNodeBits (cteCap x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>valid_objs s; (s, s') \<in> state_relation; isCNodeCap (cteCap x); ctes_of s' xa = Some x; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap x) \<and> xa = cte_map slot\<rbrakk> \<Longrightarrow> gsCNodes s' (capCNodePtr (cteCap x)) = Some (capCNodeBits (cteCap x)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b r bits g. \<lbrakk>valid_objs s; (s, s') \<in> state_relation; ctes_of s' (cte_map (a, b)) = Some x; cte_wp_at ((=) (cap.CNodeCap r bits g)) (a, b) s; cteCap x = capability.CNodeCap r bits (of_bl g) (length g)\<rbrakk> \<Longrightarrow> gsCNodes s' r = Some bits proof (prove)
goal (1 subgoal):
 1. \<And>x a b r bits g. \<lbrakk>valid_objs s; (s, s') \<in> state_relation; ctes_of s' (cte_map (a, b)) = Some x; cte_wp_at ((=) (cap.CNodeCap r bits g)) (a, b) s; cteCap x = capability.CNodeCap r bits (of_bl g) (length g); \<exists>cap. cap.CNodeCap r bits g = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> gsCNodes s' r = Some bits proof (prove)
goal:
No subgoals!