vest_lib/combinators/uints/
mod.rs

1//! Fixed-width unsigned integer combinators.
2//!
3//! The exported zero-sized formats cover 8-, 16-, 24-, 32-, and 64-bit values
4//! with explicit little- or big-endian order and allocation-free execution.
5/// Executable trait implementations for this combinator.
6pub mod exec;
7/// Correctness proofs for this combinator.
8pub mod proof;
9/// Specification trait implementations for this combinator.
10pub mod spec;
11
12use crate::core::proof::LeafNonMalleable;
13use vstd::prelude::*;
14
15verus! {
16
17/// Unsigned 8-bit integer combinator.
18///
19/// Defined as `Mapped { inner: Fixed::<1>, mapper: (u8_from_bytes, u8_to_bytes) }`.
20#[derive(Clone, Copy)]
21pub struct U8;
22
23/// Little-endian unsigned 16-bit integer.
24///
25/// Defined as `Mapped { inner: Fixed::<2>, mapper: (u16_le_from_bytes, u16_le_to_bytes) }`.
26#[derive(Clone, Copy)]
27pub struct U16Le;
28
29/// Big-endian unsigned 16-bit integer.
30///
31/// Defined as `Mapped { inner: Fixed::<2>, mapper: (u16_be_from_bytes, u16_be_to_bytes) }`.
32#[derive(Clone, Copy)]
33pub struct U16Be;
34
35/// Little-endian unsigned 24-bit integer, represented as `u32`.
36///
37/// Defined as `Mapped { inner: Fixed::<3>, mapper: (u24_le_from_bytes, u24_le_to_bytes) }`.
38#[derive(Clone, Copy)]
39pub struct U24Le;
40
41/// Big-endian unsigned 24-bit integer, represented as `u32`.
42///
43/// Defined as `Mapped { inner: Fixed::<3>, mapper: (u24_be_from_bytes, u24_be_to_bytes) }`.
44#[derive(Clone, Copy)]
45pub struct U24Be;
46
47/// Little-endian unsigned 32-bit integer.
48///
49/// Defined as `Mapped { inner: Fixed::<4>, mapper: (u32_le_from_bytes, u32_le_to_bytes) }`.
50#[derive(Clone, Copy)]
51pub struct U32Le;
52
53/// Big-endian unsigned 32-bit integer.
54///
55/// Defined as `Mapped { inner: Fixed::<4>, mapper: (u32_be_from_bytes, u32_be_to_bytes) }`.
56#[derive(Clone, Copy)]
57pub struct U32Be;
58
59/// Little-endian unsigned 64-bit integer.
60///
61/// Defined as `Mapped { inner: Fixed::<8>, mapper: (u64_le_from_bytes, u64_le_to_bytes) }`.
62#[derive(Clone, Copy)]
63pub struct U64Le;
64
65/// Big-endian unsigned 64-bit integer.
66///
67/// Defined as `Mapped { inner: Fixed::<8>, mapper: (u64_be_from_bytes, u64_be_to_bytes) }`.
68#[derive(Clone, Copy)]
69pub struct U64Be;
70
71impl LeafNonMalleable for U8 {
72    proof fn nonmal_leaf_inv(&self) {
73    }
74}
75
76impl LeafNonMalleable for U16Le {
77    proof fn nonmal_leaf_inv(&self) {
78    }
79}
80
81impl LeafNonMalleable for U16Be {
82    proof fn nonmal_leaf_inv(&self) {
83    }
84}
85
86impl LeafNonMalleable for U24Le {
87    proof fn nonmal_leaf_inv(&self) {
88    }
89}
90
91impl LeafNonMalleable for U24Be {
92    proof fn nonmal_leaf_inv(&self) {
93    }
94}
95
96impl LeafNonMalleable for U32Le {
97    proof fn nonmal_leaf_inv(&self) {
98    }
99}
100
101impl LeafNonMalleable for U32Be {
102    proof fn nonmal_leaf_inv(&self) {
103    }
104}
105
106impl LeafNonMalleable for U64Le {
107    proof fn nonmal_leaf_inv(&self) {
108    }
109}
110
111impl LeafNonMalleable for U64Be {
112    proof fn nonmal_leaf_inv(&self) {
113    }
114}
115
116} // verus!
vest_lib/combinators/uints/mod.rs

vest_lib/combinators/uints/
mod.rs
