vest_lib/combinators/uints/
exec.rs

1//! Executable fixed-width unsigned integer formats.
2use super::spec::*;
3use crate::combinators::bytes::spec::*;
4use crate::combinators::Fixed;
5use crate::core::exec::input::InputSlice;
6use crate::core::exec::output::*;
7use crate::core::exec::{
8    parser::{PResult, Parser},
9    serializer::{ByteLen, ComplianceErrorKind, PreSerializeError, Prepare, Serializer},
10    ParseError,
11};
12use crate::core::spec::{SpecParser, SpecSerializer};
13use vstd::prelude::*;
14use OutputBuf;
15
16verus! {
17
18#[verifier::external_body]
19#[inline(always)]
20pub fn u16_from_le_bytes(bytes: [u8; 2]) -> (out: u16)
21    ensures
22        out == u16_le_from_bytes(bytes),
23{
24    u16::from_le_bytes(bytes)
25}
26
27#[verifier::external_body]
28#[inline(always)]
29pub fn u16_from_be_bytes(bytes: [u8; 2]) -> (out: u16)
30    ensures
31        out == u16_be_from_bytes(bytes),
32{
33    u16::from_be_bytes(bytes)
34}
35
36#[verifier::external_body]
37#[inline(always)]
38pub fn u16_to_le_bytes(value: u16) -> (bytes: [u8; 2])
39    ensures
40        bytes == u16_le_to_bytes(value),
41{
42    value.to_le_bytes()
43}
44
45#[verifier::external_body]
46#[inline(always)]
47pub fn u16_to_be_bytes(value: u16) -> (bytes: [u8; 2])
48    ensures
49        bytes == u16_be_to_bytes(value),
50{
51    value.to_be_bytes()
52}
53
54#[inline(always)]
55pub fn u24_from_le_bytes(bytes: [u8; 3]) -> (out: u32)
56    ensures
57        out == u24_le_from_bytes(bytes),
58{
59    (bytes[0] as u32) | ((bytes[1] as u32) << 8) | ((bytes[2] as u32) << 16)
60}
61
62#[inline(always)]
63pub fn u24_from_be_bytes(bytes: [u8; 3]) -> (out: u32)
64    ensures
65        out == u24_be_from_bytes(bytes),
66{
67    ((bytes[0] as u32) << 16) | ((bytes[1] as u32) << 8) | (bytes[2] as u32)
68}
69
70#[inline(always)]
71pub fn u24_to_le_bytes(value: u32) -> (bytes: [u8; 3])
72    ensures
73        bytes == u24_le_to_bytes(value),
74{
75    [(value & 0xff) as u8, ((value >> 8) & 0xff) as u8, ((value >> 16) & 0xff) as u8]
76}
77
78#[inline(always)]
79pub fn u24_to_be_bytes(value: u32) -> (bytes: [u8; 3])
80    ensures
81        bytes == u24_be_to_bytes(value),
82{
83    [((value >> 16) & 0xff) as u8, ((value >> 8) & 0xff) as u8, (value & 0xff) as u8]
84}
85
86#[verifier::external_body]
87#[inline(always)]
88pub fn u32_from_le_bytes(bytes: [u8; 4]) -> (out: u32)
89    ensures
90        out == u32_le_from_bytes(bytes),
91{
92    u32::from_le_bytes(bytes)
93}
94
95#[verifier::external_body]
96#[inline(always)]
97pub fn u32_from_be_bytes(bytes: [u8; 4]) -> (out: u32)
98    ensures
99        out == u32_be_from_bytes(bytes),
100{
101    u32::from_be_bytes(bytes)
102}
103
104#[verifier::external_body]
105#[inline(always)]
106pub fn u32_to_le_bytes(value: u32) -> (bytes: [u8; 4])
107    ensures
108        bytes == u32_le_to_bytes(value),
109{
110    value.to_le_bytes()
111}
112
113#[verifier::external_body]
114#[inline(always)]
115pub fn u32_to_be_bytes(value: u32) -> (bytes: [u8; 4])
116    ensures
117        bytes == u32_be_to_bytes(value),
118{
119    value.to_be_bytes()
120}
121
122#[verifier::external_body]
123#[inline(always)]
124pub fn u64_from_le_bytes(bytes: [u8; 8]) -> (out: u64)
125    ensures
126        out == u64_le_from_bytes(bytes),
127{
128    u64::from_le_bytes(bytes)
129}
130
131#[verifier::external_body]
132#[inline(always)]
133pub fn u64_from_be_bytes(bytes: [u8; 8]) -> (out: u64)
134    ensures
135        out == u64_be_from_bytes(bytes),
136{
137    u64::from_be_bytes(bytes)
138}
139
140#[verifier::external_body]
141#[inline(always)]
142pub fn u64_to_le_bytes(value: u64) -> (bytes: [u8; 8])
143    ensures
144        bytes == u64_le_to_bytes(value),
145{
146    value.to_le_bytes()
147}
148
149#[verifier::external_body]
150#[inline(always)]
151pub fn u64_to_be_bytes(value: u64) -> (bytes: [u8; 8])
152    ensures
153        bytes == u64_be_to_bytes(value),
154{
155    value.to_be_bytes()
156}
157
158impl Parser<&[u8]> for super::U8 {
159    type PT = u8;
160
161    open spec fn exec_inv(&self) -> bool {
162        true
163    }
164
165    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
166        if ibuf.len() < 1 {
167            Err(ParseError::unexpected_eof())
168        } else {
169            Ok((1, ibuf[0]))
170        }
171    }
172}
173
174impl<Output: OutputBuf> Serializer<Output, u8> for super::U8 {
175    fn serialize_into(&self, v: &u8, obuf: &mut Output) {
176        obuf.write_byte(*v);
177    }
178}
179
180impl ByteLen<u8> for super::U8 {
181    fn length(&self, _v: &u8) -> (len: usize) {
182        1
183    }
184}
185
186impl Prepare<u8> for super::U8 {
187    fn prepare(&self, _v: &u8) -> (checked: Result<usize, PreSerializeError>) {
188        Ok(1)
189    }
190}
191
192impl Parser<&[u8]> for super::U16Le {
193    type PT = u16;
194
195    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
196        broadcast use lemma_array_from_seq_roundtrip;
197
198        let (n, chunk) = Fixed::<U16_BYTE_LEN>.parse(ibuf)?;
199        assert(chunk@ == ibuf@.take(U16_BYTE_LEN as int));
200
201        let bytes = [chunk[0], chunk[1]];
202        let value = u16_from_le_bytes(bytes);
203
204        assert(bytes@ == chunk@);
205
206        Ok((n, value))
207    }
208}
209
210impl<Output: OutputBuf> Serializer<Output, u16> for super::U16Le {
211    fn serialize_into(&self, v: &u16, obuf: &mut Output) {
212        let bytes = u16_to_le_bytes(*v);
213
214        obuf.write_bytes(&bytes);
215    }
216}
217
218impl ByteLen<u16> for super::U16Le {
219    fn length(&self, _v: &u16) -> (len: usize) {
220        U16_BYTE_LEN
221    }
222}
223
224impl Prepare<u16> for super::U16Le {
225    fn prepare(&self, _v: &u16) -> (checked: Result<usize, PreSerializeError>) {
226        Ok(U16_BYTE_LEN)
227    }
228}
229
230impl Parser<&[u8]> for super::U16Be {
231    type PT = u16;
232
233    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
234        broadcast use lemma_array_from_seq_roundtrip;
235
236        let (n, chunk) = Fixed::<U16_BYTE_LEN>.parse(ibuf)?;
237        assert(chunk@ == ibuf@.take(U16_BYTE_LEN as int));
238
239        let bytes = [chunk[0], chunk[1]];
240        let value = u16_from_be_bytes(bytes);
241
242        assert(bytes@ == chunk@);
243
244        Ok((n, value))
245    }
246}
247
248impl<Output: OutputBuf> Serializer<Output, u16> for super::U16Be {
249    fn serialize_into(&self, v: &u16, obuf: &mut Output) {
250        let bytes = u16_to_be_bytes(*v);
251        obuf.write_bytes(&bytes);
252    }
253}
254
255impl ByteLen<u16> for super::U16Be {
256    fn length(&self, _v: &u16) -> (len: usize) {
257        U16_BYTE_LEN
258    }
259}
260
261impl Prepare<u16> for super::U16Be {
262    fn prepare(&self, _v: &u16) -> (checked: Result<usize, PreSerializeError>) {
263        Ok(U16_BYTE_LEN)
264    }
265}
266
267impl Parser<&[u8]> for super::U24Le {
268    type PT = u32;
269
270    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
271        broadcast use lemma_array_from_seq_roundtrip;
272
273        let (n, chunk) = Fixed::<U24_BYTE_LEN>.parse(ibuf)?;
274        assert(chunk@ == ibuf@.take(U24_BYTE_LEN as int));
275
276        let bytes = [chunk[0], chunk[1], chunk[2]];
277        let value = u24_from_le_bytes(bytes);
278
279        assert(bytes@ == chunk@);
280
281        Ok((n, value))
282    }
283}
284
285impl<Output: OutputBuf> Serializer<Output, u32> for super::U24Le {
286    fn serialize_into(&self, v: &u32, obuf: &mut Output) {
287        let bytes = u24_to_le_bytes(*v);
288        obuf.write_bytes(&bytes);
289    }
290}
291
292impl ByteLen<u32> for super::U24Le {
293    fn length(&self, _v: &u32) -> (len: usize) {
294        U24_BYTE_LEN
295    }
296}
297
298impl Prepare<u32> for super::U24Le {
299    fn prepare(&self, v: &u32) -> (checked: Result<usize, PreSerializeError>) {
300        if *v < 0x01000000 {
301            Ok(U24_BYTE_LEN)
302        } else {
303            Err(PreSerializeError::not_compliant(ComplianceErrorKind::PredicateFailed))
304        }
305    }
306}
307
308impl Parser<&[u8]> for super::U24Be {
309    type PT = u32;
310
311    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
312        broadcast use lemma_array_from_seq_roundtrip;
313
314        let (n, chunk) = Fixed::<U24_BYTE_LEN>.parse(ibuf)?;
315        assert(chunk@ == ibuf@.take(U24_BYTE_LEN as int));
316
317        let bytes = [chunk[0], chunk[1], chunk[2]];
318        let value = u24_from_be_bytes(bytes);
319
320        assert(bytes@ == chunk@);
321
322        Ok((n, value))
323    }
324}
325
326impl<Output: OutputBuf> Serializer<Output, u32> for super::U24Be {
327    fn serialize_into(&self, v: &u32, obuf: &mut Output) {
328        let bytes = u24_to_be_bytes(*v);
329        obuf.write_bytes(&bytes);
330    }
331}
332
333impl ByteLen<u32> for super::U24Be {
334    fn length(&self, _v: &u32) -> (len: usize) {
335        U24_BYTE_LEN
336    }
337}
338
339impl Prepare<u32> for super::U24Be {
340    fn prepare(&self, v: &u32) -> (checked: Result<usize, PreSerializeError>) {
341        if *v < 0x01000000 {
342            Ok(U24_BYTE_LEN)
343        } else {
344            Err(PreSerializeError::not_compliant(ComplianceErrorKind::PredicateFailed))
345        }
346    }
347}
348
349impl Parser<&[u8]> for super::U32Le {
350    type PT = u32;
351
352    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
353        broadcast use lemma_array_from_seq_roundtrip;
354
355        let (n, chunk) = Fixed::<U32_BYTE_LEN>.parse(ibuf)?;
356        assert(chunk@ == ibuf@.take(U32_BYTE_LEN as int));
357
358        let bytes = [chunk[0], chunk[1], chunk[2], chunk[3]];
359        let value = u32_from_le_bytes(bytes);
360
361        assert(bytes@ == chunk@);
362
363        Ok((n, value))
364    }
365}
366
367impl<Output: OutputBuf> Serializer<Output, u32> for super::U32Le {
368    fn serialize_into(&self, v: &u32, obuf: &mut Output) {
369        let bytes = u32_to_le_bytes(*v);
370        obuf.write_bytes(&bytes);
371    }
372}
373
374impl ByteLen<u32> for super::U32Le {
375    fn length(&self, _v: &u32) -> (len: usize) {
376        U32_BYTE_LEN
377    }
378}
379
380impl Prepare<u32> for super::U32Le {
381    fn prepare(&self, _v: &u32) -> (checked: Result<usize, PreSerializeError>) {
382        Ok(U32_BYTE_LEN)
383    }
384}
385
386impl Parser<&[u8]> for super::U32Be {
387    type PT = u32;
388
389    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
390        broadcast use lemma_array_from_seq_roundtrip;
391
392        let (n, chunk) = Fixed::<U32_BYTE_LEN>.parse(ibuf)?;
393        assert(chunk@ == ibuf@.take(U32_BYTE_LEN as int));
394
395        let bytes = [chunk[0], chunk[1], chunk[2], chunk[3]];
396        let value = u32_from_be_bytes(bytes);
397
398        assert(bytes@ == chunk@);
399
400        Ok((n, value))
401    }
402}
403
404impl<Output: OutputBuf> Serializer<Output, u32> for super::U32Be {
405    fn serialize_into(&self, v: &u32, obuf: &mut Output) {
406        let bytes = u32_to_be_bytes(*v);
407        obuf.write_bytes(&bytes);
408    }
409}
410
411impl ByteLen<u32> for super::U32Be {
412    fn length(&self, _v: &u32) -> (len: usize) {
413        U32_BYTE_LEN
414    }
415}
416
417impl Prepare<u32> for super::U32Be {
418    fn prepare(&self, _v: &u32) -> (checked: Result<usize, PreSerializeError>) {
419        Ok(U32_BYTE_LEN)
420    }
421}
422
423impl Parser<&[u8]> for super::U64Le {
424    type PT = u64;
425
426    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
427        broadcast use lemma_array_from_seq_roundtrip;
428
429        let (n, chunk) = Fixed::<U64_BYTE_LEN>.parse(ibuf)?;
430        assert(chunk@ == ibuf@.take(U64_BYTE_LEN as int));
431
432        let bytes = [
433            chunk[0],
434            chunk[1],
435            chunk[2],
436            chunk[3],
437            chunk[4],
438            chunk[5],
439            chunk[6],
440            chunk[7],
441        ];
442        let value = u64_from_le_bytes(bytes);
443
444        assert(bytes@ == chunk@);
445
446        Ok((n, value))
447    }
448}
449
450impl<Output: OutputBuf> Serializer<Output, u64> for super::U64Le {
451    fn serialize_into(&self, v: &u64, obuf: &mut Output) {
452        let bytes = u64_to_le_bytes(*v);
453        obuf.write_bytes(&bytes);
454    }
455}
456
457impl ByteLen<u64> for super::U64Le {
458    fn length(&self, _v: &u64) -> (len: usize) {
459        U64_BYTE_LEN
460    }
461}
462
463impl Prepare<u64> for super::U64Le {
464    fn prepare(&self, _v: &u64) -> (checked: Result<usize, PreSerializeError>) {
465        Ok(U64_BYTE_LEN)
466    }
467}
468
469impl Parser<&[u8]> for super::U64Be {
470    type PT = u64;
471
472    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
473        broadcast use lemma_array_from_seq_roundtrip;
474
475        let (n, chunk) = Fixed::<U64_BYTE_LEN>.parse(ibuf)?;
476        assert(chunk@ == ibuf@.take(U64_BYTE_LEN as int));
477
478        let bytes = [
479            chunk[0],
480            chunk[1],
481            chunk[2],
482            chunk[3],
483            chunk[4],
484            chunk[5],
485            chunk[6],
486            chunk[7],
487        ];
488        let value = u64_from_be_bytes(bytes);
489
490        assert(bytes@ == chunk@);
491
492        Ok((n, value))
493    }
494}
495
496impl<Output: OutputBuf> Serializer<Output, u64> for super::U64Be {
497    fn serialize_into(&self, v: &u64, obuf: &mut Output) {
498        let bytes = u64_to_be_bytes(*v);
499        obuf.write_bytes(&bytes);
500    }
501}
502
503impl ByteLen<u64> for super::U64Be {
504    fn length(&self, _v: &u64) -> (len: usize) {
505        U64_BYTE_LEN
506    }
507}
508
509impl Prepare<u64> for super::U64Be {
510    fn prepare(&self, _v: &u64) -> (checked: Result<usize, PreSerializeError>) {
511        Ok(U64_BYTE_LEN)
512    }
513}
514
515} // verus!
vest_lib/combinators/uints/exec.rs

vest_lib/combinators/uints/
exec.rs
