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