Expand description
Disjointness proofs for complete ASN.1 formats. Compositional disjointness proofs for complete ASN.1 formats.
Each complete ASN.1 format exposes an over-approximation of
what can occur at the start of an accepted input, and one
generic theorem turns disjoint start domains into disjoint_domains.
Adding another ASN.1 format therefore needs one start-domain proof
rather than pairwise proofs against every existing format.
Structs§
- Asn1
Start Domain - A conservative FIRST certificate for an ASN.1 parser.
- Asn1
TagLead Mask - The 256 possible ASN.1 identifier leading octets, split into one 64-bit word per class.
Traits§
- HasAsn1
Start - Parsers whose accepted inputs have a compositional ASN.1 start-domain description.
Functions§
- asn1_
disjointness_ lemmas - asn1_
start_ any_ non_ eoc - asn1_
start_ ber_ boundary - asn1_
start_ empty - asn1_
start_ exact - asn1_
start_ exact_ uint - asn1_
start_ identity - asn1_
start_ identity_ uint - asn1_
start_ mask - asn1_
start_ union - asn1_
starts_ disjoint - empty_
tag_ lead_ mask - input_
starts_ with - lemma_
asn1_ start_ exact_ uint - lemma_
asn1_ start_ identity_ uint - lemma_
asn1_ starts_ disjoint_ exact - lemma_
asn1_ starts_ disjoint_ exact_ uint - lemma_
disjoint_ asn1_ starts - lemma_
disjoint_ defaulted - lemma_
input_ starts_ with_ union - lemma_
tag_ number_ roundtrip - tag_
lead_ bit - tag_
lead_ index - tag_
lead_ low - tag_
lead_ mask - tag_
lead_ mask_ contains - tag_
lead_ masks_ disjoint - tag_
lead_ masks_ union - tag_
leads_ distinct - tag_
leads_ distinct_ uint