fact: Definition make_tcp_syn_packet (src_addr dst_addr: word 32) (src_port dst_port: word 16) : option bytes := let ip_bs := AlignedByteString.initialize_Aligned_ByteString 20 in let tcp_bs := AlignedByteString.initialize_Aligned_ByteString 20 in match IPv4_encoder_impl ip_bs {| IPv4Header.TotalLength := natToWord _ (40); IPv4Header.ID := wzero _; IPv4Header.DF := false; IPv4Header.MF := false; IPv4Header.FragmentOffset := wzero _; IPv4Header.TTL := natToWord _ 8; IPv4Header.Protocol := ```"TCP"; IPv4Header.SourceAddress := src_addr; IPv4Header.DestAddress := dst_addr; IPv4Header.Options := [] |} with | None => None | Some (hdr, _, _) => match TCP_encoder_impl (ipv4ToByteBuffer src_addr) (ipv4ToByteBuffer dst_addr) (natToWord _ 20) {| SourcePort := natToWord _ 42; DestPort := natToWord _ 42; SeqNumber := wzero _; AckNumber := wzero _; NS := false; CWR := false; ECE := false; ACK := false; PSH := false; RST := false; SYN := true; FIN := false; WindowSize := natToWord _ 42; UrgentPointer := None; Options := []; Payload := existT _ 0 (AlignedByteString.initialize_Aligned_ByteString 0) |} tcp_bs with | None => None | Some (pkt, _, _) => Some (existT _ 40 (ByteBuffer.append hdr pkt)) end end.
imports: Fiat.QueryStructure.Automation.MasterPlan Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet ByteBuffer Fiat.Guard.TcpFilter QueryStructureNotations Narcissus.OCamlExtraction.Extraction Fiat.Common.EnumType Word