theory Fastpath_C

lemma getCTE_ccorres_helper:
  "\<lbrakk> \<And>\<sigma> cte cte'. \<Gamma> \<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte
                               \<and> cslift s (cte_Ptr slot) = Some cte'
                               \<and> ccte_relation cte cte'}
                       f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)} \<rbrakk> \<Longrightarrow>
     ccorres r xf P P' hs (getCTE slot) f" apply atomize apply (rule ccorres_guard_imp2) apply (rule ccorres_add_return2) apply (rule ccorres_pre_getCTE) apply (rule_tac P="cte_wp_at' ((=) x) slot and P"
                in ccorres_from_vcg[where P'=P']) apply (erule allEI) apply (drule_tac x="the (ctes_of \<sigma> slot)" in spec) apply (erule HoarePartial.conseq) apply (clarsimp simp: return_def cte_wp_at_ctes_of) apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) apply simp apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}) \<Longrightarrow> ccorres r xf P P' hs (getCTE slot) f proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)} \<Longrightarrow> ccorres r xf P P' hs (getCTE slot) f proof (prove)
goal (2 subgoals):
 1. \<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)} \<Longrightarrow> ccorres r xf ?Q ?Q' hs (getCTE slot) f
 2. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)} \<Longrightarrow> ccorres r xf ?Q ?Q' hs (getCTE slot >>= return) f
 2. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)} \<Longrightarrow> ccorres r xf (?P5 x) (?P'5 x) hs (return x) f
 2. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ?P5 cte s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> ?P'5 (cte_to_H cte')} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)} \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (cte_wp_at' ((=) x) slot and P) \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} f {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)}
 2. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and P) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P'} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma>. \<forall>cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)} \<Longrightarrow> \<Gamma>\<turnstile> {s. (cte_wp_at' ((=) x) slot and P) \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} f {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)}
 2. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and P) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P'} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma>. \<forall>cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some (the (ctes_of \<sigma> slot)) \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation (the (ctes_of \<sigma> slot)) cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r (the (ctes_of \<sigma> slot)) (xf s)} \<Longrightarrow> \<Gamma>\<turnstile> {s. (cte_wp_at' ((=) x) slot and P) \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} f {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)}
 2. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and P) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P'} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma>. \<forall>s. s \<in> {s. (cte_wp_at' ((=) x) slot and P) \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<longrightarrow> (\<exists>cte'. s \<in> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some (the (ctes_of \<sigma> slot)) \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation (the (ctes_of \<sigma> slot)) cte'} \<and> {s. (\<sigma>, s) \<in> rf_sr \<and> r (the (ctes_of \<sigma> slot)) (xf s)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)} \<and> {} \<subseteq> {})
 2. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and P) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P'} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma> s. \<lbrakk>ctes_of \<sigma> slot = Some x; P \<sigma>; s \<in> P'; (\<sigma>, s) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>cte'. cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation x cte'
 2. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and P) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P'} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma> s y'. \<lbrakk>ctes_of \<sigma> slot = Some x; P \<sigma>; s \<in> P'; ctes_of \<sigma> slot = Some x; ccte_relation x y'; cslift s (cte_Ptr slot) = Some y'\<rbrakk> \<Longrightarrow> \<exists>cte'. cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation x cte'
 2. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and P) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P'} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>\<sigma> cte cte'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ctes_of \<sigma> slot = Some cte \<and> cslift s (cte_Ptr slot) = Some cte' \<and> ccte_relation cte cte'} f {s. (\<sigma>, s) \<in> rf_sr \<and> r cte (xf s)}; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and P) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P'} proof (prove)
goal:
No subgoals!