proposition: Lemma CorrectAlignedEncoderForFormatChar_f {S} (proj : S -> word 8) : CorrectAlignedEncoder (Projection_Format format_word proj) (fun sz v idx s => SetCurrentByte v idx (proj s)).
proof: Proof. intros. unfold CorrectAlignedEncoder. eexists (Compose_Encode (fun c env => Some ((build_aligned_ByteString (cons (word 8) c 0 (nil (word 8))), addE env 8))) (fun s => Some (proj s))); split; [ | split]. - unfold Compose_Encode, Projection_Format, Compose_Format; intros. split; intros. + setoid_rewrite aligned_format_char_eq. injections. intros ? ?; apply unfold_computes; eexists; intuition eauto. + simpl in H; discriminate. - unfold Compose_Encode; simpl; intros. injections; reflexivity. - unfold Compose_Encode, EncodeMEquivAlignedEncodeM; intros; injections; intuition; simpl. + injections; simpl; unfold SetCurrentByte. unfold plus; fold plus. destruct (Nat.ltb idx (idx + Datatypes.S m)) eqn: ? ; try omega. * eexists (Vector.append v1 (Vector.cons _ (proj s) _ v2)); split. { repeat f_equal; try omega. clear; simpl in v. revert v v2; induction v1; intros. - replace v with (Vector.cons _ (Vector.hd v) _ (Vector.tl v)). + generalize (Vector.tl v); apply Vector.case0; reflexivity. + revert v; generalize 0; apply Vector.caseS; simpl; intros; reflexivity. - simpl; rewrite IHv1; reflexivity. } { rewrite !ByteString_enqueue_ByteString_assoc. rewrite <- !build_aligned_ByteString_append. assert (idx + 1 + m = idx + Datatypes.S m) by omega. pose proof (Vector_append_assoc _ _ _ H v1 (Vector.cons (word 8) (proj s) 0 (Vector.nil (word 8))) v2). simpl in H1; unfold Core.char in *; unfold plus in *; fold plus in *; rewrite H1. generalize (append (append v1 (Vector.cons (word 8) (proj s) 0 (Vector.nil (word 8)))) v2). rewrite H; reflexivity. } * destruct (le_lt_dec (idx + Datatypes.S m) idx); try omega. apply Nat.ltb_lt in l; congruence. + injections; simpl; unfold SetCurrentByte. destruct (Nat.ltb idx numBytes') eqn: ?; eauto. apply Nat.ltb_lt in Heqb. unfold build_aligned_ByteString in H0. unfold length_ByteString in H0; simpl padding in H0; simpl numBytes in H0. omega. + injections; simpl in *; omega. + discriminate. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad