theory Detype_R

lemma simpler_placeNewObject_def:
  "\<lbrakk>us < word_bits;is_aligned ptr (objBitsKO (injectKOS val) + us);
    pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s \<rbrakk> \<Longrightarrow> placeNewObject ptr val us s =
    modify (ksPSpace_update
       (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val))
       (ksPSpace s))) s" apply (clarsimp simp:placeNewObject_def2) apply (clarsimp simp:createObjects'_def) apply (simp add:bind_def in_monad when_def is_aligned_mask[THEN iffD1]) apply (clarsimp simp:return_def bind_def gets_def assert_def fail_def get_def split_def
                  split:option.splits) apply (clarsimp simp: new_cap_addrs_fold' word_1_le_power[where 'a=32, folded word_bits_def] lookupAround2_char1 not_less) apply (drule(1) pspace_no_overlapD'[rotated]) apply (drule_tac x = a in in_empty_interE) apply clarsimp apply (drule(1) pspace_alignedD') apply (simp add:is_aligned_no_overflow) apply (clarsimp simp: is_aligned_neg_mask_eq shiftL_nat p_assoc_help) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s\<rbrakk> \<Longrightarrow> placeNewObject ptr val us s = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s\<rbrakk> \<Longrightarrow> createObjects' ptr (Suc 0) (injectKOS val) us s = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s\<rbrakk> \<Longrightarrow> (do y <- unless (ptr && mask (objBitsKO (injectKOS val) + us) = 0) (alignError (objBitsKO (injectKOS val) + us));
ps <- gets ksPSpace;
case lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0)) ps of (before, uu_) \<Rightarrow> do y <- case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) ps))
od
od) s = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return () s). fst (case x of (y, s) \<Rightarrow> (\<Union>x\<in>fst (gets ksPSpace s). fst (case x of (ps, x) \<Rightarrow> (case lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0)) ps of (before, uu_) \<Rightarrow> \<lambda>s. (\<Union>x\<in>fst ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s). fst (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) ps)) x), (\<exists>x\<in>fst ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s). snd (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) ps)) x)) \<or> snd ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s))) x), (\<exists>x\<in>fst (gets ksPSpace s). snd (case x of (ps, x) \<Rightarrow> (case lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0)) ps of (before, uu_) \<Rightarrow> \<lambda>s. (\<Union>x\<in>fst ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s). fst (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) ps)) x), (\<exists>x\<in>fst ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s). snd (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) ps)) x)) \<or> snd ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s))) x)) \<or> snd (gets ksPSpace s))), (\<exists>x\<in>fst (return () s). snd (case x of (y, s) \<Rightarrow> (\<Union>x\<in>fst (gets ksPSpace s). fst (case x of (ps, x) \<Rightarrow> (case lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0)) ps of (before, uu_) \<Rightarrow> \<lambda>s. (\<Union>x\<in>fst ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s). fst (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) ps)) x), (\<exists>x\<in>fst ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s). snd (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) ps)) x)) \<or> snd ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s))) x), (\<exists>x\<in>fst (gets ksPSpace s). snd (case x of (ps, x) \<Rightarrow> (case lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0)) ps of (before, uu_) \<Rightarrow> \<lambda>s. (\<Union>x\<in>fst ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s). fst (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) ps)) x), (\<exists>x\<in>fst ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s). snd (case x of (y, x) \<Rightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) ps)) x)) \<or> snd ((case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr)) s))) x)) \<or> snd (gets ksPSpace s)))) \<or> snd (return () s)) = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) (ksPSpace s))) s = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) \<and> (\<forall>a. (a < ptr \<longrightarrow> (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS val))) [0 .e. 2 ^ us - 1]) (ksPSpace s))) s = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s) \<and> (\<not> a < ptr \<longrightarrow> (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> ({}, True) = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b\<rbrakk> \<Longrightarrow> ({}, True) = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; {a..a + 2 ^ objBitsKO b - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1} = {}\<rbrakk> \<Longrightarrow> ({}, True) = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b\<rbrakk> \<Longrightarrow> a \<in> {a..a + 2 ^ objBitsKO b - 1}
 2. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b\<rbrakk> \<Longrightarrow> a \<in> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1}
 3. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; False\<rbrakk> \<Longrightarrow> ({}, True) = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b\<rbrakk> \<Longrightarrow> a \<le> a + 2 ^ objBitsKO b - 1
 2. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b\<rbrakk> \<Longrightarrow> a \<in> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1}
 3. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; False\<rbrakk> \<Longrightarrow> ({}, True) = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; is_aligned a (objBitsKO b)\<rbrakk> \<Longrightarrow> a \<le> a + 2 ^ objBitsKO b - 1
 2. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b\<rbrakk> \<Longrightarrow> a \<in> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1}
 3. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; False\<rbrakk> \<Longrightarrow> ({}, True) = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b\<rbrakk> \<Longrightarrow> a \<in> {ptr..(ptr && ~~ mask (objBitsKO (injectKOS val) + us)) + 2 ^ (objBitsKO (injectKOS val) + us) - 1}
 2. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; False\<rbrakk> \<Longrightarrow> ({}, True) = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_aligned' s; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL (Suc 0) (objBitsKO (injectKOS val) + us) - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; False\<rbrakk> \<Longrightarrow> ({}, True) = modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s proof (prove)
goal:
No subgoals!