theory Ipc_C

lemma capTransferFromWords_ccorres [corres]:
  "ccorres cct_relation ret__struct_cap_transfer_C_'
           (valid_pspace' and K (is_aligned ptr 2))
           (UNIV \<inter> \<lbrace>array_assertion (Ptr ptr :: word32 ptr) 3 (hrs_htd \<acute>t_hrs)\<rbrace>
              \<inter> \<lbrace>\<acute>wptr = Ptr ptr\<rbrace>) hs
           (capTransferFromWords ptr)
           (Call capTransferFromWords_'proc)" apply (cinit lift: wptr_') apply (rule ccorres_pre_loadWordUser)+ apply (rule_tac P=\<top>
               and P'="{s. array_assertion (Ptr ptr :: word32 ptr)
                              3 (hrs_htd (t_hrs_' (globals s))) \<and>
                           cslift s (Ptr ptr) = Some rv \<and>
                           cslift s (Ptr (ptr + 4)) = Some rva \<and>
                           cslift s (Ptr (ptr + 8)) = Some rvb}"
                in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: typ_heap_simps' ptr_add_assertion_positive
                         array_assertion_shrink_right) apply (simp add: return_def) apply (simp add: cct_relation_def) apply (clarsimp simp: word_size valid_ipc_buffer_ptr'_def wordSize_def') apply safe apply (erule aligned_add_aligned | simp add: is_aligned_def word_bits_conv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres cct_relation ret__struct_cap_transfer_C_' (valid_pspace' and K (is_aligned ptr 2)) (UNIV \<inter> \<lbrace>array_assertion (PTR(32 word) ptr) 3 (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> \<lbrace>\<acute>wptr = PTR(32 word) ptr\<rbrace>) hs (capTransferFromWords ptr) (Call capTransferFromWords_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>wptr. wptr = PTR(32 word) ptr \<Longrightarrow> ccorres cct_relation ret__struct_cap_transfer_C_' (?Q180 wptr) (?Q'180 wptr) (SKIP # hs) (do w0 <- loadWordUser ptr;
w1 <- loadWordUser (ptr + word_of_nat wordSize);
w2 <- loadWordUser (ptr + 2 * word_of_nat wordSize);
return (CT w0 w1 (unat w2))
od) (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 0 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c wptr} (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 0 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>transfer :== ctReceiveRoot_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) wptr) \<acute>transfer)));;
(Guard MemorySafety \<lbrace>ptr_add_assertion wptr 1 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (wptr +\<^sub>p 1)} (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 1 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>transfer :== ctReceiveIndex_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (wptr +\<^sub>p 1)) \<acute>transfer)));;
(Guard MemorySafety \<lbrace>ptr_add_assertion wptr 2 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (wptr +\<^sub>p 2)} (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 2 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>transfer :== ctReceiveDepth_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (wptr +\<^sub>p 2)) \<acute>transfer)));;
return_C ret__struct_cap_transfer_C_'_update transfer_')))
 2. \<And>wptr s s'. \<lbrakk>wptr = PTR(32 word) ptr; (s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>y. is_aligned ptr 2)) s; s' \<in> \<lbrace>array_assertion (PTR(32 word) ptr) 3 (hrs_htd \<acute>t_hrs)\<rbrace>\<rbrakk> \<Longrightarrow> ?Q180 wptr s \<and> s' \<in> ?Q'180 wptr proof (prove)
goal (2 subgoals):
 1. \<And>wptr rv rva rvb. wptr = PTR(32 word) ptr \<Longrightarrow> ccorres cct_relation ret__struct_cap_transfer_C_' (?P190 wptr rv rva rvb) (?Q190 wptr rv rva rvb) (SKIP # hs) (return (CT rv rva (unat rvb))) (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 0 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c wptr} (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 0 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>transfer :== ctReceiveRoot_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) wptr) \<acute>transfer)));;
