vest_lib/asn1/
enumerated.rs

1//! ASN.1 ENUMERATED contents.
2//!
3//! X.690 §8.4 specifies that ENUMERATED contents are encoded exactly like the
4//! corresponding INTEGER value. This module therefore delegates to [`IntegerFmt`](crate::asn1::IntegerFmt)
5//! at every layer while retaining a distinct format marker for the ENUMERATED tag.
6use crate::core::exec::output::OutputBuf;
7use crate::core::exec::{
8    parser::{PResult, Parser},
9    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
10};
11use crate::core::{proof::*, spec::*};
12use vstd::prelude::*;
13
14use super::{EnumeratedFmt, Integer, IntegerFmt};
15
16verus! {
17
18/// Executable ENUMERATED values use the same exact integer representation as INTEGER.
19pub type Enumerated<'a> = Integer<'a>;
20
21mod derived_specs {
22    use super::*;
23    use super::super::{EnumeratedFmt, IntegerFmt};
24
25    impl SpecParser for EnumeratedFmt {
26        type PVal = int;
27
28        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
29            IntegerFmt.spec_parse(ibuf)
30        }
31    }
32
33    impl Consistency for EnumeratedFmt {
34        type Val = int;
35
36        open spec fn consistent(&self, v: Self::Val) -> bool {
37            IntegerFmt.consistent(v)
38        }
39    }
40
41    impl SpecSerializerDps for EnumeratedFmt {
42        type SValue = int;
43
44        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
45            IntegerFmt.spec_serialize_dps(v, obuf)
46        }
47    }
48
49    impl SpecSerializer for EnumeratedFmt {
50        type SVal = int;
51
52        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
53            IntegerFmt.spec_serialize(v)
54        }
55    }
56
57    impl SpecByteLen for EnumeratedFmt {
58        type T = int;
59
60        open spec fn byte_len(&self, v: Self::T) -> nat {
61            IntegerFmt.byte_len(v)
62        }
63    }
64
65}
66
67mod derived_proofs {
68    use super::*;
69    use super::super::{EnumeratedFmt, IntegerFmt};
70
71    impl SafeParser for EnumeratedFmt {
72        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
73            IntegerFmt.lemma_parse_safe(ibuf);
74        }
75    }
76
77    impl Productive for EnumeratedFmt {
78        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
79            IntegerFmt.lemma_productive(ibuf);
80        }
81    }
82
83    impl SoundParser for EnumeratedFmt {
84        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
85            IntegerFmt.lemma_parse_sound_consumption(ibuf);
86        }
87
88        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
89            IntegerFmt.lemma_parse_sound_value(ibuf);
90        }
91    }
92
93    impl GoodSerializer for EnumeratedFmt {
94        proof fn lemma_serialize_len(&self, v: Self::SVal) {
95            IntegerFmt.lemma_serialize_len(v);
96        }
97    }
98
99    impl SPRoundTripDps for EnumeratedFmt {
100        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
101            IntegerFmt.theorem_serialize_dps_parse_roundtrip(v, obuf);
102        }
103    }
104
105    impl NonMalleable for EnumeratedFmt {
106        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
107            IntegerFmt.lemma_parse_non_malleable(buf1, buf2);
108        }
109    }
110
111    impl EquivSerializers for EnumeratedFmt {
112        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
113            IntegerFmt.lemma_serialize_equiv_on_empty(v);
114        }
115    }
116
117}
118
119impl<'i> Parser<&'i [u8]> for EnumeratedFmt {
120    type PT = Enumerated<'i>;
121
122    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
123        IntegerFmt.parse(ibuf)
124    }
125}
126
127impl<'i, Output: OutputBuf> Serializer<Output, Enumerated<'i>> for EnumeratedFmt {
128    fn serialize_into(&self, v: &Enumerated<'i>, obuf: &mut Output) {
129        IntegerFmt.serialize_into(v, obuf);
130    }
131}
132
133impl<'i> Prepare<Enumerated<'i>> for EnumeratedFmt {
134    fn prepare(&self, v: &Enumerated<'i>) -> Result<usize, PreSerializeError> {
135        IntegerFmt.prepare(v)
136    }
137}
138
139impl<'i> ByteLen<Enumerated<'i>> for EnumeratedFmt {
140    fn length(&self, v: &Enumerated<'i>) -> usize {
141        IntegerFmt.length(v)
142    }
143}
144
145} // verus!
146#[cfg(test)]
147mod tests {
148    use super::*;
149    use crate::asn1::der::ENUMERATED;
150    use crate::core::exec::{Parser, Prepare, SerializerExt};
151
152    #[test]
153    fn enumerated_uses_integer_contents_rules() {
154        let input = [0x0a, 0x01, 0x02];
155        let (_, value) = ENUMERATED.parse(&&input[..]).unwrap();
156        match value {
157            Integer::Small { v } => assert_eq!(v, 2),
158            Integer::Big { .. } => panic!("small ENUMERATED value parsed as a big integer"),
159        }
160
161        let mut output = vec![0; ENUMERATED.prepare(&value).unwrap()];
162        ENUMERATED.serialize(&value, &mut output);
163        assert_eq!(output, input);
164
165        let nonminimal = [0x0a, 0x02, 0x00, 0x02];
166        assert!(ENUMERATED.parse(&&nonminimal[..]).is_err());
167    }
168}
vest_lib/asn1/enumerated.rs

vest_lib/asn1/
enumerated.rs
