proposition: Lemma ByteString_into_queue_eq : forall bs, bs = queue_into_ByteString (ByteString_into_queue bs).
proof: Proof. destruct bs; unfold queue_into_ByteString, ByteString_into_queue; simpl. rewrite <- fold_left_rev_right, rev_app_distr, fold_right_app. induction padding0. - shatter_word front0. pose proof (build_aligned_ByteString_append byteString0 (ByteBuffer.nil)). unfold ByteString_enqueue_ByteString in H; simpl in H. unfold build_aligned_ByteString in H; simpl in H. replace paddingOK0 with (build_aligned_ByteString_subproof) by apply le_uniqueness_proof; rewrite H. simpl. rewrite fold_left_rev_right. replace {| padding := 0; front := WO; paddingOK := build_aligned_ByteString_subproof; numBytes := 0; byteString := ByteBuffer.nil |} with ByteString_id by (eapply byteString_f_equal; simpl; instantiate (1 := eq_refl); reflexivity). generalize ByteString_id; clear. induction byteString0. + simpl. reflexivity. + autounfold with ByteBuffer in *. intros; simpl Vector.fold_left. first [ rewrite IHbyteString0 | unfold Vector.fold_left; rewrite IHbyteString0]. unfold ByteString_enqueue_char. unfold char in h. unfold ByteString_into_queue' at 2. fold (ByteString_into_queue' byteString0). rewrite fold_left_app. unfold wordToQueue. simpl app. rewrite <- !fold_left_cons. unfold fold_left at 3. unfold ByteString_enqueue_word; reflexivity. - rewrite (shatter_word front0). simpl. rewrite rev_app_distr, fold_right_app. simpl. assert (lt padding0 8) by omega. erewrite <- (IHpadding0 _ H). unfold ByteString_enqueue; simpl. destruct (eq_nat_dec padding0 7). subst; omega. repeat f_equal. apply le_uniqueness_proof. 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