theory Intent_DR

lemma zip_store_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_sz_at sz s_id) and (ipc_frame_ptr_at buf s_id) and valid_etcbs)
   (corrupt_frame buf)
   (zipWithM_x (store_word_offs base) xs ys)" apply (clarsimp simp:zipWithM_x_mapM_x split del: if_split) apply (induct xs arbitrary: ys) apply (clarsimp simp: mapM_x_Cons) apply (clarsimp simp: mapM_x_Nil) apply (rule corres_guard_imp[OF dcorres_dummy_corrupt_frame]) apply (simp+)[2] apply (case_tac ys) apply (clarsimp simp: mapM_x_Cons mapM_x_Nil) apply (rule corres_guard_imp[OF dcorres_dummy_corrupt_frame]) apply clarsimp+ apply (subst mapM_x_Cons) apply clarify apply (subst corrupt_frame_duplicate[symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[where P="\<top>" and r'="dc"]) apply (clarsimp simp:store_word_offs_def) 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) apply simp apply (clarsimp simp: within_page_def in_user_frame_def) 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 clarsimp apply (drule allI) apply (drule_tac x = list in spec) apply simp apply (wp store_word_offs_ipc_frame_wp)+ apply clarsimp+ done

(* 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_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (zipWithM_x (store_word_offs base) xs ys) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)) proof (prove)
goal (2 subgoals):
 1. \<And>ys. \<forall>x\<in>set []. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip [] ys))
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip (a # xs) ys)) proof (prove)
goal (2 subgoals):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) [])
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip (a # xs) ys)) proof (prove)
goal (2 subgoals):
 1. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (return ())
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip (a # xs) ys)) proof (prove)
goal (3 subgoals):
 1. \<And>s. True \<Longrightarrow> True
 2. \<And>s. (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s \<Longrightarrow> valid_etcbs s
 3. \<And>a xs ys. \<lbrakk>\<And>ys. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip (a # xs) ys)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip (a # xs) ys)) proof (prove)
goal (2 subgoals):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat x * word_of_nat word_size) sz; ys = []\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip (a # xs) ys))
 2. \<And>a xs ys aa list. \<lbrakk>\<And>ys. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat x * word_of_nat word_size) sz; ys = aa # list\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip (a # xs) ys)) proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (return ())
 2. \<And>a xs ys aa list. \<lbrakk>\<And>ys. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat x * word_of_nat word_size) sz; ys = aa # list\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip (a # xs) ys)) proof (prove)
goal (3 subgoals):
 1. \<And>a xs s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> True
 2. \<And>a xs s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> valid_etcbs s
 3. \<And>a xs ys aa list. \<lbrakk>\<And>ys. \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set (a # xs). within_page buf (base + word_of_nat x * word_of_nat word_size) sz; ys = aa # list\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip (a # xs) ys)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) ((a, aa) # zip xs list)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (do case (a, aa) of (x, xa) \<Rightarrow> store_word_offs base x xa;
mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (do store_word_offs base a aa;
mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (do _ <- corrupt_frame buf;
corrupt_frame buf
od) (do store_word_offs base a aa;
mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)
od) proof (prove)
goal (3 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (?Q29 a xs aa list) (?Q'29 a xs aa list) (do _ <- corrupt_frame buf;
corrupt_frame buf
od) (do store_word_offs base a aa;
mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)
od)
 2. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ?Q29 a xs aa list s
 3. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'29 a xs aa list s proof (prove)
goal (6 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (?P'33 a xs aa list) (corrupt_frame buf) (store_word_offs base a aa)
 2. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'33 a xs aa list and ?Q'33 a xs aa list) s proof (prove)
goal (6 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (?P'33 a xs aa list) (corrupt_frame buf) (do s <- get;
y <- assert (in_user_frame (base + word_of_nat a * word_of_nat word_size) s);
do_machine_op (storeWord (base + word_of_nat a * word_of_nat word_size) aa)
od)
 2. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'33 a xs aa list and ?Q'33 a xs aa list) s proof (prove)
goal (6 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (?P'33 a xs aa list) (corrupt_frame buf) (do y <- state_assert (in_user_frame (base + word_of_nat a * word_of_nat word_size));
do_machine_op (storeWord (base + word_of_nat a * word_of_nat word_size) aa)
od)
 2. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'33 a xs aa list and ?Q'33 a xs aa list) s proof (prove)
goal (7 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (?P'33 a xs aa list) (corrupt_frame buf) (do_machine_op (storeWord (base + word_of_nat a * word_of_nat word_size) aa))
 2. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; ?P'33 a xs aa list s\<rbrakk> \<Longrightarrow> in_user_frame (base + word_of_nat a * word_of_nat word_size) s
 3. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 5. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 7. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'33 a xs aa list and ?Q'33 a xs aa list) s proof (prove)
goal (7 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page buf (base + word_of_nat a * word_of_nat word_size) sz
 2. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (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\<rbrakk> \<Longrightarrow> in_user_frame (base + word_of_nat a * word_of_nat word_size) s
 3. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 5. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 7. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (6 subgoals):
 1. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (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\<rbrakk> \<Longrightarrow> in_user_frame (base + word_of_nat a * word_of_nat word_size) s
 2. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (6 subgoals):
 1. \<And>a xs s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at (base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s_id and valid_etcbs) (corrupt_frame (base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz))) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set xs. base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz) = base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz); buf = base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz); pspace_aligned s; pspace_distinct s; valid_objs s; ipc_frame_ptr_at (base + word_of_nat a * 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 a * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s
 2. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (6 subgoals):
 1. \<And>a xs s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at (base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s_id and valid_etcbs) (corrupt_frame (base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz))) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set xs. base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz) = base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz); buf = base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz); pspace_aligned s; pspace_distinct s; valid_objs s; ipc_frame_ptr_at (base + word_of_nat a * 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 a * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s
 2. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (6 subgoals):
 1. \<And>a xs s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at (base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s_id and valid_etcbs) (corrupt_frame (base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz))) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); \<forall>x\<in>set xs. base + word_of_nat x * word_of_nat word_size && ~~ mask (pageBitsForSize sz) = base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz); buf = base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz); pspace_aligned s; pspace_distinct s; valid_objs s; ipc_frame_ptr_at (base + word_of_nat a * 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 a * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) (base + word_of_nat a * word_of_nat word_size && ~~ mask (pageBitsForSize sz)) s
 2. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (5 subgoals):
 1. \<And>a xs aa list uu_ rv'. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dc uu_ rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list uu_) (?R'33 a xs aa list rv') (corrupt_frame buf) (K_bind (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list)) rv')
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 4. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (5 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list ()) (?R'33 a xs aa list ()) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list))
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 4. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (5 subgoals):
 1. \<And>a xs aa list. \<lbrakk>within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; \<forall>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys))\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list ()) (?R'33 a xs aa list ()) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list))
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 4. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (5 subgoals):
 1. \<And>a xs aa list. \<lbrakk>within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list))\<rbrakk> \<Longrightarrow> dcorres dc (?R33 a xs aa list ()) (?R'33 a xs aa list ()) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs list))
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>?R33 a xs aa list\<rbrace>
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>?R'33 a xs aa list\<rbrace>
 4. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (4 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a xs aa list\<rbrace> corrupt_frame buf \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 a xs aa list\<rbrace> store_word_offs base a aa \<lbrace>\<lambda>a. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs\<rbrace>
 3. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q33 a xs aa list) s
 4. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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'33 a xs aa list) s proof (prove)
goal (2 subgoals):
 1. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 2. \<And>a xs aa list s. \<lbrakk>\<And>ys. dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (mapM_x (\<lambda>(x, y). store_word_offs base x y) (zip xs ys)); within_page buf (base + word_of_nat a * word_of_nat word_size) sz; \<forall>x\<in>set xs. within_page buf (base + word_of_nat x * word_of_nat word_size) sz; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) s\<rbrakk> \<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_sz_at sz s_id s \<and> ipc_frame_ptr_at buf s_id s \<and> valid_etcbs s)) s proof (prove)
goal:
No subgoals!