proposition: Lemma malloc_items: forall v size, 0 <= size -> malloc_compatible (sizeof (Tstruct _structItem noattr) * size) v -> data_at_ Tsh (tarray tint (sizeof (Tstruct _structItem noattr) * size / sizeof tint)) v |-- data_at_ Tsh (tarray t_item size) v.
proof: Proof. intros. sep_apply data_at__memory_block_cancel. rewrite <- memory_block_data_at_. simpl sizeof. apply derives_refl'. f_equal. rewrite (Z.mul_comm 12). change 12 with (3 * 4). rewrite Zaux.Zdiv_eucl_unique. rewrite Z.mul_assoc. rewrite Z_div_mult. 1,2: lia. apply malloc_compatible_field_compatible; try reflexivity. simpl in *. rewrite Z.max_r by lia. trivial. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel