vest_lib/combinators/sints/
proof.rs

1//! Correctness proofs for fixed-width signed integers.
2use vstd::prelude::*;
3
4verus! {
5
6use crate::core::{proof::*, spec::*};
7use crate::combinators::sints::spec::*;
8use crate::combinators::bytes::spec::*;
9
10impl SPRoundTripDps for super::I8 {
11    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: i8, obuf: Seq<u8>) {
12        broadcast use lemma_i8_value_roundtrip;
13
14        i8_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
15    }
16}
17
18impl NonMalleable for super::I8 {
19    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
20        broadcast use lemma_i8_seq_roundtrip;
21
22        i8_fmt().lemma_parse_non_malleable(buf1, buf2);
23    }
24}
25
26impl NoLookAhead for super::I8 {
27    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
28        i8_fmt().lemma_no_lookahead(i1, i2);
29    }
30}
31
32impl Productive for super::I8 {
33    proof fn lemma_productive(&self, s: Seq<u8>) {
34        i8_fmt().lemma_productive(s);
35    }
36}
37
38impl EquivSerializersGeneral for super::I8 {
39    proof fn lemma_serialize_equiv(&self, v: i8, obuf: Seq<u8>) {
40        i8_fmt().lemma_serialize_equiv(v, obuf);
41    }
42}
43
44impl EquivSerializers for super::I8 {
45    proof fn lemma_serialize_equiv_on_empty(&self, v: i8) {
46        i8_fmt().lemma_serialize_equiv_on_empty(v);
47    }
48}
49
50impl SPRoundTripDps for super::I16Le {
51    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: i16, obuf: Seq<u8>) {
52        broadcast use lemma_array_from_seq_roundtrip;
53        broadcast use lemma_i16_le_value_roundtrip;
54
55        i16_le_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
56    }
57}
58
59impl NonMalleable for super::I16Le {
60    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
61        broadcast use axiom_array_from_seq;
62        broadcast use lemma_i16_le_bytes_roundtrip;
63
64        i16_le_fmt().lemma_parse_non_malleable(buf1, buf2);
65    }
66}
67
68impl NoLookAhead for super::I16Le {
69    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
70        i16_le_fmt().lemma_no_lookahead(i1, i2);
71    }
72}
73
74impl Productive for super::I16Le {
75    proof fn lemma_productive(&self, s: Seq<u8>) {
76        i16_le_fmt().lemma_productive(s);
77    }
78}
79
80impl EquivSerializersGeneral for super::I16Le {
81    proof fn lemma_serialize_equiv(&self, v: i16, obuf: Seq<u8>) {
82        i16_le_fmt().lemma_serialize_equiv(v, obuf);
83    }
84}
85
86impl EquivSerializers for super::I16Le {
87    proof fn lemma_serialize_equiv_on_empty(&self, v: i16) {
88        i16_le_fmt().lemma_serialize_equiv_on_empty(v);
89    }
90}
91
92impl SPRoundTripDps for super::I16Be {
93    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: i16, obuf: Seq<u8>) {
94        broadcast use lemma_array_from_seq_roundtrip;
95        broadcast use lemma_i16_be_value_roundtrip;
96
97        i16_be_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
98    }
99}
100
101impl NonMalleable for super::I16Be {
102    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
103        broadcast use axiom_array_from_seq;
104        broadcast use lemma_i16_be_bytes_roundtrip;
105
106        i16_be_fmt().lemma_parse_non_malleable(buf1, buf2);
107    }
108}
109
110impl NoLookAhead for super::I16Be {
111    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
112        i16_be_fmt().lemma_no_lookahead(i1, i2);
113    }
114}
115
116impl Productive for super::I16Be {
117    proof fn lemma_productive(&self, s: Seq<u8>) {
118        i16_be_fmt().lemma_productive(s);
119    }
120}
121
122impl EquivSerializersGeneral for super::I16Be {
123    proof fn lemma_serialize_equiv(&self, v: i16, obuf: Seq<u8>) {
124        i16_be_fmt().lemma_serialize_equiv(v, obuf);
125    }
126}
127
128impl EquivSerializers for super::I16Be {
129    proof fn lemma_serialize_equiv_on_empty(&self, v: i16) {
130        i16_be_fmt().lemma_serialize_equiv_on_empty(v);
131    }
132}
133
134impl SPRoundTripDps for super::I32Le {
135    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: i32, obuf: Seq<u8>) {
136        broadcast use lemma_array_from_seq_roundtrip;
137        broadcast use lemma_i32_le_value_roundtrip;
138
139        i32_le_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
140    }
141}
142
143impl NonMalleable for super::I32Le {
144    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
145        broadcast use axiom_array_from_seq;
146        broadcast use lemma_i32_le_bytes_roundtrip;
147
148        i32_le_fmt().lemma_parse_non_malleable(buf1, buf2);
149    }
150}
151
152impl NoLookAhead for super::I32Le {
153    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
154        i32_le_fmt().lemma_no_lookahead(i1, i2);
155    }
156}
157
158impl Productive for super::I32Le {
159    proof fn lemma_productive(&self, s: Seq<u8>) {
160        i32_le_fmt().lemma_productive(s);
161    }
162}
163
164impl EquivSerializersGeneral for super::I32Le {
165    proof fn lemma_serialize_equiv(&self, v: i32, obuf: Seq<u8>) {
166        i32_le_fmt().lemma_serialize_equiv(v, obuf);
167    }
168}
169
170impl EquivSerializers for super::I32Le {
171    proof fn lemma_serialize_equiv_on_empty(&self, v: i32) {
172        i32_le_fmt().lemma_serialize_equiv_on_empty(v);
173    }
174}
175
176impl SPRoundTripDps for super::I32Be {
177    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: i32, obuf: Seq<u8>) {
178        broadcast use lemma_array_from_seq_roundtrip;
179        broadcast use lemma_i32_be_value_roundtrip;
180
181        i32_be_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
182    }
183}
184
185impl NonMalleable for super::I32Be {
186    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
187        broadcast use axiom_array_from_seq;
188        broadcast use lemma_i32_be_bytes_roundtrip;
189
190        i32_be_fmt().lemma_parse_sound_consumption(buf1);  // triggers axiom_array_from_seq
191        i32_be_fmt().lemma_parse_non_malleable(buf1, buf2);
192    }
193}
194
195impl NoLookAhead for super::I32Be {
196    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
197        i32_be_fmt().lemma_no_lookahead(i1, i2);
198    }
199}
200
201impl Productive for super::I32Be {
202    proof fn lemma_productive(&self, s: Seq<u8>) {
203        i32_be_fmt().lemma_productive(s);
204    }
205}
206
207impl EquivSerializersGeneral for super::I32Be {
208    proof fn lemma_serialize_equiv(&self, v: i32, obuf: Seq<u8>) {
209        i32_be_fmt().lemma_serialize_equiv(v, obuf);
210    }
211}
212
213impl EquivSerializers for super::I32Be {
214    proof fn lemma_serialize_equiv_on_empty(&self, v: i32) {
215        i32_be_fmt().lemma_serialize_equiv_on_empty(v);
216    }
217}
218
219impl SPRoundTripDps for super::I64Le {
220    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: i64, obuf: Seq<u8>) {
221        broadcast use lemma_array_from_seq_roundtrip;
222        broadcast use lemma_i64_le_value_roundtrip;
223
224        i64_le_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
225    }
226}
227
228impl NonMalleable for super::I64Le {
229    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
230        broadcast use axiom_array_from_seq;
231        broadcast use lemma_i64_le_bytes_roundtrip;
232
233        i64_le_fmt().lemma_parse_non_malleable(buf1, buf2);
234    }
235}
236
237impl NoLookAhead for super::I64Le {
238    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
239        i64_le_fmt().lemma_no_lookahead(i1, i2);
240    }
241}
242
243impl Productive for super::I64Le {
244    proof fn lemma_productive(&self, s: Seq<u8>) {
245        i64_le_fmt().lemma_productive(s);
246    }
247}
248
249impl EquivSerializersGeneral for super::I64Le {
250    proof fn lemma_serialize_equiv(&self, v: i64, obuf: Seq<u8>) {
251        i64_le_fmt().lemma_serialize_equiv(v, obuf);
252    }
253}
254
255impl EquivSerializers for super::I64Le {
256    proof fn lemma_serialize_equiv_on_empty(&self, v: i64) {
257        i64_le_fmt().lemma_serialize_equiv_on_empty(v);
258    }
259}
260
261impl SPRoundTripDps for super::I64Be {
262    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: i64, obuf: Seq<u8>) {
263        broadcast use lemma_array_from_seq_roundtrip;
264        broadcast use lemma_i64_be_value_roundtrip;
265
266        i64_be_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
267    }
268}
269
270impl NonMalleable for super::I64Be {
271    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
272        broadcast use axiom_array_from_seq;
273        broadcast use lemma_i64_be_bytes_roundtrip;
274
275        i64_be_fmt().lemma_parse_non_malleable(buf1, buf2);
276    }
277}
278
279impl NoLookAhead for super::I64Be {
280    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
281        i64_be_fmt().lemma_no_lookahead(i1, i2);
282    }
283}
284
285impl Productive for super::I64Be {
286    proof fn lemma_productive(&self, s: Seq<u8>) {
287        i64_be_fmt().lemma_productive(s);
288    }
289}
290
291impl EquivSerializersGeneral for super::I64Be {
292    proof fn lemma_serialize_equiv(&self, v: i64, obuf: Seq<u8>) {
293        i64_be_fmt().lemma_serialize_equiv(v, obuf);
294    }
295}
296
297impl EquivSerializers for super::I64Be {
298    proof fn lemma_serialize_equiv_on_empty(&self, v: i64) {
299        i64_be_fmt().lemma_serialize_equiv_on_empty(v);
300    }
301}
302
303} // verus!
vest_lib/combinators/sints/proof.rs

vest_lib/combinators/sints/
proof.rs
