Skip to main content

lemma_and_then_serializer_congruence

vest_lib::combinators::congruence

Function lemma_and_then_serializer_congruence 

Source 
pub broadcast proof fn lemma_and_then_serializer_congruence<A1, A2, B1, B2>(
    a: AndThen<A1, B1>,
    b: AndThen<A2, B2>,
)
where
    A1: BytesCombinator + Consistency<Val = Seq<u8>> + SpecSerializer<SVal = Seq<u8>>,
    A2: BytesCombinator + Consistency<Val = Seq<u8>> + SpecSerializer<SVal = Seq<u8>>,
    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.0, b.0),
serializer_congruent(a.1, b.1),
ensures
#[trigger] serializer_congruent(a, b),