theory Fastpath_C

lemma getCTE_h_val_ccorres_split:
  assumes var: "\<And>s f s'. var (var_update f s) = f (var s)
                  \<and> ((s', var_update f s) \<in> rf_sr) = ((s', s) \<in> rf_sr)"
     and "\<And>rv' t t'. ceqv \<Gamma> var rv' t t' g (g' rv')"
     and "\<And>rv rv'. \<lbrakk> ccap_relation (cteCap rv) rv'; P rv \<rbrakk>
                \<Longrightarrow> ccorres r xf (Q rv) (Q' rv rv') hs (f rv) (g' rv')"
  shows
  "ccorres r xf (\<lambda>s. \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s)
                {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte
                          \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap)
                           \<and> slot' = cte_Ptr slot} hs
       (getCTE slot >>= (\<lambda>rv. f rv))
   ((Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot' \<rightarrow>[''cap_C'']))) s));; g)"
    (is "ccorres r xf ?G ?G' hs ?f ?g") apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) apply (rule_tac A="cte_wp_at' ((=) rv and P) slot and Q rv" and A'="?G'" in ccorres_guard_imp2) apply (rule_tac P="P rv" in ccorres_gen_asm) apply (rule ccorres_symb_exec_r) apply (rule_tac xf'=var in ccorres_abstract) apply (rule assms) apply (rule ccorres_gen_asm2, erule(1) assms) apply vcg apply (rule conseqPre, vcg, clarsimp simp: var) apply (clarsimp simp: cte_wp_at_ctes_of var) apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) apply (clarsimp simp: typ_heap_simps' dest!: ccte_relation_ccap_relation) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s) {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot} hs (getCTE slot >>= f) (Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s);;
g) proof (prove)
goal (2 subgoals):
 1. ccorres r xf ?Q ?Q' hs (getCTE slot >>= f) (Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s);;
g)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres r xf (?P3 rv) (?P'3 rv) hs (f rv) (Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s);;
g)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ?P3 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'3 (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>rv. ccorres r xf (?Q5 rv) (?Q'5 rv) hs (f rv) (Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s);;
g)
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' ((=) rv and P) slot and Q rv) s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> ?Q5 rv s \<and> s' \<in> ?Q'5 rv
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (3 subgoals):
 1. \<And>rv. P rv \<Longrightarrow> ccorres r xf (?G6 rv) (?Q'5 rv) hs (f rv) (Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s);;
g)
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' ((=) rv and P) slot and Q rv) s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (?G6 rv and (\<lambda>_. P rv)) s \<and> s' \<in> ?Q'5 rv
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (5 subgoals):
 1. \<And>rv. P rv \<Longrightarrow> ccorres r xf (?G6 rv) (?Q'7 rv) hs (f rv) g
 2. \<And>rv. P rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'5 rv) Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s) (?Q'7 rv)
 3. \<And>rv s. \<lbrakk>P rv; ?G6 rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'5 rv \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s) {s'. (s, s') \<in> rf_sr}
 4. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' ((=) rv and P) slot and Q rv) s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (?G6 rv and (\<lambda>_. P rv)) s \<and> s' \<in> ?Q'5 rv
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' t t'. P rv \<Longrightarrow> ceqv \<Gamma> var rv' t t' g (?d'11 rv rv')
 2. \<And>rv rv'. P rv \<Longrightarrow> ccorres r xf (?G6 rv) (?G'11 rv rv') hs (f rv) (?d'11 rv rv')
 3. \<And>rv. P rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'5 rv) Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s) {s. s \<in> ?G'11 rv (var s)}
 4. \<And>rv s. \<lbrakk>P rv; ?G6 rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'5 rv \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s) {s'. (s, s') \<in> rf_sr}
 5. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' ((=) rv and P) slot and Q rv) s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (?G6 rv and (\<lambda>_. P rv)) s \<and> s' \<in> ?Q'5 rv
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. P rv \<Longrightarrow> ccorres r xf (?G6 rv) (?G'11 rv rv') hs (f rv) (g' rv')
 2. \<And>rv. P rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'5 rv) Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s) {s. s \<in> ?G'11 rv (var s)}
 3. \<And>rv s. \<lbrakk>P rv; ?G6 rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'5 rv \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s) {s'. (s, s') \<in> rf_sr}
 4. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' ((=) rv and P) slot and Q rv) s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (?G6 rv and (\<lambda>_. P rv)) s \<and> s' \<in> ?Q'5 rv
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (4 subgoals):
 1. \<And>rv. P rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'5 rv) Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s) {s. s \<in> Q' rv (var s) \<inter> \<lbrace>ccap_relation (cteCap rv) (var s)\<rbrace>}
 2. \<And>rv s. \<lbrakk>P rv; Q rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'5 rv \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s) {s'. (s, s') \<in> rf_sr}
 3. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' ((=) rv and P) slot and Q rv) s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (Q rv and (\<lambda>_. P rv)) s \<and> s' \<in> ?Q'5 rv
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>P rv; Q rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s \<in> Q' rv (var (var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s)) \<and> ccap_relation (cteCap rv) (var (var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s))} \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s) {s'. (s, s') \<in> rf_sr}
 2. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' ((=) rv and P) slot and Q rv) s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (Q rv and (\<lambda>_. P rv)) s \<and> s' \<in> {s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s \<in> Q' rv (var (var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s)) \<and> ccap_relation (cteCap rv) (var (var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s))}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (2 subgoals):
 1. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; (cte_wp_at' ((=) rv and P) slot and Q rv) s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (Q rv and (\<lambda>_. P rv)) s \<and> s' \<in> {s. var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s \<in> Q' rv (var (var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s)) \<and> ccap_relation (cteCap rv) (var (var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))) s))}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (2 subgoals):
 1. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s slot = Some rv; \<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s' \<in> Q' cte cap; slot' = cte_Ptr slot; P rv; Q rv s\<rbrakk> \<Longrightarrow> var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s' \<in> Q' rv (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap rv) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (2 subgoals):
 1. \<And>rv s s' y'. \<lbrakk>ctes_of s slot = Some rv; \<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s' \<in> Q' cte cap; slot' = cte_Ptr slot; P rv; Q rv s; ctes_of s slot = Some rv; ccte_relation rv y'; cslift s' (cte_Ptr slot) = Some y'\<rbrakk> \<Longrightarrow> var_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s' \<in> Q' rv (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap rv) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> P cte \<and> Q cte s; s' \<in> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte and P) slot and Q 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> {s. (\<forall>cte cap. ccap_relation (cteCap cte) cap \<and> P cte \<longrightarrow> var_update (\<lambda>_. cap) s \<in> Q' cte cap) \<and> slot' = cte_Ptr slot}} proof (prove)
goal:
No subgoals!