vest_lib/combinators/sints/
mod.rs

1//! Fixed-width signed integer combinators.
2//!
3//! These parse and serialize two's-complement integers in explicit little- or
4//! big-endian byte order.
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/// Signed 8-bit integer combinator.
18///
19/// Defined as `Mapped { inner: Fixed::<1>, mapper: (i8_from_bytes, i8_to_bytes) }`.
20#[derive(Clone, Copy)]
21pub struct I8;
22
23/// Little-endian signed 16-bit integer.
24///
25/// Defined as `Mapped { inner: Fixed::<2>, mapper: (i16_le_from_bytes, i16_le_to_bytes) }`.
26#[derive(Clone, Copy)]
27pub struct I16Le;
28
29/// Big-endian signed 16-bit integer.
30///
31/// Defined as `Mapped { inner: Fixed::<2>, mapper: (i16_be_from_bytes, i16_be_to_bytes) }`.
32#[derive(Clone, Copy)]
33pub struct I16Be;
34
35/// Little-endian signed 32-bit integer.
36///
37/// Defined as `Mapped { inner: Fixed::<4>, mapper: (i32_le_from_bytes, i32_le_to_bytes) }`.
38#[derive(Clone, Copy)]
39pub struct I32Le;
40
41/// Big-endian signed 32-bit integer.
42///
43/// Defined as `Mapped { inner: Fixed::<4>, mapper: (i32_be_from_bytes, i32_be_to_bytes) }`.
44#[derive(Clone, Copy)]
45pub struct I32Be;
46
47/// Little-endian signed 64-bit integer.
48///
49/// Defined as `Mapped { inner: Fixed::<8>, mapper: (i64_le_from_bytes, i64_le_to_bytes) }`.
50#[derive(Clone, Copy)]
51pub struct I64Le;
52
53/// Big-endian signed 64-bit integer.
54///
55/// Defined as `Mapped { inner: Fixed::<8>, mapper: (i64_be_from_bytes, i64_be_to_bytes) }`.
56#[derive(Clone, Copy)]
57pub struct I64Be;
58
59impl LeafNonMalleable for I8 {
60    proof fn nonmal_leaf_inv(&self) {
61    }
62}
63
64impl LeafNonMalleable for I16Le {
65    proof fn nonmal_leaf_inv(&self) {
66    }
67}
68
69impl LeafNonMalleable for I16Be {
70    proof fn nonmal_leaf_inv(&self) {
71    }
72}
73
74impl LeafNonMalleable for I32Le {
75    proof fn nonmal_leaf_inv(&self) {
76    }
77}
78
79impl LeafNonMalleable for I32Be {
80    proof fn nonmal_leaf_inv(&self) {
81    }
82}
83
84impl LeafNonMalleable for I64Le {
85    proof fn nonmal_leaf_inv(&self) {
86    }
87}
88
89impl LeafNonMalleable for I64Be {
90    proof fn nonmal_leaf_inv(&self) {
91    }
92}
93
94} // verus!
vest_lib/combinators/sints/mod.rs

vest_lib/combinators/sints/
mod.rs
