Function lemma_fn_serializer_specs 

pub proof fn lemma_fn_serializer_specs<Output, T, Spec, Exec>(
    serializer: &FnSerializer<Output, T, Spec, Exec>,
    value: T::V,
)
where
    Output: OutputBuf,
    T: DeepView + ?Sized,
    Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
    Exec: Fn(&T, &mut Output),

ensures

serializer.consistent(value) == serializer.spec_fn@.consistent(value),

serializer.byte_len(value) == serializer.spec_fn@.byte_len(value),

serializer.spec_serialize(value) == serializer.spec_fn@.spec_serialize(value),

Exposes the semantic specification bundled into an FnSerializer without requiring callers to unfold the adapter’s individual trait implementations.