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    fn min_byte_len(&self) -> usize {
162        U8_BYTE_LEN
163    }
164
165    open spec fn exec_inv(&self) -> bool {
166        true
167    }
168
169    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
170        if ibuf.len() < 1 {
171            Err(ParseError::unexpected_eof())
172        } else {
173            Ok((1, ibuf[0]))
174        }
175    }
176}
177
178impl<Output: OutputBuf> Serializer<Output, u8> for super::U8 {
179    fn serialize_into(&self, v: &u8, obuf: &mut Output) {
180        obuf.write_byte(*v);
181    }
182}
183
184impl ByteLen<u8> for super::U8 {
185    fn length(&self, _v: &u8) -> (len: usize) {
186        1
187    }
188}
189
190impl Prepare<u8> for super::U8 {
191    fn prepare(&self, _v: &u8) -> (checked: Result<usize, PreSerializeError>) {
192        Ok(1)
193    }
194}
195
196impl Parser<&[u8]> for super::U16Le {
197    type PT = u16;
198
199    fn min_byte_len(&self) -> usize {
200        U16_BYTE_LEN
201    }
202
203    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
204        broadcast use lemma_array_from_seq_roundtrip;
205
206        let (n, chunk) = Fixed::<U16_BYTE_LEN>.parse(ibuf)?;
207        assert(chunk@ == ibuf@[0..U16_BYTE_LEN]);
208
209        let bytes = [chunk[0], chunk[1]];
210        let value = u16_from_le_bytes(bytes);
211
212        assert(bytes@ == chunk@);
213
214        Ok((n, value))
215    }
216}
217
218impl<Output: OutputBuf> Serializer<Output, u16> for super::U16Le {
219    fn serialize_into(&self, v: &u16, obuf: &mut Output) {
220        let bytes = u16_to_le_bytes(*v);
221
222        obuf.write_bytes(&bytes);
223    }
224}
225
226impl ByteLen<u16> for super::U16Le {
227    fn length(&self, _v: &u16) -> (len: usize) {
228        U16_BYTE_LEN
229    }
230}
231
232impl Prepare<u16> for super::U16Le {
233    fn prepare(&self, _v: &u16) -> (checked: Result<usize, PreSerializeError>) {
234        Ok(U16_BYTE_LEN)
235    }
236}
237
238impl Parser<&[u8]> for super::U16Be {
239    type PT = u16;
240
241    fn min_byte_len(&self) -> usize {
242        U16_BYTE_LEN
243    }
244
245    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
246        broadcast use lemma_array_from_seq_roundtrip;
247
248        let (n, chunk) = Fixed::<U16_BYTE_LEN>.parse(ibuf)?;
249        assert(chunk@ == ibuf@[0..U16_BYTE_LEN]);
250
251        let bytes = [chunk[0], chunk[1]];
252        let value = u16_from_be_bytes(bytes);
253
254        assert(bytes@ == chunk@);
255
256        Ok((n, value))
257    }
258}
259
260impl<Output: OutputBuf> Serializer<Output, u16> for super::U16Be {
261    fn serialize_into(&self, v: &u16, obuf: &mut Output) {
262        let bytes = u16_to_be_bytes(*v);
263        obuf.write_bytes(&bytes);
264    }
265}
266
267impl ByteLen<u16> for super::U16Be {
268    fn length(&self, _v: &u16) -> (len: usize) {
269        U16_BYTE_LEN
270    }
271}
272
273impl Prepare<u16> for super::U16Be {
274    fn prepare(&self, _v: &u16) -> (checked: Result<usize, PreSerializeError>) {
275        Ok(U16_BYTE_LEN)
276    }
277}
278
279impl Parser<&[u8]> for super::U24Le {
280    type PT = u32;
281
282    fn min_byte_len(&self) -> usize {
283        U24_BYTE_LEN
284    }
285
286    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
287        broadcast use lemma_array_from_seq_roundtrip;
288
289        let (n, chunk) = Fixed::<U24_BYTE_LEN>.parse(ibuf)?;
290        assert(chunk@ == ibuf@[0..U24_BYTE_LEN]);
291
292        let bytes = [chunk[0], chunk[1], chunk[2]];
293        let value = u24_from_le_bytes(bytes);
294
295        assert(bytes@ == chunk@);
296
297        Ok((n, value))
298    }
299}
300
301impl<Output: OutputBuf> Serializer<Output, u32> for super::U24Le {
302    fn serialize_into(&self, v: &u32, obuf: &mut Output) {
303        let bytes = u24_to_le_bytes(*v);
304        obuf.write_bytes(&bytes);
305    }
306}
307
308impl ByteLen<u32> for super::U24Le {
309    fn length(&self, _v: &u32) -> (len: usize) {
310        U24_BYTE_LEN
311    }
312}
313
314impl Prepare<u32> for super::U24Le {
315    fn prepare(&self, v: &u32) -> (checked: Result<usize, PreSerializeError>) {
316        if *v < 0x01000000 {
317            Ok(U24_BYTE_LEN)
318        } else {
319            Err(PreSerializeError::not_compliant(ComplianceErrorKind::PredicateFailed))
320        }
321    }
322}
323
324impl Parser<&[u8]> for super::U24Be {
325    type PT = u32;
326
327    fn min_byte_len(&self) -> usize {
328        U24_BYTE_LEN
329    }
330
331    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
332        broadcast use lemma_array_from_seq_roundtrip;
333
334        let (n, chunk) = Fixed::<U24_BYTE_LEN>.parse(ibuf)?;
335        assert(chunk@ == ibuf@[0..U24_BYTE_LEN]);
336
337        let bytes = [chunk[0], chunk[1], chunk[2]];
338        let value = u24_from_be_bytes(bytes);
339
340        assert(bytes@ == chunk@);
341
342        Ok((n, value))
343    }
344}
345
346impl<Output: OutputBuf> Serializer<Output, u32> for super::U24Be {
347    fn serialize_into(&self, v: &u32, obuf: &mut Output) {
348        let bytes = u24_to_be_bytes(*v);
349        obuf.write_bytes(&bytes);
350    }
351}
352
353impl ByteLen<u32> for super::U24Be {
354    fn length(&self, _v: &u32) -> (len: usize) {
355        U24_BYTE_LEN
356    }
357}
358
359impl Prepare<u32> for super::U24Be {
360    fn prepare(&self, v: &u32) -> (checked: Result<usize, PreSerializeError>) {
361        if *v < 0x01000000 {
362            Ok(U24_BYTE_LEN)
363        } else {
364            Err(PreSerializeError::not_compliant(ComplianceErrorKind::PredicateFailed))
365        }
366    }
367}
368
369impl Parser<&[u8]> for super::U32Le {
370    type PT = u32;
371
372    fn min_byte_len(&self) -> usize {
373        U32_BYTE_LEN
374    }
375
376    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
377        broadcast use lemma_array_from_seq_roundtrip;
378
379        let (n, chunk) = Fixed::<U32_BYTE_LEN>.parse(ibuf)?;
380        assert(chunk@ == ibuf@[0..U32_BYTE_LEN]);
381
382        let bytes = [chunk[0], chunk[1], chunk[2], chunk[3]];
383        let value = u32_from_le_bytes(bytes);
384
385        assert(bytes@ == chunk@);
386
387        Ok((n, value))
388    }
389}
390
391impl<Output: OutputBuf> Serializer<Output, u32> for super::U32Le {
392    fn serialize_into(&self, v: &u32, obuf: &mut Output) {
393        let bytes = u32_to_le_bytes(*v);
394        obuf.write_bytes(&bytes);
395    }
396}
397
398impl ByteLen<u32> for super::U32Le {
399    fn length(&self, _v: &u32) -> (len: usize) {
400        U32_BYTE_LEN
401    }
402}
403
404impl Prepare<u32> for super::U32Le {
405    fn prepare(&self, _v: &u32) -> (checked: Result<usize, PreSerializeError>) {
406        Ok(U32_BYTE_LEN)
407    }
408}
409
410impl Parser<&[u8]> for super::U32Be {
411    type PT = u32;
412
413    fn min_byte_len(&self) -> usize {
414        U32_BYTE_LEN
415    }
416
417    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
418        broadcast use lemma_array_from_seq_roundtrip;
419
420        let (n, chunk) = Fixed::<U32_BYTE_LEN>.parse(ibuf)?;
421        assert(chunk@ == ibuf@[0..U32_BYTE_LEN]);
422
423        let bytes = [chunk[0], chunk[1], chunk[2], chunk[3]];
424        let value = u32_from_be_bytes(bytes);
425
426        assert(bytes@ == chunk@);
427
428        Ok((n, value))
429    }
430}
431
432impl<Output: OutputBuf> Serializer<Output, u32> for super::U32Be {
433    fn serialize_into(&self, v: &u32, obuf: &mut Output) {
434        let bytes = u32_to_be_bytes(*v);
435        obuf.write_bytes(&bytes);
436    }
437}
438
439impl ByteLen<u32> for super::U32Be {
440    fn length(&self, _v: &u32) -> (len: usize) {
441        U32_BYTE_LEN
442    }
443}
444
445impl Prepare<u32> for super::U32Be {
446    fn prepare(&self, _v: &u32) -> (checked: Result<usize, PreSerializeError>) {
447        Ok(U32_BYTE_LEN)
448    }
449}
450
451impl Parser<&[u8]> for super::U64Le {
452    type PT = u64;
453
454    fn min_byte_len(&self) -> usize {
455        U64_BYTE_LEN
456    }
457
458    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
459        broadcast use lemma_array_from_seq_roundtrip;
460
461        let (n, chunk) = Fixed::<U64_BYTE_LEN>.parse(ibuf)?;
462        assert(chunk@ == ibuf@[0..U64_BYTE_LEN]);
463
464        let bytes = [
465            chunk[0],
466            chunk[1],
467            chunk[2],
468            chunk[3],
469            chunk[4],
470            chunk[5],
471            chunk[6],
472            chunk[7],
473        ];
474        let value = u64_from_le_bytes(bytes);
475
476        assert(bytes@ == chunk@);
477
478        Ok((n, value))
479    }
480}
481
482impl<Output: OutputBuf> Serializer<Output, u64> for super::U64Le {
483    fn serialize_into(&self, v: &u64, obuf: &mut Output) {
484        let bytes = u64_to_le_bytes(*v);
485        obuf.write_bytes(&bytes);
486    }
487}
488
489impl ByteLen<u64> for super::U64Le {
490    fn length(&self, _v: &u64) -> (len: usize) {
491        U64_BYTE_LEN
492    }
493}
494
495impl Prepare<u64> for super::U64Le {
496    fn prepare(&self, _v: &u64) -> (checked: Result<usize, PreSerializeError>) {
497        Ok(U64_BYTE_LEN)
498    }
499}
500
501impl Parser<&[u8]> for super::U64Be {
502    type PT = u64;
503
504    fn min_byte_len(&self) -> usize {
505        U64_BYTE_LEN
506    }
507
508    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
509        broadcast use lemma_array_from_seq_roundtrip;
510
511        let (n, chunk) = Fixed::<U64_BYTE_LEN>.parse(ibuf)?;
512        assert(chunk@ == ibuf@[0..U64_BYTE_LEN]);
513
514        let bytes = [
515            chunk[0],
516            chunk[1],
517            chunk[2],
518            chunk[3],
519            chunk[4],
520            chunk[5],
521            chunk[6],
522            chunk[7],
523        ];
524        let value = u64_from_be_bytes(bytes);
525
526        assert(bytes@ == chunk@);
527
528        Ok((n, value))
529    }
530}
531
532impl<Output: OutputBuf> Serializer<Output, u64> for super::U64Be {
533    fn serialize_into(&self, v: &u64, obuf: &mut Output) {
534        let bytes = u64_to_be_bytes(*v);
535        obuf.write_bytes(&bytes);
536    }
537}
538
539impl ByteLen<u64> for super::U64Be {
540    fn length(&self, _v: &u64) -> (len: usize) {
541        U64_BYTE_LEN
542    }
543}
544
545impl Prepare<u64> for super::U64Be {
546    fn prepare(&self, _v: &u64) -> (checked: Result<usize, PreSerializeError>) {
547        Ok(U64_BYTE_LEN)
548    }
549}
550
551} // verus!
vest_lib/combinators/uints/exec.rs

vest_lib/combinators/uints/
exec.rs
