verdict_parser/asn1/
big_int.rs

1use super::*;
2use std::fmt::{self, Debug, Formatter};
3use vstd::prelude::*;
4
5verus! {
6
7/// If it's expected that an INTEGER field is larger than the Int type,
8/// then use this combinator to read it as an octet string (with
9/// some minimality constraints).
10#[derive(Debug, View)]
11pub struct BigInt;
12
13asn1_tagged!(BigInt, tag_of!(INTEGER));
14
15/// BigInt represents the integer with a sequence of bytes in big-endian order
16/// (same as ASN.1) and the most significant bit of the first byte is the sign bit.
17pub type SpecBigIntValue = Seq<u8>;
18pub struct BigIntValue<'a>(&'a [u8]);
19
20#[allow(dead_code)]
21pub struct BigIntOwned(Vec<u8>);
22
23impl<'a> View for BigIntValue<'a> {
24    type V = Seq<u8>;
25
26    closed spec fn view(&self) -> Self::V {
27        self.0@
28    }
29}
30
31impl<'a> PolyfillEq for BigIntValue<'a> {
32    #[inline(always)]
33    fn polyfill_eq(&self, other: &Self) -> bool {
34        self.0.polyfill_eq(&other.0)
35    }
36}
37
38impl View for BigIntOwned {
39    type V = Seq<u8>;
40
41    closed spec fn view(&self) -> Self::V {
42        self.0@
43    }
44}
45
46impl<'a> PolyfillClone for BigIntValue<'a> {
47    #[inline(always)]
48    fn clone(&self) -> Self {
49        proof {
50            use_type_invariant(self);
51        }
52        BigIntValue(&self.0)
53    }
54}
55
56impl<'a> BigIntValue<'a> {
57    #[verifier::type_invariant]
58    closed spec fn inv(self) -> bool {
59        Self::spec_wf(self@)
60    }
61
62    /// `bytes` should be the minimal encoding
63    /// i.e. the first byte should not be 0 unless
64    ///   1. bytes.len() == 1
65    ///   2. bytes[1] >= 0x80
66    pub open spec fn spec_wf(bytes: Seq<u8>) -> bool {
67        &&& bytes.len() != 0
68        &&& bytes[0] == 0 ==> {
69            ||| bytes.len() == 1
70            // the first byte cannot be removed, otherwise it will turn into a negative number
71            ||| bytes[1] >= 0x80
72        }
73    }
74
75    #[inline(always)]
76    pub fn wf(bytes: &'a [u8]) -> (res: bool)
77        ensures res == BigIntValue::spec_wf(bytes@)
78    {
79        bytes.len() != 0 &&
80        (bytes[0] != 0 || bytes.len() == 1 || bytes[1] >= 0x80)
81    }
82
83    pub open spec fn spec_byte_len(&self) -> usize {
84        (self@.len() - 1) as usize
85    }
86
87    /// The minimum number of bytes to represent the integer
88    #[inline(always)]
89    pub fn byte_len(&self) -> (res: usize)
90        ensures res == self.spec_byte_len()
91    {
92        proof {
93            use_type_invariant(self);
94        }
95        self.0.len() - 1
96    }
97
98    #[inline(always)]
99    pub fn bytes(&self) -> (res: &[u8])
100        ensures res@ == self@
101    {
102        self.0
103    }
104
105    // TODO: add more methods to interpret BigIntValue as an integer
106}
107
108impl SpecCombinator for BigInt {
109    type SpecResult = Seq<u8>;
110
111    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
112        new_spec_big_int_inner().spec_parse(s)
113    }
114
115    proof fn spec_parse_wf(&self, s: Seq<u8>) {
116        new_spec_big_int_inner().spec_parse_wf(s)
117    }
118
119    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
120        new_spec_big_int_inner().spec_serialize(v)
121    }
122}
123
124impl SecureSpecCombinator for BigInt {
125    open spec fn is_prefix_secure() -> bool {
126        true
127    }
128
129    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
130        new_spec_big_int_inner().theorem_serialize_parse_roundtrip(v);
131    }
132
133    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
134        new_spec_big_int_inner().theorem_parse_serialize_roundtrip(buf);
135    }
136
137    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
138        new_spec_big_int_inner().lemma_prefix_secure(s1, s2);
139    }
140}
141
142impl Combinator for BigInt {
143    type Result<'a> = BigIntValue<'a>;
144    type Owned = BigIntOwned;
145
146    open spec fn spec_length(&self) -> Option<usize> {
147        None
148    }
149
150    fn length(&self) -> Option<usize> {
151        None
152    }
153
154    #[inline(always)]
155    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
156        let (len, v) = new_big_int_inner().parse(s)?;
157        Ok((len, BigIntValue(v)))
158    }
159
160    #[inline(always)]
161    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
162        new_big_int_inner().serialize(v.0, data, pos)
163    }
164}
165
166/// A condition that the minimal encoding is used
167#[derive(View)]
168pub struct MinimalBigIntPred;
169
170impl SpecPred for MinimalBigIntPred {
171    type Input = Seq<u8>;
172
173    closed spec fn spec_apply(&self, i: &Self::Input) -> bool {
174        BigIntValue::spec_wf(*i)
175    }
176}
177
178impl Pred for MinimalBigIntPred {
179    type Input<'a> = &'a [u8];
180    type InputOwned = Vec<u8>;
181
182    fn apply(&self, i: &Self::Input<'_>) -> (res: bool)
183    {
184        BigIntValue::wf(i)
185    }
186}
187
188type BigIntInner = Refined<OctetString, MinimalBigIntPred>;
189
190pub closed spec fn new_spec_big_int_inner() -> BigIntInner
191{
192    Refined {
193        inner: OctetString,
194        predicate: MinimalBigIntPred,
195    }
196}
197
198#[inline(always)]
199fn new_big_int_inner() -> (res: BigIntInner)
200    ensures res@ == new_spec_big_int_inner()
201{
202    Refined {
203        inner: OctetString,
204        predicate: MinimalBigIntPred,
205    }
206}
207
208}
209
210impl<'a> Debug for BigIntValue<'a> {
211    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
212        // Print self.0 as a big-endian big integer
213        write!(f, "BigIntValue(0x")?;
214        for b in self.0 {
215            write!(f, "{:02x}", b)?;
216        }
217        write!(f, ")")
218    }
219}
verdict_parser/asn1/big_int.rs

verdict_parser/asn1/
big_int.rs
