verdict_parser/asn1/
bounds.rs

1use super::*;
2/// Some bounds on n-byte integers
3/// Most implemented in macros so that they can be used in BV proofs
4/// NOTE: many macro definitions here are actually part of the spec
5use vstd::prelude::*;
6
7verus! {
8
9/// Signed/unsigned integer types used to represent values in ASN.1
10/// All definitions below are relative to these two types
11///
12/// NOTE: proofs in this module should be independent of the choice of UInt/Int.
13/// To change their definitions (to u128/i128, for example), we only need to
14/// change the macro uint_size!
15pub type UInt = u64;
16pub type Int = i64;
17
18#[allow(unused_macros)]
19macro_rules! uint_size { () => { 8 } }
20pub(super) use uint_size;
21
22/// Max value for an n-byte unsigned integer
23#[allow(unused_macros)]
24macro_rules! n_byte_max_unsigned {
25    ($n:expr) => { if $n == 0 { 0 } else { UInt::MAX >> (8 * (uint_size!() - $n) as usize) } }
26}
27pub(super) use n_byte_max_unsigned;
28
29/// Max value for an n-byte signed integer
30#[allow(unused_macros)]
31macro_rules! n_byte_max_signed {
32    ($n:expr) => { (n_byte_max_unsigned!($n) >> 1) as Int }
33}
34pub(super) use n_byte_max_signed;
35
36/// Min value for an n-byte signed integer
37#[allow(unused_macros)]
38macro_rules! n_byte_min_signed {
39    ($n:expr) => { if $n == 0 { 0 as Int } else { !(n_byte_max_unsigned!($n) >> 1) as Int } }
40}
41pub(super) use n_byte_min_signed;
42
43/// Check if the unsigned value can be represented in n bytes
44#[allow(unused_macros)]
45macro_rules! fits_n_bytes_unsigned {
46    ($v:expr, $n:expr) => {
47        $v <= n_byte_max_unsigned!($n)
48    };
49}
50pub(super) use fits_n_bytes_unsigned;
51
52/// Check if the signed value can be represented in n bytes
53#[allow(unused_macros)]
54macro_rules! fits_n_bytes_signed {
55    ($v:expr, $n:expr) => {
56        n_byte_min_signed!($n) <= $v && $v <= n_byte_max_signed!($n)
57    };
58}
59pub(super) use fits_n_bytes_signed;
60
61#[allow(unused_macros)]
62macro_rules! n_bit_max_unsigned {
63    ($n:expr) => { if $n == 0 { 0 } else { UInt::MAX >> (((8 * uint_size!()) - $n) as usize) } }
64}
65pub(super) use n_bit_max_unsigned;
66
67/// Get the nth-least significant byte (counting from 0)
68#[allow(unused_macros)]
69macro_rules! get_nth_byte {
70    ($v:expr, $n:expr) => {
71        (($v as UInt) >> (8 * ($n as usize))) as u8
72    };
73}
74pub(super) use get_nth_byte;
75
76/// Prepend $b as the $n-th byte (counting from 0) of $v
77/// Assuming $v fits in $n bytes
78#[allow(unused_macros)]
79macro_rules! prepend_byte {
80    ($v:expr, $b:expr, $n:expr) => {
81        ($v + (($b as UInt) << (8 * ($n as usize)))) as UInt
82    };
83}
84pub(super) use prepend_byte;
85
86/// Sign extend a UInt (assumed to have $n bytes only) to a Int
87#[allow(unused_macros)]
88macro_rules! sign_extend {
89    ($v:expr, $n:expr) => {
90        if get_nth_byte!($v, $n - 1) & 0x80 == 0 {
91            $v as Int
92        } else {
93            ($v as UInt + !n_byte_max_unsigned!($n)) as Int
94        }
95    };
96}
97pub(super) use sign_extend;
98
99/// Take the lowest 7 bits as an u8
100#[allow(unused_macros)]
101macro_rules! take_low_7_bits {
102    ($v:expr) => {
103        $v as u8 & 0x7f
104    };
105}
106pub(super) use take_low_7_bits;
107
108/// Set the highest bit to 1 as an u8
109#[allow(unused_macros)]
110macro_rules! set_high_8_bit {
111    ($v:expr) => {
112        ($v | 0x80) as u8
113    };
114}
115pub(super) use set_high_8_bit;
116
117/// Check if the highest bit is set in an u8
118#[allow(unused_macros)]
119macro_rules! is_high_8_bit_set {
120    ($v:expr) => {
121        $v as u8 >= 0x80
122    };
123}
124pub(super) use is_high_8_bit_set;
125
126/// Specifies the minimum number of bytes required to represent an unsigned integer
127pub open spec fn is_min_num_bytes_unsigned(v: UInt, n: UInt) -> bool
128{
129    &&& 0 < n <= uint_size!()
130    &&& if v == 0 {
131        n == 1
132    } else {
133        &&& n > 0
134        &&& fits_n_bytes_unsigned!(v, n)
135        &&& !fits_n_bytes_unsigned!(v, n - 1)
136    }
137}
138
139/// Signed version of is_min_num_bytes_unsigned
140/// TODO: merge with is_min_num_bytes_unsigned?
141pub open spec fn is_min_num_bytes_signed(v: Int, n: UInt) -> bool {
142    &&& 0 < n <= uint_size!()
143    &&& if v == 0 {
144        n == 1
145    } else {
146        &&& fits_n_bytes_signed!(v, n)
147        &&& !fits_n_bytes_signed!(v, n - 1)
148    }
149}
150
151pub open spec fn min_num_bytes_unsigned(v: UInt) -> UInt
152{
153    choose |n| is_min_num_bytes_unsigned(v, n)
154}
155
156pub open spec fn min_num_bytes_signed(v: Int) -> UInt
157{
158    choose |n| is_min_num_bytes_signed(v, n)
159}
160
161/// A helper induction lemma
162proof fn lemma_well_ordering(p: spec_fn(UInt) -> bool, n: UInt)
163    requires p(n) && !p(0)
164    ensures exists |i| 0 < i <= n && (#[trigger] p(i)) && !p((i - 1) as UInt)
165    decreases n
166{
167    if n > 1 && p((n - 1) as UInt) {
168        lemma_well_ordering(p, (n - 1) as UInt);
169    }
170}
171
172/// min_num_bytes_unsigned exists and is unique
173pub proof fn lemma_min_num_bytes_unsigned(v: UInt)
174    ensures
175        exists |n| is_min_num_bytes_unsigned(v, n),
176        forall |n1, n2|
177            is_min_num_bytes_unsigned(v, n1) &&
178            is_min_num_bytes_unsigned(v, n2) ==> n1 == n2,
179{
180    // Show uniqueness
181    if v == 0 {
182        assert(is_min_num_bytes_unsigned(v, 1));
183    } else {
184        assert(v != 0 ==> !fits_n_bytes_unsigned!(v, 0)) by (bit_vector);
185        assert(fits_n_bytes_unsigned!(v, uint_size!())) by (bit_vector);
186
187        let fits_n = |n: UInt| fits_n_bytes_unsigned!(v, n);
188        let bytes = choose |i| 0 < i <= uint_size!() && #[trigger] fits_n(i) && !fits_n((i - 1) as UInt);
189
190        lemma_well_ordering(fits_n, uint_size!());
191        assert(is_min_num_bytes_unsigned(v, bytes));
192    }
193
194    // Show existence
195    assert forall |n1, n2|
196        is_min_num_bytes_unsigned(v, n1) &&
197        is_min_num_bytes_unsigned(v, n2)
198    implies n1 == n2 by {
199        // By contradiction: if n2 < n1 or n1 < n2, then we can derive false by BV reasoning
200        assert(n2 < n1 <= uint_size!() ==> !(fits_n_bytes_unsigned!(v, n2) && !fits_n_bytes_unsigned!(v, n1 - 1))) by (bit_vector);
201        assert(n1 < n2 <= uint_size!() ==> !(fits_n_bytes_unsigned!(v, n1) && !fits_n_bytes_unsigned!(v, n2 - 1))) by (bit_vector);
202    };
203}
204
205/// Exec version of is_min_num_bytes_signed
206pub fn is_min_num_bytes_signed_exec(v: Int, n: UInt) -> (res: bool)
207    ensures res == is_min_num_bytes_signed(v, n)
208{
209    n > 0 &&
210    n <= uint_size!() &&
211    if v == 0 {
212        n == 1
213    } else {
214        fits_n_bytes_signed!(v, n) &&
215        !fits_n_bytes_signed!(v, n - 1)
216    }
217}
218
219/// min_num_bytes_signed exists and is unique
220pub proof fn lemma_min_num_bytes_signed(v: Int)
221    ensures
222        exists |n| is_min_num_bytes_signed(v, n),
223        forall |n1, n2|
224            is_min_num_bytes_signed(v, n1) &&
225            is_min_num_bytes_signed(v, n2) ==> n1 == n2,
226{
227    // Uniqueness
228    if v == 0 {
229        assert(is_min_num_bytes_signed(v, 1));
230    } else {
231        assert(v != 0 ==> !fits_n_bytes_signed!(v, 0)) by (bit_vector);
232        assert(fits_n_bytes_signed!(v, uint_size!())) by (bit_vector);
233
234        let fits_n = |n: UInt| fits_n_bytes_signed!(v, n);
235        let bytes = choose |i| 0 < i <= uint_size!() && #[trigger] fits_n(i) && !fits_n((i - 1) as UInt);
236
237        lemma_well_ordering(fits_n, uint_size!());
238        assert(is_min_num_bytes_signed(v, bytes));
239    }
240
241    // Existence
242    assert forall |n1, n2|
243        is_min_num_bytes_signed(v, n1) &&
244        is_min_num_bytes_signed(v, n2)
245    implies n1 == n2 by {
246        // By contradiction: if n2 < n1 or n1 < n2, then we can derive false by BV reasoning
247        assert(n2 < n1 <= uint_size!() ==> !(fits_n_bytes_signed!(v, n2) && !fits_n_bytes_signed!(v, n1 - 1))) by (bit_vector);
248        assert(n1 < n2 <= uint_size!() ==> !(fits_n_bytes_signed!(v, n1) && !fits_n_bytes_signed!(v, n2 - 1))) by (bit_vector);
249    };
250}
251
252/// Exec version of min_num_bytes_unsigned
253pub fn min_num_bytes_unsigned_exec(v: UInt) -> (res: UInt)
254    ensures is_min_num_bytes_unsigned(v, res)
255{
256    let mut n = uint_size!();
257
258    assert(n == uint_size!() ==> fits_n_bytes_unsigned!(v, n)) by (bit_vector);
259
260    while n > 0
261        invariant
262            0 <= n <= uint_size!(),
263            fits_n_bytes_unsigned!(v, n),
264        decreases n
265    {
266        if !fits_n_bytes_unsigned!(v, n - 1) {
267            return n;
268        }
269        n = n - 1;
270    }
271
272    assert(fits_n_bytes_unsigned!(v, 0) ==> v == 0) by (bit_vector);
273
274    return 1;
275}
276
277/// Exec version of min_num_bytes_signed
278pub fn min_num_bytes_signed_exec(v: Int) -> (res: UInt)
279    ensures is_min_num_bytes_signed(v, res)
280{
281    let mut n = uint_size!();
282
283    assert(n == uint_size!() ==> fits_n_bytes_signed!(v, n)) by (bit_vector);
284
285    while n > 0
286        invariant
287            0 <= n <= uint_size!(),
288            fits_n_bytes_signed!(v, n),
289        decreases n
290    {
291        if !fits_n_bytes_signed!(v, n - 1) {
292            assert(v == 0 && !fits_n_bytes_signed!(v, n - 1) ==> n == 1) by (bit_vector);
293            return n;
294        }
295        n = n - 1;
296    }
297
298    assert(fits_n_bytes_signed!(v, 0) ==> v == 0) by (bit_vector);
299
300    return 1;
301}
302
303impl PolyfillClone for UInt {
304    fn clone(&self) -> Self {
305        *self
306    }
307}
308
309impl PolyfillClone for Int {
310    fn clone(&self) -> Self {
311        *self
312    }
313}
314
315}
verdict_parser/asn1/bounds.rs

verdict_parser/asn1/
bounds.rs
