theory Ipc_C

lemma setExtraBadge_ccorres:
  "ccorres dc xfdc
           (valid_pspace' and valid_ipc_buffer_ptr' buffer and (\<lambda>_. msg_max_length + 2 + n < unat max_ipc_words))
           (UNIV \<inter> \<lbrace>\<acute>bufferPtr = Ptr buffer\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>i = of_nat n\<rbrace>)
           hs
           (setExtraBadge buffer badge n)
           (Call setExtraBadge_'proc)" apply (rule ccorres_gen_asm) apply (cinit lift: bufferPtr_' badge_' i_') apply (unfold storeWordUser_def) apply (rule ccorres_pre_stateAssert) apply (simp only: K_bind_def) apply (rule ccorres_move_array_assertion_ipc_buffer
               ccorres_Guard[where F=C_Guard]
               ccorres_Guard[where F=SignedArithmetic]
               )+ apply (ctac add: storeWord_ccorres) apply (clarsimp simp: bufferCPtrOffset_def word_size msgMaxLength_def wordSize_def'
                        seL4_MsgLengthBits_def seL4_MsgMaxLength_def Types_H.msgLengthBits_def
                        field_simps Collect_const_mem) apply (subgoal_tac " is_aligned (buffer + (of_nat n * 4 + 0x1E8)) 2") apply clarsimp prefer 2 apply (clarsimp simp: valid_ipc_buffer_ptr'_def) apply (erule aligned_add_aligned, simp_all add: word_bits_def) apply (rule_tac n=2 in aligned_add_aligned, simp_all add: word_bits_def) apply (rule is_aligned_mult_triv2 [where n = 2, simplified]) apply (simp add: is_aligned_def) apply (auto simp: pointerInUserData_c_guard pointerInUserData_h_t_valid
                    msg_align_bits max_ipc_words_def msg_max_length_def
                    capTransferDataSize_def msgMaxLength_def msgMaxExtraCaps_def
                    msgExtraCapBits_def unat_word_ariths unat_of_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and valid_ipc_buffer_ptr' buffer and (\<lambda>_. msg_max_length + 2 + n < unat max_ipc_words)) (UNIV \<inter> \<lbrace>\<acute>bufferPtr = PTR(32 word) buffer\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>i = word_of_nat n\<rbrace>) hs (setExtraBadge buffer badge n) (Call setExtraBadge_'proc) proof (prove)
goal (1 subgoal):
 1. msg_max_length + 2 + n < unat max_ipc_words \<Longrightarrow> ccorres dc xfdc (valid_pspace' and valid_ipc_buffer_ptr' buffer) (UNIV \<inter> \<lbrace>\<acute>bufferPtr = PTR(32 word) buffer\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace> \<inter> \<lbrace>\<acute>i = word_of_nat n\<rbrace>) hs (setExtraBadge buffer badge n) (Call setExtraBadge_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>i badgea bufferPtr. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q138 i badgea bufferPtr) (?Q'138 i badgea bufferPtr) (SKIP # hs) (storeWordUser (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) badge) (Guard MemorySafety \<lbrace>SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i = 0 \<or> array_assertion bufferPtr (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i))} (Guard SignedArithmetic \<lbrace>0 \<le> 2147483650 + sint seL4_MsgMaxLength \<and> sint seL4_MsgMaxLength \<le> 2147483645\<rbrace> (Guard MemorySafety \<lbrace>SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i = 0 \<or> array_assertion bufferPtr (Suc (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) badgea)))))))
 2. \<And>i badgea bufferPtr s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q138 i badgea bufferPtr s \<and> s' \<in> ?Q'138 i badgea bufferPtr proof (prove)
goal (2 subgoals):
 1. \<And>i badgea bufferPtr. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q138 i badgea bufferPtr) (?Q'138 i badgea bufferPtr) (SKIP # hs) (do stateAssert (pointerInUserData (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize)) [];
doMachineOp $ storeWord (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) badge
od) (Guard MemorySafety \<lbrace>SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i = 0 \<or> array_assertion bufferPtr (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i))} (Guard SignedArithmetic \<lbrace>0 \<le> 2147483650 + sint seL4_MsgMaxLength \<and> sint seL4_MsgMaxLength \<le> 2147483645\<rbrace> (Guard MemorySafety \<lbrace>SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i = 0 \<or> array_assertion bufferPtr (Suc (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) badgea)))))))
 2. \<And>i badgea bufferPtr s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q138 i badgea bufferPtr s \<and> s' \<in> ?Q'138 i badgea bufferPtr proof (prove)
