Crate verdict_parser Copy item path Source pub use vec_deep;pub use vec_deep ;asn1 x509 asn1 Allows multiple definitions involving SEQUENCE, SEQUENCE OF, SET OF, and CHOICE asn1_choice Generate a combinator for an ASN.1 CHOICE asn1_sequence Generate a combinator for an ASN.1 SEQUENCE (with default or optional fields) asn1_sequence_of Generate a combinator for an ASN.1 SEQUENCE OF asn1_set_of Same as above, but for SET OF asn1_tagged Macro to generate a ASN1Tagged and ViewWithASN1Tagged trait impl gen_backward_body gen_choice_backward Given variants, generate if let branches to transform $src
to a nested Either term
if let variant1(p) = x {
inj_ord_choice_result!(…)
} else if let variant2(p) = x {
…
} … gen_choice_backward_branches gen_choice_forward Given variants, generate if let branches to transform $src
from a nested Either term to a specific variant gen_choice_forward_branches gen_choice_last_field_pat Generate inj_ord_choice_pat!(*, …, *, p) with |$variant| stars before p gen_field_poly_type gen_forward_body gen_inner_combinator gen_inner_combinator_poly_result_type gen_inner_combinator_type gen_inner_combinator_type!((optional, type1); (, type2); (default(v), type3)) gen_lemma_disjoint Macro to generate a lemma that states the disjointness of a list of spec terms
NOTE: the disjointness of the provided terms are trusted
incorrect calls to this might lead to unsoundness gen_lemma_disjoint_helper gen_match_continuation_apply gen_match_continuation_apply_helper gen_match_continuation_spec_apply gen_match_continuation_spec_apply_helper get_end_field inj_ord_choice_pat Same as above but for patterns inj_ord_choice_result Maps x:Ti to ord_choice_result!(T1, …, Tn) match_continuation Generate a continuation that matches the input
against a set of values and for each value,
the result is parsed with different a combinator
and stored in the suitable variant. oid Macro for constructing an OID oid_match_continuation Special case for matching against OIDs oid_name Map OID names to their values
NOTE: to add a new OID, add an entry here
and also in gen_oid_axioms below (if disjointness is required) ord_choice This macro constructs a nested OrdChoice combinator
in the form of OrdChoice(…, OrdChoice(…, OrdChoice(…, …))) ord_choice_result Build a type for the result of ord_choice! ord_choice_type Build a type for the ord_choice! macro spec_oid vec_deep AndThen Combinator that monadically chains two combinators. Base64 Base64 combinator (RFC 4648) Bytes Combinator for parsing and serializing a fixed number of bytes (dynamically known). BytesN Combinator for parsing and serializing a fixed number of bytes (statically known). Cached Same behavior as T, but also returns the slice
consumed by T in the exec version CachedValue Cond Combinator that checks if cond is true and then delegates to the inner combinator. Default Default(a, C1, C2) is similar to Optional(C1, C2)
except that if C1 is not matched, a is used in place
Conversely, if C1 exists, the value cannot be a. Depend Combinator that sequentially applies two combinators, where the second combinator depends on
the result of the first one. End A combinator that only matches the end of the buffer EndValue Fail Combinator used for custom error message IdentityMapper An identity mapper that does not change the parsed object
Used in situations when we need prove U: DisjointFrom<Mapped<…>>
in which case we can wrap U in Mapped and use existing impls Mapped Combinator that maps the result of an inner combinator with an isomorphism that implements
Iso Optional Essentially doing OrdChoice((C1, C2), C2),
but the result is mapped through
Left((A, B)) <-> (Some(A), B)
Right(B) <-> (None, B) OrdChoice Combinator that tries the Fst combinator and if it fails, tries the Snd combinator. Pair PairValue Preceded Combinator that sequentially applies two combinators and returns the result of the second one. Refined Combinator that refines the result of an inner combinator with a predicate that implements
Pred Repeat A combinator to repeatedly parse/serialize the inner combinator C
until the end of the buffer. SpecDepend Spec version of Depend Tag Generic tag combinator that matches the input with a given value and discards it
e.g. Tag(Int::<u8>, 0) matches the byte 0; Tag(Bytes::<3>, &[1, 2, 3]) matches the
bytes [1, 2, 3] TagPred tag predicate that matches the input with a given value Tail Combinator that returns the rest of the input bytes from the current position. TryMap Combinator that maps the result of an inner combinator with a faillible conversion
that implements TryFromInto U8 Combinator for parsing and serializing unsigned u8 integers. U16 Combinator for parsing and serializing unsigned u16 integers. U32 Combinator for parsing and serializing unsigned u32 integers. U64 Combinator for parsing and serializing unsigned u64 integers. Unreachable Similar to Fail, but without error message VecDeep A wrapper for Vec with its View implemented
one layer deeper than the original Vec Either Error Sum of both parse and serialize errors OptionDeep An Option type with “deep” View ParseError Parser errors SerializeError Serializer errors Combinator Implementation for parser and serializer combinators. A combinator’s view must be a
SecureSpecCombinator Compare A helper trait for two different types that can be compared. Continuation Use this Continuation trait instead of Fn(Input) -> Output
to avoid unsupported Verus features DisjointFrom A helper trait for OrdChoice From Vest equivalent of std::convert::From FromToBytes A trait for converting an integer type to and from a sequence of bytes. Into Vest equivalent of std::convert::Into Iso All isomorphisms to be used in MappedSelf::applySelf::rev_applySpecIso::spec_iso] and [SpecIso::spec_iso_rev] for more details. PolyfillClone A temporary replacement Clone PolyfillEq A temporary replacement Clone Pred All predicates to be used in Refined SecureSpecCombinator Theorems and lemmas that must be proven for a combinator to be considered correct and secure. SpecCombinator Specification for parser and serializer Combinator SpecFrom Spec version of From SpecInto Spec version of Into SpecIso Spec version of Iso SpecIsoFn Similar fix to https://github.com/secure-foundations/vest/issues/16 SpecPred The spec version of Pred SpecTryFrom Spec version of TryFrom SpecTryFromInto Spec version of TryFromInto SpecTryFromIntoFn Similar fix to https://github.com/secure-foundations/vest/issues/16 SpecTryInto Spec version of TryInto TryFrom Vest equivalent of std::convert::TryFrom TryFromInto Faillible version of Iso TryInto Vest equivalent of std::convert::TryInto ViewReflex Helper trait for types that have a reflexive view. compare_slice Helper function to compare two slices. decode_base64 Decodes a Base64-encoded sequence of bytes. init_vec_u8 Helper function to initialize a vector of u8 with zeros. new_wrapped parse_x509_der Parses the given bytes in ASN.1 DER format
to a x509::CertificateValue set_range Helper function to set a range of bytes in a vector. DefaultValue OptionalValue Wrapped Sometimes it is useful to wrap an existing combinator
within a Mapped combinator so that the SpecFrom trait
works better