Function lemma_bits_parser_congruence

Source

pub broadcast proof fn lemma_bits_parser_congruence<R1, R2, Tuple, Nominal>(
    a: Bits<R1, Tuple, Nominal>,
    b: Bits<R2, Tuple, Nominal>,
)where
    R1: SpecByteLen + SpecParser<PVal = R1::T>,
    R2: SpecByteLen<T = R1::T> + SpecParser<PVal = R1::T>,

Expand description

requires

parser_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] parser_congruent(a, b),

lemma_bits_parser_congruence

Function lemma_bits_parser_congruence Copy item path

Function lemma_bits_parser_congruence