theory Intent_DR

lemma copy_mrs_corres:
  "valid_message_info mi \<Longrightarrow>
   dcorres dc \<top> ((valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y
     and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs))
    (do corrupt_tcb_intent y;corrupt_frame buf od)
    (copy_mrs thread rv y (Some (buf + (bptr && mask (pageBitsForSize sz))))
               (mi_length mi))" supply option.case_cong[cong] apply (simp add:copy_mrs_def del:upt.simps) apply (rule dcorres_expand_pfx) apply (rule corres_guard_imp) apply (rule corres_split[where r'="dc"]) apply (rule set_registers_corres) apply (wpc) apply (rule corres_dummy_return_l) apply (rule corres_split[where r'="dc"]) apply (rule dcorres_dummy_corrupt_frame) apply (rule corres_free_return[where P="\<top>" and P'="\<top>"]) apply wp apply (clarify,simp del:upt.simps ) apply (rule corres_dummy_return_l) apply (rule corres_split[where r'="dc"]) apply (rule_tac s_id = y and sz = sz in zip_cpy_word_corres) apply (clarsimp simp del:upt.simps) apply (rule within_page_ipc_buf) apply simp+ apply (clarsimp simp:msg_align_bits valid_message_info_def msg_max_length_def) apply (erule less_trans) apply (rule le_less_trans[where y =  "Suc (unat (0x78))"]) apply (rule iffD2[OF Suc_le_mono]) apply (erule iffD1[OF word_le_nat_alt]) apply simp apply (rule corres_free_return[where P="\<top>" and P'="\<top>"]) apply wp+ apply ((clarsimp|wp)+)[1] apply (rule mapM_wp_inv) apply (case_tac rv) apply clarsimp apply wp apply (clarsimp|rule conjI)+ apply ((wp|clarsimp)+)[3] apply (case_tac rv) apply (fastforce simp: ipc_buffer_wp_at_def obj_at_def tcb_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_message_info mi \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) (do corrupt_tcb_intent y;
