theory Ipc_C

lemma loadCapTransfer_ccorres [corres]:
  "ccorres  cct_relation ret__struct_cap_transfer_C_'
           (valid_pspace' and valid_ipc_buffer_ptr' buffer)
           (UNIV \<inter> \<lbrace>\<acute>buffer = Ptr buffer\<rbrace>) hs
           (loadCapTransfer buffer)
           (Call loadCapTransfer_'proc)" apply (cinit lift: buffer_') apply (rule ccorres_Guard_Seq)+ apply csymbr apply (simp add: seL4_MsgLengthBits_def
                    seL4_MsgExtraCapBits_def
                    seL4_MsgMaxLength_def
                    ptr_add_assertion_positive) apply (rule ccorres_move_array_assertion_ipc_buffer
               ccorres_rhs_assoc)+ apply (rule ccorres_add_return2) apply (ctac(no_vcg)) apply (rule ccorres_move_array_assertion_ipc_buffer) apply simp apply (ctac (no_vcg) add: ccorres_return_C) apply (wp capTransferFromWords_inv | simp)+ apply (clarsimp simp: word_size) apply (simp add: seL4_MsgLengthBits_def
                   seL4_MsgExtraCapBits_def
                   seL4_MsgMaxLength_def
                   word_size word_sle_def
                   msgMaxLength_def msgMaxExtraCaps_def
                   msgLengthBits_def msgExtraCapBits_def
                   Collect_const_mem msg_align_bits) apply (frule(1) valid_ipc_buffer_ptr_array[where p="Ptr p'" for p', simplified],
    rule order_refl, simp_all add: msg_align_bits) apply (clarsimp simp: valid_ipc_buffer_ptr'_def wordSize_def') apply (subst array_assertion_shrink_left_add_div, assumption) apply (simp add: msgMaxLength_def msgExtraCaps_def msgMaxExtraCaps_def msgExtraCapBits_def
                    shiftL_nat) apply simp apply (erule aligned_add_aligned, simp_all add: is_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres cct_relation ret__struct_cap_transfer_C_' (valid_pspace' and valid_ipc_buffer_ptr' buffer) (UNIV \<inter> \<lbrace>\<acute>buffer = PTR(32 word) buffer\<rbrace>) hs (loadCapTransfer buffer) (Call loadCapTransfer_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>buffera. buffera = PTR(32 word) buffer \<Longrightarrow> ccorres cct_relation ret__struct_cap_transfer_C_' (?Q115 buffera) (?Q'115 buffera) (SKIP # hs) (capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) (Guard ShiftError \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace> (Guard ShiftError \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> (\<acute>offset___int :== UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))));;
(Guard MemorySafety \<lbrace>ptr_add_assertion buffera (sint \<acute>offset___int) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ret__struct_cap_transfer_C :== CALL capTransferFromWords_'proc(buffera +\<^sub>p sint \<acute>offset___int);;
Guard MemorySafety \<lbrace>ptr_add_assertion buffera (sint \<acute>offset___int) False (hrs_htd \<acute>t_hrs)\<rbrace> SKIP);;
return_C ret__struct_cap_transfer_C_'_update ret__struct_cap_transfer_C_'))
 2. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q115 buffera s \<and> s' \<in> ?Q'115 buffera proof (prove)
goal (2 subgoals):
 1. \<And>buffera. buffera = PTR(32 word) buffer \<Longrightarrow> ccorres cct_relation ret__struct_cap_transfer_C_' (?Q115 buffera) (?C'123 buffera) (SKIP # hs) (capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) (\<acute>offset___int :== UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits));;
(Guard MemorySafety \<lbrace>ptr_add_assertion buffera (sint \<acute>offset___int) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ret__struct_cap_transfer_C :== CALL capTransferFromWords_'proc(buffera +\<^sub>p sint \<acute>offset___int);;
Guard MemorySafety \<lbrace>ptr_add_assertion buffera (sint \<acute>offset___int) False (hrs_htd \<acute>t_hrs)\<rbrace> SKIP);;
return_C ret__struct_cap_transfer_C_'_update ret__struct_cap_transfer_C_'))
 2. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q115 buffera s \<and> s' \<in> ?C'123 buffera \<inter> \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>buffera. buffera = PTR(32 word) buffer \<Longrightarrow> ccorres cct_relation ret__struct_cap_transfer_C_' (?Q115 buffera) (?G'127 buffera) (SKIP # hs) (capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) (Guard MemorySafety \<lbrace>ptr_add_assertion buffera (sint (UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits)))) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ret__struct_cap_transfer_C :== CALL capTransferFromWords_'proc(buffera +\<^sub>p sint (UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))));;
Guard MemorySafety \<lbrace>ptr_add_assertion buffera (sint (UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits)))) False (hrs_htd \<acute>t_hrs)\<rbrace> SKIP);;
return_C ret__struct_cap_transfer_C_'_update ret__struct_cap_transfer_C_')
 2. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q115 buffera s \<and> s' \<in> {s. s\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> ?G'127 buffera} \<inter> \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace> proof (prove)
