theory Syscall_C

lemma getMRs_length:
  "\<lbrace>\<lambda>s. msgLength mi \<le> 120\<rbrace> getMRs thread buffer mi
  \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi))
            else length args = unat (msgLength mi)\<rbrace>" supply if_cong[cong] apply (cases buffer) apply (simp add: getMRs_def) apply (rule hoare_pre, wp) apply (rule asUser_const_rv) apply simp apply (wp mapM_length) apply (simp add: min_def length_msgRegisters) apply (clarsimp simp: n_msgRegisters_def) apply (simp add: getMRs_def) apply (rule hoare_pre, wp) apply simp apply (wp mapM_length asUser_const_rv mapM_length)+ apply (clarsimp simp: length_msgRegisters) apply (simp add: min_def split: if_splits) apply (clarsimp simp: word_le_nat_alt) apply (simp add: msgMaxLength_def msgLengthBits_def n_msgRegisters_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (2 subgoals):
 1. buffer = None \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace>
 2. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (2 subgoals):
 1. buffer = None \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> do hardwareMRValues <- asUser thread (mapM getRegister TCB_H.msgRegisters);
return (take (unat (msgLength mi)) hardwareMRValues)
od \<lbrace>\<lambda>args s. length args = min (unat n_msgRegisters) (unat (msgLength mi))\<rbrace>
 2. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (3 subgoals):
 1. buffer = None \<Longrightarrow> \<lbrace>?Q4\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>x a. length (take (unat (msgLength mi)) x) = min (unat n_msgRegisters) (unat (msgLength mi))\<rbrace>
 2. \<And>s. \<lbrakk>buffer = None; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (3 subgoals):
 1. buffer = None \<Longrightarrow> \<lbrace>\<lambda>s. ?Q12\<rbrace> mapM getRegister TCB_H.msgRegisters \<lbrace>\<lambda>x s. length (take (unat (msgLength mi)) x) = min (unat n_msgRegisters) (unat (msgLength mi))\<rbrace>
 2. \<And>s. \<lbrakk>buffer = None; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> ?Q12
 3. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (3 subgoals):
 1. buffer = None \<Longrightarrow> \<lbrace>\<lambda>s. ?Q12\<rbrace> mapM getRegister TCB_H.msgRegisters \<lbrace>\<lambda>x s. min (length x) (unat (msgLength mi)) = min (unat n_msgRegisters) (unat (msgLength mi))\<rbrace>
 2. \<And>s. \<lbrakk>buffer = None; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> ?Q12
 3. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>buffer = None; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> min (length TCB_H.msgRegisters) (unat (msgLength mi)) = min (unat n_msgRegisters) (unat (msgLength mi))
 2. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>buffer = None; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> (if unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) \<le> unat (msgLength mi) then unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) else unat (msgLength mi)) = (if unat n_msgRegisters \<le> unat (msgLength mi) then unat n_msgRegisters else unat (msgLength mi))
 2. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) else length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. msgLength mi \<le> 0x78\<rbrace> do hardwareMRValues <- asUser thread (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]);
return (take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues)
od \<lbrace>\<lambda>args s. length args = unat (msgLength mi)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a x. buffer = Some a \<Longrightarrow> \<lbrace>?B23 a x\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>\<lambda>bufferMRValues a. length (take (unat (msgLength mi)) x @ take (unat (msgLength mi) - length x) bufferMRValues) = unat (msgLength mi)\<rbrace>
 2. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>?Q19 a\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>?B23 a\<rbrace>
 3. \<And>a s. \<lbrakk>buffer = Some a; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> ?Q19 a s proof (prove)
goal (3 subgoals):
 1. \<And>a x. buffer = Some a \<Longrightarrow> \<lbrace>?B23 a x\<rbrace> mapM loadWordUser (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) \<lbrace>\<lambda>bufferMRValues a. min (length x) (unat (msgLength mi)) + min (length bufferMRValues) (unat (msgLength mi) - length x) = unat (msgLength mi)\<rbrace>
 2. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>?Q19 a\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>?B23 a\<rbrace>
 3. \<And>a s. \<lbrakk>buffer = Some a; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> ?Q19 a s proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>buffer = Some a; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> min (length TCB_H.msgRegisters) (unat (msgLength mi)) + min (length (map (\<lambda>x. a + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength])) (unat (msgLength mi) - length TCB_H.msgRegisters) = unat (msgLength mi) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>buffer = Some a; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> min (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (unat (msgLength mi)) + min (Suc (unat msgMaxLength) - unat (1 + SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (unat (msgLength mi) - unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = unat (msgLength mi) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>buffer = Some a; msgLength mi \<le> 0x78\<rbrakk> \<Longrightarrow> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) \<le> unat (msgLength mi) \<longrightarrow> Suc (unat msgMaxLength) - unat (1 + SCAST(32 signed \<rightarrow> 32) n_msgRegisters) \<le> unat (msgLength mi) - unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) \<longrightarrow> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) + (Suc (unat msgMaxLength) - unat (1 + SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = unat (msgLength mi) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>buffer = Some a; unat (msgLength mi) \<le> 120; unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) \<le> unat (msgLength mi); Suc (unat msgMaxLength) - unat (1 + SCAST(32 signed \<rightarrow> 32) n_msgRegisters) \<le> unat (msgLength mi) - unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)\<rbrakk> \<Longrightarrow> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) + (Suc (unat msgMaxLength) - unat (1 + SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) = unat (msgLength mi) proof (prove)
goal:
No subgoals!