verdict_parser/asn1/
integer.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Combinator for ASN.1 integers (without the preceding tag)
7/// This combinator uses IntegerInner with the additional constraint
8/// of is_min_num_bytes_signed
9#[derive(Debug, View)]
10pub struct Integer;
11
12asn1_tagged!(Integer, tag_of!(INTEGER));
13
14pub type IntegerValue = VarIntResult;
15
16impl SpecCombinator for Integer {
17    type SpecResult = IntegerValue;
18
19    /// Same as new_spec_integer_inner(), but filters out tuples (n, v)
20    /// where v is *not* the minimum number of bytes required to represent v
21    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
22        match new_spec_integer_inner().spec_parse(s) {
23            Ok((len, (n, v))) => {
24                if is_min_num_bytes_signed(v, n as VarUIntResult) {
25                    Ok((len, v))
26                } else {
27                    Err(())
28                }
29            }
30            Err(..) => Err(()),
31        }
32    }
33
34    proof fn spec_parse_wf(&self, s: Seq<u8>) {
35        new_spec_integer_inner().spec_parse_wf(s);
36    }
37
38    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
39        new_spec_integer_inner().spec_serialize((min_num_bytes_signed(v) as LengthValue, v))
40    }
41}
42
43impl SecureSpecCombinator for Integer {
44    open spec fn is_prefix_secure() -> bool {
45        true
46    }
47
48    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
49        new_spec_integer_inner().theorem_serialize_parse_roundtrip((min_num_bytes_signed(v) as LengthValue, v));
50        lemma_min_num_bytes_signed(v);
51    }
52
53    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
54        new_spec_integer_inner().theorem_parse_serialize_roundtrip(buf);
55
56        if let Ok((_, (n, v))) = new_spec_integer_inner().spec_parse(buf) {
57            lemma_min_num_bytes_signed(v);
58        }
59    }
60
61    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
62        new_spec_integer_inner().lemma_prefix_secure(s1, s2);
63    }
64}
65
66impl Combinator for Integer {
67    type Result<'a> = IntegerValue;
68    type Owned = IntegerValue;
69
70    closed spec fn spec_length(&self) -> Option<usize> {
71        None
72    }
73
74    fn length(&self) -> Option<usize> {
75        None
76    }
77
78    #[inline(always)]
79    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
80        let (len, (n, v)) = new_integer_inner().parse(s)?;
81
82        if is_min_num_bytes_signed_exec(v, n as VarUIntResult) {
83            Ok((len, v))
84        } else {
85            Err(ParseError::Other("Non-minimal integer encoding".to_string()))
86        }
87    }
88
89    #[inline(always)]
90    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
91        proof {
92            lemma_min_num_bytes_signed(v);
93        }
94        new_integer_inner().serialize((min_num_bytes_signed_exec(v) as LengthValue, v), data, pos)
95    }
96}
97
98/// This is a function that takes in a VarUIntResult (`l`)
99/// and returns a VarInt combinator that reads `l` bytes
100struct IntegerCont;
101
102impl Continuation for IntegerCont {
103    type Input<'a> = LengthValue;
104    type Output = VarInt;
105
106    #[inline(always)]
107    fn apply<'a>(&self, i: Self::Input<'a>) -> (o: Self::Output) {
108        VarInt(i as usize)
109    }
110
111    closed spec fn requires<'a>(&self, i: Self::Input<'a>) -> bool {
112        true
113    }
114
115    closed spec fn ensures<'a>(&self, i: Self::Input<'a>, o: Self::Output) -> bool {
116        o == VarInt(i as usize)
117    }
118}
119
120/// A combinator that parses (n, v) where v is a VarInt parsed from n bytes
121/// This does not check if n is the minimum number of bytes required to represent v
122#[allow(dead_code)]
123type SpecIntegerInner = SpecDepend<Length, VarInt>;
124type IntegerInner = Depend<Length, VarInt, IntegerCont>;
125
126closed spec fn new_spec_integer_inner() -> SpecIntegerInner {
127    let ghost spec_snd = |l| {
128        VarInt(l as usize)
129    };
130
131    SpecDepend {
132        fst: Length,
133        snd: spec_snd,
134    }
135}
136
137#[inline(always)]
138fn new_integer_inner() -> (res: IntegerInner)
139    ensures res.view() == new_spec_integer_inner()
140{
141    let ghost spec_snd = |l| {
142        VarInt(l as usize)
143    };
144
145    Depend {
146        fst: Length,
147        snd: IntegerCont,
148        spec_snd: Ghost(spec_snd),
149    }
150}
151
152}
153
154#[cfg(test)]
155mod test {
156    use super::*;
157    use der::Encode;
158
159    #[test]
160    fn parse() {
161        assert_eq!(Integer.parse(&[0x01, 0x00]).unwrap(), (2, 0));
162        assert_eq!(Integer.parse(&[0x01, 0xff]).unwrap(), (2, -1));
163        assert_eq!(Integer.parse(&[0x02, 0x00, 0xff]).unwrap(), (3, 0xff));
164
165        assert!(Integer.parse(&[0x00]).is_err());
166        assert!(Integer.parse(&[0x81, 0x01, 0xff]).is_err());
167        assert!(Integer.parse(&[0x02, 0x00, 0x7f]).is_err()); // violation of minimal encoding
168    }
169
170    fn serialize_int(v: IntegerValue) -> Result<Vec<u8>, SerializeError> {
171        let mut data = vec![0; 16];
172        let len = ASN1(Integer).serialize(v, &mut data, 0)?;
173        data.truncate(len);
174        Ok(data)
175    }
176
177    /// Compare results of serialize to a common ASN.1 DER library
178    #[test]
179    fn diff_with_der() {
180        let diff = |i| {
181            let res1 = serialize_int(i).map_err(|_| ());
182            let res2 = i.to_der().map_err(|_| ());
183            assert_eq!(res1, res2);
184        };
185
186        diff(0);
187        diff(i64::MAX);
188        diff(i64::MIN);
189
190        for i in 0..65535i64 {
191            diff(i);
192        }
193
194        for i in -65535i64..0 {
195            diff(i);
196        }
197    }
198}
verdict_parser/asn1/integer.rs

verdict_parser/asn1/
integer.rs
