proposition: Lemma queue_into_ByteString_eq_split_Vector_bool : forall l, exists paddingOK', queue_into_ByteString l = {| front := projT2 (snd (split_Vector_bool l)); paddingOK := paddingOK'; byteString := projT2 (fst (split_Vector_bool l)) |}.
proof: Proof. intro; generalize (le_refl (length l)); remember (length l). unfold queue_into_ByteString. replace (projT2 (fst (split_Vector_bool l))) with (Vector.append (byteString ByteString_id) (projT2 (fst (split_Vector_bool l)))) by reflexivity. assert (padding ByteString_id = 0) as H' by reflexivity; revert H'. assert (forall sz bs, padding bs = 0 -> numBytes bs = sz -> (n <= n)%nat -> exists paddingOK' : (projT1 (snd (split_Vector_bool l)) < 8)%nat, fold_left (fun (bs : ByteString) (b : bool) => ByteString_enqueue b bs) l bs = {| padding := projT1 (snd (split_Vector_bool l)); front := projT2 (snd (split_Vector_bool l)); paddingOK := paddingOK'; numBytes := _ + projT1 (fst (split_Vector_bool l)); byteString := Vector.append (byteString bs) (projT2 (fst (split_Vector_bool l))) |}); [ | intros; eapply (H 0); eauto ]. setoid_rewrite Heqn at 1; clear Heqn; revert l; induction n. - intros; destruct l; simpl; intros. + eexists (lt_0_Sn _). symmetry in H0. symmetry in H. destruct bs; simpl in *. subst. eapply byteString_f_equal with (padding_eq := _); simpl. * instantiate (1 := eq_refl); simpl; shatter_word front0; reflexivity. * instantiate (1 := sym_eq (plus_n_O numBytes0)). eauto using Vector_append_nil_r. + inversion H1. - intros l sz b H0 H'' H; destruct l as [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? ] ] ] ] ] ] ] ]; try match goal with |- exists _ : lt ?z 8, _ => let H := fresh in try (assert (lt z 8) as H by (simpl; omega); exists H; simpl in H); solve [unfold queue_into_ByteString, ByteString_id; simpl; destruct b; simpl in *; subst; erewrite ByteString_enqueue_simpl by (simpl; omega); shatter_word front0; repeat f_equal; eauto using app_nil_r, le_uniqueness_proof; simpl; intros; eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity); eauto using Vector_append_nil_r] end. + unfold queue_into_ByteString, ByteString_id; simpl; unfold ByteString_enqueue; simpl; repeat f_equal. eexists (lt_0_Sn _). symmetry in H0. symmetry in H''. destruct b; simpl in *. subst. eapply byteString_f_equal with (padding_eq := _); simpl. * instantiate (1 := eq_refl); simpl; shatter_word front0; reflexivity. * instantiate (1 := sym_eq (plus_n_O numBytes0)). eauto using Vector_append_nil_r. + destruct (split_Vector_bool l) eqn : ?. destruct b. destruct (IHn l (S sz) {| front := WO; paddingOK := lt_0_Sn _; byteString := Vector.append byteString0 (Vector.cons _ (WS b7 (WS b6 (WS b5 (WS b4 (WS b3 (WS b2 (WS b1 (WS b0 WO)))))))) _ (ByteBuffer.nil)) |}). simpl in *; omega. simpl in *; omega. simpl in *; omega. simpl split_Vector_bool. revert x H0 H1; rewrite Heqp; intros; clear Heqp. exists x. simpl byteString. unfold fst. simpl in H0. revert front0 paddingOK0 H''. rewrite H0; intros. shatter_word front0. rewrite fold_left_enqueue_simpl, H1; intros; simpl. assert (numBytes0 + (S (projT1 s)) = numBytes0 + 1 + projT1 s) by omega. eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). instantiate (1 := H2). clear; induction byteString0; simpl; intros. * autounfold with ByteBuffer in *; erewrite eq_rect_Vector_cons; f_equal. instantiate (1 := eq_refl); reflexivity. * unfold ByteBuffer.t in *; erewrite eq_rect_Vector_cons; f_equal. erewrite IHbyteString0; f_equal. Unshelve. simpl; omega. simpl; omega. simpl; omega. simpl; omega. simpl; omega. simpl; omega. simpl; omega. 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