theory CSpaceAcc_C

lemma locateSlotTCB_ccorres [corres]:
  assumes gl: "\<And>v s. globals (xfu v s) = globals s" \<comment> \<open>for state rel. preservation\<close>
  and     fg: "\<And>v s. xf (xfu (\<lambda>_. v) s) = v"
  shows "ccorres (\<lambda>v v'. v' = Ptr v) xf \<top> {_. cnode = cnode' \<and> offset = offset'} hs
    (locateSlotTCB cnode offset)
    (Basic (\<lambda>s. xfu (\<lambda>_. Ptr (cnode' + offset' * of_nat (size_of TYPE(cte_C))) :: cte_C ptr) s))" unfolding locateSlot_conv using gl fg apply - apply (simp add: size_of_def split del: if_split) apply (rule ccorres_return) apply (rule conseqPre) apply vcg apply (clarsimp simp: fg objBits_simps cte_level_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>v v'. v' = cte_Ptr v) xf (\<lambda>_. True) \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> hs (locateSlotTCB cnode offset) (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * word_of_nat (size_of TYPE(cte_C)))))) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>v v'. v' = cte_Ptr v) xf (\<lambda>_. True) \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> hs (return (cnode + 2 ^ cte_level_bits * offset)) (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * word_of_nat (size_of TYPE(cte_C)))))) proof (prove)
using this:
globals (xfu ?v1 ?s1) = globals ?s1
xf (xfu (\<lambda>_. ?v1) ?s1) = ?v1

goal (1 subgoal):
 1. ccorres (\<lambda>v v'. v' = cte_Ptr v) xf (\<lambda>_. True) \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> hs (return (cnode + 2 ^ cte_level_bits * offset)) (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * word_of_nat (size_of TYPE(cte_C)))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v s. globals (xfu v s) = globals s; \<And>v s. xf (xfu (\<lambda>_. v) s) = v\<rbrakk> \<Longrightarrow> ccorres (\<lambda>v v'. v' = cte_Ptr v) xf (\<lambda>_. True) \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> hs (return (cnode + 2 ^ cte_level_bits * offset)) (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * word_of_nat (size_of TYPE(cte_C)))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v s. globals (xfu v s) = globals s; \<And>v s. xf (xfu (\<lambda>_. v) s) = v\<rbrakk> \<Longrightarrow> ccorres (\<lambda>v v'. v' = cte_Ptr v) xf (\<lambda>_. True) (if cnode = cnode' \<and> offset = offset' then UNIV else {}) hs (return (cnode + 2 ^ cte_level_bits * offset)) (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>v s. globals (xfu v s) = globals s; \<And>v s. xf (xfu (\<lambda>_. v) s) = v; True\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ((if cnode = cnode' \<and> offset = offset' then UNIV else {}) \<inter> {s'. (s, s') \<in> rf_sr}) Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10))) {s'. (s, s') \<in> rf_sr \<and> xf s' = cte_Ptr (cnode + 2 ^ cte_level_bits * offset)} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>v s. globals (xfu v s) = globals s; \<And>v s. xf (xfu (\<lambda>_. v) s) = v; True\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'8 s) Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10))) {s'. (s, s') \<in> rf_sr \<and> xf s' = cte_Ptr (cnode + 2 ^ cte_level_bits * offset)}
 2. \<And>s. \<lbrakk>\<And>v s. globals (xfu v s) = globals s; \<And>v s. xf (xfu (\<lambda>_. v) s) = v; True\<rbrakk> \<Longrightarrow> (if cnode = cnode' \<and> offset = offset' then UNIV else {}) \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> ?P'8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>v s. globals (xfu v s) = globals s; \<And>v s. xf (xfu (\<lambda>_. v) s) = v; True\<rbrakk> \<Longrightarrow> (if cnode = cnode' \<and> offset = offset' then UNIV else {}) \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10)) sa) \<in> rf_sr \<and> xf (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10)) sa) = cte_Ptr (cnode + 2 ^ cte_level_bits * offset)} proof (prove)
goal:
No subgoals!