theory Ipc_C

lemma setMR_ccorres:
  notes if_cong[cong]
  shows
  "ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_'
     (valid_pspace' and  case_option \<top> valid_ipc_buffer_ptr' buf
           and (\<lambda>s. offset < msgMaxLength))
     (UNIV \<inter> {s. offset_' s = of_nat offset} \<inter> {s. reg_' s = v}
             \<inter> {s. receiver_' s = tcb_ptr_to_ctcb_ptr thread}
             \<inter> {s. receiveIPCBuffer_' s = option_to_ptr buf}) []
     (setMR thread buf offset v) (Call setMR_'proc)" apply (rule ccorres_gen_asm) apply (cinit lift: offset_' reg_' receiver_' receiveIPCBuffer_') apply (rule ccorres_cond2'[where R=\<top>]) apply (simp add: msgRegisters_unfold n_msgRegisters_def Collect_const_mem
                      linorder_not_less word_le_nat_alt unat_of_nat32
                      word_bits_def msgMaxLength_unfold) apply arith apply wpc apply (simp add: option_to_ptr_def option_to_0_def Collect_False
                      ccorres_cond_iffs
                 del: Collect_const) apply (rule ccorres_return_C, simp+)[1] apply (simp add: option_to_ptr_def option_to_0_def Collect_True
                     ccorres_cond_iffs
                del: Collect_const ptr_add_def') apply (rule ccorres_cond_true) apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_move_array_assertion_ipc_buffer
               | (rule ccorres_flip_Guard, rule ccorres_move_array_assertion_ipc_buffer))+ apply (rule storeWordUser_ccorres) apply ceqv apply (rule ccorres_return_C, simp+)[1] apply wp apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) apply (simp add: msgLengthBits_def msgMaxLength_def
                     unat_arith_simps less_mask_eq unat_of_nat
                del: Collect_const) apply ctac apply (rule ccorres_return_C, simp+)[1] apply wp apply (simp del: Collect_const) apply (vcg exspec=setRegister_modifies) apply (simp add: Collect_const_mem option_to_0_def
                   unat_gt_0 option_to_ptr_def) apply (intro impI conjI allI, simp_all) apply (clarsimp simp: valid_ipc_buffer_ptr'_def) apply (erule aligned_add_aligned) apply (simp only: word_size_def is_aligned_mult_triv2[where n=2, simplified]) apply (simp add: msg_align_bits) apply (simp add: n_msgRegisters_def length_msgRegisters msgLengthBits_def mask_def) apply (simp add: msg_align_bits word_size_def msgMaxLength_def
                         length_msgRegisters n_msgRegisters_def) apply (simp add: unat_word_ariths msg_align_bits msgMaxLength_def
                        word_less_nat_alt unat_of_nat) apply (simp add: unat_word_ariths msg_align_bits msgMaxLength_def
                       word_less_nat_alt unat_of_nat) apply (clarsimp simp: valid_ipc_buffer_ptr'_def) apply (simp add: unat_of_nat32 word_bits_def msgMaxLength_unfold
                     word_le_nat_alt msgRegisters_ccorres n_msgRegisters_def) apply (simp add: unat_of_nat32 msgMaxLength_unfold word_bits_def
                    unat_add_lem[THEN iffD1] less_mask_eq msgLengthBits_def
                    word_less_nat_alt) apply (simp add: linorder_not_le n_msgRegisters_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. offset < msgMaxLength)) (UNIV \<inter> \<lbrace>\<acute>offset = word_of_nat offset\<rbrace> \<inter> \<lbrace>\<acute>reg = v\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr buf\<rbrace>) [] (setMR thread buf offset v) (Call setMR_'proc) proof (prove)
goal (1 subgoal):
 1. offset < msgMaxLength \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (UNIV \<inter> \<lbrace>\<acute>offset = word_of_nat offset\<rbrace> \<inter> \<lbrace>\<acute>reg = v\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr buf\<rbrace>) [] (setMR thread buf offset v) (Call setMR_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Q587 receiveIPCBuffer receiver reg offseta) (?Q'587 receiveIPCBuffer receiver reg offseta) [SKIP] (if offset < length TCB_H.msgRegisters then do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od else case buf of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (offset + 1) * word_size) v;
return (offset + 1)
od) (IF SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta THEN
  IF receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (unat (offseta + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer +\<^sub>p uint (offseta + 1))} (Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (Suc (unat (offseta + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (receiveIPCBuffer +\<^sub>p uint (offseta + 1)) reg)))));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI
ELSE
  Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
FI)
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q587 receiveIPCBuffer receiver reg offseta s \<and> s' \<in> ?Q'587 receiveIPCBuffer receiver reg offseta proof (prove)
goal (4 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> (\<not> offset < length TCB_H.msgRegisters) = (s' \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace>)
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pt593 receiveIPCBuffer receiver reg offseta) (?Rt593 receiveIPCBuffer receiver reg offseta) [SKIP] (case buf of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (offset + 1) * word_size) v;
return (offset + 1)
od) (IF receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (unat (offseta + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer +\<^sub>p uint (offseta + 1))} (Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (Suc (unat (offseta + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (receiveIPCBuffer +\<^sub>p uint (offseta + 1)) reg)))));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI)
 3. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 4. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> ?Pt593 receiveIPCBuffer receiver reg offseta s) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rt593 receiveIPCBuffer receiver reg offseta) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (4 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < 120; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> (Suc (Suc (Suc (Suc 0))) \<le> offset) = (4 \<le> offset)
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pt593 receiveIPCBuffer receiver reg offseta) (?Rt593 receiveIPCBuffer receiver reg offseta) [SKIP] (case buf of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (offset + 1) * word_size) v;
return (offset + 1)
od) (IF receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (unat (offseta + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer +\<^sub>p uint (offseta + 1))} (Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (Suc (unat (offseta + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (receiveIPCBuffer +\<^sub>p uint (offseta + 1)) reg)))));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI)
 3. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 4. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> ?Pt593 receiveIPCBuffer receiver reg offseta s) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rt593 receiveIPCBuffer receiver reg offseta) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (3 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pt593 receiveIPCBuffer receiver reg offseta) (?Rt593 receiveIPCBuffer receiver reg offseta) [SKIP] (case buf of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (offset + 1) * word_size) v;
return (offset + 1)
od) (IF receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (unat (offseta + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer +\<^sub>p uint (offseta + 1))} (Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (Suc (unat (offseta + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (receiveIPCBuffer +\<^sub>p uint (offseta + 1)) reg)))));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI)
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> ?Pt593 receiveIPCBuffer receiver reg offseta s) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rt593 receiveIPCBuffer receiver reg offseta) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (4 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = None\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?R637 receiveIPCBuffer receiver reg offseta) (?R''639 receiveIPCBuffer receiver reg offseta) [SKIP] (return (length TCB_H.msgRegisters)) (IF receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (unat (offseta + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer +\<^sub>p uint (offseta + 1))} (Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (Suc (unat (offseta + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (receiveIPCBuffer +\<^sub>p uint (offseta + 1)) reg)))));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI)
 2. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?R638 receiveIPCBuffer receiver reg offseta x2) (?R''640 receiveIPCBuffer receiver reg offseta x2) [SKIP] (do storeWordUser (x2 + word_of_nat (offset + 1) * word_size) v;
return (offset + 1)
od) (IF receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (unat (offseta + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer +\<^sub>p uint (offseta + 1))} (Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (Suc (unat (offseta + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (receiveIPCBuffer +\<^sub>p uint (offseta + 1)) reg)))));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI)
 3. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 4. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> ?R637 receiveIPCBuffer receiver reg offseta s) \<and> (\<forall>x. buf = Some x \<longrightarrow> ?R638 receiveIPCBuffer receiver reg offseta x s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> ?R''639 receiveIPCBuffer receiver reg offseta} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> ?R''640 receiveIPCBuffer receiver reg offseta x}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (4 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = NULL; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = None\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?R637 NULL (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset)) (?R''639 NULL (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset)) [SKIP] (return (length TCB_H.msgRegisters)) (return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters))
 2. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?R638 receiveIPCBuffer receiver reg offseta x2) (?R''640 receiveIPCBuffer receiver reg offseta x2) [SKIP] (do storeWordUser (x2 + word_of_nat (offset + 1) * word_size) v;
return (offset + 1)
od) (IF receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (unat (offseta + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer +\<^sub>p uint (offseta + 1))} (Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (Suc (unat (offseta + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (receiveIPCBuffer +\<^sub>p uint (offseta + 1)) reg)))));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI)
 3. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 4. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> ?R637 receiveIPCBuffer receiver reg offseta s) \<and> (\<forall>x. buf = Some x \<longrightarrow> ?R638 receiveIPCBuffer receiver reg offseta x s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> ?R''639 receiveIPCBuffer receiver reg offseta} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> ?R''640 receiveIPCBuffer receiver reg offseta x}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (3 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?R638 receiveIPCBuffer receiver reg offseta x2) (?R''640 receiveIPCBuffer receiver reg offseta x2) [SKIP] (do storeWordUser (x2 + word_of_nat (offset + 1) * word_size) v;
return (offset + 1)
od) (IF receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (unat (offseta + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer +\<^sub>p uint (offseta + 1))} (Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion receiveIPCBuffer (Suc (unat (offseta + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (receiveIPCBuffer +\<^sub>p uint (offseta + 1)) reg)))));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI)
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> ?R638 receiveIPCBuffer receiver reg offseta x s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> ?R''640 receiveIPCBuffer receiver reg offseta x}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (3 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?R638 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2) (?R''640 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2) [SKIP] (do y <- storeWordUser (x2 + (1 + word_of_nat offset) * word_size) v;
return (Suc offset)
od) (IF x2 \<noteq> 0 THEN
  Guard MemorySafety \<lbrace>word_of_nat offset + 1 = 0 \<or> array_assertion (PTR(32 word) x2) (unat (word_of_nat offset + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) x2 +\<^sub>p uint (word_of_nat offset + 1))} (Guard MemorySafety \<lbrace>word_of_nat offset + 1 = 0 \<or> array_assertion (PTR(32 word) x2) (Suc (unat (word_of_nat offset + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) x2 +\<^sub>p uint (word_of_nat offset + 1)) v)))));;
