theory Retype_R

lemma createObjects_ret:
  "\<lbrakk>n < 2^word_bits;n\<noteq> 0\<rbrakk> \<Longrightarrow>
   \<lbrace>\<top>\<rbrace> createObjects y n ko gbits
   \<lbrace>\<lambda>r s. r = map (\<lambda>p. ptr_add y (p * 2 ^ objBitsKO ko * 2 ^ gbits))
                [0..< n]\<rbrace>" unfolding createObjects_def createObjects'_def apply (simp add: split_def) apply (wp|simp cong: if_cong)+ apply (clarsimp simp: ptr_add_def upto_enum_def o_def
                        unat_sub word_le_nat_alt
                        power_sub[symmetric]
                        objBits_def[symmetric]
              simp del: upt_Suc) apply (clarsimp simp: unat_of_nat_minus_1 word_bits_def
                        shiftl_t2n power_add) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ word_bits; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> createObjects y n ko gbits \<lbrace>\<lambda>r s. r = map (\<lambda>p. ptr_add y (p * 2 ^ objBitsKO ko * 2 ^ gbits)) [0..<n]\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ word_bits; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do oBits <- return (objBitsKO ko);
gBits <- return (oBits + gbits);
do oBits <- return (objBitsKO ko);
gBits <- return (oBits + gbits);
unless (fromPPtr y && mask gBits = 0) $ alignError gBits;
ps <- gets ksPSpace;
end <- return (fromPPtr y + fromIntegral (n `~shiftL~` gBits - 1));
(before, uu_) <- return (lookupAround2 end (psMap ps));
case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> haskell_assert (x < fromPPtr y) [];
addresses <- return (map (\<lambda>n. fromPPtr y + n `~shiftL~` oBits) [0 .e. fromIntegral n `~shiftL~` gbits - 1]);
map' <- return (foldR (\<lambda>addr. data_map_insert addr ko) (psMap ps) addresses);
ps' <- return (psMap_update (\<lambda>_. map') ps);
modify (ksPSpace_update (\<lambda>_. ps'))
od;
return (map (\<lambda>n. y + n `~shiftL~` gBits) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>r s. r = map (\<lambda>p. ptr_add y (p * 2 ^ objBitsKO ko * 2 ^ gbits)) [0..<n]\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ word_bits; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do ya <- do ya <- unless (y && mask (objBitsKO ko + gbits) = 0) (alignError (objBitsKO ko + gbits));
ps <- gets ksPSpace;
ya <- case fst (lookupAround2 (y + word_of_nat (shiftL n (objBitsKO ko + gbits) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < y);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (map (\<lambda>n. y + (n << objBitsKO ko)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od;
return (map (\<lambda>n. y + (n << objBitsKO ko + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>r s. r = map (\<lambda>p. ptr_add y (p * 2 ^ objBitsKO ko * 2 ^ gbits)) [0..<n]\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ word_bits; 0 < n\<rbrakk> \<Longrightarrow> map (\<lambda>n. y + (n << objBitsKO ko + gbits)) [0 .e. word_of_nat n - 1] = map (\<lambda>p. ptr_add y (p * 2 ^ objBitsKO ko * 2 ^ gbits)) [0..<n] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ word_bits; 0 < n\<rbrakk> \<Longrightarrow> map (\<lambda>x. y + (toEnum x << objBitsKO ko + gbits)) [0..<Suc (unat (word_of_nat n - 1))] = map (\<lambda>p. y + word_of_nat p * 2 ^ objBitsKO ko * 2 ^ gbits) [0..<n] proof (prove)
goal:
No subgoals!