fact: Definition TCP_Packet_Format : FormatM TCP_Packet ByteString := (format_word ◦ SourcePort ++ format_word ◦ DestPort ++ format_word ◦ SeqNumber ++ format_word ◦ AckNumber ++ format_nat 4 ◦ (plus 5) ◦ (@length _) ◦ Options ++ format_unused_word 3 ++ format_bool ◦ NS ++ format_bool ◦ CWR ++ format_bool ◦ ECE ++ format_bool ◦ (fun urg_opt => Ifopt urg_opt as urg Then true Else false) ◦ UrgentPointer ++ format_bool ◦ ACK ++ format_bool ◦ PSH ++ format_bool ◦ RST ++ format_bool ◦ SYN ++ format_bool ◦ FIN ++ format_word ◦ WindowSize) ThenChecksum (Pseudo_Checksum_Valid srcAddr destAddr tcpLength (natToWord 8 6)) OfSize 16 ThenCarryOn (format_option format_word (format_unused_word 16) ◦ UrgentPointer ++ format_list format_word ◦ Options ++ format_bytebuffer ◦ Payload).
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