goal (2 subgoals):
 1. \<And>i badgea bufferPtr rv. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q144 i badgea bufferPtr rv) (?Q'144 i badgea bufferPtr rv) (SKIP # hs) (K_bind (doMachineOp $ storeWord (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) badge) rv) (Guard MemorySafety \<lbrace>SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i = 0 \<or> array_assertion bufferPtr (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i))} (Guard SignedArithmetic \<lbrace>0 \<le> 2147483650 + sint seL4_MsgMaxLength \<and> sint seL4_MsgMaxLength \<le> 2147483645\<rbrace> (Guard MemorySafety \<lbrace>SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i = 0 \<or> array_assertion bufferPtr (Suc (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) badgea)))))))
 2. \<And>i badgea bufferPtr s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (pointerInUserData (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) s \<longrightarrow> ?Q144 i badgea bufferPtr () s) \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q144 i badgea bufferPtr rv s \<longrightarrow> s' \<in> ?Q'144 i badgea bufferPtr rv} proof (prove)
goal (2 subgoals):
 1. \<And>i badgea bufferPtr rv. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q144 (word_of_nat n) badge (PTR(32 word) buffer) rv) (?Q'144 (word_of_nat n) badge (PTR(32 word) buffer) rv) (SKIP # hs) (doMachineOp $ storeWord (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) badge) (Guard MemorySafety \<lbrace>SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + word_of_nat n = 0 \<or> array_assertion (PTR(32 word) buffer) (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + word_of_nat n)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (PTR(32 word) buffer +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + word_of_nat n))} (Guard SignedArithmetic \<lbrace>0 \<le> 2147483650 + sint seL4_MsgMaxLength \<and> sint seL4_MsgMaxLength \<le> 2147483645\<rbrace> (Guard MemorySafety \<lbrace>SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + word_of_nat n = 0 \<or> array_assertion (PTR(32 word) buffer) (Suc (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + word_of_nat n))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) buffer +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + word_of_nat n)) badge)))))))
 2. \<And>i badgea bufferPtr s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (pointerInUserData (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) s \<longrightarrow> ?Q144 i badgea bufferPtr () s) \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q144 i badgea bufferPtr rv s \<longrightarrow> s' \<in> ?Q'144 i badgea bufferPtr rv} proof (prove)