corrupt_frame buf
od) (copy_mrs thread rv y (Some (buf + (bptr && mask (pageBitsForSize sz)))) (mi_length mi)) proof (prove)
goal (1 subgoal):
 1. valid_message_info mi \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) (do corrupt_tcb_intent y;
corrupt_frame buf
od) (copy_mrs thread rv y (Some (buf + (bptr && mask (pageBitsForSize sz)))) (mi_length mi)) proof (prove)
goal (1 subgoal):
 1. valid_message_info mi \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) (do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (do y <- mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers);
buf_mrs <- case rv of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (do y <- mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers);
buf_mrs <- case rv of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q11 s s') (?Q'11 s s') (do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (do y <- mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers);
buf_mrs <- case rv of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 2. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ?Q11 s s' sa
 3. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> ?Q'11 s s' sa proof (prove)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P15 s s') (?P'15 s s') (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers))
 2. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R15 s s' ya) (?R'15 s s' rv') (corrupt_frame buf) (do buf_mrs <- case rv of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 3. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>?R15 s s'\<rbrace>
 4. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>?R'15 s s'\<rbrace>
 5. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (?P15 s s' and ?Q15 s s') sa
 6. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (?P'15 s s' and ?Q'15 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R15 s s' ya) (?R'15 s s' rv') (corrupt_frame buf) (do buf_mrs <- case rv of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 2. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>?R15 s s'\<rbrace>
 3. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>?R'15 s s'\<rbrace>
 4. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 5. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc (?R29 s s' ya) (?R'31 s s' rv') (corrupt_frame buf) (do buf_mrs <- return [];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 2. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?R30 s s' ya x2) (?R'32 s s' rv' x2) (corrupt_frame buf) (do buf_mrs <- mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 3. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ?R29 s s' y sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R30 s s' y x sa)\<rbrace>
 4. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> ?R'31 s s' rv' sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R'32 s s' rv' x sa)\<rbrace>
 5. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 6. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc (?R29 s s' ya) (?R'31 s s' rv') (corrupt_frame buf >>= return) (do buf_mrs <- return [];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 2. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?R30 s s' ya x2) (?R'32 s s' rv' x2) (corrupt_frame buf) (do buf_mrs <- mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 3. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ?R29 s s' y sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R30 s s' y x sa)\<rbrace>
 4. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> ?R'31 s s' rv' sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R'32 s s' rv' x sa)\<rbrace>
 5. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 6. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc (?P37 s s' ya) (?P'39 s s' rv') (corrupt_frame buf) (return [])
 2. \<And>s s' ya rv' x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R36 s s' ya rv' x) (?R'36 s s' ya rv' buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 3. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q38 s s' ya\<rbrace> corrupt_frame buf \<lbrace>?R36 s s' ya rv'\<rbrace>
 4. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'40 s s' rv'\<rbrace> return [] \<lbrace>?R'36 s s' ya rv'\<rbrace>
 5. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?R30 s s' ya x2) (?R'32 s s' rv' x2) (corrupt_frame buf) (do buf_mrs <- mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> (?P37 s s' y and ?Q38 s s' y) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R30 s s' y x sa)\<rbrace>
 7. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (?P'39 s s' rv' and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R'32 s s' rv' x sa)\<rbrace>
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 9. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s s' ya rv' x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R36 s s' ya rv' x) (?R'36 s s' ya rv' buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 2. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q38 s s' ya\<rbrace> corrupt_frame buf \<lbrace>?R36 s s' ya rv'\<rbrace>
 3. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'40 s s' rv'\<rbrace> return [] \<lbrace>?R'36 s s' ya rv'\<rbrace>
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?R30 s s' ya x2) (?R'32 s s' rv' x2) (corrupt_frame buf) (do buf_mrs <- mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and ?Q38 s s' y) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R30 s s' y x sa)\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R'32 s s' rv' x sa)\<rbrace>
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q38 s s' ya\<rbrace> corrupt_frame buf \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'40 s s' rv'\<rbrace> return [] \<lbrace>\<lambda>buf_mrs _. True\<rbrace>
 3. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?R30 s s' ya x2) (?R'32 s s' rv' x2) (corrupt_frame buf) (do buf_mrs <- mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 4. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and ?Q38 s s' y) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R30 s s' y x sa)\<rbrace>
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R'32 s s' rv' x sa)\<rbrace>
 6. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' ya rv'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'40 s s' rv'\<rbrace> return [] \<lbrace>\<lambda>buf_mrs _. True\<rbrace>
 2. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?R30 s s' ya x2) (?R'32 s s' rv' x2) (corrupt_frame buf) (do buf_mrs <- mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 3. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R30 s s' y x sa)\<rbrace>
 4. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R'32 s s' rv' x sa)\<rbrace>
 5. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 6. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?R30 s s' ya x2) (?R'32 s s' rv' x2) (corrupt_frame buf) (do buf_mrs <- mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 2. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R30 s s' y x sa)\<rbrace>
 3. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R'32 s s' rv' x sa)\<rbrace>
 4. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 5. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?R30 s s' ya x2) (?R'32 s s' rv' x2) (corrupt_frame buf >>= return) (do buf_mrs <- mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))];
