proposition: Lemma build_aligned_ByteString_append {numBytes'} : forall (v' : ByteBuffer.t numBytes') {numBytes} (v : ByteBuffer.t numBytes), build_aligned_ByteString (Vector.append v v') = ByteString_enqueue_ByteString (build_aligned_ByteString v) (build_aligned_ByteString v').
proof: Proof. simpl; intros; rewrite <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq (build_aligned_ByteString v)), <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq (build_aligned_ByteString v')), ByteString_enqueue_ByteString_ByteStringToBoundedByteString. unfold build_aligned_ByteString; simpl. unfold BoundedByteStringToByteString; simpl. erewrite <- massage_queue_into_ByteString. unfold ByteStringToBoundedByteString; simpl. assert (Datatypes.length ((Vector.to_list v) ++ (Vector.to_list v')) = numBytes0 + numBytes'). rewrite app_length, <- !ByteBuffer.to_list_length; reflexivity. eapply byteString_f_equal with (numBytes_eq := H); simpl. apply Eqdep_dec.eq_rect_eq_dec; intros; eauto using Peano_dec.eq_nat_dec. induction v; simpl in *. induction v'. - apply Eqdep_dec.eq_rect_eq_dec; intros; eauto using Peano_dec.eq_nat_dec. - simpl in H; injection H; intros. autounfold with ByteBuffer in *. simpl; rewrite eq_rect_Vector_cons with (H' := H0); simpl. f_equal. eapply IHv'. - simpl in H; injection H; intros. autounfold with ByteBuffer in *. simpl; rewrite eq_rect_Vector_cons with (H' := H0); simpl. f_equal. eapply IHv. Unshelve. omega. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer