theory SyscallArgs_C

lemma getMRs_user_word:
  "\<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info
      \<and> msgLength info \<le> msgMaxLength \<and> i >= scast n_msgRegisters\<rbrace>
  getMRs thread (Some buffer) info
  \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace>" supply if_cong[cong] apply (rule hoare_assume_pre) apply (elim conjE) apply (thin_tac "valid_ipc_buffer_ptr' x y" for x y) apply (simp add: getMRs_def) apply wp apply (rule_tac P="length hardwareMRValues = unat n_msgRegisters" in hoare_gen_asm) apply (clarsimp simp: nth_append word_le_nat_alt
                         word_less_nat_alt word_size
                         linorder_not_less [symmetric]) apply (wp mapM_loadWordUser_user_words_at) apply (wp hoare_vcg_all_lift) apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post) apply wp apply clarsimp defer apply simp apply (wp asUser_const_rv) apply (simp add: msgRegisters_unfold n_msgRegisters_def) apply (erule_tac x="unat i - unat n_msgRegisters" in allE) apply (erule impE) apply (simp add: msgRegisters_unfold
                    msgMaxLength_def msgLengthBits_def n_msgRegisters_def) apply (drule (1) order_less_le_trans) apply (simp add: word_less_nat_alt word_le_nat_alt) apply (simp add: msgRegisters_unfold
                   msgMaxLength_def msgLengthBits_def n_msgRegisters_def) apply (simp add: upto_enum_word del: upt_rec_numeral) apply (subst (asm) nth_map) apply (simp del: upt_rec_numeral) apply (drule (1) order_less_le_trans) apply (simp add: word_less_nat_alt word_le_nat_alt) apply (subst (asm) nth_upt) apply simp apply (drule (1) order_less_le_trans) apply (simp add: word_less_nat_alt word_le_nat_alt) apply (simp add: word_le_nat_alt add.commute add.left_commute mult.commute mult.left_commute
                   wordSize_def' take_bit_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info \<and> msgLength info \<le> msgMaxLength \<and> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrace> getMRs thread (Some buffer) info \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info \<and> msgLength info \<le> msgMaxLength \<and> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrace> getMRs thread (Some buffer) info \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info \<and> msgLength info \<le> msgMaxLength \<and> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i \<Longrightarrow> \<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info \<and> msgLength info \<le> msgMaxLength \<and> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrace> getMRs thread (Some buffer) info \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_ipc_buffer_ptr' buffer s; i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info \<and> msgLength info \<le> msgMaxLength \<and> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrace> getMRs thread (Some buffer) info \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info \<and> msgLength info \<le> msgMaxLength \<and> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrace> getMRs thread (Some buffer) info \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' buffer\<rbrace> do hardwareMRValues <- asUser thread (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat (msgLength info)) hardwareMRValues @ take (unat (msgLength info) - length hardwareMRValues) bufferMRValues)
od \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>hardwareMRValues. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?B10 hardwareMRValues\<rbrace> mapM loadWordUser (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>\<lambda>bufferMRValues. user_word_at ((take (unat (msgLength info)) hardwareMRValues @ take (unat (msgLength info) - length hardwareMRValues) bufferMRValues) ! unat i) (buffer + (i * 4 + 4))\<rbrace>
 2. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?Q9\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>?B10\<rbrace>
 3. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. \<And>hardwareMRValues. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; length hardwareMRValues = unat n_msgRegisters\<rbrakk> \<Longrightarrow> \<lbrace>?P'13 hardwareMRValues\<rbrace> mapM loadWordUser (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>\<lambda>bufferMRValues. user_word_at ((take (unat (msgLength info)) hardwareMRValues @ take (unat (msgLength info) - length hardwareMRValues) bufferMRValues) ! unat i) (buffer + (i * 4 + 4))\<rbrace>
 2. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?Q9\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>hardwareMRValues. ?P'13 hardwareMRValues and K (length hardwareMRValues = unat n_msgRegisters)\<rbrace>
 3. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. \<And>hardwareMRValues. \<lbrakk>unat i < unat (msgLength info); \<not> unat msgMaxLength < unat (msgLength info); \<not> unat i < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); length hardwareMRValues = unat n_msgRegisters\<rbrakk> \<Longrightarrow> \<lbrace>?P'13 hardwareMRValues\<rbrace> mapM loadWordUser (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>\<lambda>bufferMRValues. user_word_at (if unat i < unat n_msgRegisters then hardwareMRValues ! unat i else bufferMRValues ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4))\<rbrace>
 2. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?Q9\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>hardwareMRValues. ?P'13 hardwareMRValues and K (length hardwareMRValues = unat n_msgRegisters)\<rbrace>
 3. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?Q9\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>hardwareMRValues. (\<lambda>s. \<forall>rv. (\<forall>x<length (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]). user_word_at (rv ! x) (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! x) s) \<and> length rv = length (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<longrightarrow> user_word_at (if unat i < unat n_msgRegisters then hardwareMRValues ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s) and K (length hardwareMRValues = unat n_msgRegisters)\<rbrace>
 2. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. \<And>rv. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?P127 rv\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rva s. (\<forall>x<length (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]). user_word_at (rv ! x) (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! x) s) \<and> length rv = length (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s\<rbrace>
 2. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?P'126\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv. K (length rv = unat n_msgRegisters)\<rbrace>
 3. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> (\<forall>x. ?P127 x s) \<and> ?P'126 s proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?P127 rv\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; True\<rbrakk> \<Longrightarrow> (\<forall>x<length (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]). user_word_at (rv ! x) (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! x) s) \<and> length rv = length (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s
 3. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?P'126\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv. K (length rv = unat n_msgRegisters)\<rbrace>
 4. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> (\<forall>x. ?P127 x s) \<and> ?P'126 s proof (prove)
goal (3 subgoals):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; True\<rbrakk> \<Longrightarrow> (\<forall>x<length (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]). user_word_at (rv ! x) (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! x) s) \<and> length rv = length (map (\<lambda>x. buffer + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s
 2. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?P'126\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv. K (length rv = unat n_msgRegisters)\<rbrace>
 3. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> (\<forall>x. True) \<and> ?P'126 s proof (prove)
goal (3 subgoals):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; \<forall>x<Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)). user_word_at (rv ! x) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! x * word_of_nat wordSize) s; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s
 2. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?P'126\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv. K (length rv = unat n_msgRegisters)\<rbrace>
 3. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> (\<forall>x. True) \<and> ?P'126 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?P'126\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv. K (length rv = unat n_msgRegisters)\<rbrace>
 2. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> (\<forall>x. True) \<and> ?P'126 s
 3. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; \<forall>x<Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)). user_word_at (rv ! x) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! x * word_of_nat wordSize) s; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i\<rbrakk> \<Longrightarrow> \<lbrace>?P'126\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. length rv = unat n_msgRegisters\<rbrace>
 2. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> (\<forall>x. True) \<and> ?P'126 s
 3. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; \<forall>x<Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)). user_word_at (rv ! x) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! x * word_of_nat wordSize) s; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> (\<forall>x. True) \<and> length TCB_H.msgRegisters = unat n_msgRegisters
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; \<forall>x<Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)). user_word_at (rv ! x) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! x * word_of_nat wordSize) s; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s proof (prove)
goal (1 subgoal):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; \<forall>x<Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)). user_word_at (rv ! x) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! x * word_of_nat wordSize) s; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s proof (prove)
goal (1 subgoal):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)); unat i - unat n_msgRegisters < Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)) \<longrightarrow> user_word_at (rv ! (unat i - unat n_msgRegisters)) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! (unat i - unat n_msgRegisters) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> unat i - unat n_msgRegisters < Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)); user_word_at (rv ! (unat i - unat n_msgRegisters)) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! (unat i - unat n_msgRegisters) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116\<rbrakk> \<Longrightarrow> unat i - 4 < 116
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)); user_word_at (rv ! (unat i - unat n_msgRegisters)) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! (unat i - unat n_msgRegisters) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrakk>msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; i < 0x78\<rbrakk> \<Longrightarrow> unat i - 4 < 116
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)); user_word_at (rv ! (unat i - unat n_msgRegisters)) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! (unat i - unat n_msgRegisters) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s proof (prove)
goal (1 subgoal):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> msgMaxLength; SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> i; length rv = Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)); user_word_at (rv ! (unat i - unat n_msgRegisters)) (buffer + [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength] ! (unat i - unat n_msgRegisters) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < unat n_msgRegisters then rva ! unat i else rv ! (unat i - unat n_msgRegisters)) (buffer + (i * 4 + 4)) s proof (prove)
goal (1 subgoal):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + [5 .e. 0x78] ! (unat i - 4) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal (1 subgoal):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + map word_of_nat [5..<121] ! (unat i - 4) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116\<rbrakk> \<Longrightarrow> unat i - 4 < length [5..<121]
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + word_of_nat ([5..<121] ! (unat i - 4)) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116\<rbrakk> \<Longrightarrow> unat i - 4 < 116
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + word_of_nat ([5..<121] ! (unat i - 4)) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrakk>msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; i < 0x78\<rbrakk> \<Longrightarrow> unat i - 4 < 116
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + word_of_nat ([5..<121] ! (unat i - 4)) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal (1 subgoal):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + word_of_nat ([5..<121] ! (unat i - 4)) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116\<rbrakk> \<Longrightarrow> 5 + (unat i - 4) < 121
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + word_of_nat (5 + (unat i - 4)) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116\<rbrakk> \<Longrightarrow> unat i - 4 < 116
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + word_of_nat (5 + (unat i - 4)) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrakk>msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; i < 0x78\<rbrakk> \<Longrightarrow> unat i - 4 < 116
 2. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + word_of_nat (5 + (unat i - 4)) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal (1 subgoal):
 1. \<And>rv rva s. \<lbrakk>i < msgLength info; msgLength info \<le> 0x78; 4 \<le> i; length rv = 116; user_word_at (rv ! (unat i - 4)) (buffer + word_of_nat (5 + (unat i - 4)) * word_of_nat wordSize) s\<rbrakk> \<Longrightarrow> user_word_at (if unat i < 4 then rva ! unat i else rv ! (unat i - 4)) (buffer + (i * 4 + 4)) s proof (prove)
goal:
No subgoals!