Function sp_roundtrip_dps 

pub open spec fn sp_roundtrip_dps<T>(
    parser: ParserFnSpec<T>,
    consistent: PredFnSpec<T>,
    byte_len: ByteLenFnSpec<T>,
    serializer_dps: SerializerDPSFnSpec<T>,
) -> bool

{
    forall |v: T, obuf: Seq<u8>| {
        consistent(v)
            ==> #[trigger] parser(serializer_dps(v, obuf))
                == Some((byte_len(v) as int, v))
    }
}

Functional version of SPRoundTripDps for parser/serializer callback bundles.