proposition: Lemma ByteString2ListOfChar_eq : forall (b ext : ByteString), padding b = 0 -> ByteString2ListOfChar (bin_measure b) (mappend b ext) = Core.byteString (BoundedByteStringToByteString b).
proof: Proof. simpl; intros. destruct b; simpl in *; subst. unfold length_ByteString; simpl padding; rewrite plus_O_n. simpl Core.byteString. revert front paddingOK; induction byteString; intros. - reflexivity. - simpl numBytes in *. rewrite Mult.mult_succ_r, NPeano.Nat.add_comm. rewrite Mult.mult_comm. do 8 rewrite plus_Sn_m. rewrite plus_O_n. symmetry. unfold ByteBuffer.to_list, to_list in *; simpl. rewrite <- (IHbyteString WO paddingOK) at 1. replace (ByteString_enqueue_ByteString {| padding := 0; front := front; paddingOK := paddingOK; byteString := h :: byteString |} ext) with (ByteString_enqueue_ByteString (ByteStringToBoundedByteString (word_into_ByteString (m := 1) paddingOK h)) (ByteString_enqueue_ByteString {| padding := 0; front := front; paddingOK := paddingOK; byteString := byteString |} ext) ). rewrite (fun ext => monoid_dequeue_enqueue_word h ext paddingOK). rewrite mult_comm; shatter_word front; reflexivity. rewrite ByteString_enqueue_ByteString_assoc. f_equal. shatter_word front. unfold char in h; shatter_word h. unfold word_into_ByteString; simpl. unfold ByteStringToBoundedByteString, ByteBuffer.of_list, of_list; simpl. unfold ByteString_enqueue_ByteString; simpl. match goal with |- context [ ?w :: byteString] => generalize w end. intros. assert (forall byteString m (l : ByteBuffer.t m), ByteBuffer.fold_left ByteString_enqueue_char {| padding := 0; front := WO; paddingOK := paddingOK; numBytes := m; byteString := l |} byteString = {| padding := 0; front := WO; paddingOK := paddingOK; numBytes := m + n; byteString := Vector.append l byteString |}). { clear; induction byteString. - simpl; intros; rewrite Vector_append_nil_r'. revert l; rewrite (plus_n_O m); simpl; reflexivity. - simpl; intros. assert (m + 1 + n = m + (1 + n)) by omega. pose proof (Vector_append_assoc _ _ _ H l [h] byteString)%vector. simpl in H0; rewrite H0; clear H0. revert H. simpl. replace (ByteString_enqueue_char {| padding := 0; front := WO; paddingOK := paddingOK; numBytes := m; byteString := l |} h) with {| padding := 0; front := WO; paddingOK := paddingOK; numBytes := m + 1; byteString := l ++ [h]|}%vector. generalize (l ++ [h])%vector. rewrite (plus_comm m 1). simpl. rewrite <- (plus_n_Sm m n). intros. destruct H; simpl. apply IHbyteString. unfold char in h; shatter_word h. unfold ByteString_enqueue_char. rewrite <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq {| padding := 0; front := WO; paddingOK := paddingOK; numBytes := m; byteString := l |}). rewrite <- ByteStringToBoundedByteString_enqueue_word. simpl. Local Transparent Core.ByteString_enqueue_word. simpl. unfold Core.ByteString_enqueue at 6. simpl. unfold Core.ByteString_enqueue at 5. simpl. unfold Core.ByteString_enqueue at 4. simpl. unfold Core.ByteString_enqueue at 3. simpl. unfold Core.ByteString_enqueue at 2. simpl. unfold Core.ByteString_enqueue at 1. simpl. rewrite <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq {| padding := 0; front := WO; paddingOK := paddingOK; numBytes := m + 1; byteString := l ++ _ |})%vector. f_equal. unfold BoundedByteStringToByteString. simpl. f_equal. apply le_uniqueness_proof. unfold eq_rec_r; simpl. rewrite (ByteBuffer_to_list_append _ l _ [_]); reflexivity. } apply H7. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.InternetChecksum Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats Bedrock.Word