return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI)
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> ?R638 receiveIPCBuffer receiver reg offseta x s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> ?R''640 receiveIPCBuffer receiver reg offseta x}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (3 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?R638 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2) (?R'658 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2) [SKIP] (do y <- storeWordUser (x2 + (1 + word_of_nat offset) * word_size) v;
return (Suc offset)
od) (Guard MemorySafety \<lbrace>word_of_nat offset + 1 = 0 \<or> array_assertion (PTR(32 word) x2) (unat (word_of_nat offset + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) x2 +\<^sub>p uint (word_of_nat offset + 1))} (Guard MemorySafety \<lbrace>word_of_nat offset + 1 = 0 \<or> array_assertion (PTR(32 word) x2) (Suc (unat (word_of_nat offset + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) x2 +\<^sub>p uint (word_of_nat offset + 1)) v)))));;
return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1))
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> ?R638 receiveIPCBuffer receiver reg offseta x s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> ?R'658 receiveIPCBuffer receiver reg offseta x \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (7 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ccorres (?r'662 receiveIPCBuffer receiver reg offseta x2) (?xf'662 receiveIPCBuffer receiver reg offseta x2) (?P668 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2) (?R'658 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2) [] (storeWordUser (x2 + (1 + word_of_nat offset) * word_size) v) (Guard MemorySafety \<lbrace>word_of_nat offset + 1 = 0 \<or> array_assertion (PTR(32 word) x2) (unat (word_of_nat offset + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) x2 +\<^sub>p uint (word_of_nat offset + 1))} (Guard MemorySafety \<lbrace>word_of_nat offset + 1 = 0 \<or> array_assertion (PTR(32 word) x2) (Suc (unat (word_of_nat offset + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) x2 +\<^sub>p uint (word_of_nat offset + 1)) v))))))
 2. \<And>receiveIPCBuffer receiver reg offseta x2 rv' t t'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'662 receiveIPCBuffer receiver reg offseta x2) rv' t t' (return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1)) (?d'662 receiveIPCBuffer receiver reg offseta x2 rv')
 3. \<And>receiveIPCBuffer receiver reg offseta x2 rv rv'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2; ?r'662 receiveIPCBuffer receiver reg offseta x2 rv rv'\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Q662 receiveIPCBuffer receiver reg offseta x2 rv) (?Q'662 receiveIPCBuffer receiver reg offseta x2 rv rv') [SKIP] (return (Suc offset)) (?d'662 receiveIPCBuffer receiver reg offseta x2 rv')
 4. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R666 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2\<rbrace> storeWordUser (x2 + (1 + word_of_nat offset) * word_size) v \<lbrace>?Q662 receiveIPCBuffer receiver reg offseta x2\<rbrace>
 5. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'662 receiveIPCBuffer receiver reg offseta x2) (?xf'662 receiveIPCBuffer receiver reg offseta x2) (?Q'662 receiveIPCBuffer receiver reg offseta x2)
 6. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 7. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (?P668 receiveIPCBuffer receiver reg offseta x and ?R666 receiveIPCBuffer receiver reg offseta x) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> ?R'658 receiveIPCBuffer receiver reg offseta x \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (7 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ccorres (?r'662 receiveIPCBuffer receiver reg offseta x2) (?xf'662 receiveIPCBuffer receiver reg offseta x2) (?A690 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2) (?C'687 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2) [] (storeWordUser (x2 + (1 + word_of_nat offset) * word_size) v) (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) x2 +\<^sub>p uint (word_of_nat offset + 1))} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) x2 +\<^sub>p uint (word_of_nat offset + 1)) v))))
 2. \<And>receiveIPCBuffer receiver reg offseta x2 rv' t t'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'662 receiveIPCBuffer receiver reg offseta x2) rv' t t' (return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1)) (?d'662 receiveIPCBuffer receiver reg offseta x2 rv')
 3. \<And>receiveIPCBuffer receiver reg offseta x2 rv rv'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2; ?r'662 receiveIPCBuffer receiver reg offseta x2 rv rv'\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Q662 receiveIPCBuffer receiver reg offseta x2 rv) (?Q'662 receiveIPCBuffer receiver reg offseta x2 rv rv') [SKIP] (return (Suc offset)) (?d'662 receiveIPCBuffer receiver reg offseta x2 rv')
 4. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R666 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2\<rbrace> storeWordUser (x2 + (1 + word_of_nat offset) * word_size) v \<lbrace>?Q662 receiveIPCBuffer receiver reg offseta x2\<rbrace>
 5. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'662 receiveIPCBuffer receiver reg offseta x2) (?xf'662 receiveIPCBuffer receiver reg offseta x2) (?Q'662 receiveIPCBuffer receiver reg offseta x2)
 6. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 7. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (?A690 receiveIPCBuffer receiver reg offseta x and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and ?R666 receiveIPCBuffer receiver reg offseta x) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> ?C'687 receiveIPCBuffer receiver reg offseta x \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (6 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta x2 rv' t t'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1)) (?d'662 receiveIPCBuffer receiver reg offseta x2 rv')
 2. \<And>receiveIPCBuffer receiver reg offseta x2 rv rv'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Q662 receiveIPCBuffer receiver reg offseta x2 rv) (?Q'662 receiveIPCBuffer receiver reg offseta x2 rv rv') [SKIP] (return (Suc offset)) (?d'662 receiveIPCBuffer receiver reg offseta x2 rv')
 3. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R666 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2\<rbrace> storeWordUser (x2 + (1 + word_of_nat offset) * word_size) v \<lbrace>?Q662 receiveIPCBuffer receiver reg offseta x2\<rbrace>
 4. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'662 receiveIPCBuffer receiver reg offseta x2)
 5. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 6. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and ?R666 receiveIPCBuffer receiver reg offseta x) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (5 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta x2 rv rv'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Q662 receiveIPCBuffer receiver reg offseta x2 rv) (?Q'662 receiveIPCBuffer receiver reg offseta x2 rv rv') [SKIP] (return (Suc offset)) (return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1))
 2. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R666 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2\<rbrace> storeWordUser (x2 + (1 + word_of_nat offset) * word_size) v \<lbrace>?Q662 receiveIPCBuffer receiver reg offseta x2\<rbrace>
 3. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'662 receiveIPCBuffer receiver reg offseta x2)
 4. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 5. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and ?R666 receiveIPCBuffer receiver reg offseta x) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (4 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R666 (PTR(32 word) x2) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset) x2\<rbrace> storeWordUser (x2 + (1 + word_of_nat offset) * word_size) v \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. \<lbrace>Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)\<rbrace>)
 3. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 4. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and ?R666 receiveIPCBuffer receiver reg offseta x) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (3 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta x2. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x2; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; buf = Some x2\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. \<lbrace>Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)\<rbrace>)
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and (\<lambda>a. True)) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>offset < msgMaxLength; buf = Some x2\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and (\<lambda>a. True)) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Pf593 receiveIPCBuffer receiver reg offseta) (?Rf593 receiveIPCBuffer receiver reg offseta) [SKIP] (do y <- asUser thread (setRegister (TCB_H.msgRegisters ! offset) v);
return (Suc offset)
od) (Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and (\<lambda>a. True)) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ?Pf593 receiveIPCBuffer receiver reg offseta s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> ?Rf593 receiveIPCBuffer receiver reg offseta)} proof (prove)
goal (4 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta rv xfdc. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_' (?Q722 receiveIPCBuffer receiver reg offseta rv) (?Q'722 receiveIPCBuffer receiver reg offseta rv xfdc) [SKIP] (return (Suc offset)) (return_C ret__unsigned_'_update (\<lambda>s. offseta + 1))
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> \<lbrace>?R722 receiveIPCBuffer receiver reg offseta\<rbrace> asUser thread (setRegister (TCB_H.msgRegisters ! offset) v) \<lbrace>?Q722 receiveIPCBuffer receiver reg offseta\<rbrace>
 3. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'722 receiveIPCBuffer receiver reg offseta) CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'722 receiveIPCBuffer receiver reg offseta rv (xfdc s)}
 4. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and (\<lambda>a. True)) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ((\<lambda>_. True) and ?R722 receiveIPCBuffer receiver reg offseta) s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. reg) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = v\<rbrace>} \<inter> ?R'722 receiveIPCBuffer receiver reg offseta \<inter> \<lbrace>offseta < 4\<rbrace>)} proof (prove)
goal (3 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> \<lbrace>?R722 receiveIPCBuffer receiver reg offseta\<rbrace> asUser thread (setRegister (TCB_H.msgRegisters ! offset) v) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'722 receiveIPCBuffer receiver reg offseta) CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>Suc offset = unat (offseta + 1 && mask msgLengthBits)\<rbrace>}
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and (\<lambda>a. True)) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ((\<lambda>_. True) and ?R722 receiveIPCBuffer receiver reg offseta) s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. reg) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = v\<rbrace>} \<inter> ?R'722 receiveIPCBuffer receiver reg offseta \<inter> \<lbrace>offseta < 4\<rbrace>)} proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'722 receiveIPCBuffer receiver reg offseta) CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],reg) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>Suc offset = unat (offseta + 1 && mask msgLengthBits)\<rbrace>}
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and (\<lambda>a. True)) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. reg) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = v\<rbrace>} \<inter> ?R'722 receiveIPCBuffer receiver reg offseta \<inter> \<lbrace>offseta < 4\<rbrace>)} proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'722 (option_to_ptr buf) (tcb_ptr_to_ctcb_ptr thread) v (word_of_nat offset)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],v) \<lbrace>Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)\<rbrace>
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and (\<lambda>a. True)) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. reg) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = v\<rbrace>} \<inter> ?R'722 receiveIPCBuffer receiver reg offseta \<inter> \<lbrace>offseta < 4\<rbrace>)} proof (prove)
goal (1 subgoal):
 1. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = option_to_ptr buf; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; (valid_pspace' and (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> offset < length TCB_H.msgRegisters \<longrightarrow> (buf = None \<longrightarrow> True) \<and> (\<forall>x. buf = Some x \<longrightarrow> (valid_pspace' and (\<lambda>_. is_aligned (x + (1 + offseta) * word_size) 2) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and valid_ipc_buffer_ptr' (ptr_val receiveIPCBuffer) and (\<lambda>a. True)) s)) and (\<lambda>s. offset < length TCB_H.msgRegisters \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. buf = None \<longrightarrow> s \<in> \<lbrace>length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. buf = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>receiveIPCBuffer +\<^sub>p uint (offseta + 1) = PTR(32 word) (x + (1 + offseta) * word_size)\<rbrace> \<inter> \<lbrace>reg = reg\<rbrace> \<inter> \<lbrace>Suc (unat (offseta + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> Suc (unat (offseta + 1)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>unat (offseta + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> (offseta + 1 \<noteq> 0 \<longrightarrow> unat (offseta + 1) \<noteq> 0)\<rbrace> \<inter> \<lbrace>x \<noteq> 0\<rbrace>}}) \<and> (s \<notin> \<lbrace>SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta\<rbrace> \<longrightarrow> s \<in> {s. w_'_update (\<lambda>_. reg) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = v\<rbrace>} \<inter> \<lbrace>Suc offset = unat (offseta + 1 && mask msgLengthBits)\<rbrace> \<inter> \<lbrace>offseta < 4\<rbrace>)} proof (prove)
goal (1 subgoal):
 1. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s\<rbrakk> \<Longrightarrow> (\<not> offset < length TCB_H.msgRegisters \<longrightarrow> (\<forall>x. buf = Some x \<longrightarrow> is_aligned (x + (1 + word_of_nat offset) * word_size) 2 \<and> valid_ipc_buffer_ptr' x s)) \<and> (SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset \<longrightarrow> (buf = None \<longrightarrow> length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)) \<and> (\<forall>x. buf = Some x \<longrightarrow> word_of_nat offset * 4 + 4 = (1 + word_of_nat offset) * word_size \<and> Suc (unat (word_of_nat offset + 1)) \<le> 2 ^ (msg_align_bits - 2) \<and> unat (word_of_nat offset + 1) \<le> 2 ^ (msg_align_bits - 2) \<and> x \<noteq> 0)) \<and> (\<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset \<longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset) \<and> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits) \<and> word_of_nat offset < 4) proof (prove)
goal (9 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; \<not> offset < length TCB_H.msgRegisters; buf = Some x\<rbrakk> \<Longrightarrow> is_aligned (x + (1 + word_of_nat offset) * word_size) 2
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = NULL; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = None\<rbrakk> \<Longrightarrow> length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)
 3. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> word_of_nat offset * 4 + 4 = (1 + word_of_nat offset) * word_size
 4. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> Suc (unat (word_of_nat offset + 1)) \<le> 2 ^ (msg_align_bits - 2)
 5. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> unat (word_of_nat offset + 1) \<le> 2 ^ (msg_align_bits - 2)
 6. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> x \<noteq> 0
 7. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 8. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 9. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (9 subgoals):
 1. \<And>s s' x. \<lbrakk>offset < msgMaxLength; (s, s') \<in> rf_sr; \<not> offset < length TCB_H.msgRegisters; buf = Some x; valid_pspace' s; is_aligned x msg_align_bits; typ_at' UserDataT (x && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned (x + (1 + word_of_nat offset) * word_size) 2
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = NULL; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = None\<rbrakk> \<Longrightarrow> length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)
 3. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> word_of_nat offset * 4 + 4 = (1 + word_of_nat offset) * word_size
 4. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> Suc (unat (word_of_nat offset + 1)) \<le> 2 ^ (msg_align_bits - 2)
 5. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> unat (word_of_nat offset + 1) \<le> 2 ^ (msg_align_bits - 2)
 6. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> x \<noteq> 0
 7. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 8. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 9. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (10 subgoals):
 1. \<And>s s' x. \<lbrakk>offset < msgMaxLength; (s, s') \<in> rf_sr; \<not> offset < length TCB_H.msgRegisters; buf = Some x; valid_pspace' s; typ_at' UserDataT (x && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned ((1 + word_of_nat offset) * word_size) 2
 2. \<And>s s' x. \<lbrakk>offset < msgMaxLength; (s, s') \<in> rf_sr; \<not> offset < length TCB_H.msgRegisters; buf = Some x; valid_pspace' s; typ_at' UserDataT (x && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = NULL; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = None\<rbrakk> \<Longrightarrow> length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)
 4. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> word_of_nat offset * 4 + 4 = (1 + word_of_nat offset) * word_size
 5. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> Suc (unat (word_of_nat offset + 1)) \<le> 2 ^ (msg_align_bits - 2)
 6. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> unat (word_of_nat offset + 1) \<le> 2 ^ (msg_align_bits - 2)
 7. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> x \<noteq> 0
 8. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 9. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 10. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (9 subgoals):
 1. \<And>s s' x. \<lbrakk>offset < msgMaxLength; (s, s') \<in> rf_sr; \<not> offset < length TCB_H.msgRegisters; buf = Some x; valid_pspace' s; typ_at' UserDataT (x && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = NULL; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = None\<rbrakk> \<Longrightarrow> length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)
 3. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> word_of_nat offset * 4 + 4 = (1 + word_of_nat offset) * word_size
 4. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> Suc (unat (word_of_nat offset + 1)) \<le> 2 ^ (msg_align_bits - 2)
 5. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> unat (word_of_nat offset + 1) \<le> 2 ^ (msg_align_bits - 2)
 6. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> x \<noteq> 0
 7. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 8. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 9. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (8 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = NULL; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = None\<rbrakk> \<Longrightarrow> length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters && mask msgLengthBits)
 2. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> word_of_nat offset * 4 + 4 = (1 + word_of_nat offset) * word_size
 3. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> Suc (unat (word_of_nat offset + 1)) \<le> 2 ^ (msg_align_bits - 2)
 4. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> unat (word_of_nat offset + 1) \<le> 2 ^ (msg_align_bits - 2)
 5. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> x \<noteq> 0
 6. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 7. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 8. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (7 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> word_of_nat offset * 4 + 4 = (1 + word_of_nat offset) * word_size
 2. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> Suc (unat (word_of_nat offset + 1)) \<le> 2 ^ (msg_align_bits - 2)
 3. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> unat (word_of_nat offset + 1) \<le> 2 ^ (msg_align_bits - 2)
 4. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> x \<noteq> 0
 5. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 6. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 7. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (6 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> Suc (unat (word_of_nat offset + 1)) \<le> 2 ^ (msg_align_bits - 2)
 2. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> unat (word_of_nat offset + 1) \<le> 2 ^ (msg_align_bits - 2)
 3. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> x \<noteq> 0
 4. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 5. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 6. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (5 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> unat (word_of_nat offset + 1) \<le> 2 ^ (msg_align_bits - 2)
 2. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> x \<noteq> 0
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 4. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 5. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (4 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta s s' x. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) x; receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' x s; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset; buf = Some x\<rbrakk> \<Longrightarrow> x \<noteq> 0
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 4. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (3 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset)
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 3. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> Suc offset = unat (word_of_nat offset + 1 && mask msgLengthBits)
 2. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal (1 subgoal):
 1. \<And>receiveIPCBuffer receiver reg offseta s s'. \<lbrakk>offset < msgMaxLength; receiveIPCBuffer = PTR(32 word) (case buf of None \<Rightarrow> 0 | Some y \<Rightarrow> y); receiver = tcb_ptr_to_ctcb_ptr thread; reg = v; offseta = word_of_nat offset; (s, s') \<in> rf_sr; valid_pspace' s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<not> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 proof (prove)
goal:
No subgoals!