goal (2 subgoals):
 1. ccorres cct_relation ret__struct_cap_transfer_C_' (?Q115 (PTR(32 word) buffer)) (?G'127 (PTR(32 word) buffer)) (SKIP # hs) (capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) (Guard MemorySafety \<lbrace>array_assertion (PTR(32 word) buffer) 125 (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ret__struct_cap_transfer_C :== CALL capTransferFromWords_'proc(PTR(32 word) (buffer + 0x1F4));;
Guard MemorySafety \<lbrace>array_assertion (PTR(32 word) buffer) 125 (hrs_htd \<acute>t_hrs)\<rbrace> SKIP);;
return_C ret__struct_cap_transfer_C_'_update ret__struct_cap_transfer_C_')
 2. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q115 buffera s \<and> s' \<in> {s. s\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> ?G'127 buffera} \<inter> \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace> proof (prove)
goal (2 subgoals):
 1. ccorres cct_relation ret__struct_cap_transfer_C_' (?A208 (PTR(32 word) buffer)) (?C'206 (PTR(32 word) buffer)) (SKIP # hs) (capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) (\<acute>ret__struct_cap_transfer_C :== CALL capTransferFromWords_'proc(PTR(32 word) (buffer + 0x1F4));;
(Guard MemorySafety \<lbrace>array_assertion (PTR(32 word) buffer) 125 (hrs_htd \<acute>t_hrs)\<rbrace> SKIP;;
return_C ret__struct_cap_transfer_C_'_update ret__struct_cap_transfer_C_'))
 2. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A208 buffera and valid_ipc_buffer_ptr' (ptr_val buffera)) s \<and> s' \<in> {s. s\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> ?C'206 buffera \<inter> \<lbrace>125 \<le> 2 ^ (msg_align_bits - 2) \<and> (Suc 0 \<noteq> 0 \<longrightarrow> 125 \<noteq> 0)\<rbrace>} \<inter> \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace> proof (prove)
goal (2 subgoals):
 1. ccorres cct_relation ret__struct_cap_transfer_C_' (?A208 (PTR(32 word) buffer)) (?C'206 (PTR(32 word) buffer)) (SKIP # hs) (capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) >>= return) (\<acute>ret__struct_cap_transfer_C :== CALL capTransferFromWords_'proc(PTR(32 word) (buffer + 0x1F4));;
(Guard MemorySafety \<lbrace>array_assertion (PTR(32 word) buffer) 125 (hrs_htd \<acute>t_hrs)\<rbrace> SKIP;;
return_C ret__struct_cap_transfer_C_'_update ret__struct_cap_transfer_C_'))
 2. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A208 buffera and valid_ipc_buffer_ptr' (ptr_val buffera)) s \<and> s' \<in> {s. s\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> ?C'206 buffera \<inter> \<lbrace>125 \<le> 2 ^ (msg_align_bits - 2) \<and> (Suc 0 \<noteq> 0 \<longrightarrow> 125 \<noteq> 0)\<rbrace>} \<inter> \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv ret__struct_cap_transfer_C. cct_relation rv ret__struct_cap_transfer_C \<Longrightarrow> ccorres cct_relation ret__struct_cap_transfer_C_' (?Q216 rv) (?Q'216 rv ret__struct_cap_transfer_C) (SKIP # hs) (return rv) (Guard MemorySafety \<lbrace>array_assertion (PTR(32 word) buffer) 125 (hrs_htd \<acute>t_hrs)\<rbrace> SKIP;;
return_C ret__struct_cap_transfer_C_'_update (\<lambda>a. ret__struct_cap_transfer_C))
 2. \<lbrace>?R225 (PTR(32 word) buffer)\<rbrace> capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) \<lbrace>?Q216\<rbrace>
 3. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) 2) and ?R225 buffera and valid_ipc_buffer_ptr' (ptr_val buffera)) s \<and> s' \<in> {s. s\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> {s. wptr_'_update (\<lambda>_. PTR(32 word) (buffer + 0x1F4)) s \<in> UNIV \<inter> \<lbrace>array_assertion (PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) 3 (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> \<lbrace>\<acute>wptr = PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)\<rbrace>} \<inter> {s'. \<forall>t rv. cct_relation rv (ret__struct_cap_transfer_C_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__struct_cap_transfer_C_' := ret__struct_cap_transfer_C_' t\<rparr> \<in> ?Q'222 buffera t rv} \<inter> \<lbrace>125 \<le> 2 ^ (msg_align_bits - 2) \<and> (Suc 0 \<noteq> 0 \<longrightarrow> 125 \<noteq> 0)\<rbrace>} \<inter> \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace>
flex-flex pairs:
?Q'222 (PTR(32 word) buffer) \<equiv>\<^sup>? \<lambda>t rv. ?Q'216 rv (ret__struct_cap_transfer_C_' t) proof (prove)
goal (3 subgoals):
 1. \<And>rv ret__struct_cap_transfer_C. cct_relation rv ret__struct_cap_transfer_C \<Longrightarrow> ccorres cct_relation ret__struct_cap_transfer_C_' (?A288 rv) (?C'284 rv ret__struct_cap_transfer_C) (SKIP # hs) (return rv) (SKIP;;
return_C ret__struct_cap_transfer_C_'_update (\<lambda>a. ret__struct_cap_transfer_C))
 2. \<lbrace>?R225 (PTR(32 word) buffer)\<rbrace> capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) \<lbrace>\<lambda>a. ?A288 a and valid_ipc_buffer_ptr' (ptr_val (PTR(32 word) buffer))\<rbrace>
 3. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) 2) and ?R225 buffera and valid_ipc_buffer_ptr' (ptr_val buffera)) s \<and> s' \<in> {s. s\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> {s. wptr_'_update (\<lambda>_. PTR(32 word) (buffer + 0x1F4)) s \<in> UNIV \<inter> \<lbrace>array_assertion (PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) 3 (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> \<lbrace>\<acute>wptr = PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)\<rbrace>} \<inter> {s'. \<forall>t rv. cct_relation rv (ret__struct_cap_transfer_C_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__struct_cap_transfer_C_' := ret__struct_cap_transfer_C_' t\<rparr> \<in> ?C'286 buffera t rv \<inter> \<lbrace>125 \<le> 2 ^ (msg_align_bits - 2) \<and> (Suc 0 \<noteq> 0 \<longrightarrow> 125 \<noteq> 0)\<rbrace>} \<inter> \<lbrace>125 \<le> 2 ^ (msg_align_bits - 2) \<and> (Suc 0 \<noteq> 0 \<longrightarrow> 125 \<noteq> 0)\<rbrace>} \<inter> \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace>
flex-flex pairs:
?C'286 (PTR(32 word) buffer) \<equiv>\<^sup>? \<lambda>t rv. ?C'284 rv (ret__struct_cap_transfer_C_' t) proof (prove)
goal (3 subgoals):
 1. \<And>rv ret__struct_cap_transfer_C. cct_relation rv ret__struct_cap_transfer_C \<Longrightarrow> ccorres cct_relation ret__struct_cap_transfer_C_' (?A288 rv) (?C'284 rv ret__struct_cap_transfer_C) (SKIP # hs) (return rv) (return_C ret__struct_cap_transfer_C_'_update (\<lambda>a. ret__struct_cap_transfer_C))
 2. \<lbrace>?R225 (PTR(32 word) buffer)\<rbrace> capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) \<lbrace>\<lambda>a. ?A288 a and valid_ipc_buffer_ptr' (ptr_val (PTR(32 word) buffer))\<rbrace>
 3. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) 2) and ?R225 buffera and valid_ipc_buffer_ptr' (ptr_val buffera)) s \<and> s' \<in> {s. s\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> {s. wptr_'_update (\<lambda>_. PTR(32 word) (buffer + 0x1F4)) s \<in> UNIV \<inter> \<lbrace>array_assertion (PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) 3 (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> \<lbrace>\<acute>wptr = PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)\<rbrace>} \<inter> {s'. \<forall>t rv. cct_relation rv (ret__struct_cap_transfer_C_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__struct_cap_transfer_C_' := ret__struct_cap_transfer_C_' t\<rparr> \<in> ?C'286 buffera t rv \<inter> \<lbrace>125 \<le> 2 ^ (msg_align_bits - 2) \<and> (Suc 0 \<noteq> 0 \<longrightarrow> 125 \<noteq> 0)\<rbrace>} \<inter> \<lbrace>125 \<le> 2 ^ (msg_align_bits - 2) \<and> (Suc 0 \<noteq> 0 \<longrightarrow> 125 \<noteq> 0)\<rbrace>} \<inter> \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace>
flex-flex pairs:
?C'286 (PTR(32 word) buffer) \<equiv>\<^sup>? \<lambda>t rv. ?C'284 rv (ret__struct_cap_transfer_C_' t) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R225 (PTR(32 word) buffer)\<rbrace> capTransferFromWords (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) \<lbrace>\<lambda>a. (\<lambda>a. True) and valid_ipc_buffer_ptr' (ptr_val (PTR(32 word) buffer))\<rbrace>
 2. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; (valid_pspace' and valid_ipc_buffer_ptr' buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) 2) and ?R225 buffera and valid_ipc_buffer_ptr' (ptr_val buffera)) s \<and> s' \<in> {s. s\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> {s. wptr_'_update (\<lambda>_. PTR(32 word) (buffer + 0x1F4)) s \<in> UNIV \<inter> \<lbrace>array_assertion (PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) 3 (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> \<lbrace>\<acute>wptr = PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)\<rbrace>} \<inter> {s'. \<forall>t rv. cct_relation rv (ret__struct_cap_transfer_C_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__struct_cap_transfer_C_' := ret__struct_cap_transfer_C_' t\<rparr> \<in> \<lbrace>cct_relation rv \<^bsup>t\<^esup>ret__struct_cap_transfer_C\<rbrace> \<inter> \<lbrace>125 \<le> 2 ^ (msg_align_bits - 2) \<and> (Suc 0 \<noteq> 0 \<longrightarrow> 125 \<noteq> 0)\<rbrace>} \<inter> \<lbrace>125 \<le> 2 ^ (msg_align_bits - 2) \<and> (Suc 0 \<noteq> 0 \<longrightarrow> 125 \<noteq> 0)\<rbrace>} \<inter> \<lbrace>seL4_MsgExtraCapBits <s 0x20\<rbrace> \<inter> \<lbrace>0 \<le>s seL4_MsgExtraCapBits\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>buffera s s'. \<lbrakk>buffera = PTR(32 word) buffer; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> is_aligned (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) 2 \<and> array_assertion (PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) 3 (hrs_htd (t_hrs_' (globals s'))) \<and> (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize = 0x1F4 \<and> (\<forall>t. (\<exists>rv. cct_relation rv (ret__struct_cap_transfer_C_' t)) \<longrightarrow> s'\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits)), globals := globals t, ret__struct_cap_transfer_C_' := ret__struct_cap_transfer_C_' t\<rparr> \<in> (if 125 \<le> 2 ^ (msg_align_bits - 2) then UNIV else {})) \<and> s'\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> (if 125 \<le> 2 ^ (msg_align_bits - 2) then UNIV else {}) \<and> s' \<in> (if seL4_MsgExtraCapBits <s 0x20 then UNIV else {}) \<and> s' \<in> (if 0 \<le>s seL4_MsgExtraCapBits then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> is_aligned (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) 2 \<and> array_assertion (PTR(32 word) (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize)) 3 (hrs_htd (t_hrs_' (globals s'))) \<and> (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize = 0x1F4 \<and> (\<forall>t. (\<exists>rv. cct_relation rv (ret__struct_cap_transfer_C_' t)) \<longrightarrow> s'\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits)), globals := globals t, ret__struct_cap_transfer_C_' := ret__struct_cap_transfer_C_' t\<rparr> \<in> (if 125 \<le> 2 ^ (msg_align_bits - 2) then UNIV else {})) \<and> s'\<lparr>offset___int_' := UCAST(32 \<rightarrow> 32 signed) (1 + (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength + 2 ^ unat seL4_MsgExtraCapBits))\<rparr> \<in> (if 125 \<le> 2 ^ (msg_align_bits - 2) then UNIV else {}) \<and> s' \<in> (if seL4_MsgExtraCapBits <s 0x20 then UNIV else {}) \<and> s' \<in> (if 0 \<le>s seL4_MsgExtraCapBits then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s\<rbrakk> \<Longrightarrow> is_aligned (buffer + 0x7D * word_of_nat wordSize) 2 \<and> array_assertion (PTR(32 word) (buffer + 0x7D * word_of_nat wordSize)) 3 (hrs_htd (t_hrs_' (globals s'))) \<and> 0x7D * word_of_nat wordSize = 0x1F4 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; valid_ipc_buffer_ptr' buffer s; array_assertion (PTR(32 word) buffer) 128 (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> is_aligned (buffer + 0x7D * word_of_nat wordSize) 2 \<and> array_assertion (PTR(32 word) (buffer + 0x7D * word_of_nat wordSize)) 3 (hrs_htd (t_hrs_' (globals s'))) \<and> 0x7D * word_of_nat wordSize = 0x1F4 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; array_assertion (PTR(32 word) buffer) 128 (hrs_htd (t_hrs_' (globals s'))); is_aligned buffer msg_align_bits; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned (buffer + 0x1F4) 2 \<and> array_assertion (PTR(32 word) (buffer + 0x1F4)) 3 (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; array_assertion (PTR(32 word) buffer) 128 (hrs_htd (t_hrs_' (globals s'))); is_aligned buffer msg_align_bits; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> 0x1F4 = word_of_nat (unat 0x1F4 div size_of TYPE(32 word)) * word_of_nat (size_of TYPE(32 word)) \<and> 3 + unat 0x1F4 div size_of TYPE(32 word) \<le> 128 \<and> 0 < 3
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; array_assertion (PTR(32 word) buffer) 128 (hrs_htd (t_hrs_' (globals s'))); is_aligned buffer msg_align_bits; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned (buffer + 0x1F4) 2 \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; array_assertion (PTR(32 word) buffer) 128 (hrs_htd (t_hrs_' (globals s'))); is_aligned buffer msg_align_bits; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned (buffer + 0x1F4) 2 \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_pspace' s; array_assertion (PTR(32 word) buffer) 128 (hrs_htd (t_hrs_' (globals s'))); is_aligned buffer msg_align_bits; typ_at' UserDataT (buffer && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned (buffer + 0x1F4) 2 proof (prove)
goal:
No subgoals!