theory Intent_DR

lemma set_mrs_corres:
  "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)
   (set_mrs y (Some (buf + (bptr && mask (pageBitsForSize sz)))) b)" apply (simp add:set_mrs_def arch_tcb_update_aux3 arch_tcb_set_registers_def del:upt.simps) apply (rule dcorres_absorb_gets_the) apply (rule corres_guard_imp) apply (rule corres_split [where r'=dc]) apply (clarsimp, drule(1) valid_etcbs_get_tcb_get_etcb) apply (rule_tac s'=s' in set_cxt_none_det_intent_corres; clarsimp) apply (clarsimp dest!: get_tcb_SomeD) apply (clarsimp dest!: get_etcb_SomeD) apply (rule corres_dummy_return_l) apply (rule corres_split[where r'=dc and R'="%x. \<top>" and R="%x. \<top>"]) apply (rule_tac s_id = y and sz = sz in zip_store_word_corres) apply (clarsimp simp del:upt.simps) apply (rule within_page_ipc_buf) apply ((simp add:msg_align_bits msg_max_length_def)+)[7] apply (rule corres_free_return) apply wp+ apply (wp set_object_valid_etcbs) apply (simp del:upt.simps) apply (auto dest!:get_tcb_SomeD simp:obj_at_def ipc_frame_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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) (set_mrs y (Some (buf + (bptr && mask (pageBitsForSize sz)))) b) proof (prove)
goal (1 subgoal):
 1. 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 tcb <- gets_the (get_tcb y);
y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg)) tcb));
y <- zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b);
return (word_of_nat (min (length b) msg_max_length))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (do y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj'));
y <- zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b);
return (word_of_nat (min (length b) msg_max_length))
od) proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc (?Q3 s' obj') (?Q'3 s' obj') (do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (do y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj'));
y <- zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b);
return (word_of_nat (min (length b) msg_max_length))
od)
 2. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ?Q3 s' obj' s
 3. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ?Q'3 s' obj' s proof (prove)
goal (6 subgoals):
 1. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc (?P7 s' obj') (?P'7 s' obj') (corrupt_tcb_intent y) (KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')))
 2. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R7 s' obj' ya) (?R'7 s' obj' rv') (corrupt_frame buf) (do y <- zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b);
return (word_of_nat (min (length b) msg_max_length))
od)
 3. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>?R7 s' obj'\<rbrace>
 4. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>?R'7 s' obj'\<rbrace>
 5. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> (?P7 s' obj' and ?Q7 s' obj') s
 6. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> (?P'7 s' obj' and ?Q'7 s' obj') s proof (prove)
goal (6 subgoals):
 1. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; 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'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc (?P7 s' obj') (?P'7 s' obj') (corrupt_tcb_intent y) (KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')))
 2. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R7 s' obj' ya) (?R'7 s' obj' rv') (corrupt_frame buf) (do y <- zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b);
return (word_of_nat (min (length b) msg_max_length))
od)
 3. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>?R7 s' obj'\<rbrace>
 4. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>?R'7 s' obj'\<rbrace>
 5. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> (?P7 s' obj' and ?Q7 s' obj') s
 6. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> (?P'7 s' obj' and ?Q'7 s' obj') s proof (prove)
goal (7 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb y s' = Some obj'; 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'; get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' y = Some (TCB obj')
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb y s' = Some obj'; 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'; get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>ya. ekheap s' y = Some ya
 3. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R7 s' obj' ya) (?R'7 s' obj' rv') (corrupt_frame buf) (do y <- zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b);
return (word_of_nat (min (length b) msg_max_length))
od)
 4. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>?R7 s' obj'\<rbrace>
 5. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>?R'7 s' obj'\<rbrace>
 6. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and ?Q7 s' obj') s
 7. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'7 s' obj') s proof (prove)
goal (6 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb y s' = Some obj'; 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'; get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>ya. ekheap s' y = Some ya
 2. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R7 s' obj' ya) (?R'7 s' obj' rv') (corrupt_frame buf) (do y <- zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b);
