vest_lib/asn1/
oid.rs

1//! ASN.1 OBJECT IDENTIFIER contents.
2//!
3//! The first two arcs are represented on the wire by the single subidentifier
4//! `40 * first + second`.  Importantly, that subidentifier is itself encoded using
5//! the same minimal base-128 form as every later arc; it is not restricted to one
6//! octet.
7use crate::combinators::{Pair, RepeatTillEnd};
8use crate::core::exec::output::OutputBuf;
9use crate::core::exec::{
10    parser::{PResult, Parser},
11    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
12    ParseError,
13};
14use crate::core::{proof::*, spec::*};
15use crate::primitives::base128::{Base128Fmt, UInt};
16#[cfg(feature = "alloc")]
17use alloc::vec::Vec;
18use vstd::prelude::*;
19
20use super::ObjectIdentifierFmt;
21
22verus! {
23
24pub type ObjectIdentifierInnerFmt = Pair<Base128Fmt<true>, RepeatTillEnd<Base128Fmt<true>>>;
25
26#[verifier::allow_in_spec]
27pub fn object_identifier_inner() -> (inner: ObjectIdentifierInnerFmt)
28    returns
29        Pair(Base128Fmt::<true>, RepeatTillEnd(Base128Fmt::<true>)),
30{
31    Pair(Base128Fmt::<true>, RepeatTillEnd(Base128Fmt::<true>))
32}
33
34/// Exact semantic representation of an OBJECT IDENTIFIER.
35#[verifier::ext_equal]
36pub struct ObjectIdentifierSpec {
37    pub first: UInt,
38    pub second: UInt,
39    pub rest: Seq<UInt>,
40}
41
42impl ObjectIdentifierSpec {
43    /// Structural restrictions imposed by X.690 §8.19, plus the finite `UInt` backend bound
44    /// on the combined first subidentifier.
45    pub open spec fn wf(&self) -> bool {
46        &&& self.first <= 2
47        &&& (self.first < 2 ==> self.second < 40)
48        &&& (self.first == 2 ==> self.second <= UInt::MAX - 80)
49    }
50}
51
52pub open spec fn oid_first_subidentifier(v: ObjectIdentifierSpec) -> UInt {
53    if !v.wf() {
54        0
55    } else if v.first < 2 {
56        (v.first * 40 + v.second) as UInt
57    } else {
58        (80 + v.second) as UInt
59    }
60}
61
62pub open spec fn oid_to_subidentifiers(v: ObjectIdentifierSpec) -> (UInt, Seq<UInt>) {
63    (oid_first_subidentifier(v), v.rest)
64}
65
66pub open spec fn oid_from_subidentifiers(
67    first_subidentifier: UInt,
68    rest: Seq<UInt>,
69) -> ObjectIdentifierSpec {
70    if first_subidentifier < 40 {
71        ObjectIdentifierSpec { first: 0, second: first_subidentifier, rest }
72    } else if first_subidentifier < 80 {
73        ObjectIdentifierSpec { first: 1, second: (first_subidentifier - 40u64) as UInt, rest }
74    } else {
75        ObjectIdentifierSpec { first: 2, second: (first_subidentifier - 80u64) as UInt, rest }
76    }
77}
78
79pub proof fn lemma_oid_from_subidentifiers_wf(first: UInt, rest: Seq<UInt>)
80    ensures
81        oid_from_subidentifiers(first, rest).wf(),
82{
83}
84
85pub proof fn lemma_oid_subidentifier_roundtrip(first: UInt, rest: Seq<UInt>)
86    ensures
87        oid_to_subidentifiers(oid_from_subidentifiers(first, rest)) == (first, rest),
88{
89    lemma_oid_from_subidentifiers_wf(first, rest);
90}
91
92pub proof fn lemma_oid_arcs_roundtrip(v: ObjectIdentifierSpec)
93    requires
94        v.wf(),
95    ensures
96        oid_from_subidentifiers(oid_first_subidentifier(v), v.rest) == v,
97{
98}
99
100mod derived_specs {
101    use super::*;
102
103    impl SpecParser for ObjectIdentifierFmt {
104        type PVal = ObjectIdentifierSpec;
105
106        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
107            match object_identifier_inner().spec_parse(ibuf) {
108                Some((n, (first, rest))) => Some((n, oid_from_subidentifiers(first, rest))),
109                None => None,
110            }
111        }
112    }
113
114    impl Consistency for ObjectIdentifierFmt {
115        type Val = ObjectIdentifierSpec;
116
117        open spec fn consistent(&self, v: Self::Val) -> bool {
118            v.wf() && object_identifier_inner().consistent(oid_to_subidentifiers(v))
119        }
120    }
121
122    impl SpecSerializerDps for ObjectIdentifierFmt {
123        type SValue = ObjectIdentifierSpec;
124
125        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
126            object_identifier_inner().spec_serialize_dps(oid_to_subidentifiers(v), obuf)
127        }
128    }
129
130    impl SpecSerializer for ObjectIdentifierFmt {
131        type SVal = ObjectIdentifierSpec;
132
133        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
134            object_identifier_inner().spec_serialize(oid_to_subidentifiers(v))
135        }
136    }
137
138    impl SpecByteLen for ObjectIdentifierFmt {
139        type T = ObjectIdentifierSpec;
140
141        open spec fn byte_len(&self, v: Self::T) -> nat {
142            object_identifier_inner().byte_len(oid_to_subidentifiers(v))
143        }
144    }
145
146}
147
148mod derived_proofs {
149    use super::*;
150
151    impl SafeParser for ObjectIdentifierFmt {
152        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
153            object_identifier_inner().lemma_parse_safe(ibuf);
154        }
155    }
156
157    impl Productive for ObjectIdentifierFmt {
158        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
159            object_identifier_inner().lemma_productive(ibuf);
160        }
161    }
162
163    impl SoundParser for ObjectIdentifierFmt {
164        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
165            let inner = object_identifier_inner();
166            inner.lemma_parse_sound_consumption(ibuf);
167            if let Some((_, (first, rest))) = inner.spec_parse(ibuf) {
168                lemma_oid_subidentifier_roundtrip(first, rest);
169            }
170        }
171
172        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
173            let inner = object_identifier_inner();
174            inner.lemma_parse_sound_value(ibuf);
175            if let Some((_, (first, rest))) = inner.spec_parse(ibuf) {
176                lemma_oid_from_subidentifiers_wf(first, rest);
177                lemma_oid_subidentifier_roundtrip(first, rest);
178            }
179        }
180    }
181
182    impl GoodSerializer for ObjectIdentifierFmt {
183        proof fn lemma_serialize_len(&self, v: Self::SVal) {
184            object_identifier_inner().lemma_serialize_len(oid_to_subidentifiers(v));
185        }
186    }
187
188    impl SPRoundTripDps for ObjectIdentifierFmt {
189        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
190            let inner = object_identifier_inner();
191            lemma_oid_arcs_roundtrip(v);
192            inner.theorem_serialize_dps_parse_roundtrip(oid_to_subidentifiers(v), obuf);
193        }
194    }
195
196    impl NonMalleable for ObjectIdentifierFmt {
197        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
198            let inner = object_identifier_inner();
199            if let Some((_, (first1, rest1))) = inner.spec_parse(buf1) {
200                if let Some((_, (first2, rest2))) = inner.spec_parse(buf2) {
201                    lemma_oid_subidentifier_roundtrip(first1, rest1);
202                    lemma_oid_subidentifier_roundtrip(first2, rest2);
203                    inner.lemma_parse_non_malleable(buf1, buf2);
204                }
205            }
206        }
207    }
208
209    impl EquivSerializers for ObjectIdentifierFmt {
210        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
211            object_identifier_inner().lemma_serialize_equiv_on_empty(oid_to_subidentifiers(v));
212        }
213    }
214
215}
216
217/// Executable OBJECT IDENTIFIER value.
218///
219/// Keeping the first two arcs separate avoids a second allocation when parsing: the
220/// remaining subidentifiers are already produced as one `Vec` by `RepeatTillEnd`.
221#[cfg(feature = "alloc")]
222pub struct ObjectIdentifier {
223    first: UInt,
224    second: UInt,
225    rest: Vec<UInt>,
226}
227
228#[cfg(feature = "alloc")]
229impl DeepView for ObjectIdentifier {
230    type V = ObjectIdentifierSpec;
231
232    closed spec fn deep_view(&self) -> Self::V {
233        ObjectIdentifierSpec { first: self.first, second: self.second, rest: self.rest.deep_view() }
234    }
235}
236
237#[cfg(feature = "alloc")]
238impl ObjectIdentifier {
239    pub fn new(first: UInt, second: UInt, rest: Vec<UInt>) -> Self {
240        Self { first, second, rest }
241    }
242
243    pub fn first(&self) -> (first: UInt)
244        ensures
245            first == self.deep_view().first,
246    {
247        self.first
248    }
249
250    pub fn second(&self) -> (second: UInt)
251        ensures
252            second == self.deep_view().second,
253    {
254        self.second
255    }
256
257    pub fn rest(&self) -> &[UInt] {
258        self.rest.as_slice()
259    }
260
261    pub(crate) fn rest_vec(&self) -> (rest: &Vec<UInt>)
262        ensures
263            rest.deep_view() == self.deep_view().rest,
264    {
265        &self.rest
266    }
267
268    pub(crate) fn combined_first_subidentifier(&self) -> (combined: UInt)
269        ensures
270            combined == oid_first_subidentifier(self.deep_view()),
271    {
272        oid_first_subidentifier_exec(self.first, self.second)
273    }
274}
275
276pub(crate) fn oid_first_subidentifier_exec(first: UInt, second: UInt) -> (combined: UInt)
277    ensures
278        combined == oid_first_subidentifier(
279            ObjectIdentifierSpec { first, second, rest: Seq::empty() },
280        ),
281{
282    if first > 2 || (first < 2 && second >= 40) || (first == 2 && second > UInt::MAX - 80) {
283        0
284    } else if first < 2 {
285        first * 40 + second
286    } else {
287        80 + second
288    }
289}
290
291#[cfg(feature = "alloc")]
292impl Parser<&[u8]> for ObjectIdentifierFmt {
293    type PT = ObjectIdentifier;
294
295    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
296        let (n, (first_subidentifier, rest)) = object_identifier_inner().parse(ibuf)?;
297        let (first, second) = if first_subidentifier < 40 {
298            (0, first_subidentifier)
299        } else if first_subidentifier < 80 {
300            (1, first_subidentifier - 40)
301        } else {
302            (2, first_subidentifier - 80)
303        };
304        proof {
305            lemma_oid_from_subidentifiers_wf(first_subidentifier, rest.deep_view());
306        }
307        Ok((n, ObjectIdentifier { first, second, rest }))
308    }
309}
310
311#[cfg(feature = "alloc")]
312impl<Output: OutputBuf> Serializer<Output, ObjectIdentifier> for ObjectIdentifierFmt {
313    fn serialize_into(&self, v: &ObjectIdentifier, obuf: &mut Output) {
314        let ghost vv = v.deep_view();
315        let combined = oid_first_subidentifier_exec(v.first, v.second);
316        let rest = v.rest.as_slice();
317        let pair = (combined, rest);
318        object_identifier_inner().serialize_into(&pair, obuf);
319    }
320}
321
322#[cfg(feature = "alloc")]
323impl Prepare<ObjectIdentifier> for ObjectIdentifierFmt {
324    fn prepare(&self, v: &ObjectIdentifier) -> Result<usize, PreSerializeError> {
325        if v.first > 2 {
326            return Err(PreSerializeError::custom("OBJECT IDENTIFIER first arc exceeds 2"));
327        }
328        if v.first < 2 && v.second >= 40 {
329            return Err(
330                PreSerializeError::custom(
331                    "OBJECT IDENTIFIER second arc exceeds 39 for first arc 0 or 1",
332                ),
333            );
334        }
335        if v.first == 2 && v.second > UInt::MAX - 80 {
336            return Err(PreSerializeError::length_too_large());
337        }
338        let combined = oid_first_subidentifier_exec(v.first, v.second);
339        let rest = v.rest.as_slice();
340        let pair = (combined, rest);
341        let len = object_identifier_inner().prepare(&pair)?;
342        Ok(len)
343    }
344}
345
346#[cfg(feature = "alloc")]
347impl ByteLen<ObjectIdentifier> for ObjectIdentifierFmt {
348    fn length(&self, v: &ObjectIdentifier) -> usize {
349        let combined = oid_first_subidentifier_exec(v.first, v.second);
350        let rest = v.rest.as_slice();
351        let pair = (combined, rest);
352        object_identifier_inner().length(&pair)
353    }
354}
355
356} // verus!
357#[cfg(all(test, feature = "alloc"))]
358mod tests {
359    use super::*;
360    use crate::asn1::der::OBJECT_IDENTIFIER;
361    use crate::core::exec::{Parser, Prepare, SerializerExt};
362
363    #[test]
364    fn oid_roundtrips_multibyte_first_subidentifier() {
365        let input = [0x06, 0x03, 0x88, 0x37, 0x03]; // 2.999.3
366        let (_, value) = OBJECT_IDENTIFIER.parse(&&input[..]).unwrap();
367        assert_eq!(value.first(), 2);
368        assert_eq!(value.second(), 999);
369        assert_eq!(value.rest(), &[3]);
370
371        let mut output = vec![0; OBJECT_IDENTIFIER.prepare(&value).unwrap()];
372        OBJECT_IDENTIFIER.serialize(&value, &mut output);
373        assert_eq!(output, input);
374    }
375
376    #[test]
377    fn oid_rejects_nonminimal_subidentifier() {
378        let input = [0x06, 0x02, 0x80, 0x2a];
379        assert!(OBJECT_IDENTIFIER.parse(&&input[..]).is_err());
380    }
381}
vest_lib/asn1/oid.rs

vest_lib/asn1/
oid.rs