return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs)))
od)
 2. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R30 s s' y x sa)\<rbrace>
 3. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R'32 s s' rv' x sa)\<rbrace>
 4. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 5. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?P64 s s' ya x2) (?P'66 s s' rv' x2) (corrupt_frame buf) (mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))])
 2. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 3. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (?P64 s s' y x and ?Q65 s s' y x) sa)\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (?P'66 s s' rv' x and ?Q'67 s s' rv' x) sa)\<rbrace>
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [Suc (length msg_registers)..<Suc (unat (mi_length mi))]. within_page buf (buf + (bptr && mask (pageBitsForSize sz)) + word_of_nat (x * word_size)) sz
 2. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 3. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s' x2 x. \<lbrakk>valid_message_info mi; rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi))\<rbrakk> \<Longrightarrow> within_page buf (buf + (bptr && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) sz
 2. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 3. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (14 subgoals):
 1. \<And>s' x2 x. \<lbrakk>valid_message_info mi; rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi))\<rbrakk> \<Longrightarrow> valid_objs (?s87 s' x2 x)
 2. \<And>s' x2 x. \<lbrakk>valid_message_info mi; rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi))\<rbrakk> \<Longrightarrow> pspace_aligned (?s87 s' x2 x)
 3. \<And>s' x2 x. \<lbrakk>valid_message_info mi; rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi))\<rbrakk> \<Longrightarrow> pspace_distinct (?s87 s' x2 x)
 4. \<And>s' x2 x. \<lbrakk>valid_message_info mi; rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi))\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at buf (?y87 s' x2 x) (?s87 s' x2 x)
 5. \<And>s' x2 x. \<lbrakk>valid_message_info mi; rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi))\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz (?y87 s' x2 x) (?s87 s' x2 x)
 6. \<And>s' x2 x. \<lbrakk>valid_message_info mi; rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi))\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at bptr (?y87 s' x2 x) (?s87 s' x2 x)
 7. \<And>s' x2 x. \<lbrakk>valid_message_info mi; rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi))\<rbrakk> \<Longrightarrow> x < 2 ^ (msg_align_bits - 2)
 8. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 9. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 10. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
A total of 14 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>s' x2 x. \<lbrakk>valid_message_info mi; rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi))\<rbrakk> \<Longrightarrow> x < 2 ^ (msg_align_bits - 2)
 2. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 3. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s' x2 x. \<lbrakk>rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; x < Suc (unat (mi_length mi)); mi_length mi \<le> 0x78; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> x < 128
 2. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 3. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s' x2 x. \<lbrakk>rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; mi_length mi \<le> 0x78; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> Suc (unat (mi_length mi)) < 128
 2. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 3. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s' x2 x. \<lbrakk>rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; mi_length mi \<le> 0x78; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> Suc (unat (mi_length mi)) \<le> Suc (unat 0x78)
 2. \<And>s' x2 x. \<lbrakk>rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; mi_length mi \<le> 0x78; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> Suc (unat 0x78) < 128
 3. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 5. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 7. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 9. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s' x2 x. \<lbrakk>rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; mi_length mi \<le> 0x78; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> unat (mi_length mi) \<le> unat 0x78
 2. \<And>s' x2 x. \<lbrakk>rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; mi_length mi \<le> 0x78; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> Suc (unat 0x78) < 128
 3. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 5. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 7. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 9. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s' x2 x. \<lbrakk>rv = Some x2; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'; Suc (length msg_registers) \<le> x; mi_length mi \<le> 0x78; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> Suc (unat 0x78) < 128
 2. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 3. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 4. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 6. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 8. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' ya rv' x2 x buf_mrs. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2; dc x buf_mrs\<rbrakk> \<Longrightarrow> dcorres dc (?R63 s s' ya rv' x2 x) (?R'63 s s' ya rv' x2 buf_mrs) (return x) (return (min (mi_length mi) (word_of_nat (min (length msg_registers) (unat (mi_length mi))) + word_of_nat (length buf_mrs))))
 2. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>?R63 s s' ya rv' x2\<rbrace>
 3. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>?R'63 s s' ya rv' x2\<rbrace>
 4. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 5. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 6. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 7. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 s s' ya x2\<rbrace> corrupt_frame buf \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>s s' ya rv' x2. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; dc ya rv'; rv = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'67 s s' rv' x2\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs (buf + (bptr && mask (pageBitsForSize sz))) x) [Suc (length msg_registers)..<Suc (unat (mi_length mi))] \<lbrace>\<lambda>buf_mrs _. True\<rbrace>
 3. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y sa. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and ?Q65 s s' y x) sa)\<rbrace>
 4. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and ?Q'67 s s' rv' x) sa)\<rbrace>
 5. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 6. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 s s'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y s. (rv = None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s)\<rbrace>
 2. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace>
 3. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 4. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 s s'\<rbrace> mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (take (unat (mi_length mi)) msg_registers) \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'40 s s' rv') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace>
 2. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 3. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and ?Q'15 s s') sa proof (prove)
goal (3 subgoals):
 1. \<And>s s' x. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace> do v <- as_user thread (getRegister x);
as_user y (setRegister x v)
od \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace>
 2. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 3. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and (\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa))) sa proof (prove)
goal (4 subgoals):
 1. \<And>s s' x. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace> do v <- as_user thread (getRegister x);
