fact: Definition composeChecksum (format1 : FormatM A B) (format2 : FormatM A B) (a : A) (ctx : _) := `(p, ctx) <- format1 a ctx; `(q, ctx) <- format2 a (addE ctx checksum_sz); c <- { c : word checksum_sz | forall ext, checksum_Valid (bin_measure (mappend p (mappend (format_checksum c) q))) (mappend (mappend p (mappend (format_checksum c) q)) ext) }; ret (mappend p (mappend (format_checksum c) q), ctx)%comp.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats