Skip to main content

lemma_preceded_serializer_congruence

vest_lib::combinators::congruence

Function lemma_preceded_serializer_congruence 

Source 
pub broadcast proof fn lemma_preceded_serializer_congruence<A1, A2, B1, B2, const CHECK: bool>(
    a: Preceded<A1, A1::Val, B1, CHECK>,
    b: Preceded<A2, A1::Val, B2, CHECK>,
)
where
    A1: Consistency + SpecByteLen<T = A1::Val> + SpecSerializer<SVal = A1::Val>,
    A2: Consistency<Val = A1::Val> + SpecByteLen<T = A1::Val> + SpecSerializer<SVal = A1::Val>,
    B1: Consistency + SpecByteLen<T = B1::Val> + SpecSerializer<SVal = B1::Val>,
    B2: Consistency<Val = B1::Val> + SpecByteLen<T = B1::Val> + SpecSerializer<SVal = B1::Val>,
Expand description
requires
serializer_congruent(a.a, b.a),
serializer_congruent(a.b, b.b),
a.a_val == b.a_val,
ensures
#[trigger] serializer_congruent(a, b),