Function prepare_congruent 

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

{
    &&& forall |v: A::Val| a.consistent(v) <==> b.consistent(v)
    &&& forall |v: A::Val| a.byte_len(v) == b.byte_len(v)

}

Equality of the two semantic components used by executable preparation.