Function serializer_congruent 

pub open spec fn serializer_congruent<A, B>(a: A, b: B) -> bool
where
    A: Consistency + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,

{
    &&& prepare_congruent(a, b)
    &&& forall |v: A::Val| a.spec_serialize(v) == b.spec_serialize(v)

}

Equality of the full semantic interface used by executable serialization.