Skip to main content

lemma_disjoint_defaulted

vest_lib::asn1::disjoint

Function lemma_disjoint_defaulted 

Source 
pub broadcast proof fn lemma_disjoint_defaulted<Parser, Field, Rest, const DER: bool>(
    parser: Parser,
    defaulted: DefaultedFmt<Field, Field::PVal, Rest, DER>,
)
where
    Parser: SpecParser,
    Field: SpecByteLen + SpecParser<PVal = Field::T>,
    Rest: SpecByteLen + SpecParser<PVal = Rest::T>,
Expand description
requires
disjoint_domains(parser, defaulted.0),
disjoint_domains(parser, defaulted.2),
ensures
#[trigger] disjoint_domains(parser, defaulted),

A defaulted field can start either at the field itself or at its continuation.

This structural rule complements the bitmap leaf rule: it lets ordinary combinator automation reduce a DEFAULT chain without asking the SMT solver to evaluate bitwise operations itself.