goal (2 subgoals):
 1. \<And>i badgea bufferPtr rv. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A167 (word_of_nat n) badge (PTR(32 word) buffer) rv) (?C'164 (word_of_nat n) badge (PTR(32 word) buffer) rv) (SKIP # hs) (doMachineOp $ storeWord (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) badge) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) buffer +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + word_of_nat n)) badge)))
 2. \<And>i badgea bufferPtr s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (pointerInUserData (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) s \<longrightarrow> (?A167 i badgea bufferPtr () and valid_ipc_buffer_ptr' (ptr_val bufferPtr) and valid_ipc_buffer_ptr' (ptr_val bufferPtr)) s) \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?A167 i badgea bufferPtr rv and valid_ipc_buffer_ptr' (ptr_val bufferPtr) and valid_ipc_buffer_ptr' (ptr_val bufferPtr)) s \<longrightarrow> s' \<in> ?C'164 i badgea bufferPtr rv \<inter> \<lbrace>Suc (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) \<le> 2 ^ (msg_align_bits - 2) \<and> (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i \<noteq> 0 \<longrightarrow> Suc (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>0 \<le> 2147483650 + sint seL4_MsgMaxLength \<and> sint seL4_MsgMaxLength \<le> 2147483645\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c (bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i))} \<inter> \<lbrace>unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i) \<le> 2 ^ (msg_align_bits - 2) \<and> (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i \<noteq> 0 \<longrightarrow> unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i) \<noteq> 0)\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>i badgea bufferPtr s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; i = word_of_nat n; badgea = badge; bufferPtr = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (pointerInUserData (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) s \<longrightarrow> (valid_pspace' and K (is_aligned (buffer + bufferCPtrOffset + i * word_of_nat wordSize) 2) and pointerInUserData (buffer + bufferCPtrOffset + i * word_of_nat wordSize) and valid_ipc_buffer_ptr' (ptr_val bufferPtr) and valid_ipc_buffer_ptr' (ptr_val bufferPtr)) s) \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (valid_pspace' and K (is_aligned (buffer + bufferCPtrOffset + i * word_of_nat wordSize) 2) and pointerInUserData (buffer + bufferCPtrOffset + i * word_of_nat wordSize) and valid_ipc_buffer_ptr' (ptr_val bufferPtr) and valid_ipc_buffer_ptr' (ptr_val bufferPtr)) s \<longrightarrow> s' \<in> UNIV \<inter> \<lbrace>bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i) = PTR(32 word) (buffer + bufferCPtrOffset + i * word_of_nat wordSize)\<rbrace> \<inter> \<lbrace>c_guard (bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i))\<rbrace> \<inter> \<lbrace>badgea = badgea\<rbrace> \<inter> \<lbrace>Suc (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) \<le> 2 ^ (msg_align_bits - 2) \<and> (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i \<noteq> 0 \<longrightarrow> Suc (unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i)) \<noteq> 0)\<rbrace> \<inter> \<lbrace>0 \<le> 2147483650 + sint seL4_MsgMaxLength \<and> sint seL4_MsgMaxLength \<le> 2147483645\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c (bufferPtr +\<^sub>p uint (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i))} \<inter> \<lbrace>unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i) \<le> 2 ^ (msg_align_bits - 2) \<and> (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i \<noteq> 0 \<longrightarrow> unat (SCAST(32 signed \<rightarrow> 32) (seL4_MsgMaxLength + 2) + i) \<noteq> 0)\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> (pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) s \<longrightarrow> is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> valid_pspace' s \<and> is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2 \<and> pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) s \<and> valid_ipc_buffer_ptr' buffer s) \<longrightarrow> c_guard (PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8))) \<and> Suc (unat (word_of_nat n + 0x7A)) \<le> 2 ^ (msg_align_bits - 2) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8)) \<and> unat (word_of_nat n + 0x7A) \<le> 2 ^ (msg_align_bits - 2) \<and> (word_of_nat n + 0x7A \<noteq> 0 \<longrightarrow> 0 < unat (word_of_nat n + 0x7A))) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s; is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2\<rbrakk> \<Longrightarrow> (pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) s \<longrightarrow> is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> valid_pspace' s \<and> is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2 \<and> pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) s \<and> valid_ipc_buffer_ptr' buffer s) \<longrightarrow> c_guard (PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8))) \<and> Suc (unat (word_of_nat n + 0x7A)) \<le> 2 ^ (msg_align_bits - 2) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8)) \<and> unat (word_of_nat n + 0x7A) \<le> 2 ^ (msg_align_bits - 2) \<and> (word_of_nat n + 0x7A \<noteq> 0 \<longrightarrow> 0 < unat (word_of_nat n + 0x7A)))
 2. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s; is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2; (sa, s') \<in> rf_sr; valid_pspace' sa; pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) sa; valid_ipc_buffer_ptr' buffer sa\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8))) \<and> Suc (unat (word_of_nat n + 0x7A)) \<le> 2 ^ (msg_align_bits - 2) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8)) \<and> unat (word_of_nat n + 0x7A) \<le> 2 ^ (msg_align_bits - 2) \<and> (word_of_nat n + 0x7A \<noteq> 0 \<longrightarrow> 0 < unat (word_of_nat n + 0x7A))
 2. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2
 2. \<And>s s' sa. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s; is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2; (sa, s') \<in> rf_sr; valid_pspace' sa; pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) sa; valid_ipc_buffer_ptr' buffer sa\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8))) \<and> Suc (unat (word_of_nat n + 0x7A)) \<le> 2 ^ (msg_align_bits - 2) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8)) \<and> unat (word_of_nat n + 0x7A) \<le> 2 ^ (msg_align_bits - 2) \<and> (word_of_nat n + 0x7A \<noteq> 0 \<longrightarrow> 0 < unat (word_of_nat n + 0x7A)) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; is_aligned buffer msg_align_bits; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2
 2. \<And>s s' sa. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s; is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2; (sa, s') \<in> rf_sr; valid_pspace' sa; pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) sa; valid_ipc_buffer_ptr' buffer sa\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8))) \<and> Suc (unat (word_of_nat n + 0x7A)) \<le> 2 ^ (msg_align_bits - 2) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8)) \<and> unat (word_of_nat n + 0x7A) \<le> 2 ^ (msg_align_bits - 2) \<and> (word_of_nat n + 0x7A \<noteq> 0 \<longrightarrow> 0 < unat (word_of_nat n + 0x7A)) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat n * 4 + 0x1E8) 2
 2. \<And>s s' sa. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s; is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2; (sa, s') \<in> rf_sr; valid_pspace' sa; pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) sa; valid_ipc_buffer_ptr' buffer sa\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8))) \<and> Suc (unat (word_of_nat n + 0x7A)) \<le> 2 ^ (msg_align_bits - 2) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8)) \<and> unat (word_of_nat n + 0x7A) \<le> 2 ^ (msg_align_bits - 2) \<and> (word_of_nat n + 0x7A \<noteq> 0 \<longrightarrow> 0 < unat (word_of_nat n + 0x7A)) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat n * 4) 2
 2. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned 0x1E8 2
 3. \<And>s s' sa. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s; is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2; (sa, s') \<in> rf_sr; valid_pspace' sa; pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) sa; valid_ipc_buffer_ptr' buffer sa\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8))) \<and> Suc (unat (word_of_nat n + 0x7A)) \<le> 2 ^ (msg_align_bits - 2) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8)) \<and> unat (word_of_nat n + 0x7A) \<le> 2 ^ (msg_align_bits - 2) \<and> (word_of_nat n + 0x7A \<noteq> 0 \<longrightarrow> 0 < unat (word_of_nat n + 0x7A)) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned 0x1E8 2
 2. \<And>s s' sa. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s; is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2; (sa, s') \<in> rf_sr; valid_pspace' sa; pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) sa; valid_ipc_buffer_ptr' buffer sa\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8))) \<and> Suc (unat (word_of_nat n + 0x7A)) \<le> 2 ^ (msg_align_bits - 2) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8)) \<and> unat (word_of_nat n + 0x7A) \<le> 2 ^ (msg_align_bits - 2) \<and> (word_of_nat n + 0x7A \<noteq> 0 \<longrightarrow> 0 < unat (word_of_nat n + 0x7A)) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>Suc (Suc (msg_max_length + n)) < unat max_ipc_words; (s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s; is_aligned (buffer + (word_of_nat n * 4 + 0x1E8)) 2; (sa, s') \<in> rf_sr; valid_pspace' sa; pointerInUserData (buffer + (word_of_nat n * 4 + 0x1E8)) sa; valid_ipc_buffer_ptr' buffer sa\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8))) \<and> Suc (unat (word_of_nat n + 0x7A)) \<le> 2 ^ (msg_align_bits - 2) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) (buffer + (word_of_nat n * 4 + 0x1E8)) \<and> unat (word_of_nat n + 0x7A) \<le> 2 ^ (msg_align_bits - 2) \<and> (word_of_nat n + 0x7A \<noteq> 0 \<longrightarrow> 0 < unat (word_of_nat n + 0x7A)) proof (prove)
goal:
No subgoals!