as_user y (setRegister x v)
od \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace>
 2. \<And>s s' x a. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; rv = Some a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace> do v <- as_user thread (getRegister x);
as_user y (setRegister x v)
od \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace>
 3. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 4. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and (\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa))) sa proof (prove)
goal (4 subgoals):
 1. \<And>s' x. \<lbrakk>valid_message_info mi; rv = None; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_etcbs s \<and> ?Q'119 (transform s') s' s\<rbrace> do v <- as_user thread (getRegister x);
as_user y (setRegister x v)
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> ?Q'119 (transform s') s' s\<rbrace>
 2. \<And>s s' x a. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; rv = Some a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace> do v <- as_user thread (getRegister x);
as_user y (setRegister x v)
od \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace>
 3. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 4. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and (\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ?Q'119 s s') sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s s' x a. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; rv = Some a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ipc_buffer_wp_at (?buf145 s s') (?y143 s s')) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace> do v <- as_user thread (getRegister x);
as_user y (setRegister x v)
od \<lbrace>\<lambda>rv' sa. (rv = None \<longrightarrow> (valid_etcbs and ipc_buffer_wp_at (?buf145 s s') (?y143 s s')) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa)\<rbrace>
 2. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 3. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and (\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ipc_buffer_wp_at (?buf145 s s') (?y143 s s')) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s' x a. \<lbrakk>valid_message_info mi; rv = Some a; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread y s'; ipc_frame_ptr_at buf y s'; ipc_frame_sz_at sz y s'; ipc_buffer_wp_at bptr y s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> ipc_frame_ptr_at buf y s \<and> ipc_frame_sz_at sz y s \<and> valid_etcbs s\<rbrace> do v <- as_user thread (getRegister x);
as_user y (setRegister x v)
od \<lbrace>\<lambda>rv' s. pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> ipc_frame_ptr_at buf y s \<and> ipc_frame_sz_at sz y s \<and> valid_etcbs s\<rbrace>
 2. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q15 s s') sa
 3. \<And>s s' sa. \<lbrakk>valid_message_info mi; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread y and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and ipc_buffer_wp_at bptr y and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs and (\<lambda>sa. (rv = None \<longrightarrow> (valid_etcbs and ipc_buffer_wp_at (?buf145 s s') (?y143 s s')) sa) \<and> (\<forall>x. rv = Some x \<longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf y and ipc_frame_sz_at sz y and valid_etcbs and (\<lambda>a. True)) sa))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>valid_message_info mi; valid_idle sa; valid_objs sa; pspace_aligned sa; pspace_distinct sa; not_idle_thread y sa; ipc_frame_ptr_at buf y sa; ipc_frame_sz_at sz y sa; ipc_buffer_wp_at bptr y sa; valid_etcbs sa\<rbrakk> \<Longrightarrow> tcb_at y sa \<and> (rv = None \<longrightarrow> ipc_buffer_wp_at (?buf145 (transform sa) sa) (?y143 (transform sa) sa) sa) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>valid_message_info mi; valid_idle sa; valid_objs sa; pspace_aligned sa; pspace_distinct sa; not_idle_thread y sa; ipc_frame_ptr_at buf y sa; ipc_frame_sz_at sz y sa; ipc_buffer_wp_at bptr y sa; valid_etcbs sa; rv = None\<rbrakk> \<Longrightarrow> tcb_at y sa \<and> (rv = None \<longrightarrow> ipc_buffer_wp_at (?buf145 (transform sa) sa) (?y143 (transform sa) sa) sa)
 2. \<And>sa a. \<lbrakk>valid_message_info mi; valid_idle sa; valid_objs sa; pspace_aligned sa; pspace_distinct sa; not_idle_thread y sa; ipc_frame_ptr_at buf y sa; ipc_frame_sz_at sz y sa; ipc_buffer_wp_at bptr y sa; valid_etcbs sa; rv = Some a\<rbrakk> \<Longrightarrow> tcb_at y sa \<and> (rv = None \<longrightarrow> ipc_buffer_wp_at (?buf145 (transform sa) sa) (?y143 (transform sa) sa) sa) proof (prove)
goal:
No subgoals!