fact: Record TCP_Packet := {SourcePort : word 16; DestPort : word 16; SeqNumber : word 32; AckNumber : word 32; NS : bool; CWR : bool; ECE : bool; ACK : bool; PSH : bool; RST : bool; SYN : bool; FIN : bool; WindowSize : word 16; UrgentPointer : option (word 16); Options : list (word 32); Payload : { n : _ & ByteBuffer.t n }}.
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