section‹Simple Packet› theory Simple_Packet imports "Primitives/L4_Protocol" begin text‹Packet constants are prefixed with ‹p›› text‹@{typ "'i::len word"} is an IP address of variable length. 32bit for IPv4, 128bit for IPv6› text‹A simple packet with IP addresses and layer four ports. Also has the following phantom fields: Input and Output network interfaces›