return (word_of_nat (min (length b) msg_max_length))
od)
 3. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>?R7 s' obj'\<rbrace>
 4. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>?R'7 s' obj'\<rbrace>
 5. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and ?Q7 s' obj') s
 6. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'7 s' obj') s proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R7 s' obj' ya) (?R'7 s' obj' rv') (corrupt_frame buf) (do y <- zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b);
return (word_of_nat (min (length b) msg_max_length))
od)
 2. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>?R7 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>?R'7 s' obj'\<rbrace>
 4. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and ?Q7 s' obj') s
 5. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'7 s' obj') s proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R7 s' obj' ya) (?R'7 s' obj' rv') (corrupt_frame buf >>= return) (do y <- zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b);
return (word_of_nat (min (length b) msg_max_length))
od)
 2. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>?R7 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>?R'7 s' obj'\<rbrace>
 4. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and ?Q7 s' obj') s
 5. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'7 s' obj') s proof (prove)
goal (8 subgoals):
 1. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?P47 s' obj' ya) (?P'49 s' obj' rv') (corrupt_frame buf) (zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b))
 2. \<And>s' obj' ya rv' x yaa. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'; dc x yaa\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (word_of_nat (min (length b) msg_max_length)))
 3. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 s' obj' ya\<rbrace> corrupt_frame buf \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 s' obj' rv'\<rbrace> zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y. ?P47 s' obj' y and ?Q48 s' obj' y\<rbrace>
 6. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>\<lambda>rv'. ?P'49 s' obj' rv' and ?Q'50 s' obj' rv'\<rbrace>
 7. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and ?Q7 s' obj') s
 8. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'7 s' obj') s proof (prove)
goal (8 subgoals):
 1. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [Suc (length msg_registers)..<Suc msg_max_length]. within_page buf (buf + (bptr && mask (pageBitsForSize sz)) + word_of_nat (x * word_size)) sz
 2. \<And>s' obj' ya rv' x yaa. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'; dc x yaa\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (word_of_nat (min (length b) msg_max_length)))
 3. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 s' obj' ya\<rbrace> corrupt_frame buf \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 s' obj' rv'\<rbrace> zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q48 s' obj' y\<rbrace>
 6. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>\<lambda>rv'. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz y and ipc_frame_ptr_at buf y and valid_etcbs and ?Q'50 s' obj' rv'\<rbrace>
 7. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and ?Q7 s' obj') s
 8. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'7 s' obj') s proof (prove)
goal (8 subgoals):
 1. \<And>s' obj' x. \<lbrakk>get_tcb y s' = Some obj'; 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 msg_max_length\<rbrakk> \<Longrightarrow> within_page buf (buf + (bptr && mask (pageBitsForSize sz)) + word_of_nat x * word_of_nat word_size) sz
 2. \<And>s' obj' ya rv' x yaa. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'; dc x yaa\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (word_of_nat (min (length b) msg_max_length)))
 3. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 s' obj' ya\<rbrace> corrupt_frame buf \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 s' obj' rv'\<rbrace> zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b) \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q48 s' obj' y\<rbrace>
 6. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>\<lambda>rv'. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz y and ipc_frame_ptr_at buf y and valid_etcbs and ?Q'50 s' obj' rv'\<rbrace>
 7. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and ?Q7 s' obj') s
 8. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'7 s' obj') s proof (prove)
