theory CSpaceAcc_C

lemma locateSlotCNode_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
    (locateSlotCNode cnode bits offset)
    (Guard MemorySafety
          {s. x s = 0 \<or> array_assertion (cte_Ptr cnode') (unat offset') (hrs_htd (t_hrs_' (globals s)))}
          (Basic (\<lambda>s. xfu (\<lambda>_. cte_Ptr (cnode' + offset'
              * of_nat (size_of TYPE(cte_C)))) s)))" apply (simp add: locateSlot_conv split del: if_split) apply (rule ccorres_guard_imp2) apply (rule_tac P="cnode = cnode' \<and> offset = offset'" in ccorres_gen_asm2) apply (rule ccorres_stateAssert) apply (rule ccorres_move_array_assertion_cnode_ctes) apply (rule ccorres_return[where R="\<top>" and R'=UNIV]) apply (rule conseqPre, vcg) apply (clarsimp simp: fg rf_sr_def gl cte_level_bits_def field_simps) apply (clarsimp simp: Collect_const_mem split: option.split_asm) apply (rule unat_le_helper, simp) 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 (locateSlotCNode cnode bits offset) (Guard MemorySafety {s. x s = (0::'b) \<or> array_assertion (cte_Ptr cnode') (unat offset') (hrs_htd (t_hrs_' (globals s)))} (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) (if cnode = cnode' \<and> offset = offset' then UNIV else {}) hs (do x <- stateAssert (\<lambda>s. case gsCNodes s cnode of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> offset < 2 ^ n) [];
return (cnode + 2 ^ cte_level_bits * offset)
od) (Guard MemorySafety {s. x s = (0::'b) \<or> array_assertion (cte_Ptr cnode') (unat offset') (hrs_htd (t_hrs_' (globals s)))} (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10))))) proof (prove)
goal (2 subgoals):
 1. ccorres (\<lambda>v v'. v' = cte_Ptr v) xf ?Q6 ?Q'6 hs (do x <- stateAssert (\<lambda>s. case gsCNodes s cnode of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> offset < 2 ^ n) [];
return (cnode + 2 ^ cte_level_bits * offset)
od) (Guard MemorySafety {s. x s = (0::'b) \<or> array_assertion (cte_Ptr cnode') (unat offset') (hrs_htd (t_hrs_' (globals s)))} (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10)))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> (if cnode = cnode' \<and> offset = offset' then UNIV else {})\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?Q'6 proof (prove)
goal (2 subgoals):
 1. cnode = cnode' \<and> offset = offset' \<Longrightarrow> ccorres (\<lambda>v v'. v' = cte_Ptr v) xf ?Q6 ?G'9 hs (do x <- stateAssert (\<lambda>s. case gsCNodes s cnode of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> offset < 2 ^ n) [];
return (cnode + 2 ^ cte_level_bits * offset)
od) (Guard MemorySafety {s. x s = (0::'b) \<or> array_assertion (cte_Ptr cnode') (unat offset') (hrs_htd (t_hrs_' (globals s)))} (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10)))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> (if cnode = cnode' \<and> offset = offset' then UNIV else {})\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?G'9 \<inter> \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> proof (prove)
goal (2 subgoals):
 1. cnode = cnode' \<and> offset = offset' \<Longrightarrow> ccorres (\<lambda>v v'. v' = cte_Ptr v) xf ?P10 ?G'9 hs (return (cnode + 2 ^ cte_level_bits * offset)) (Guard MemorySafety {s. x s = (0::'b) \<or> array_assertion (cte_Ptr cnode') (unat offset') (hrs_htd (t_hrs_' (globals s)))} (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10)))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> (if cnode = cnode' \<and> offset = offset' then UNIV else {})\<rbrakk> \<Longrightarrow> ((case gsCNodes s cnode of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> offset < 2 ^ n) \<longrightarrow> ?P10 s) \<and> s' \<in> ?G'9 \<inter> \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> proof (prove)
goal (2 subgoals):
 1. cnode = cnode' \<and> offset = offset' \<Longrightarrow> ccorres (\<lambda>v v'. v' = cte_Ptr v) xf ?A12 ?C'12 hs (return (cnode + 2 ^ cte_level_bits * offset)) (Basic (xfu (\<lambda>_. cte_Ptr (cnode' + offset' * 0x10))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> (if cnode = cnode' \<and> offset = offset' then UNIV else {})\<rbrakk> \<Longrightarrow> ((case gsCNodes s cnode of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> offset < 2 ^ n) \<longrightarrow> (?A12 and (\<lambda>s. \<exists>n. gsCNodes s cnode' = Some n \<and> unat offset' \<le> 2 ^ n)) s) \<and> s' \<in> ?C'12 \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cnode = cnode' \<and> offset = offset'; True\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<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)}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> (if cnode = cnode' \<and> offset = offset' then UNIV else {})\<rbrakk> \<Longrightarrow> ((case gsCNodes s cnode of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> offset < 2 ^ n) \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<exists>n. gsCNodes s cnode' = Some n \<and> unat offset' \<le> 2 ^ n)) s) \<and> s' \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cnode = cnode' \<and> offset = offset'; True\<rbrakk> \<Longrightarrow> UNIV \<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)}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> (if cnode = cnode' \<and> offset = offset' then UNIV else {})\<rbrakk> \<Longrightarrow> ((case gsCNodes s cnode of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> offset < 2 ^ n) \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<exists>n. gsCNodes s cnode' = Some n \<and> unat offset' \<le> 2 ^ n)) s) \<and> s' \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> (if cnode = cnode' \<and> offset = offset' then UNIV else {})\<rbrakk> \<Longrightarrow> ((case gsCNodes s cnode of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> offset < 2 ^ n) \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<exists>n. gsCNodes s cnode' = Some n \<and> unat offset' \<le> 2 ^ n)) s) \<and> s' \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>cnode = cnode' \<and> offset = offset'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; cnode = cnode'; offset = offset'; gsCNodes s cnode' = Some bits; offset' < 2 ^ bits\<rbrakk> \<Longrightarrow> unat offset' \<le> 2 ^ bits proof (prove)
goal:
No subgoals!