Function lemma_exact_len_serializer_congruence

Source

pub broadcast proof fn lemma_exact_len_serializer_congruence<A, B, L1, L2>(
    a: ExactLen<A, L1>,
    b: ExactLen<B, L2>,
)where
    A: Consistency + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    L1: AsLen,
    L2: AsLen,

Expand description

requires

serializer_congruent(a.1, b.1),

a.0.as_nat() == b.0.as_nat(),

ensures

#[trigger] serializer_congruent(a, b),

lemma_exact_len_serializer_congruence

Function lemma_exact_len_serializer_congruence Copy item path

Function lemma_exact_len_serializer_congruence