vest_lib/combinators/uints/
proof.rs

1//! Correctness proofs for fixed-width unsigned integers.
2use super::spec::*;
3use crate::combinators::bytes::spec::*;
4use crate::core::{proof::*, spec::*};
5use vstd::prelude::*;
6
7verus! {
8
9impl SPRoundTripDps for super::U8 {
10    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: u8, obuf: Seq<u8>) {
11        assert(self.spec_parse(self.spec_serialize_dps(v, obuf)) == Some((1int, v)));
12    }
13}
14
15impl NonMalleable for super::U8 {
16    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
17    }
18}
19
20impl NoLookAhead for super::U8 {
21    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
22        if let Some((n, v)) = self.spec_parse(i1) {
23            if 0 <= n <= i2.len() {
24                if i2.take(n) == i1.take(n) {
25                    assert(i2.take(1int)[0] == i1.take(1int)[0]);
26                    assert(self.spec_parse(i2) == Some((n, v)));
27                }
28            }
29        }
30    }
31}
32
33impl Productive for super::U8 {
34    proof fn lemma_productive(&self, s: Seq<u8>) {
35    }
36}
37
38impl EquivSerializersGeneral for super::U8 {
39    proof fn lemma_serialize_equiv(&self, v: u8, obuf: Seq<u8>) {
40    }
41}
42
43impl EquivSerializers for super::U8 {
44    proof fn lemma_serialize_equiv_on_empty(&self, v: u8) {
45    }
46}
47
48impl SPRoundTripDps for super::U16Le {
49    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: u16, obuf: Seq<u8>) {
50        broadcast use lemma_u16_le_value_roundtrip;
51        broadcast use lemma_array_from_seq_roundtrip;
52
53        u16_le_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
54    }
55}
56
57impl NonMalleable for super::U16Le {
58    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
59        broadcast use lemma_u16_le_bytes_roundtrip;
60        broadcast use axiom_array_from_seq;
61
62        u16_le_fmt().lemma_parse_non_malleable(buf1, buf2);
63    }
64}
65
66impl NoLookAhead for super::U16Le {
67    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
68        u16_le_fmt().lemma_no_lookahead(i1, i2);
69    }
70}
71
72impl Productive for super::U16Le {
73    proof fn lemma_productive(&self, s: Seq<u8>) {
74        u16_le_fmt().lemma_productive(s);
75    }
76}
77
78impl EquivSerializersGeneral for super::U16Le {
79    proof fn lemma_serialize_equiv(&self, v: u16, obuf: Seq<u8>) {
80        u16_le_fmt().lemma_serialize_equiv(v, obuf);
81    }
82}
83
84impl EquivSerializers for super::U16Le {
85    proof fn lemma_serialize_equiv_on_empty(&self, v: u16) {
86        u16_le_fmt().lemma_serialize_equiv_on_empty(v);
87    }
88}
89
90impl SPRoundTripDps for super::U16Be {
91    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: u16, obuf: Seq<u8>) {
92        broadcast use lemma_array_from_seq_roundtrip;
93        broadcast use lemma_u16_be_value_roundtrip;
94
95        u16_be_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
96    }
97}
98
99impl NonMalleable for super::U16Be {
100    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
101        broadcast use axiom_array_from_seq;
102        broadcast use lemma_u16_be_bytes_roundtrip;
103
104        u16_be_fmt().lemma_parse_non_malleable(buf1, buf2);
105    }
106}
107
108impl NoLookAhead for super::U16Be {
109    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
110        u16_be_fmt().lemma_no_lookahead(i1, i2);
111    }
112}
113
114impl Productive for super::U16Be {
115    proof fn lemma_productive(&self, s: Seq<u8>) {
116        u16_be_fmt().lemma_productive(s);
117    }
118}
119
120impl EquivSerializersGeneral for super::U16Be {
121    proof fn lemma_serialize_equiv(&self, v: u16, obuf: Seq<u8>) {
122        u16_be_fmt().lemma_serialize_equiv(v, obuf);
123    }
124}
125
126impl EquivSerializers for super::U16Be {
127    proof fn lemma_serialize_equiv_on_empty(&self, v: u16) {
128        u16_be_fmt().lemma_serialize_equiv_on_empty(v);
129    }
130}
131
132impl SPRoundTripDps for super::U24Le {
133    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: u32, obuf: Seq<u8>) {
134        broadcast use lemma_array_from_seq_roundtrip;
135        broadcast use lemma_u24_le_value_roundtrip;
136
137        u24_le_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
138    }
139}
140
141impl NonMalleable for super::U24Le {
142    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
143        broadcast use axiom_array_from_seq;
144        broadcast use lemma_u24_le_bytes_roundtrip;
145
146        u24_le_fmt().lemma_parse_non_malleable(buf1, buf2);
147    }
148}
149
150impl NoLookAhead for super::U24Le {
151    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
152        u24_le_fmt().lemma_no_lookahead(i1, i2);
153    }
154}
155
156impl Productive for super::U24Le {
157    proof fn lemma_productive(&self, s: Seq<u8>) {
158        u24_le_fmt().lemma_productive(s);
159    }
160}
161
162impl EquivSerializersGeneral for super::U24Le {
163    proof fn lemma_serialize_equiv(&self, v: u32, obuf: Seq<u8>) {
164        u24_le_fmt().lemma_serialize_equiv(v, obuf);
165    }
166}
167
168impl EquivSerializers for super::U24Le {
169    proof fn lemma_serialize_equiv_on_empty(&self, v: u32) {
170        u24_le_fmt().lemma_serialize_equiv_on_empty(v);
171    }
172}
173
174impl SPRoundTripDps for super::U24Be {
175    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: u32, obuf: Seq<u8>) {
176        broadcast use lemma_array_from_seq_roundtrip;
177        broadcast use lemma_u24_be_value_roundtrip;
178
179        u24_be_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
180    }
181}
182
183impl NonMalleable for super::U24Be {
184    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
185        broadcast use axiom_array_from_seq;
186        broadcast use lemma_u24_be_bytes_roundtrip;
187
188        u24_be_fmt().lemma_parse_non_malleable(buf1, buf2);
189    }
190}
191
192impl NoLookAhead for super::U24Be {
193    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
194        u24_be_fmt().lemma_no_lookahead(i1, i2);
195    }
196}
197
198impl Productive for super::U24Be {
199    proof fn lemma_productive(&self, s: Seq<u8>) {
200        u24_be_fmt().lemma_productive(s);
201    }
202}
203
204impl EquivSerializersGeneral for super::U24Be {
205    proof fn lemma_serialize_equiv(&self, v: u32, obuf: Seq<u8>) {
206        u24_be_fmt().lemma_serialize_equiv(v, obuf);
207    }
208}
209
210impl EquivSerializers for super::U24Be {
211    proof fn lemma_serialize_equiv_on_empty(&self, v: u32) {
212        u24_be_fmt().lemma_serialize_equiv_on_empty(v);
213    }
214}
215
216impl SPRoundTripDps for super::U32Le {
217    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: u32, obuf: Seq<u8>) {
218        broadcast use lemma_array_from_seq_roundtrip;
219        broadcast use lemma_u32_le_value_roundtrip;
220
221        u32_le_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
222    }
223}
224
225impl NonMalleable for super::U32Le {
226    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
227        broadcast use axiom_array_from_seq;
228        broadcast use lemma_u32_le_bytes_roundtrip;
229
230        u32_le_fmt().lemma_parse_non_malleable(buf1, buf2);
231    }
232}
233
234impl NoLookAhead for super::U32Le {
235    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
236        u32_le_fmt().lemma_no_lookahead(i1, i2);
237    }
238}
239
240impl Productive for super::U32Le {
241    proof fn lemma_productive(&self, s: Seq<u8>) {
242        u32_le_fmt().lemma_productive(s);
243    }
244}
245
246impl EquivSerializersGeneral for super::U32Le {
247    proof fn lemma_serialize_equiv(&self, v: u32, obuf: Seq<u8>) {
248        u32_le_fmt().lemma_serialize_equiv(v, obuf);
249    }
250}
251
252impl EquivSerializers for super::U32Le {
253    proof fn lemma_serialize_equiv_on_empty(&self, v: u32) {
254        u32_le_fmt().lemma_serialize_equiv_on_empty(v);
255    }
256}
257
258impl SPRoundTripDps for super::U32Be {
259    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: u32, obuf: Seq<u8>) {
260        broadcast use lemma_array_from_seq_roundtrip;
261        broadcast use lemma_u32_be_value_roundtrip;
262
263        u32_be_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
264    }
265}
266
267impl NonMalleable for super::U32Be {
268    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
269        broadcast use axiom_array_from_seq;
270        broadcast use lemma_u32_be_bytes_roundtrip;
271
272        u32_be_fmt().lemma_parse_non_malleable(buf1, buf2);
273    }
274}
275
276impl NoLookAhead for super::U32Be {
277    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
278        u32_be_fmt().lemma_no_lookahead(i1, i2);
279    }
280}
281
282impl Productive for super::U32Be {
283    proof fn lemma_productive(&self, s: Seq<u8>) {
284        u32_be_fmt().lemma_productive(s);
285    }
286}
287
288impl EquivSerializersGeneral for super::U32Be {
289    proof fn lemma_serialize_equiv(&self, v: u32, obuf: Seq<u8>) {
290        u32_be_fmt().lemma_serialize_equiv(v, obuf);
291    }
292}
293
294impl EquivSerializers for super::U32Be {
295    proof fn lemma_serialize_equiv_on_empty(&self, v: u32) {
296        u32_be_fmt().lemma_serialize_equiv_on_empty(v);
297    }
298}
299
300impl SPRoundTripDps for super::U64Le {
301    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: u64, obuf: Seq<u8>) {
302        broadcast use lemma_array_from_seq_roundtrip;
303        broadcast use lemma_u64_le_value_roundtrip;
304
305        u64_le_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
306    }
307}
308
309impl NonMalleable for super::U64Le {
310    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
311        broadcast use axiom_array_from_seq;
312        broadcast use lemma_u64_le_bytes_roundtrip;
313
314        u64_le_fmt().lemma_parse_non_malleable(buf1, buf2);
315    }
316}
317
318impl NoLookAhead for super::U64Le {
319    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
320        u64_le_fmt().lemma_no_lookahead(i1, i2);
321    }
322}
323
324impl Productive for super::U64Le {
325    proof fn lemma_productive(&self, s: Seq<u8>) {
326        u64_le_fmt().lemma_productive(s);
327    }
328}
329
330impl EquivSerializersGeneral for super::U64Le {
331    proof fn lemma_serialize_equiv(&self, v: u64, obuf: Seq<u8>) {
332        u64_le_fmt().lemma_serialize_equiv(v, obuf);
333    }
334}
335
336impl EquivSerializers for super::U64Le {
337    proof fn lemma_serialize_equiv_on_empty(&self, v: u64) {
338        u64_le_fmt().lemma_serialize_equiv_on_empty(v);
339    }
340}
341
342impl SPRoundTripDps for super::U64Be {
343    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: u64, obuf: Seq<u8>) {
344        broadcast use lemma_array_from_seq_roundtrip;
345        broadcast use lemma_u64_be_value_roundtrip;
346
347        u64_be_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
348    }
349}
350
351impl NonMalleable for super::U64Be {
352    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
353        broadcast use axiom_array_from_seq;
354        broadcast use lemma_u64_be_bytes_roundtrip;
355
356        u64_be_fmt().lemma_parse_non_malleable(buf1, buf2);
357    }
358}
359
360impl NoLookAhead for super::U64Be {
361    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
362        u64_be_fmt().lemma_no_lookahead(i1, i2);
363    }
364}
365
366impl Productive for super::U64Be {
367    proof fn lemma_productive(&self, s: Seq<u8>) {
368        u64_be_fmt().lemma_productive(s);
369    }
370}
371
372impl EquivSerializersGeneral for super::U64Be {
373    proof fn lemma_serialize_equiv(&self, v: u64, obuf: Seq<u8>) {
374        u64_be_fmt().lemma_serialize_equiv(v, obuf);
375    }
376}
377
378impl EquivSerializers for super::U64Be {
379    proof fn lemma_serialize_equiv_on_empty(&self, v: u64) {
380        u64_be_fmt().lemma_serialize_equiv_on_empty(v);
381    }
382}
383
384} // verus!
vest_lib/combinators/uints/proof.rs

vest_lib/combinators/uints/
proof.rs
