theory Detype_R

lemma createObjects_gsUntypedZeroRanges_commute':
  "monad_commute \<top>
     (createObjects' ptr n ko us)
     (modify (\<lambda>s. s \<lparr> gsUntypedZeroRanges := f (gsUntypedZeroRanges s) \<rparr> ))" apply (simp add: createObjects'_def unless_def when_def alignError_def
                   fail_commute) apply clarsimp apply (rule commute_commute) apply (strengthen monad_commute_guard_imp[OF monad_commute_split[where P="\<top>" and Q="\<top>\<top>"], OF _ _ hoare_vcg_prop]
     | simp add: modify_commute split: option.split prod.split)+ apply (simp add: monad_commute_def exec_modify exec_gets assert_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (createObjects' ptr n ko us) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. ptr && mask (objBitsKO ko + us) = 0 \<longrightarrow> monad_commute (\<lambda>_. True) (do ps <- gets ksPSpace;
case lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) ps of (before, uu_) \<Rightarrow> do y <- case before of None \<Rightarrow> return () | Some (xa, xaa) \<Rightarrow> assert (xa < 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
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. ptr && mask (objBitsKO ko + us) = 0 \<Longrightarrow> monad_commute (\<lambda>_. True) (do ps <- gets ksPSpace;
case lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + 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> ko)) (map (\<lambda>n. ptr + (n << objBitsKO ko)) [0 .e. (word_of_nat n << us) - 1]) ps))
od
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. ptr && mask (objBitsKO ko + us) = 0 \<Longrightarrow> monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (do ps <- gets ksPSpace;
case lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + 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> ko)) (map (\<lambda>n. ptr + (n << objBitsKO ko)) [0 .e. (word_of_nat n << us) - 1]) ps))
od
od) proof (prove)
goal (1 subgoal):
 1. ptr && mask (objBitsKO ko + us) = 0 \<Longrightarrow> (\<forall>x xa. (\<exists>b x2. lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO ko + us) - Suc 0)) x = (Some (xa, b), x2)) \<longrightarrow> monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (assert (xa < ptr))) \<and> monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (gets ksPSpace) proof (prove)
goal:
No subgoals!