Trait HasAsn1Start 

pub trait HasAsn1Start: SpecParser {
    // Required methods
    spec fn asn1_start(&self) -> Asn1StartDomain;
    proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>);
}

Parsers whose accepted inputs have a compositional ASN.1 start-domain description.

Required Methods

spec fn asn1_start(&self) -> Asn1StartDomain

proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>)

ensures

self.spec_parse(input) is Some ==> input_starts_with(input, self.asn1_start()),

Implementors

impl HasAsn1Start for Const<TagFmt, Tag>

A constant ASN.1 tag has the exact start domain of its required tag value.

impl HasAsn1Start for Eof

EOF accepts only the empty input.

impl HasAsn1Start for BerEndFmt

BER_END recognizes either EOF or an EOC prefix without consuming it.

impl<Content: SpecCombinator> HasAsn1Start for BerSequenceFmt<Content>

BER SEQUENCE has one exact, necessarily constructed outer tag.

impl<Content: SpecCombinator> HasAsn1Start for BerSequenceOfFmt<Content>

BER SEQUENCE OF has one exact, necessarily constructed outer tag.

impl<Content: SpecCombinator, const DER: bool> HasAsn1Start for ASN1Fmt<Content, DER>

Ordinary definite-length TLVs have one exact outer tag.

impl<Content: SpecCombinator, const LIMIT: usize> HasAsn1Start for BerCharStringFmt<Content, LIMIT>

BER restricted character strings inherit the primitive/constructed identity of their underlying recursive OCTET STRING.

impl<Field, Rest, const DER: bool> HasAsn1Start for DefaultedFmt<Field, Field::PVal, Rest, DER>

where Field: SpecByteLen + HasAsn1Start<PVal = Field::T>, Rest: SpecByteLen + HasAsn1Start<PVal = Rest::T>,

ASN.1 DEFAULT has the same possible starts as OPTIONAL: the field or its continuation.

impl<Field: HasAsn1Start, Rest: HasAsn1Start> HasAsn1Start for Optional<Field, Rest>

An optional field starts with either the present field or its continuation.

impl<Format> HasAsn1Start for ImplicitlyTaggedFmt<Format>

where Format: Retaggable + HasAsn1Start,

IMPLICIT tagging delegates parsing and its start domain to the concretely retagged format.

impl<Inner, Mapper> HasAsn1Start for Mapped<Inner, Mapper>

where Inner: HasAsn1Start, Mapper: SpecMapper<In = Inner::PVal>,

Semantic mapping does not change the accepted byte domain.

impl<Inner, Mapper, Reverse> HasAsn1Start for Mapped<Inner, BiMap<Mapper, Reverse>>

where Inner: HasAsn1Start, Mapper: SpecMap<Input = Inner::PVal>, Reverse: SpecMap<Input = Mapper::Output, Output = Mapper::Input>,

BiMap mapping does not change the accepted byte domain.

impl<Inner: HasAsn1Start> HasAsn1Start for Named<Inner>

Diagnostic naming does not change the accepted byte domain.

impl<Inner: HasAsn1Start> HasAsn1Start for Ref<Inner>

Borrowing adaptation does not change the accepted byte domain.

impl<Inner: HasAsn1Start, Predicate: SpecPred<Inner::PVal>> HasAsn1Start for Refined<Inner, Predicate>

Refinement can only narrow an accepted input domain.

impl<Left: HasAsn1Start, Right: SpecParser> HasAsn1Start for Pair<Left, Right>

A required pair starts wherever its required left component starts.

impl<Left: HasAsn1Start, Right: HasAsn1Start> HasAsn1Start for Choice<Left, Right>

A structural choice accepts the union of the starts accepted by either branch.

impl<const DER: bool> HasAsn1Start for AnyFmt<DER>

Definite-length ANY accepts every complete tag except EOC.

impl<const LIMIT: usize> HasAsn1Start for BerAnyFmt<LIMIT>

Recursive BER ANY accepts every complete tag except EOC.

impl<const LIMIT: usize> HasAsn1Start for BerBitStringFmt<LIMIT>

Recursive BER BIT STRING accepts primitive and constructed forms of one tag identity.

impl<const LIMIT: usize> HasAsn1Start for BerOctetStringFmt<LIMIT>

Recursive BER OCTET STRING accepts primitive and constructed forms of one tag identity.

impl<const NONDETERMINISTIC: bool, Left: HasAsn1Start, Right: HasAsn1Start<PVal = Left::PVal>> HasAsn1Start for Alt<Left, Right, NONDETERMINISTIC>

Ordered alternatives have the same accepted start union as structural choices.