(Guard MemorySafety \<lbrace>ptr_add_assertion wptr 1 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (wptr +\<^sub>p 1)} (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 1 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>transfer :== ctReceiveIndex_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (wptr +\<^sub>p 1)) \<acute>transfer)));;
(Guard MemorySafety \<lbrace>ptr_add_assertion wptr 2 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (wptr +\<^sub>p 2)} (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 2 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>transfer :== ctReceiveDepth_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (wptr +\<^sub>p 2)) \<acute>transfer)));;
return_C ret__struct_cap_transfer_C_'_update transfer_')))
 2. \<And>wptr s s'. \<lbrakk>wptr = PTR(32 word) ptr; (s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>y. is_aligned ptr 2)) s; s' \<in> \<lbrace>array_assertion (PTR(32 word) ptr) 3 (hrs_htd \<acute>t_hrs)\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + word_of_nat wordSize) 2) and (\<lambda>s. \<forall>va. user_word_at va (ptr + word_of_nat wordSize) s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + 2 * word_of_nat wordSize) 2) and (\<lambda>s. \<forall>vb. user_word_at vb (ptr + 2 * word_of_nat wordSize) s \<longrightarrow> ?P190 wptr v va vb s)) s)) s)) s \<and> s' \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> {s. \<forall>va. cslift s (PTR(32 word) (ptr + word_of_nat wordSize)) = Some va \<longrightarrow> s \<in> {s. \<forall>vb. cslift s (PTR(32 word) (ptr + 2 * word_of_nat wordSize)) = Some vb \<longrightarrow> s \<in> ?Q190 wptr v va vb}}} proof (prove)
goal (2 subgoals):
 1. \<And>wptr rv rva rvb. wptr = PTR(32 word) ptr \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> {s. array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s))) \<and> cslift s (PTR(32 word) ptr) = Some rv \<and> cslift s (PTR(32 word) (ptr + 4)) = Some rva \<and> cslift s (PTR(32 word) (ptr + 8)) = Some rvb} \<and> (\<sigma>, s) \<in> rf_sr} Guard MemorySafety \<lbrace>ptr_add_assertion wptr 0 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c wptr} (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 0 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>transfer :== ctReceiveRoot_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) wptr) \<acute>transfer)));;
(Guard MemorySafety \<lbrace>ptr_add_assertion wptr 1 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (wptr +\<^sub>p 1)} (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 1 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>transfer :== ctReceiveIndex_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (wptr +\<^sub>p 1)) \<acute>transfer)));;
(Guard MemorySafety \<lbrace>ptr_add_assertion wptr 2 False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (wptr +\<^sub>p 2)} (Guard MemorySafety \<lbrace>ptr_add_assertion wptr 2 True (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>transfer :== ctReceiveDepth_C_update (\<lambda>_. h_val (hrs_mem \<acute>t_hrs) (wptr +\<^sub>p 2)) \<acute>transfer)));;
return_C ret__struct_cap_transfer_C_'_update transfer_')) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (CT rv rva (unat rvb)) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> cct_relation rv (ret__struct_cap_transfer_C_' s)}
 2. \<And>wptr s s'. \<lbrakk>wptr = PTR(32 word) ptr; (s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>y. is_aligned ptr 2)) s; s' \<in> \<lbrace>array_assertion (PTR(32 word) ptr) 3 (hrs_htd \<acute>t_hrs)\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + word_of_nat wordSize) s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + 2 * word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + 2 * word_of_nat wordSize) s \<longrightarrow> True)) s)) s)) s \<and> s' \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> {s. \<forall>va. cslift s (PTR(32 word) (ptr + word_of_nat wordSize)) = Some va \<longrightarrow> s \<in> {s. \<forall>vb. cslift s (PTR(32 word) (ptr + 2 * word_of_nat wordSize)) = Some vb \<longrightarrow> s \<in> {s. array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s))) \<and> cslift s (PTR(32 word) ptr) = Some v \<and> cslift s (PTR(32 word) (ptr + 4)) = Some va \<and> cslift s (PTR(32 word) (ptr + 8)) = Some vb}}}} proof (prove)
goal (2 subgoals):
 1. \<And>wptr rv rva rvb \<sigma>. wptr = PTR(32 word) ptr \<Longrightarrow> {s. True \<and> s \<in> {s. array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s))) \<and> cslift s (PTR(32 word) ptr) = Some rv \<and> cslift s (PTR(32 word) (ptr + 4)) = Some rva \<and> cslift s (PTR(32 word) (ptr + 8)) = Some rvb} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. ptr_add_assertion wptr 0 False (hrs_htd (t_hrs_' (globals s))) \<and> s \<Turnstile>\<^sub>c wptr \<and> ptr_add_assertion wptr 0 True (hrs_htd (t_hrs_' (globals s))) \<and> ptr_add_assertion wptr 1 False (hrs_htd (t_hrs_' (globals s))) \<and> s \<Turnstile>\<^sub>c (wptr +\<^sub>p 1) \<and> ptr_add_assertion wptr 1 True (hrs_htd (t_hrs_' (globals s))) \<and> ptr_add_assertion wptr 2 False (hrs_htd (t_hrs_' (globals s))) \<and> s \<Turnstile>\<^sub>c (wptr +\<^sub>p 2) \<and> ptr_add_assertion wptr 2 True (hrs_htd (t_hrs_' (globals s))) \<and> (\<exists>(rv, \<sigma>')\<in>fst (return (CT rv rva (unat rvb)) \<sigma>). (\<sigma>', s\<lparr>transfer_' := ctReceiveDepth_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (wptr +\<^sub>p 2)) (ctReceiveIndex_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (wptr +\<^sub>p 1)) (ctReceiveRoot_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) wptr) (transfer_' s))), ret__struct_cap_transfer_C_' := ctReceiveDepth_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (wptr +\<^sub>p 2)) (ctReceiveIndex_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (wptr +\<^sub>p 1)) (ctReceiveRoot_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) wptr) (transfer_' s))), global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> cct_relation rv (ctReceiveDepth_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (wptr +\<^sub>p 2)) (ctReceiveIndex_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (wptr +\<^sub>p 1)) (ctReceiveRoot_C_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) wptr) (transfer_' s)))))}
 2. \<And>wptr s s'. \<lbrakk>wptr = PTR(32 word) ptr; (s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>y. is_aligned ptr 2)) s; s' \<in> \<lbrace>array_assertion (PTR(32 word) ptr) 3 (hrs_htd \<acute>t_hrs)\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + word_of_nat wordSize) s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + 2 * word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + 2 * word_of_nat wordSize) s \<longrightarrow> True)) s)) s)) s \<and> s' \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> {s. \<forall>va. cslift s (PTR(32 word) (ptr + word_of_nat wordSize)) = Some va \<longrightarrow> s \<in> {s. \<forall>vb. cslift s (PTR(32 word) (ptr + 2 * word_of_nat wordSize)) = Some vb \<longrightarrow> s \<in> {s. array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s))) \<and> cslift s (PTR(32 word) ptr) = Some v \<and> cslift s (PTR(32 word) (ptr + 4)) = Some va \<and> cslift s (PTR(32 word) (ptr + 8)) = Some vb}}}} proof (prove)
goal (2 subgoals):
 1. \<And>rv rva rvb \<sigma> x. \<lbrakk>array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals x))); cslift x (PTR(32 word) ptr) = Some rv; cslift x (PTR(32 word) (ptr + 4)) = Some rva; cslift x (PTR(32 word) (ptr + 8)) = Some rvb; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (return (CT rv rva (unat rvb)) \<sigma>). case xa of (rvc, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> cct_relation rvc (ctReceiveDepth_C_update (\<lambda>_. rvb) (ctReceiveIndex_C_update (\<lambda>_. rva) (ctReceiveRoot_C_update (\<lambda>_. rv) (transfer_' x))))
 2. \<And>wptr s s'. \<lbrakk>wptr = PTR(32 word) ptr; (s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>y. is_aligned ptr 2)) s; s' \<in> \<lbrace>array_assertion (PTR(32 word) ptr) 3 (hrs_htd \<acute>t_hrs)\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + word_of_nat wordSize) s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + 2 * word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + 2 * word_of_nat wordSize) s \<longrightarrow> True)) s)) s)) s \<and> s' \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> {s. \<forall>va. cslift s (PTR(32 word) (ptr + word_of_nat wordSize)) = Some va \<longrightarrow> s \<in> {s. \<forall>vb. cslift s (PTR(32 word) (ptr + 2 * word_of_nat wordSize)) = Some vb \<longrightarrow> s \<in> {s. array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s))) \<and> cslift s (PTR(32 word) ptr) = Some v \<and> cslift s (PTR(32 word) (ptr + 4)) = Some va \<and> cslift s (PTR(32 word) (ptr + 8)) = Some vb}}}} proof (prove)
goal (2 subgoals):
 1. \<And>rv rva rvb \<sigma> x. \<lbrakk>array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals x))); cslift x (PTR(32 word) ptr) = Some rv; cslift x (PTR(32 word) (ptr + 4)) = Some rva; cslift x (PTR(32 word) (ptr + 8)) = Some rvb; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> cct_relation (CT rv rva (unat rvb)) (ctReceiveDepth_C_update (\<lambda>_. rvb) (ctReceiveIndex_C_update (\<lambda>_. rva) (ctReceiveRoot_C_update (\<lambda>_. rv) (transfer_' x))))
 2. \<And>wptr s s'. \<lbrakk>wptr = PTR(32 word) ptr; (s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>y. is_aligned ptr 2)) s; s' \<in> \<lbrace>array_assertion (PTR(32 word) ptr) 3 (hrs_htd \<acute>t_hrs)\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + word_of_nat wordSize) s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + 2 * word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + 2 * word_of_nat wordSize) s \<longrightarrow> True)) s)) s)) s \<and> s' \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> {s. \<forall>va. cslift s (PTR(32 word) (ptr + word_of_nat wordSize)) = Some va \<longrightarrow> s \<in> {s. \<forall>vb. cslift s (PTR(32 word) (ptr + 2 * word_of_nat wordSize)) = Some vb \<longrightarrow> s \<in> {s. array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s))) \<and> cslift s (PTR(32 word) ptr) = Some v \<and> cslift s (PTR(32 word) (ptr + 4)) = Some va \<and> cslift s (PTR(32 word) (ptr + 8)) = Some vb}}}} proof (prove)
goal (1 subgoal):
 1. \<And>wptr s s'. \<lbrakk>wptr = PTR(32 word) ptr; (s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>y. is_aligned ptr 2)) s; s' \<in> \<lbrace>array_assertion (PTR(32 word) ptr) 3 (hrs_htd \<acute>t_hrs)\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + word_of_nat wordSize) s \<longrightarrow> (valid_pspace' and K (is_aligned (ptr + 2 * word_of_nat wordSize) 2) and (\<lambda>s. \<forall>v. user_word_at v (ptr + 2 * word_of_nat wordSize) s \<longrightarrow> True)) s)) s)) s \<and> s' \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> {s. \<forall>va. cslift s (PTR(32 word) (ptr + word_of_nat wordSize)) = Some va \<longrightarrow> s \<in> {s. \<forall>vb. cslift s (PTR(32 word) (ptr + 2 * word_of_nat wordSize)) = Some vb \<longrightarrow> s \<in> {s. array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s))) \<and> cslift s (PTR(32 word) ptr) = Some v \<and> cslift s (PTR(32 word) (ptr + 4)) = Some va \<and> cslift s (PTR(32 word) (ptr + 8)) = Some vb}}}} proof (prove)
goal (1 subgoal):
 1. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s'))); valid_pspace' s; is_aligned ptr 2; user_word_at v ptr s\<rbrakk> \<Longrightarrow> is_aligned (ptr + 4) 2 \<and> ((\<exists>v. user_word_at v (ptr + 4) s) \<longrightarrow> is_aligned (ptr + 8) 2) proof (prove)
goal (2 subgoals):
 1. \<And>s s' v. \<lbrakk>(s, s') \<in> rf_sr; array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s'))); valid_pspace' s; is_aligned ptr 2; user_word_at v ptr s\<rbrakk> \<Longrightarrow> is_aligned (ptr + 4) 2
 2. \<And>s s' v va. \<lbrakk>(s, s') \<in> rf_sr; array_assertion (PTR(32 word) ptr) 3 (hrs_htd (t_hrs_' (globals s'))); valid_pspace' s; is_aligned ptr 2; user_word_at v ptr s; user_word_at va (ptr + 4) s\<rbrakk> \<Longrightarrow> is_aligned (ptr + 8) 2 proof (prove)
goal:
No subgoals!