theory DetWP

lemma det_wp_getMRs:
  "det_wp (tcb_at' thread and case_option \<top> valid_ipc_buffer_ptr' buffer) (getMRs thread buffer mi)" apply (clarsimp simp: getMRs_def) apply (rule det_wp_pre) apply (wp det_mapM det_getRegister order_refl det_wp_mapM) apply (simp add: word_size) apply (wp asUser_inv mapM_wp' getRegister_inv) apply clarsimp apply (rule conjI) apply (simp add: pointerInUserData_def wordSize_def' word_size) apply (erule valid_ipc_buffer_ptr'D2) apply (rule word_mult_less_mono1) apply (erule order_le_less_trans) apply (simp add: msgMaxLength_def max_ipc_words) apply simp apply (simp add: max_ipc_words) apply (simp add: is_aligned_mult_triv2 [where n = 2, simplified] word_bits_conv) apply (erule valid_ipc_buffer_ptr_aligned_2) apply (simp add: wordSize_def' is_aligned_mult_triv2 [where n = 2, simplified] word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (getMRs thread buffer mi) proof (prove)
goal (1 subgoal):
 1. det_wp (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do hardwareMRValues <- asUser thread (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser;
return (take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues)
od) proof (prove)
goal (2 subgoals):
 1. det_wp ?P' (do hardwareMRValues <- asUser thread (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser;
return (take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues)
od)
 2. \<And>s. (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'22\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. (\<forall>y. buffer = Some y \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. \<forall>x\<in>set (map (\<lambda>x. y + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]). (pointerInUserData x and K (is_aligned x 2)) a)) s) \<and> True\<rbrace>
 2. \<And>s. (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> (tcb_at' thread and (\<lambda>s. (buffer = None \<longrightarrow> True) \<and> ?P'22 s)) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'22\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. \<forall>y. buffer = Some y \<longrightarrow> (\<forall>x. 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x \<and> x \<le> msgMaxLength \<longrightarrow> pointerInUserData (y + x * word_of_nat wordSize) s \<and> is_aligned (y + x * word_of_nat wordSize) 2)\<rbrace>
 2. \<And>s. (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> (tcb_at' thread and (\<lambda>s. (buffer = None \<longrightarrow> True) \<and> ?P'22 s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> (tcb_at' thread and (\<lambda>s. (buffer = None \<longrightarrow> True) \<and> (\<forall>y. buffer = Some y \<longrightarrow> (\<forall>x. 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x \<and> x \<le> msgMaxLength \<longrightarrow> pointerInUserData (y + x * word_of_nat wordSize) s \<and> is_aligned (y + x * word_of_nat wordSize) 2)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> pointerInUserData (y + x * word_of_nat wordSize) s \<and> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> pointerInUserData (y + x * word_of_nat wordSize) s
 2. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> typ_at' UserDataT (y + x * 4 && ~~ mask pageBits) s
 2. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (3 subgoals):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> x * 4 < max_ipc_words * 4
 2. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (x * 4) 2
 3. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (5 subgoals):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> x < max_ipc_words
 2. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> 0 < 4
 3. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> unat max_ipc_words * unat 4 < 2 ^ LENGTH(32)
 4. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (x * 4) 2
 5. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (5 subgoals):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x\<rbrakk> \<Longrightarrow> msgMaxLength < max_ipc_words
 2. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> 0 < 4
 3. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> unat max_ipc_words * unat 4 < 2 ^ LENGTH(32)
 4. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (x * 4) 2
 5. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (4 subgoals):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> 0 < 4
 2. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> unat max_ipc_words * unat 4 < 2 ^ LENGTH(32)
 3. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (x * 4) 2
 4. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (3 subgoals):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> unat max_ipc_words * unat 4 < 2 ^ LENGTH(32)
 2. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (x * 4) 2
 3. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (x * 4) 2
 2. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (1 subgoal):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; valid_ipc_buffer_ptr' y s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (y + x * word_of_nat wordSize) 2 proof (prove)
goal (1 subgoal):
 1. \<And>s y x. \<lbrakk>tcb_at' thread s; buffer = Some y; 1 + word_of_nat (length TCB_H.msgRegisters) \<le> x; x \<le> msgMaxLength\<rbrakk> \<Longrightarrow> is_aligned (x * word_of_nat wordSize) 2 proof (prove)
goal:
No subgoals!