fact: Definition dhcp_offer_input : input := must (input_of_bytes FORWARD (bytes_of_ByteBuffer dhcp_offer)).
imports: Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.Ports Coq.Vectors.Vector