fact: Definition WrapEncoder {A B} sz (impl: forall {sz}, ByteBuffer.t sz -> A -> option (ByteBuffer.t sz * nat * B)) (pkt: A) (out: ByteBuffer.t sz) : option (ByteBuffer.t sz) := match impl out pkt with | Some (out, _, _) => Some out | None => None end.
imports: Bedrock.Word Fiat.Narcissus.Examples.NetworkStack.EthernetHeader Fiat.Narcissus.Examples.NetworkStack.ARPPacket Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Fiat.Narcissus.Examples.NetworkStack.UDP_Packet AlignedByteString