vest_lib/asn1/
mod.rs

1#![allow(non_upper_case_globals)]
2
3//! Verified ASN.1 contents, tag-length-value wrappers, and schema combinators.
4//!
5//! [`der`] exposes notation-like constants and modifiers for canonical DER.
6//! [`ber`] provides specialized formats for BER alternatives such as
7//! constructed strings and indefinite-length containers. Shared modules define
8//! contents formats, tags, constraints, retagging, disjointness certificates,
9//! and allocation-free DER ordering.
10//!
11//! The [`vest_asn1` frontend guide](https://secure-foundations.github.io/vest/guide/asn1/)
12//! describes schema generation and the supported ASN.1 subset. Direct backend
13//! users should start with [`der`] or [`ber`] rather than assembling raw TLVs.
14
15/// ASN.1 ANY / open-type complete TLV format.
16pub mod any;
17/// BER indefinite-length and constructed-value combinators.
18pub mod ber;
19/// ASN.1 BIT STRING contents octets.
20pub mod bitstring;
21/// ASN.1 BMPString contents.
22pub mod bmpstring;
23/// ASN.1 BOOLEAN contents octet.
24pub mod boolean;
25/// Reusable ASN.1 subtype-constraint predicates.
26pub mod constraints;
27/// Shared semantic date/time values and calendar operations.
28pub mod datetime;
29/// ASN.1 notation-style aliases for universal formats with DER encoding.
30pub mod der;
31/// Allocation-free ordering of values by their DER encodings.
32pub mod der_ord;
33/// Disjointness proofs for complete ASN.1 formats.
34pub mod disjoint;
35/// ASN.1 ENUMERATED contents octets.
36pub mod enumerated;
37/// ASN.1 GeneralizedTime contents.
38pub mod generalizedtime;
39/// ASN.1 IA5String contents.
40pub mod ia5string;
41/// ASN.1 INTEGER contents octets.
42pub mod integer;
43/// ASN.1 definite length octets.
44pub mod length;
45/// Macros for implementing verified nominal ASN.1 formats.
46pub mod macros;
47/// Shared ASN.1 tagging and component modifiers.
48pub mod modifiers;
49/// ASN.1 NumericString contents.
50pub mod numericstring;
51/// ASN.1 OBJECT IDENTIFIER contents octets.
52pub mod oid;
53/// ASN.1 PrintableString contents.
54pub mod printablestring;
55/// ASN.1 REAL contents octets.
56pub mod real;
57/// ASN.1 DER SET OF contents.
58pub mod set_of;
59/// ASN.1 tag octets.
60pub mod tag;
61/// ASN.1 TeletexString contents.
62pub mod teletexstring;
63/// ASN.1 TLV wrapper.
64pub mod tlv;
65/// ASN.1 UniversalString contents.
66pub mod universalstring;
67/// ASN.1 UTCTime contents.
68pub mod utctime;
69/// ASN.1 UTF8String contents.
70pub mod utf8string;
71
72#[cfg(feature = "alloc")]
73pub use any::AnyOwned;
74pub use any::{Any, AnySpec};
75pub use ber::{
76    BerAnyFmt, BerBitStringFmt, BerBmpStringFmt, BerCharStringFmt, BerIa5StringFmt,
77    BerOctetStringFmt, BerPrintableStringFmt, BerSequenceFmt, BerSequenceOfFmt,
78    BerTeletexStringFmt, BerUtf8StringFmt, EocFmt, EOC,
79};
80#[cfg(feature = "alloc")]
81pub use bitstring::BitStringOwned;
82pub use bitstring::{BitString, BitStringSpec};
83#[cfg(feature = "alloc")]
84pub use bmpstring::BmpString;
85pub use bmpstring::BmpStringSpec;
86pub use constraints::{ConstraintAnd, ConstraintNot, ConstraintOr, IntegerRange, Size};
87pub use datetime::{DateTime, TimePrecision, TimeZone};
88pub use der::*;
89pub use der_ord::{DeepViewIdentity, DerOrd};
90pub use enumerated::Enumerated;
91pub use generalizedtime::{GeneralizedTime, GeneralizedTimeSpec};
92#[cfg(feature = "alloc")]
93pub use ia5string::Ia5StringOwned;
94pub use ia5string::{Ia5String, Ia5StringSpec};
95pub use integer::{Integer, Integer16Fmt, Integer8Fmt};
96pub use modifiers::{DefaultedFmt, ImplicitlyTaggedFmt, Retaggable};
97#[cfg(feature = "alloc")]
98pub use numericstring::NumericStringOwned;
99pub use numericstring::{NumericString, NumericStringFmt, NumericStringSpec};
100#[cfg(feature = "alloc")]
101pub use oid::ObjectIdentifier;
102pub use oid::ObjectIdentifierSpec;
103#[cfg(feature = "alloc")]
104pub use printablestring::PrintableStringOwned;
105pub use printablestring::{PrintableString, PrintableStringSpec};
106pub use real::{Real, RealSpec};
107pub use set_of::SetOfFmt;
108pub use tag::{constructed_tag, primitive_tag, Class, Tag};
109#[cfg(feature = "alloc")]
110pub use teletexstring::TeletexStringOwned;
111pub use teletexstring::{TeletexString, TeletexStringSpec};
112#[cfg(feature = "alloc")]
113pub use universalstring::UniversalString;
114pub use universalstring::UniversalStringSpec;
115pub use utctime::UtcTime;
116pub use utf8string::Utf8String;
117#[cfg(feature = "alloc")]
118pub use utf8string::Utf8StringOwned;
119
120use crate::{
121    combinators::{
122        implicit::NBytesOf, mapped::spec::FnSpecMapper, Const, Empty, PrefixTagged, Tail, TryMap,
123        U8,
124    },
125    core::proof::{Leaf, LeafNonMalleable},
126};
127use vstd::prelude::*;
128
129verus! {
130
131pub const DER: bool = true;
132
133pub const BER: bool = false;
134
135#[derive(Copy)]
136pub struct ASN1Fmt<Content, const DER: bool = true>(pub Tag, pub Content);
137
138impl<Content: Clone, const DER: bool> Clone for ASN1Fmt<Content, DER> {
139    fn clone(&self) -> (cloned: Self)
140        ensures
141            call_ensures(Content::clone, (&self.1,), cloned.1),
142    {
143        ASN1Fmt(self.0, self.1.clone())
144    }
145}
146
147/// ASN.1 BOOLEAN format.
148///
149/// When `DER = true` (the default), this is the canonical DER form:
150/// FALSE = `0x00`, TRUE = `0xFF`.
151///
152/// When `DER = false`, this is the more permissive BER form:
153/// FALSE = `0x00`, TRUE = any non-zero byte.
154#[derive(Clone, Copy)]
155pub struct BoolFmt<const DER: bool = true>;
156
157/// Convenience type alias for the BER variant of ASN.1 BOOLEAN.
158pub type BerBoolFmt = BoolFmt<false>;
159
160/// Convenience type alias for the DER variant of ASN.1 BOOLEAN.
161pub type DerBoolFmt = BoolFmt<true>;
162
163/// Convenience value alias for the BER variant of ASN.1 BOOLEAN.
164pub const BerBoolFmt: BoolFmt<false> = BoolFmt;
165
166/// Convenience value alias for the DER variant of ASN.1 BOOLEAN.
167pub const DerBoolFmt: BoolFmt<true> = BoolFmt;
168
169/// ASN.1 ANY/open-type format.
170///
171/// Unlike the content markers in this module, `AnyFmt` parses and serializes one complete
172/// tag-length-value encoding.
173#[derive(Clone, Copy)]
174pub struct AnyFmt<const DER: bool = true>;
175
176/// Definite-length-only BER ANY format.
177///
178/// Prefer [`ber::BerAnyFmt`] when indefinite constructed open values must be accepted.
179pub type BerDefiniteAnyFmt = AnyFmt<false>;
180
181pub type DerAnyFmt = AnyFmt<true>;
182
183pub const BerDefiniteAnyFmt: BerDefiniteAnyFmt = AnyFmt;
184
185pub const DerAnyFmt: DerAnyFmt = AnyFmt;
186
187/// ASN.1 definite length format whose codomain is `nat`
188#[derive(Clone, Copy)]
189pub struct NatLengthFmt<const DER: bool = true>;
190
191/// ASN.1 definite length format.
192///
193/// When `DER = true` (the default), only the canonical DER definite form is
194/// accepted/produced.
195///
196/// When `DER = false`, the parser/serializer is BER-permissive over short and long
197/// definite forms, without minimality constraints.
198#[derive(Clone, Copy)]
199pub struct LengthFmt<const DER: bool = true>;
200
201/// BER length, including the indefinite form (`0x80`).
202#[derive(StructuralEq, Copy, Clone, PartialEq, Eq, Debug)]
203pub enum BerLength {
204    Definite(usize),
205    Indefinite,
206}
207
208impl DeepView for BerLength {
209    type V = Self;
210
211    open spec fn deep_view(&self) -> Self::V {
212        *self
213    }
214}
215
216/// BER length determinant accepting both definite and indefinite encodings.
217#[derive(Clone, Copy)]
218pub struct BerLengthFmt;
219
220/// ASN.1 INTEGER contents format.
221#[derive(Clone, Copy)]
222pub struct IntegerFmt;
223
224/// ASN.1 ENUMERATED contents format.
225#[derive(Clone, Copy)]
226pub struct EnumeratedFmt;
227
228/// ASN.1 OBJECT IDENTIFIER contents format.
229#[derive(Clone, Copy)]
230pub struct ObjectIdentifierFmt;
231
232/// ASN.1 REAL contents format.
233///
234/// `DER = true` accepts only the canonical DER forms. `DER = false` accepts the
235/// additional binary and ISO 6093 decimal forms permitted by BER.
236#[derive(Clone, Copy)]
237pub struct RealFmt<const DER: bool = true>;
238
239/// ASN.1 BIT STRING contents format.
240///
241/// When `DER = true` (the default), only the canonical DER form is accepted, which requires
242/// the trailing unused bits to be zero.
243///
244/// When `DER = false`, the parser allows any value for the trailing unused bits.
245#[derive(Clone, Copy)]
246pub struct BitStringFmt<const DER: bool = true>;
247
248/// Convenience type alias for primitive BER BIT STRING contents.
249pub type BerBitStringContentFmt = BitStringFmt<false>;
250
251/// ASN.1 tag format combinator.
252///
253/// Only the canonical DER form is accepted:
254/// - Tag numbers 0–30 must use the short (1-byte) form.
255/// - High tag numbers must have no leading zero in the base-128 encoding.
256#[derive(Clone, Copy)]
257pub struct TagFmt;
258
259/// Convenience type alias for the DER variant of ASN.1 BIT STRING.
260pub type DerBitStringFmt = BitStringFmt<true>;
261
262/// ASN.1 OCTET STRING contents format (primitive).
263///
264/// This content format intentionally handles only primitive bytes. Recursive
265/// constructed BER OCTET STRINGs are provided by
266/// [`ber::BerOctetStringFmt`].
267/// For example, a constructed encoding may have the following shape:
268///
269/// ### Example
270///
271/// 24 80 04 03 42 45 52 24 80 04 01 2D 04 05 52 55 4C 45 53 00 00 00 00
272/// │  │  │  │  └───────┘ │  │  │  │  │  │  │  └──────────────┘ │     │
273/// │  │  │  │  "BER"     │  │  │  │  │  │  └─ Len: 5 "RULES"   │     └─ Outer EOC
274/// │  │  │  └─ Len: 3    │  │  │  │  │  └─ Primitive           └─ Inner EOC
275/// │  │  └─ Primitive    │  │  │  │  └─ "-"
276/// │  └─ Indefinite      │  │  │  └─ Len: 1
277/// └─ Outer Outer        │  │  └─ Primitive
278///                       │  └─ Indefinite
279///                       └─ Inner Constructed
280///
281/// [TAG: 24] Constructed OCTET STRING (Indefinite Length)
282///  │
283///  ├── [TAG: 04] Primitive OCTET STRING (Definite Length: 3)
284///  │      └── Value: "BER" (Hex: 42 45 52)
285///  │
286///  ├── [TAG: 24] Constructed OCTET STRING (Indefinite Length)
287///  │      │
288///  │      ├── [TAG: 04] Primitive OCTET STRING (Definite Length: 1)
289///  │      │      └── Value: "-" (Hex: 2D)
290///  │      │
291///  │      ├── [TAG: 04] Primitive OCTET STRING (Definite Length: 5)
292///  │      │      └── Value: "RULES" (Hex: 52 55 4C 45 53)
293///  │      │
294///  │      └── [TAG: 00] End-of-Contents (EOC) Marker (Hex: 00 00)
295///  │             └── Meaning: Closes the Inner Constructed String
296///  │
297///  └── [TAG: 00] End-of-Contents (EOC) Marker (Hex: 00 00)
298///         └── Meaning: Closes the Outer Constructed String
299pub type OctetStringFmt = Tail;
300
301/// Convenience value alias for ASN.1 OCTET STRING contents format.
302pub const OctetStringFmt: Tail = Tail;
303
304/// ASN.1 NULL format.
305pub type NullFmt = Empty;
306
307/// Convenience value alias for ASN.1 NULL format.
308pub const NullFmt: Empty = Empty;
309
310/// ASN.1 UTCTime format.
311#[derive(Clone, Copy)]
312pub struct UtcTimeFmt<const DER: bool = true>;
313
314pub type BerUtcTimeFmt = UtcTimeFmt<false>;
315
316pub type DerUtcTimeFmt = UtcTimeFmt<true>;
317
318pub const BerUtcTimeFmt: BerUtcTimeFmt = UtcTimeFmt;
319
320pub const DerUtcTimeFmt: DerUtcTimeFmt = UtcTimeFmt;
321
322/// ASN.1 UTF8String format.
323#[derive(Clone, Copy)]
324pub struct Utf8StringFmt;
325
326/// ASN.1 PrintableString format.
327#[derive(Clone, Copy)]
328pub struct PrintableStringFmt;
329
330/// ASN.1 IA5String format.
331#[derive(Clone, Copy)]
332pub struct Ia5StringFmt;
333
334/// ASN.1 BMPString format.
335#[derive(Clone, Copy)]
336pub struct BmpStringFmt;
337
338/// ASN.1 TeletexString format.
339#[derive(Clone, Copy)]
340pub struct TeletexStringFmt;
341
342/// ASN.1 UniversalString format.
343#[derive(Clone, Copy)]
344pub struct UniversalStringFmt;
345
346/// ASN.1 GeneralizedTime format.
347#[derive(Clone, Copy)]
348pub struct GeneralizedTimeFmt<const DER: bool = true>;
349
350pub type BerGeneralizedTimeFmt = GeneralizedTimeFmt<false>;
351
352pub type DerGeneralizedTimeFmt = GeneralizedTimeFmt<true>;
353
354pub const BerGeneralizedTimeFmt: BerGeneralizedTimeFmt = GeneralizedTimeFmt;
355
356pub const DerGeneralizedTimeFmt: DerGeneralizedTimeFmt = GeneralizedTimeFmt;
357
358impl LeafNonMalleable for DerBoolFmt {
359    proof fn nonmal_leaf_inv(&self) {
360    }
361}
362
363impl Leaf for BerBoolFmt {
364    proof fn leaf_inv(&self) {
365    }
366}
367
368// impl LeafNonMalleable for DerLengthFmt {
369//     proof fn nonmal_leaf_inv(&self) {
370//     }
371// }
372// impl Leaf for BerLengthFmt {
373//     proof fn leaf_inv(&self) {
374//     }
375// }
376} // verus!
vest_lib/asn1/mod.rs

vest_lib/asn1/
mod.rs
