theory Detype_R

lemma createObjects'_psp_aligned:
  "\<lbrace>pspace_aligned' and pspace_distinct' and
    pspace_no_overlap' ptr sz and
    K (range_cover ptr sz ((objBitsKO ko) + us) n \<and> n \<noteq> 0
    \<and> is_aligned ptr (objBitsKO ko + us) \<and> objBitsKO ko + us < word_bits)\<rbrace>
    createObjects' ptr n ko us
    \<lbrace>\<lambda>rv s. pspace_aligned' s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: createObjects'_def split_def) apply (subst new_cap_addrs_fold') apply (drule range_cover_not_zero_shift[where gbits = us,rotated]) apply simp+ apply unat_arith apply (rule hoare_pre) apply (wpc|wp|simp add: unless_def alignError_def del: fun_upd_apply hoare_fail_any)+ apply clarsimp apply (frule(2) retype_aligned_distinct'(2)[where ko = ko and n= "n*2^us" ]) apply (erule range_cover_rel) apply simp apply clarsimp apply (subst data_map_insert_def[symmetric])+ apply (simp add: range_cover.unat_of_nat_n_shift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz (objBitsKO ko + us) n \<and> n \<noteq> 0 \<and> is_aligned ptr (objBitsKO ko + us) \<and> objBitsKO ko + us < word_bits)\<rbrace> createObjects' ptr n ko us \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz (objBitsKO ko + us) n \<and> n \<noteq> 0 \<and> is_aligned ptr (objBitsKO ko + us) \<and> objBitsKO ko + us < word_bits)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> createObjects' ptr n ko us \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- unless (ptr && mask (objBitsKO ko + us) = 0) (alignError (objBitsKO ko + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (map (\<lambda>n. ptr + (n << objBitsKO ko)) [0 .e. (word_of_nat n << us) - 1]) ps))
od \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s _ ya ps y a. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n << us
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- unless (ptr && mask (objBitsKO ko + us) = 0) (alignError (objBitsKO ko + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) ps))
od \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s _ ya ps y a. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits\<rbrakk> \<Longrightarrow> us \<le> objBitsKO ko + us
 2. \<And>s _ ya ps y a. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<And>s _ ya ps y a. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; word_of_nat n << us \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n << us
 4. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- unless (ptr && mask (objBitsKO ko + us) = 0) (alignError (objBitsKO ko + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) ps))
od \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; word_of_nat n << us \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> word_of_nat n << us
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- unless (ptr && mask (objBitsKO ko + us) = 0) (alignError (objBitsKO ko + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) ps))
od \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- unless (ptr && mask (objBitsKO ko + us) = 0) (alignError (objBitsKO ko + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) ps))
od \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q22 s\<rbrace> do y <- unless (ptr && mask (objBitsKO ko + us) = 0) (alignError (objBitsKO ko + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) ps))
od \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
 2. \<And>s sa. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; s = sa\<rbrakk> \<Longrightarrow> ?Q22 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; s = sa\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO ko + us) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = None \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = None \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO ko) (n * 2 ^ us)
 2. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0; pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (n * 2 ^ us) ptr ko) (ksPSpace sa)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = None \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> objBitsKO ko + us
 2. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0\<rbrakk> \<Longrightarrow> n * 2 ^ us = 2 ^ (objBitsKO ko + us - objBitsKO ko) * n
 3. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0; pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (n * 2 ^ us) ptr ko) (ksPSpace sa)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = None \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0\<rbrakk> \<Longrightarrow> n * 2 ^ us = 2 ^ (objBitsKO ko + us - objBitsKO ko) * n
 2. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0; pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (n * 2 ^ us) ptr ko) (ksPSpace sa)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = None \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0; pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (n * 2 ^ us) ptr ko) (ksPSpace sa)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = None \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> ko)) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr sz sa; range_cover ptr sz (objBitsKO ko + us) n; 0 < n; is_aligned ptr (objBitsKO ko + us); objBitsKO ko + us < word_bits; ptr && mask (objBitsKO ko + us) = 0; pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (n * 2 ^ us) ptr ko) (ksPSpace sa)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = None \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) (ksPSpace sa)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_aligned' (sa\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (unat (word_of_nat n << us)) ptr ko) (ksPSpace sa)\<rparr>)) proof (prove)
goal:
No subgoals!