fact: Definition deserialize_packet (p : @packet _ serialized_multi_params) : option (@packet _ orig_multi_params) := match deserialize_top deserialize (pBody p) with | None => None | Some body => Some (@mkPacket _ orig_multi_params (pSrc p) (pDst p) body) end.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)