fact: Definition input_of_bytes (chn: chain) (bs: bytes) : option input := match ipv4_decode bs with | Some ip4 => let ip4_in := ipv4_input_pkt_of_pkt ip4 in match tcp_decode ip4 bs with | Some tcp => Some {| in_ip4 := ip4_in; in_tsp := TCPInput (tcp_input_pkt_of_pkt tcp); in_chn := chn |} | None => match udp_decode ip4 bs with | Some udp => Some {| in_ip4 := ip4_in; in_tsp := UDPInput (udp_input_pkt_of_pkt udp); in_chn := chn |} | None => None end end | None => None end.
imports: Coq.Lists.List Fiat.Narcissus.Examples.Guard.Core