theory Retype_C

lemma placeNewObject_eq:
  notes option.case_cong_weak [cong]
  shows
  "\<lbrakk> groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object));
    no_fail ((=) s) (placeNewObject ptr object groupSizeBits) \<rbrakk> \<Longrightarrow>
  ((), (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr>))
                \<in> fst (placeNewObject ptr object groupSizeBits s)" apply (clarsimp simp: placeNewObject_def placeNewObject'_def) apply (clarsimp simp: split_def field_simps split del: if_split) apply (clarsimp simp: no_fail_def) apply (subst lookupAround2_pspace_no) apply assumption apply (subst (asm) lookupAround2_pspace_no) apply assumption apply (clarsimp simp add: in_monad' split_def bind_assoc field_simps
    snd_bind ball_to_all unless_def  split: option.splits if_split_asm) apply (clarsimp simp: data_map_insert_def new_cap_addrs_def) apply (subst upto_enum_red2) apply (fold word_bits_def, assumption) apply (clarsimp simp: field_simps shiftl_t2n power_add mult.commute mult.left_commute
           cong: foldr_cong map_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); no_fail ((=) s) (placeNewObject ptr object groupSizeBits)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr>) \<in> fst (placeNewObject ptr object groupSizeBits s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); no_fail ((=) s) (do y <- unless (ptr && mask (objBitsKO (injectKOS object) + groupSizeBits) = 0) (alignError (objBitsKO (injectKOS object) + groupSizeBits));
ps <- gets ksPSpace;
case lookupAround2 (ptr + (2 ^ (objBitsKO (injectKOS object) + groupSizeBits) - 1)) ps of (before, uu_) \<Rightarrow> do y <- case before of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) [];
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od
od)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr>) \<in> fst ((do y <- unless (ptr && mask (objBitsKO (injectKOS object) + groupSizeBits) = 0) (alignError (objBitsKO (injectKOS object) + groupSizeBits));
ps <- gets ksPSpace;
case lookupAround2 (ptr + (2 ^ (objBitsKO (injectKOS object) + groupSizeBits) - 1)) ps of (before, uu_) \<Rightarrow> do y <- case before of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) [];
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od
od) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); no_fail ((=) s) (do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1) ps) of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) [];
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr>) \<in> fst ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1) ps) of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) [];
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); \<not> snd ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1) ps) of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) [];
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr>) \<in> fst ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1) ps) of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) [];
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s) proof (prove)
goal (2 subgoals):
 1. \<And>ps y. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); \<not> snd ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1) ps) of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) [];
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s)\<rbrakk> \<Longrightarrow> is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object))
 2. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); \<not> snd ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1) ps) of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) [];
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr>) \<in> fst ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- assert ({ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom ps = {});
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); \<not> snd ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1) ps) of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) [];
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr>) \<in> fst ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- assert ({ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom ps = {});
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object))\<rbrakk> \<Longrightarrow> is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object))
 2. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); \<not> snd ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- assert ({ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom ps = {});
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr>) \<in> fst ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- assert ({ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom ps = {});
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); \<not> snd ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- assert ({ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom ps = {});
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr>) \<in> fst ((do y <- unless (ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0) (alignError (groupSizeBits + objBitsKO (injectKOS object)));
ps <- gets ksPSpace;
y <- assert ({ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom ps = {});
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) ps))
od) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0; {ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom (ksPSpace s) = {}; \<not> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (new_cap_addrs (2 ^ groupSizeBits) ptr (injectKOS object)) (ksPSpace s)\<rparr> = s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) (ksPSpace s)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0; {ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom (ksPSpace s) = {}; \<not> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (map (\<lambda>p. ptr + (word_of_nat p << objBitsKO (injectKOS object))) [0..<2 ^ groupSizeBits]) (ksPSpace s)\<rparr> = s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) (ksPSpace s)\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>_. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0; {ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom (ksPSpace s) = {}; \<not> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> groupSizeBits < LENGTH(32)
 2. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0; {ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom (ksPSpace s) = {}; \<not> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (map (\<lambda>p. ptr + (word_of_nat p << objBitsKO (injectKOS object))) [0..<2 ^ groupSizeBits]) (ksPSpace s)\<rparr> = s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) (map word_of_nat [0..<2 ^ groupSizeBits])) (ksPSpace s)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>groupSizeBits < word_bits; is_aligned ptr (groupSizeBits + objBitsKO (injectKOS object)); ptr && mask (groupSizeBits + objBitsKO (injectKOS object)) = 0; {ptr..ptr + 2 ^ (groupSizeBits + objBitsKO (injectKOS object)) - 1} \<inter> dom (ksPSpace s) = {}; \<not> snd (modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) [0 .e. 2 ^ groupSizeBits - 1]) (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS object)) (map (\<lambda>p. ptr + (word_of_nat p << objBitsKO (injectKOS object))) [0..<2 ^ groupSizeBits]) (ksPSpace s)\<rparr> = s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS object)) (map (\<lambda>n. ptr + (n << objBitsKO (injectKOS object))) (map word_of_nat [0..<2 ^ groupSizeBits])) (ksPSpace s)\<rparr> proof (prove)
goal:
No subgoals!