proposition: Lemma CorrectAlignedDecoder2CorrectDecoder {A} {cache : Cache.Cache} Invariant (FormatSpec : Specs.FormatM A _) (decoder : CorrectAlignedDecoderFor Invariant FormatSpec) : Specs.CorrectDecoderFor Invariant FormatSpec.
proof: Proof. eexists (projT1 (projT2 decoder)). abstract (destruct decoder as [aligned_decoder [ [decoder Inv] ? ] ]; simpl in *; intuition eauto). Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Monoid Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedByteBuffer Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedIPChecksum