proposition: Lemma CorrectAlignedEncoderForChecksum' {S} (checksum_valid : nat -> ByteString -> Prop) (format_A format_B : FormatM S ByteString) (encode_A encode_B : forall sz, AlignedEncodeM sz) (encoder_A_OK : CorrectAlignedEncoder format_A encode_A) (encoder_B_OK : CorrectAlignedEncoder format_B encode_B) (f : nat -> forall {sz}, Vector.t (word 8) sz -> nat -> word 16) (f_OK : forall idx n m (t : Vector.t Core.char n) (v1 : Vector.t Core.char idx) (v2 : Vector.t Core.char m), f n t 0 = f n (v1 ++ t ++ v2) idx) n1 (format_B_sz_eq : forall s ce t ce', format_B s ce ∋ (t, ce') -> bin_measure t = n1) (checksum_OK : forall b1 b3 ext, (exists s ce ce', format_B s ce ∋ (b1, ce')) -> (exists s ce ce', format_A s ce ∋ (b3, ce')) -> let a := (f_bit_aligned_free f) (mappend b1 (mappend (format_checksum _ _ _ _ (wzero 16)) b3)) in let b2 := format_checksum _ _ _ 16 a in checksum_valid (bin_measure (mappend b1 (mappend b2 b3))) (mappend (mappend b1 (mappend b2 b3)) ext)) : CorrectAlignedEncoder (format_B ThenChecksum checksum_valid OfSize 16 ThenCarryOn format_A) (AlignedEncoderForChecksum n1 encode_B encode_A f).
proof: Proof. unfold AlignedEncoderForChecksum. eapply CorrectAlignedEncoderForChecksum; intros; eauto using (EncodeMEquivAlignedEncodeM_word_const (n:=2)); simpl in H; match goal with | H : Some (?a, _) = Some (?b, _) |- _ => replace b with a in * by congruence | H : Some _ = None |- _ => discriminate H end. - apply encode_word'_padding. - rewrite length_encode_word'. reflexivity. - unfold format_checksum in *. eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith 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.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Stores.EmptyStore Bedrock.Word