fact: Definition out := Eval compute in match (@TCP_decoder_impl srcAddr destAddr (natToWord _ (Vector_length tcp_decode_input)) _ tcp_decode_input) with | Some (p, _, _) => (Some (Vector.fold_right (fun c s => String (Ascii.ascii_of_N (wordToN c)) s) (projT2 p.(Payload)) EmptyString), match (@TCP_encoder_impl srcAddr destAddr (natToWord _ (Vector_length tcp_decode_input)) p _ (Vector.const (natToWord 8 0) (Vector_length tcp_decode_input))) with | Some (v, _, _) => Some (Vector.map (@wordToNat 8) v) | None => None end) | None => (None, None) end.
imports: 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 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 Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Automation.AlignedAutomation Bedrock.Word