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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
pub use crate::utils::*;
// use core::rc::Rc;
use alloc::vec::Vec;
use vstd::prelude::*;
use vstd::slice::*;
use vstd::*;
verus! {
//////////////////////////////////////////////////////////////////////////////
/// Trait definitions
/// Trait for types that can be used as input for Vest parsers, roughly corresponding to byte buffers.
/// `VestInput` does not expose the contents of the buffer, so opaque buffer types for side-channel
/// security can implement `VestInput`.
pub trait VestInput: View<V = Seq<u8>> {
/// The length of the buffer.
fn len(&self) -> (res: usize)
ensures
res == self@.len(),
;
/// Analogous to `vstd::slice_subrange`
fn subrange(&self, i: usize, j: usize) -> (res: Self) where Self: Sized
requires
0 <= i <= j <= self@.len(),
ensures
res@ == self@.subrange(i as int, j as int),
;
/// Creates another buffer with the same contents.
/// For good performance, this function should be cheap, just creating a new reference rather than
/// actually copying the buffer.
fn clone(&self) -> (res: Self) where Self: Sized
ensures
res@ == self@,
;
}
/// Trait for types that can be used as input for Vest parsers, roughly corresponding to byte buffers.
/// `VestPublicInput` can be set using transparent bytes, so it cannot provide type abstraction for side-channel security.
pub trait VestPublicInput: VestInput {
/// Returns a byte slice with the contents of the buffer
fn as_byte_slice(&self) -> (res: &[u8])
ensures
res@ == self@,
;
}
/// Trait for types that can be used as output for Vest serializers.
/// `VestOutput` does not expose the contents of the buffer, so opaque buffer types for side-channel
/// security can implement `VestOutput`.
pub trait VestOutput<I>: View<V = Seq<u8>> where I: View<V = Seq<u8>> {
/// The length of the buffer.
fn len(&self) -> (res: usize)
ensures
res == self@.len(),
;
/// Copy `input` to `self` starting at index `i`.
fn set_range(&mut self, i: usize, input: &I) -> (res: ())
requires
0 <= i + input@.len() <= old(self)@.len() <= usize::MAX,
ensures
final(self)@.len() == old(self)@.len() && final(self)@ == old(self)@.subrange(0, i as int).add(
input@,
).add(old(self)@.subrange(i + input@.len(), final(self)@.len() as int)),
;
}
/// Trait for types that can be used as output for Vest serializers.
/// `VestPublicOutput` can be set using transparent bytes, so it cannot provide type abstraction for side-channel security.
pub trait VestPublicOutput<I>: VestOutput<I> where I: View<V = Seq<u8>> {
/// Set the byte at index `i` to `value`.
fn set_byte(&mut self, i: usize, value: u8)
requires
i < old(self)@.len(),
ensures
final(self)@ == old(self)@.update(i as int, value),
;
/// Copy `input` to `self` starting at index `i`. (Same as `set_range` but with byte slice input.)
fn set_byte_range(&mut self, i: usize, input: &[u8]) -> (res: ())
requires
0 <= i + input@.len() <= old(self)@.len() <= usize::MAX,
ensures
final(self)@.len() == old(self)@.len() && final(self)@ == old(self)@.subrange(0, i as int).add(
input@,
).add(old(self)@.subrange(i + input@.len(), final(self)@.len() as int)),
;
}
//////////////////////////////////////////////////////////////////////////////
/// Implementations for common types
impl<'a> VestInput for &'a [u8] {
fn len(&self) -> usize {
<[u8]>::len(self)
}
fn subrange(&self, i: usize, j: usize) -> &'a [u8] {
slice_subrange(*self, i, j)
}
fn clone(&self) -> &'a [u8] {
*self
}
}
impl<'a> VestPublicInput for &'a [u8] {
fn as_byte_slice(&self) -> &[u8] {
*self
}
}
// /// Provided to demonstrate flexibility of the trait, but likely should not be used,
// /// since this impl copies the `Vec` every time you call `subrange` or `clone`.
// impl VestSecretInput for Vec<u8> {
// fn len(&self) -> usize {
// Vec::len(self)
// }
// fn subrange(&self, i: usize, j: usize) -> Vec<u8> {
// let mut res = Vec::new();
// vec_u8_extend_from_slice(&mut res, slice_subrange(self.as_slice(), i, j));
// proof {
// assert_seqs_equal!(res@, self@.subrange(i as int, j as int));
// }
// res
// }
// fn clone(&self) -> Vec<u8> {
// Clone::clone(self)
// }
// }
// impl VestInput for Vec<u8> {
// fn as_byte_slice(&self) -> &[u8] {
// self.as_slice()
// }
// }
// /// Provided to demonstrate flexibility of the trait, but likely should not be used,
// /// since this impl copies the `Vec` every time you call `subrange` or `clone`.
// impl VestSecretInput for Rc<Vec<u8>> {
// fn len(&self) -> usize {
// Vec::len(self)
// }
// fn subrange(&self, i: usize, j: usize) -> Rc<Vec<u8>> {
// let mut res = Vec::new();
// vec_u8_extend_from_slice(&mut res, slice_subrange(self.as_slice(), i, j));
// proof {
// assert_seqs_equal!(res@, self@.subrange(i as int, j as int));
// }
// Rc::new(res)
// }
// fn clone(&self) -> Rc<Vec<u8>> {
// Clone::clone(self)
// }
// }
// impl VestInput for Rc<Vec<u8>> {
// fn as_byte_slice(&self) -> &[u8] {
// self.as_slice()
// }
// }
impl<I> VestOutput<I> for Vec<u8> where I: VestPublicInput {
fn len(&self) -> usize {
Vec::len(self)
}
fn set_range(&mut self, i: usize, input: &I) {
set_range(self, i, input.as_byte_slice());
}
}
impl<I> VestPublicOutput<I> for Vec<u8> where I: VestPublicInput {
fn set_byte(&mut self, i: usize, value: u8) {
self.set(i, value);
}
fn set_byte_range(&mut self, i: usize, input: &[u8]) {
set_range(self, i, input);
}
}
} // verus!