vest_lib/combinators/
length.rs

1//! The length abstraction [`AsLen`] for types usable as format length (or count) fields.
2//!
3//! Implemented for [`u8`], [`u16`], [`u32`], and [`usize`].
4use vstd::prelude::*;
5
6verus! {
7
8/// Types that can serve as format length (or count) fields.
9///
10/// The spec-facing conversion is to `nat`, which is the natural domain for lengths in proofs. The
11/// exec-facing conversion is to `usize`, which is the natural domain for runtime indexing.
12pub trait AsLen: Sized + Copy {
13    /// The mathematical length represented by this value.
14    spec fn as_nat(self) -> nat;
15
16    /// The runtime length represented by this value.
17    fn get(self) -> (len: usize)
18        ensures
19            len as nat == self.as_nat(),
20    ;
21
22    /// Construct from a `nat`.
23    spec fn as_self(n: nat) -> Self;
24
25    /// `as_self(v.as_nat()) == v`.
26    proof fn lemma_lossless_casting(v: Self)
27        ensures
28            Self::as_self(v.as_nat()) == v,
29    ;
30}
31
32} // verus!
33macro_rules! impl_as_len_for_uint {
34    ($ty:ty) => {
35        verus! {
36            impl AsLen for $ty {
37                open spec fn as_nat(self) -> nat {
38                    self as nat
39                }
40
41                fn get(self) -> (len: usize) {
42                    self as usize
43                }
44
45                open spec fn as_self(n: nat) -> Self {
46                    n as $ty
47                }
48
49                proof fn lemma_lossless_casting(v: Self) {
50                }
51            }
52        }
53    };
54}
55
56impl_as_len_for_uint!(u8);
57impl_as_len_for_uint!(u16);
58impl_as_len_for_uint!(u32);
59impl_as_len_for_uint!(usize);
60
61verus! {
62
63global size_of usize == 8;
64
65impl AsLen for u64 {
66    open spec fn as_nat(self) -> nat {
67        self as nat
68    }
69
70    fn get(self) -> (len: usize) {
71        self as usize
72    }
73
74    open spec fn as_self(n: nat) -> Self {
75        n as u64
76    }
77
78    proof fn lemma_lossless_casting(v: Self) {
79    }
80}
81
82impl<T: AsLen> AsLen for &T {
83    open spec fn as_nat(self) -> nat {
84        (*self).as_nat()
85    }
86
87    fn get(self) -> (len: usize) {
88        (*self).get()
89    }
90
91    open spec fn as_self(n: nat) -> Self {
92        &T::as_self(n)
93    }
94
95    proof fn lemma_lossless_casting(v: Self) {
96        T::lemma_lossless_casting(*v);
97    }
98}
99
100} // verus!
vest_lib/combinators/length.rs

vest_lib/combinators/
length.rs
