theory Retype_R

lemma createObjects_pspace_domain_valid':
  "\<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0
      \<and> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}
      \<and> pspace_domain_valid s\<rbrace>
       createObjects' ptr n val gbits
   \<lbrace>\<lambda>_. pspace_domain_valid\<rbrace>" apply (simp add: createObjects'_def split_def unless_def) apply (rule hoare_pre) apply (wp | wpc | simp only: alignError_def haskell_assert_def)+ apply (clarsimp simp: new_cap_addrs_fold' unat_1_0 unat_gt_0
                        range_cover_not_zero_shift
                        caps_overlap_reserved'_def) apply (simp add: pspace_domain_valid_def foldr_upd_app_if
                   fun_upd_def[symmetric]) apply (subgoal_tac " \<forall>x \<in> set (new_cap_addrs (unat (of_nat n << gbits)) ptr
                           val). {x..x + 2 ^ objBitsKO val - 1}
                                \<subseteq> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}") apply blast apply (rule ballI) apply (rule new_range_subset) apply (erule range_cover_rel, simp+) apply (simp add: range_cover.unat_of_nat_n_shift field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> pspace_domain_valid s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>_. pspace_domain_valid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> pspace_domain_valid s\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) (alignError (objBitsKO val + gbits));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - 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> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od \<lbrace>\<lambda>_. pspace_domain_valid\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) (alignError (objBitsKO val + gbits));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - 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> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od \<lbrace>\<lambda>_. pspace_domain_valid\<rbrace>
 2. \<And>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> pspace_domain_valid s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> pspace_domain_valid s \<Longrightarrow> (if ptr && mask (objBitsKO val + gbits) \<noteq> 0 then \<lambda>_. True else (\<lambda>s. (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> pspace_domain_valid (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>)) \<and> (\<forall>x. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some x \<longrightarrow> fst x < ptr \<longrightarrow> pspace_domain_valid (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) (ksPSpace s)\<rparr>)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; pspace_domain_valid s; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> pspace_domain_valid (s\<lparr>ksPSpace := foldr (\<lambda>addr map a. if a = addr then Some val else map a) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_domain_valid (s\<lparr>ksPSpace := foldr (\<lambda>addr map a. if a = addr then Some val else map a) (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) (ksPSpace s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x. x \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) \<longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> kernel_data_refs = {})) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x. x \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) \<longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> kernel_data_refs = {})) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; ptr && mask (objBitsKO val + gbits) = 0; \<forall>x\<in>set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val). {x..x + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x. x \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) \<longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> kernel_data_refs = {})) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x. x \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val) \<longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> kernel_data_refs = {}))
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val). {x..x + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; ptr && mask (objBitsKO val + gbits) = 0\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val). {x..x + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; ptr && mask (objBitsKO val + gbits) = 0; x \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val)\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; ptr && mask (objBitsKO val + gbits) = 0; x \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val)\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val) (?n128 s x)
 2. \<And>s x. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; ptr && mask (objBitsKO val + gbits) = 0; x \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val)\<rbrakk> \<Longrightarrow> x \<in> set (new_cap_addrs (?n128 s x) ptr val) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; ptr && mask (objBitsKO val + gbits) = 0; x \<in> set (new_cap_addrs (unat (word_of_nat n << gbits)) ptr val)\<rbrakk> \<Longrightarrow> x \<in> set (new_cap_addrs (2 ^ gbits * n) ptr val) proof (prove)
goal:
No subgoals!