goal (14 subgoals):
 1. \<And>s' obj' x. \<lbrakk>get_tcb y s' = Some obj'; 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 msg_max_length\<rbrakk> \<Longrightarrow> valid_objs (?s69 s' obj' x)
 2. \<And>s' obj' x. \<lbrakk>get_tcb y s' = Some obj'; 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 msg_max_length\<rbrakk> \<Longrightarrow> pspace_aligned (?s69 s' obj' x)
 3. \<And>s' obj' x. \<lbrakk>get_tcb y s' = Some obj'; 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 msg_max_length\<rbrakk> \<Longrightarrow> pspace_distinct (?s69 s' obj' x)
 4. \<And>s' obj' x. \<lbrakk>get_tcb y s' = Some obj'; 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 msg_max_length\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at buf (?y69 s' obj' x) (?s69 s' obj' x)
 5. \<And>s' obj' x. \<lbrakk>get_tcb y s' = Some obj'; 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 msg_max_length\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz (?y69 s' obj' x) (?s69 s' obj' x)
 6. \<And>s' obj' x. \<lbrakk>get_tcb y s' = Some obj'; 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 msg_max_length\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at bptr (?y69 s' obj' x) (?s69 s' obj' x)
 7. \<And>s' obj' x. \<lbrakk>get_tcb y s' = Some obj'; 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 msg_max_length\<rbrakk> \<Longrightarrow> x < 2 ^ (msg_align_bits - 2)
 8. \<And>s' obj' ya rv' x yaa. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'; dc x yaa\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (word_of_nat (min (length b) msg_max_length)))
 9. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 s' obj' ya\<rbrace> corrupt_frame buf \<lbrace>\<lambda>x _. True\<rbrace>
 10. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 s' obj' rv'\<rbrace> zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b) \<lbrace>\<lambda>x _. True\<rbrace>
A total of 14 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>s' obj' ya rv' x yaa. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'; dc x yaa\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (word_of_nat (min (length b) msg_max_length)))
 2. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 s' obj' ya\<rbrace> corrupt_frame buf \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 s' obj' rv'\<rbrace> zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q48 s' obj' y\<rbrace>
 5. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>\<lambda>rv'. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz y and ipc_frame_ptr_at buf y and valid_etcbs and ?Q'50 s' obj' rv'\<rbrace>
 6. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and ?Q7 s' obj') s
 7. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'7 s' obj') s proof (prove)
goal (6 subgoals):
 1. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 s' obj' ya\<rbrace> corrupt_frame buf \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>s' obj' ya rv'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'50 s' obj' rv'\<rbrace> zipWithM_x (store_word_offs (buf + (bptr && mask (pageBitsForSize sz)))) [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) b) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 s' obj'\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q48 s' obj' y\<rbrace>
 4. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>\<lambda>rv'. pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz y and ipc_frame_ptr_at buf y and valid_etcbs and ?Q'50 s' obj' rv'\<rbrace>
 5. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and ?Q7 s' obj') s
 6. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'7 s' obj') s proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>(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'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'107 s' obj'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length b) msg_registers) then b ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>\<lambda>rv s. valid_etcbs s \<and> True\<rbrace>
 2. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. True \<and> True)) s
 3. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and (\<lambda>s. (ko_at (TCB obj') y and pspace_aligned) s \<and> (ko_at (TCB obj') y and pspace_distinct) s \<and> (ko_at (TCB obj') y and valid_objs) s \<and> (ko_at (TCB obj') y and ipc_frame_sz_at sz y) s \<and> (ko_at (TCB obj') y and ipc_frame_ptr_at buf y) s \<and> ?P'107 s' obj' s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. True \<and> True)) s
 2. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and (\<lambda>s. (ko_at (TCB obj') y and pspace_aligned) s \<and> (ko_at (TCB obj') y and pspace_distinct) s \<and> (ko_at (TCB obj') y and valid_objs) s \<and> (ko_at (TCB obj') y and ipc_frame_sz_at sz y) s \<and> (ko_at (TCB obj') y and ipc_frame_ptr_at buf y) s \<and> (valid_etcbs and (\<lambda>s. kheap s y = Some (TCB (?tcba112 s' obj')))) s \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s' obj' s. \<lbrakk>(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'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and (\<lambda>s. (ko_at (TCB obj') y and pspace_aligned) s \<and> (ko_at (TCB obj') y and pspace_distinct) s \<and> (ko_at (TCB obj') y and valid_objs) s \<and> (ko_at (TCB obj') y and ipc_frame_sz_at sz y) s \<and> (ko_at (TCB obj') y and ipc_frame_ptr_at buf y) s \<and> (valid_etcbs and (\<lambda>s. kheap s y = Some (TCB (?tcba112 s' obj')))) s \<and> True)) s proof (prove)
goal:
No subgoals!