theory Intent_DR

lemma zip_cpy_word_corres:
  "\<forall>x\<in> set xs. within_page buf (base + of_nat(x*word_size)) sz
    \<Longrightarrow> dcorres dc \<top>
   (pspace_aligned and pspace_distinct and valid_objs
    and (ipc_frame_ptr_at buf s_id) and (ipc_frame_sz_at sz s_id) and valid_etcbs)
   (corrupt_frame buf)
   (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x)
            xs)" proof (induct xs) case Nil show ?case apply (rule corres_guard_imp) apply (clarsimp simp:mapM_def sequence_def) apply (rule dcorres_dummy_corrupt_frame[THEN corres_guard_imp,unfolded dc_def]) apply simp+ done next case (Cons x xs) show ?case apply (subst corrupt_frame_duplicate[symmetric]) apply (rule corres_guard_imp) apply (clarsimp simp:mapM_Cons) apply (rule corres_split) apply (rule corres_symb_exec_r) apply (simp add: store_word_offs_def bind_assoc[symmetric]
                              state_assert_def[symmetric]) apply (rule corres_state_assert) apply (rule_tac s_id = s_id and sz = sz in store_word_corres) using Cons.prems apply simp using Cons.prems apply (clarsimp simp: within_page_def in_user_frame_def) apply (thin_tac "Ball S P" for S P) apply (rule_tac x=sz in exI) apply (frule (2) ipc_frame_ptr_at_frame_at) apply (simp add: obj_at_def a_type_simps) apply wp+ apply clarsimp+ apply (rule corres_dummy_return_l) apply (rule corres_split) apply (rule Cons.hyps) using Cons apply clarsimp apply (rule corres_free_return[where P = \<top> and P'=\<top> ]) apply wp+ apply (wp store_word_offs_ipc_frame_wp)+ by (fastforce simp:ipc_frame_wp_at_def)+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs) proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>set []. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) [])
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat (x * word_size)) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) (a # xs)) proof (state)
this:
\<forall>x\<in>set []. within_page buf (base + word_of_nat (x * word_size)) sz

goal (2 subgoals):
 1. \<forall>x\<in>set []. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) [])
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat (x * word_size)) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) (a # xs)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) []) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) [])
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. dcorres (\<lambda>a b. True) ?Q ?Q' (corrupt_frame buf) (return [])
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (4 subgoals):
 1. \<And>s. ?Q s \<Longrightarrow> True
 2. \<And>s. ?Q' s \<Longrightarrow> valid_etcbs s
 3. \<And>s. True \<Longrightarrow> ?Q s
 4. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) [])

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat (x * word_size)) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) (a # xs)) proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat (x * word_size)) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) (a # xs)) proof (state)
this:
\<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs)
\<forall>x\<in>set (x # xs). within_page buf (base + word_of_nat (x * word_size)) sz

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat (x * word_size)) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) (a # xs)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) (x # xs)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (do _ <- corrupt_frame buf;
corrupt_frame buf
od) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) (x # xs)) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (do _ <- corrupt_frame buf;
corrupt_frame buf
od) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) (x # xs))
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (do _ <- corrupt_frame buf;
corrupt_frame buf
od) (do y <- load_word_offs src_a x >>= store_word_offs base x;
ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. dcorres ?r'6 ?P6 ?P'6 (corrupt_frame buf) (load_word_offs src_a x >>= store_word_offs base x)
 2. \<And>uu_ y. ?r'6 uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 3. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>rv. dcorres ?r'6 ?P6 (?Q'11 rv) (corrupt_frame buf) (store_word_offs base x rv)
 2. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>?Q'11\<rbrace>
 3. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 5. \<And>uu_ y. ?r'6 uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 6. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 9. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>rv. dcorres ?r'6 ?P6 (?Q'11 rv) (corrupt_frame buf) (do y <- state_assert (in_user_frame (base + word_of_nat x * word_of_nat word_size));
do_machine_op (storeWord (base + word_of_nat x * word_of_nat word_size) rv)
od)
 2. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>?Q'11\<rbrace>
 3. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 5. \<And>uu_ y. ?r'6 uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 6. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 9. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>rv. dcorres ?r'6 ?P6 (?Q'11 rv) (corrupt_frame buf) (do_machine_op (storeWord (base + word_of_nat x * word_of_nat word_size) rv))
 2. \<And>rv s. ?Q'11 rv s \<Longrightarrow> in_user_frame (base + word_of_nat x * word_of_nat word_size) s
 3. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>?Q'11\<rbrace>
 4. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 6. \<And>uu_ y. ?r'6 uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 7. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 9. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 10. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>rv. within_page buf (base + word_of_nat x * word_of_nat word_size) sz
 2. \<And>rv s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> in_user_frame (base + word_of_nat x * word_of_nat word_size) s
 3. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>rv. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs\<rbrace>
 4. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 6. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 7. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
using this:
\<forall>x\<in>set (x # xs). within_page buf (base + word_of_nat (x * word_size)) sz

goal (10 subgoals):
 1. \<And>rv. within_page buf (base + word_of_nat x * word_of_nat word_size) sz
 2. \<And>rv s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> in_user_frame (base + word_of_nat x * word_of_nat word_size) s
 3. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>rv. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs\<rbrace>
 4. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 6. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 7. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>rv s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> in_user_frame (base + word_of_nat x * word_of_nat word_size) s
 2. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>rv. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs\<rbrace>
 3. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 5. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 6. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
using this:
\<forall>x\<in>set (x # xs). within_page buf (base + word_of_nat (x * word_size)) sz

goal (9 subgoals):
 1. \<And>rv s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> in_user_frame (base + word_of_nat x * word_of_nat word_size) s
 2. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>rv. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs\<rbrace>
 3. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 5. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 6. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned s; \<forall>xa\<in>set xs. base + word_of_nat xa * word_of_nat word_size && ~~ mask (pageBitsForSize sz) = base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz); buf = base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz); pspace_distinct s; valid_objs s; ipc_frame_ptr_at (base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s_id s; ipc_frame_sz_at sz s_id s; valid_etcbs s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s
 2. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>rv. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs\<rbrace>
 3. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 5. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 6. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned s; buf = base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz); pspace_distinct s; valid_objs s; ipc_frame_ptr_at (base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s_id s; ipc_frame_sz_at sz s_id s; valid_etcbs s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s
 2. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>rv. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs\<rbrace>
 3. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 5. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 6. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned s; buf = base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz); pspace_distinct s; valid_objs s; ipc_frame_ptr_at (base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s_id s; ipc_frame_sz_at sz s_id s; valid_etcbs s\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s
 2. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>rv. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs\<rbrace>
 3. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 5. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 6. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned s; buf = base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz); pspace_distinct s; valid_objs s; ipc_frame_ptr_at (base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s_id s; ipc_frame_sz_at sz s_id s; valid_etcbs s; ako_at (DataPage False sz) (base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s
 2. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>rv. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs\<rbrace>
 3. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 5. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 6. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<lbrace>?P'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>rv. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs\<rbrace>
 2. \<And>s. ?P'6 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail ?P'6 (load_word_offs src_a x)
 4. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 5. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. False \<Longrightarrow> no_fail (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (load_word_offs src_a x)
 2. \<And>uu_ y. dc uu_ y \<Longrightarrow> dcorres dc (?R6 uu_) (?R'6 y) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 3. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. dcorres dc (?R6 ()) (?R'6 ()) (corrupt_frame buf) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 2. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. dcorres dc (?R6 ()) (?R'6 ()) (corrupt_frame buf >>= return) (do ys <- mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs;
return (() # ys)
od)
 2. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. dcorres ?r'54 (?P62 ()) (?P'60 ()) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs)
 2. \<And>x rv'. ?r'54 x rv' \<Longrightarrow> dcorres dc (?R54 x) (?R'54 rv') (return x) (return (() # rv'))
 3. \<lbrace>?Q61 ()\<rbrace> corrupt_frame buf \<lbrace>?R54\<rbrace>
 4. \<lbrace>?Q'59 ()\<rbrace> mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs \<lbrace>?R'54\<rbrace>
 5. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. ?P62 a and ?Q61 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>\<lambda>a. ?P'60 a and ?Q'59 a\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz
 2. \<And>x rv'. dc x rv' \<Longrightarrow> dcorres dc (?R54 x) (?R'54 rv') (return x) (return (() # rv'))
 3. \<lbrace>?Q61 ()\<rbrace> corrupt_frame buf \<lbrace>?R54\<rbrace>
 4. \<lbrace>?Q'59 ()\<rbrace> mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs \<lbrace>?R'54\<rbrace>
 5. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q61 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>\<lambda>a. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'59 a\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'6) s proof (prove)
using this:
\<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs)
\<forall>x\<in>set (x # xs). within_page buf (base + word_of_nat (x * word_size)) sz

goal (8 subgoals):
 1. \<forall>x\<in>set xs. within_page buf (base + word_of_nat (x * word_size)) sz
 2. \<And>x rv'. dc x rv' \<Longrightarrow> dcorres dc (?R54 x) (?R'54 rv') (return x) (return (() # rv'))
 3. \<lbrace>?Q61 ()\<rbrace> corrupt_frame buf \<lbrace>?R54\<rbrace>
 4. \<lbrace>?Q'59 ()\<rbrace> mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs \<lbrace>?R'54\<rbrace>
 5. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q61 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>\<lambda>a. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'59 a\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>x rv'. dc x rv' \<Longrightarrow> dcorres dc (?R54 x) (?R'54 rv') (return x) (return (() # rv'))
 2. \<lbrace>?Q61 ()\<rbrace> corrupt_frame buf \<lbrace>?R54\<rbrace>
 3. \<lbrace>?Q'59 ()\<rbrace> mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs \<lbrace>?R'54\<rbrace>
 4. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q61 a\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>\<lambda>a. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'59 a\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q61 ()\<rbrace> corrupt_frame buf \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrace>?Q'59 ()\<rbrace> mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) xs \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<lbrace>?Q6\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q61 a\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x >>= store_word_offs base x \<lbrace>\<lambda>a. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'59 a\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrace>?P'95 xa\<rbrace> store_word_offs base x xa \<lbrace>\<lambda>rv s. ipc_frame_ptr_at buf s_id s \<and> ipc_frame_sz_at sz s_id s \<and> valid_etcbs s \<and> True\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> load_word_offs src_a x \<lbrace>\<lambda>x s. pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> ?P'95 x s\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 4. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs and (\<lambda>s. pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> ipc_frame_ptr_at buf s_id s \<and> ipc_frame_sz_at sz s_id s \<and> valid_etcbs s \<and> True)) s proof (state)
this:
dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs src_a x >>= store_word_offs base x) (x # xs))

goal:
No subgoals!