Skip to main content

lemma_bits_serializer_congruence

vest_lib::combinators::congruence

Function lemma_bits_serializer_congruence 

Source 
pub broadcast proof fn lemma_bits_serializer_congruence<R1, R2, Tuple, Nominal>(
    a: Bits<R1, Tuple, Nominal>,
    b: Bits<R2, Tuple, Nominal>,
)
where
    R1: SpecByteLen + Consistency<Val = R1::T> + SpecSerializer<SVal = R1::T>,
    R2: SpecByteLen<T = R1::T> + Consistency<Val = R1::T> + SpecSerializer<SVal = R1::T>,
Expand description
requires
serializer_congruent(a.repr, b.repr),
a.unpack == b.unpack,
a.pack == b.pack,
a.refinement == b.refinement,
a.ctor == b.ctor,
a.dtor == b.dtor,
a.consistent == b.consistent,
ensures
#[trigger] serializer_congruent(a, b),