theory CNode_DR

lemma dcorres_storeWord_mapM_x_cvt:
  "\<forall>x\<in>set ls. within_page buf x sz
   \<Longrightarrow> dcorres dc (\<lambda>_. True) (ko_at (ArchObj (DataPage False sz)) buf and  valid_objs and pspace_distinct and pspace_aligned and valid_etcbs)
    (corrupt_frame buf)
       (do_machine_op (mapM (\<lambda>p. storeWord p 0) ls))" proof (induct ls) case Nil show ?case apply (clarsimp simp:mapM_def sequence_def dc_def[symmetric]) apply (rule corres_guard_imp[OF dcorres_dummy_corrupt_frame]) apply simp+ done next case (Cons ls x) show ?case apply (clarsimp simp:mapM_Cons) apply (subst do_machine_op_bind) apply (clarsimp simp:ef_storeWord empty_fail_cond)+ apply (subst corrupt_frame_duplicate[symmetric]) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule dcorres_store_word_conservative[where sz = sz]) using Cons apply simp apply (clarsimp) apply (subst do_machine_op_bind) apply (rule empty_fail_mapM,clarsimp simp:ef_storeWord) apply (clarsimp simp:dc_def[symmetric])+ apply (rule corres_dummy_return_l) apply (rule corres_split) apply (rule_tac Cons.hyps) using Cons apply simp apply (rule corres_free_return[where P = \<top> and P'=\<top>]) apply wp+ using Cons apply fastforce apply (wp|clarsimp|force)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set ls. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) ls)) proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>set []. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) []))
 2. \<And>a ls. \<lbrakk>\<forall>x\<in>set ls. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) ls)); \<forall>x\<in>set (a # ls). within_page buf x sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) (a # ls))) proof (state)
this:
\<forall>x\<in>set []. within_page buf x sz

goal (2 subgoals):
 1. \<forall>x\<in>set []. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) []))
 2. \<And>a ls. \<lbrakk>\<forall>x\<in>set ls. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) ls)); \<forall>x\<in>set (a # ls). within_page buf x sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) (a # ls))) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) [])) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>a. ako_at (DataPage False sz) buf a \<and> valid_objs a \<and> pspace_distinct a \<and> pspace_aligned a \<and> valid_etcbs a) (corrupt_frame buf) (return []) proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> True
 2. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> valid_etcbs s proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) []))

goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>\<forall>x\<in>set ls. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) ls)); \<forall>x\<in>set (a # ls). within_page buf x sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) (a # ls))) proof (state)
goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>\<forall>x\<in>set ls. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) ls)); \<forall>x\<in>set (a # ls). within_page buf x sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) (a # ls))) proof (state)
this:
\<forall>x\<in>set x. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) x))
\<forall>x\<in>set (ls # x). within_page buf x sz

goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>\<forall>x\<in>set ls. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) ls)); \<forall>x\<in>set (a # ls). within_page buf x sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) (a # ls))) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) (ls # x))) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. ako_at (DataPage False sz) buf a \<and> valid_objs a \<and> pspace_distinct a \<and> pspace_aligned a \<and> valid_etcbs a) (corrupt_frame buf) (do_machine_op (do y <- storeWord ls 0;
ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od)) proof (prove)
goal (3 subgoals):
 1. empty_fail (storeWord ls 0)
 2. \<And>xa. empty_fail (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od)
 3. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. ako_at (DataPage False sz) buf a \<and> valid_objs a \<and> pspace_distinct a \<and> pspace_aligned a \<and> valid_etcbs a) (corrupt_frame buf) (do rv <- do_machine_op (storeWord ls 0);
do_machine_op (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od)
od) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. ako_at (DataPage False sz) buf a \<and> valid_objs a \<and> pspace_distinct a \<and> pspace_aligned a \<and> valid_etcbs a) (corrupt_frame buf) (do rv <- do_machine_op (storeWord ls 0);
do_machine_op (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od)
od) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. ako_at (DataPage False sz) buf a \<and> valid_objs a \<and> pspace_distinct a \<and> pspace_aligned a \<and> valid_etcbs a) (do _ <- corrupt_frame buf;
corrupt_frame buf
od) (do rv <- do_machine_op (storeWord ls 0);
do_machine_op (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od)
od) proof (prove)
goal (3 subgoals):
 1. dcorres (\<lambda>a b. True) ?Q ?Q' (do _ <- corrupt_frame buf;
corrupt_frame buf
od) (do rv <- do_machine_op (storeWord ls 0);
do_machine_op (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. dcorres ?r'4 ?P4 ?P'4 (corrupt_frame buf) (do_machine_op (storeWord ls 0))
 2. \<And>uu_ rv. ?r'4 uu_ rv \<Longrightarrow> dcorres (\<lambda>a b. True) (?R4 uu_) (?R'4 rv) (corrupt_frame buf) (do_machine_op (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od))
 3. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. within_page buf ls sz
 2. \<And>uu_ rv. dc uu_ rv \<Longrightarrow> dcorres (\<lambda>a b. True) (?R4 uu_) (?R'4 rv) (corrupt_frame buf) (do_machine_op (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od))
 3. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s proof (prove)
using this:
\<forall>x\<in>set x. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) x))
\<forall>x\<in>set (ls # x). within_page buf x sz

goal (6 subgoals):
 1. within_page buf ls sz
 2. \<And>uu_ rv. dc uu_ rv \<Longrightarrow> dcorres (\<lambda>a b. True) (?R4 uu_) (?R'4 rv) (corrupt_frame buf) (do_machine_op (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od))
 3. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>uu_ rv. dc uu_ rv \<Longrightarrow> dcorres (\<lambda>a b. True) (?R4 uu_) (?R'4 rv) (corrupt_frame buf) (do_machine_op (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od))
 2. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. dcorres (\<lambda>a b. True) (?R4 ()) (?R'4 ()) (corrupt_frame buf) (do_machine_op (do ys <- mapM (\<lambda>p. storeWord p 0) x;
return (() # ys)
od))
 2. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. empty_fail (mapM (\<lambda>p. storeWord p 0) x)
 2. \<And>x. empty_fail (return (() # x))
 3. dcorres (\<lambda>a b. True) (?R16 ()) (?R'16 ()) (corrupt_frame buf) (do rv <- do_machine_op (mapM (\<lambda>p. storeWord p 0) x);
do_machine_op (return (() # rv))
od)
 4. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>?R4\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>?R'4\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s
flex-flex pairs:
?R'16 () \<equiv>\<^sup>? ?R'4 ()
?R16 () \<equiv>\<^sup>? ?R4 () proof (prove)
goal (6 subgoals):
 1. \<And>x. empty_fail (return (() # x))
 2. dcorres (\<lambda>a b. True) (?R16 ()) (?R'16 ()) (corrupt_frame buf) (do rv <- do_machine_op (mapM (\<lambda>p. storeWord p 0) x);
do_machine_op (return (() # rv))
od)
 3. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s
flex-flex pairs:
?R'16 () \<equiv>\<^sup>? ?R'4 ()
?R16 () \<equiv>\<^sup>? ?R4 () proof (prove)
goal (5 subgoals):
 1. dcorres dc (?R16 ()) (?R'16 ()) (corrupt_frame buf) (do rv <- do_machine_op (mapM (\<lambda>p. storeWord p 0) x);
return (() # rv)
od)
 2. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s
flex-flex pairs:
?R'16 () \<equiv>\<^sup>? ?R'4 ()
?R16 () \<equiv>\<^sup>? ?R4 () proof (prove)
goal (5 subgoals):
 1. dcorres dc (?R16 ()) (?R'16 ()) (corrupt_frame buf >>= return) (do rv <- do_machine_op (mapM (\<lambda>p. storeWord p 0) x);
return (() # rv)
od)
 2. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s
flex-flex pairs:
?R'16 () \<equiv>\<^sup>? ?R'4 ()
?R16 () \<equiv>\<^sup>? ?R4 () proof (prove)
goal (8 subgoals):
 1. dcorres ?r'24 (?P38 ()) (?P'34 ()) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) x))
 2. \<And>x rv'. ?r'24 x rv' \<Longrightarrow> dcorres dc (?R24 x) (?R'24 rv') (return x) (return (() # rv'))
 3. \<lbrace>?Q37 ()\<rbrace> corrupt_frame buf \<lbrace>?R24\<rbrace>
 4. \<lbrace>?Q'33 ()\<rbrace> do_machine_op (mapM (\<lambda>p. storeWord p 0) x) \<lbrace>?R'24\<rbrace>
 5. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. ?P40 a and ?Q39 a\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>\<lambda>a. ?P'36 a and ?Q'35 a\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s
flex-flex pairs:
?P40 () \<equiv>\<^sup>? ?P38 ()
?Q39 () \<equiv>\<^sup>? ?Q37 ()
?P'36 () \<equiv>\<^sup>? ?P'34 ()
?Q'35 () \<equiv>\<^sup>? ?Q'33 () proof (prove)
goal (8 subgoals):
 1. \<forall>x\<in>set x. within_page buf x sz
 2. \<And>x rv'. dc x rv' \<Longrightarrow> dcorres dc (?R24 x) (?R'24 rv') (return x) (return (() # rv'))
 3. \<lbrace>?Q37 ()\<rbrace> corrupt_frame buf \<lbrace>?R24\<rbrace>
 4. \<lbrace>?Q'33 ()\<rbrace> do_machine_op (mapM (\<lambda>p. storeWord p 0) x) \<lbrace>?R'24\<rbrace>
 5. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q39 a\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>\<lambda>a. ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'35 a\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s
flex-flex pairs:
?Q39 () \<equiv>\<^sup>? ?Q37 ()
?Q'35 () \<equiv>\<^sup>? ?Q'33 () proof (prove)
using this:
\<forall>x\<in>set x. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) x))
\<forall>x\<in>set (ls # x). within_page buf x sz

goal (8 subgoals):
 1. \<forall>x\<in>set x. within_page buf x sz
 2. \<And>x rv'. dc x rv' \<Longrightarrow> dcorres dc (?R24 x) (?R'24 rv') (return x) (return (() # rv'))
 3. \<lbrace>?Q37 ()\<rbrace> corrupt_frame buf \<lbrace>?R24\<rbrace>
 4. \<lbrace>?Q'33 ()\<rbrace> do_machine_op (mapM (\<lambda>p. storeWord p 0) x) \<lbrace>?R'24\<rbrace>
 5. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q39 a\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>\<lambda>a. ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'35 a\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s
flex-flex pairs:
?Q39 () \<equiv>\<^sup>? ?Q37 ()
?Q'35 () \<equiv>\<^sup>? ?Q'33 () proof (prove)
goal (7 subgoals):
 1. \<And>x rv'. dc x rv' \<Longrightarrow> dcorres dc (?R24 x) (?R'24 rv') (return x) (return (() # rv'))
 2. \<lbrace>?Q37 ()\<rbrace> corrupt_frame buf \<lbrace>?R24\<rbrace>
 3. \<lbrace>?Q'33 ()\<rbrace> do_machine_op (mapM (\<lambda>p. storeWord p 0) x) \<lbrace>?R'24\<rbrace>
 4. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q39 a\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>\<lambda>a. ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'35 a\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s
flex-flex pairs:
?Q39 () \<equiv>\<^sup>? ?Q37 ()
?Q'35 () \<equiv>\<^sup>? ?Q'33 () proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q37 ()\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<lbrace>?Q'33 ()\<rbrace> do_machine_op (mapM (\<lambda>p. storeWord p 0) x) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrace>?Q4\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q39 a\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> do_machine_op (storeWord ls 0) \<lbrace>\<lambda>a. ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'35 a\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'4) s
flex-flex pairs:
?Q39 () \<equiv>\<^sup>? ?Q37 ()
?Q'35 () \<equiv>\<^sup>? ?Q'33 () proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and (\<lambda>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<and> True)) s proof (prove)
using this:
\<forall>x\<in>set x. within_page buf x sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) x))
\<forall>x\<in>set (ls # x). within_page buf x sz

goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and (\<lambda>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<Longrightarrow> (ako_at (DataPage ?dev9 sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and (\<lambda>s. ako_at (DataPage False sz) buf s \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_etcbs s \<and> True)) s proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres dc (\<lambda>_. True) (ako_at (DataPage False sz) buf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame buf) (do_machine_op (mapM (\<lambda>p. storeWord p 0) (ls # x)))

goal:
No subgoals!