proposition: Lemma massage_queue_into_ByteString : forall n w1 paddingOK' paddingOK'' paddingOK''' sz' (l' : Vector.t _ sz') sz (l : Vector.t _ sz), {| padding := n; front := w1; paddingOK := paddingOK'; byteString := Vector.append l l' |} = ByteString_enqueue_ByteString {| padding := 0; front := WO; paddingOK := paddingOK'''; byteString := l|} {| padding := n; front := w1; paddingOK := paddingOK''; byteString := l' |}.
proof: Proof. induction l'. - simpl; intros. unfold ByteString_enqueue_ByteString; simpl. rewrite (Vector_append_nil_r _ l) at -1. destruct n as [ | [ | [ | [ | [ | [ | [ | [ | ] ] ] ] ] ] ] ]; try solve [inversion paddingOK']; try shatter_word w1; simpl; unfold queue_into_ByteString; simpl; repeat f_equal. + eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := plus_n_O _). rewrite Vector_append_nil_r' at 1. simpl. f_equal. apply Vector_append_nil_r. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue, ByteString_enqueue; simpl. eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := plus_n_O _). rewrite Vector_append_nil_r' at 1. simpl. f_equal. apply Vector_append_nil_r. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue, ByteString_enqueue; simpl. eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := plus_n_O _). rewrite Vector_append_nil_r' at 1. simpl. f_equal. apply Vector_append_nil_r. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := plus_n_O _). rewrite Vector_append_nil_r' at 1. simpl. f_equal. apply Vector_append_nil_r. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 4; simpl. unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl. unfold ByteString_enqueue at 1; simpl. eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := plus_n_O _). rewrite Vector_append_nil_r' at 1. simpl. f_equal. apply Vector_append_nil_r. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := plus_n_O _). rewrite Vector_append_nil_r' at 1. simpl. f_equal. apply Vector_append_nil_r. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := plus_n_O _). rewrite Vector_append_nil_r' at 1. simpl. f_equal. apply Vector_append_nil_r. + unfold queue_into_ByteString, ByteString_id; simpl. unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := plus_n_O _). rewrite Vector_append_nil_r' at 1. simpl. f_equal. apply Vector_append_nil_r. + omega. - intros. pose proof (IHl' _ (Vector.append l (Vector.cons _ h _ (ByteBuffer.nil)))) as e; simpl in e. unfold ByteString_enqueue_ByteString in *; simpl in *. revert e. unfold ByteString_enqueue_char at 3; simpl. unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. unfold char in *. shatter_word h. simpl. intros H'. assert (sz + 1 + n0 = sz + (S n0)) by omega. transitivity {| padding := n; front := w1; paddingOK := paddingOK'; numBytes := sz + 1 + n0; byteString := Vector.append (Vector.append l (Vector.cons (word 8) (WS x (WS x0 (WS x1 (WS x2 (WS x3 (WS x4 (WS x5 (WS x6 WO)))))))) 0 (Vector.nil (word 8)))) l' |}. * eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := H7). clear; induction l; simpl; intros. unfold ByteBuffer.t; erewrite eq_rect_Vector_cons; f_equal. instantiate (1 := eq_refl); reflexivity. unfold ByteBuffer.t; erewrite eq_rect_Vector_cons; f_equal. erewrite IHl; f_equal. * autounfold with ByteBuffer in *. simpl in *. match goal with |- ?l'' = _ => replace l'' with (ByteString_enqueue_word w1 (Vector.fold_left ByteString_enqueue_char {| padding := 0; front := WO; paddingOK := paddingOK'''; numBytes := sz + 1; byteString := Vector.append l (Vector.cons (word 8) (WS x (WS x0 (WS x1 (WS x2 (WS x3 (WS x4 (WS x5 (WS x6 WO)))))))) 0 (Vector.nil char)) |} l')) end. f_equal; f_equal. eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). rewrite <- H'; reflexivity. Unshelve. omega. 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