vest_lib/combinators/uints/
spec.rs

1//! Specifications for fixed-width unsigned integers.
2use crate::combinators::bytes::spec::*;
3use crate::combinators::mapped::spec::{FnSpecMapper, LosslessMapper, LossyMapper, SpecMapper};
4use crate::combinators::{Fixed, Mapped};
5use crate::core::{proof::*, spec::*};
6use vstd::prelude::*;
7
8verus! {
9
10pub const U8_BYTE_LEN: usize = 1;
11
12pub const U16_BYTE_LEN: usize = 2;
13
14pub const U24_BYTE_LEN: usize = 3;
15
16pub const U32_BYTE_LEN: usize = 4;
17
18pub const U64_BYTE_LEN: usize = 8;
19
20pub type U16LeFmt = Mapped<Fixed<2>, FnSpecMapper<Seq<u8>, u16>>;
21
22pub type U16BeFmt = Mapped<Fixed<2>, FnSpecMapper<Seq<u8>, u16>>;
23
24pub struct U24LeMapper;
25
26pub struct U24BeMapper;
27
28pub type U24LeFmt = Mapped<Fixed<3>, U24LeMapper>;
29
30pub type U24BeFmt = Mapped<Fixed<3>, U24BeMapper>;
31
32pub type U32LeFmt = Mapped<Fixed<4>, FnSpecMapper<Seq<u8>, u32>>;
33
34pub type U32BeFmt = Mapped<Fixed<4>, FnSpecMapper<Seq<u8>, u32>>;
35
36pub type U64LeFmt = Mapped<Fixed<8>, FnSpecMapper<Seq<u8>, u64>>;
37
38pub type U64BeFmt = Mapped<Fixed<8>, FnSpecMapper<Seq<u8>, u64>>;
39
40pub open spec fn u16_le_fmt() -> U16LeFmt {
41    Mapped {
42        inner: Fixed::<2>,
43        mapper: (|i: Seq<u8>| u16_le_from_bytes(array_from_seq(i)), |o: u16| u16_le_to_bytes(o)@),
44    }
45}
46
47pub open spec fn u16_be_fmt() -> U16BeFmt {
48    Mapped {
49        inner: Fixed::<2>,
50        mapper: (|i: Seq<u8>| u16_be_from_bytes(array_from_seq(i)), |o: u16| u16_be_to_bytes(o)@),
51    }
52}
53
54pub open spec fn u24_le_fmt() -> U24LeFmt {
55    Mapped { inner: Fixed::<3>, mapper: U24LeMapper }
56}
57
58pub open spec fn u24_be_fmt() -> U24BeFmt {
59    Mapped { inner: Fixed::<3>, mapper: U24BeMapper }
60}
61
62pub open spec fn u32_le_fmt() -> U32LeFmt {
63    Mapped {
64        inner: Fixed::<4>,
65        mapper: (|i: Seq<u8>| u32_le_from_bytes(array_from_seq(i)), |o: u32| u32_le_to_bytes(o)@),
66    }
67}
68
69pub open spec fn u32_be_fmt() -> U32BeFmt {
70    Mapped {
71        inner: Fixed::<4>,
72        mapper: (|i: Seq<u8>| u32_be_from_bytes(array_from_seq(i)), |o: u32| u32_be_to_bytes(o)@),
73    }
74}
75
76pub open spec fn u64_le_fmt() -> U64LeFmt {
77    Mapped {
78        inner: Fixed::<8>,
79        mapper: (|i: Seq<u8>| u64_le_from_bytes(array_from_seq(i)), |o: u64| u64_le_to_bytes(o)@),
80    }
81}
82
83pub open spec fn u64_be_fmt() -> U64BeFmt {
84    Mapped {
85        inner: Fixed::<8>,
86        mapper: (|i: Seq<u8>| u64_be_from_bytes(array_from_seq(i)), |o: u64| u64_be_to_bytes(o)@),
87    }
88}
89
90pub open spec fn u16_le_from_bytes(i: [u8; 2]) -> u16 {
91    (i[0] as u16) | (i[1] as u16) << 8
92}
93
94pub open spec fn u16_le_to_bytes(o: u16) -> [u8; 2] {
95    [(o & 0xff) as u8, ((o >> 8) & 0xff) as u8]
96}
97
98pub broadcast proof fn lemma_u16_le_bytes_roundtrip(i: [u8; 2])
99    ensures
100        #[trigger] u16_le_to_bytes(u16_le_from_bytes(i)) == i,
101{
102    let x = u16_le_from_bytes(i);
103    let i0 = i[0] as u16;
104    let i1 = i[1] as u16;
105    assert(((x == i0 | i1 << 8) && (i0 < 256) && (i1 < 256)) ==> i0 == (x & 0xff) && i1 == ((x >> 8)
106        & 0xff)) by (bit_vector);
107}
108
109pub broadcast proof fn lemma_u16_le_value_roundtrip(o: u16)
110    ensures
111        #[trigger] u16_le_from_bytes(u16_le_to_bytes(o)) == o,
112{
113    assert({
114        &&& o & 0xff < 256
115        &&& (o >> 8) & 0xff < 256
116    }) by (bit_vector);
117    assert(o == ((o & 0xff) | ((o >> 8) & 0xff) << 8)) by (bit_vector);
118}
119
120pub open spec fn u16_be_from_bytes(i: [u8; 2]) -> u16 {
121    (i[0] as u16) << 8 | (i[1] as u16)
122}
123
124pub open spec fn u16_be_to_bytes(o: u16) -> [u8; 2] {
125    [((o >> 8) & 0xff) as u8, (o & 0xff) as u8]
126}
127
128pub broadcast proof fn lemma_u16_be_bytes_roundtrip(i: [u8; 2])
129    ensures
130        #[trigger] u16_be_to_bytes(u16_be_from_bytes(i)) == i,
131{
132    let x = u16_be_from_bytes(i);
133    let i0 = i[0] as u16;
134    let i1 = i[1] as u16;
135    assert(((x == i0 << 8 | i1) && (i0 < 256) && (i1 < 256)) ==> i0 == ((x >> 8) & 0xff) && i1 == (x
136        & 0xff)) by (bit_vector);
137}
138
139pub broadcast proof fn lemma_u16_be_value_roundtrip(o: u16)
140    ensures
141        #[trigger] u16_be_from_bytes(u16_be_to_bytes(o)) == o,
142{
143    assert({
144        &&& o & 0xff < 256
145        &&& (o >> 8) & 0xff < 256
146    }) by (bit_vector);
147    assert(o == (((o >> 8) & 0xff) << 8 | (o & 0xff))) by (bit_vector);
148}
149
150pub open spec fn u24_le_from_bytes(i: [u8; 3]) -> u32 {
151    (i[0] as u32) | (i[1] as u32) << 8 | (i[2] as u32) << 16
152}
153
154pub open spec fn u24_le_to_bytes(o: u32) -> [u8; 3] {
155    [(o & 0xff) as u8, ((o >> 8) & 0xff) as u8, ((o >> 16) & 0xff) as u8]
156}
157
158pub broadcast proof fn lemma_u24_le_bytes_roundtrip(i: [u8; 3])
159    ensures
160        #[trigger] u24_le_to_bytes(u24_le_from_bytes(i)) == i,
161{
162    let x = u24_le_from_bytes(i);
163    let i0 = i[0] as u32;
164    let i1 = i[1] as u32;
165    let i2 = i[2] as u32;
166    assert(((x == i0 | i1 << 8 | i2 << 16) && (i0 < 256) && (i1 < 256) && (i2 < 256)) ==> i0 == (x
167        & 0xff) && i1 == ((x >> 8) & 0xff) && i2 == ((x >> 16) & 0xff)) by (bit_vector);
168}
169
170pub broadcast proof fn lemma_u24_le_value_roundtrip(o: u32)
171    requires
172        o < 0x01000000,
173    ensures
174        #[trigger] u24_le_from_bytes(u24_le_to_bytes(o)) == o,
175{
176    assert({
177        &&& o & 0xff < 256
178        &&& (o >> 8) & 0xff < 256
179        &&& (o >> 16) & 0xff < 256
180    }) by (bit_vector);
181    assert(o < 0x01000000 ==> o == ((o & 0xff) | ((o >> 8) & 0xff) << 8 | ((o >> 16) & 0xff) << 16))
182        by (bit_vector);
183}
184
185pub proof fn lemma_u24_le_from_bytes_range(i: [u8; 3])
186    ensures
187        u24_le_from_bytes(i) < 0x01000000,
188{
189    let b0 = i[0];
190    let b1 = i[1];
191    let b2 = i[2];
192    assert(((b0 as u32) | ((b1 as u32) << 8) | ((b2 as u32) << 16)) < 0x01000000u32)
193        by (bit_vector);
194}
195
196pub open spec fn u24_be_from_bytes(i: [u8; 3]) -> u32 {
197    (i[0] as u32) << 16 | (i[1] as u32) << 8 | (i[2] as u32)
198}
199
200pub open spec fn u24_be_to_bytes(o: u32) -> [u8; 3] {
201    [((o >> 16) & 0xff) as u8, ((o >> 8) & 0xff) as u8, (o & 0xff) as u8]
202}
203
204pub broadcast proof fn lemma_u24_be_bytes_roundtrip(i: [u8; 3])
205    ensures
206        #[trigger] u24_be_to_bytes(u24_be_from_bytes(i)) == i,
207{
208    let x = u24_be_from_bytes(i);
209    let i0 = i[0] as u32;
210    let i1 = i[1] as u32;
211    let i2 = i[2] as u32;
212    assert(((x == i0 << 16 | i1 << 8 | i2) && (i0 < 256) && (i1 < 256) && (i2 < 256)) ==> i0 == ((x
213        >> 16) & 0xff) && i1 == ((x >> 8) & 0xff) && i2 == (x & 0xff)) by (bit_vector);
214}
215
216pub broadcast proof fn lemma_u24_be_value_roundtrip(o: u32)
217    requires
218        o < 0x01000000,
219    ensures
220        #[trigger] u24_be_from_bytes(u24_be_to_bytes(o)) == o,
221{
222    assert({
223        &&& o & 0xff < 256
224        &&& (o >> 8) & 0xff < 256
225        &&& (o >> 16) & 0xff < 256
226    }) by (bit_vector);
227    assert(o < 0x01000000 ==> o == (((o >> 16) & 0xff) << 16 | ((o >> 8) & 0xff) << 8 | (o & 0xff)))
228        by (bit_vector);
229}
230
231pub proof fn lemma_u24_be_from_bytes_range(i: [u8; 3])
232    ensures
233        u24_be_from_bytes(i) < 0x01000000,
234{
235    let b0 = i[0];
236    let b1 = i[1];
237    let b2 = i[2];
238    assert((((b0 as u32) << 16) | ((b1 as u32) << 8) | (b2 as u32)) < 0x01000000u32)
239        by (bit_vector);
240}
241
242impl SpecMapper for U24LeMapper {
243    type In = Seq<u8>;
244
245    type Out = u32;
246
247    open spec fn spec_map(&self, i: Self::In) -> Self::Out {
248        u24_le_from_bytes(array_from_seq(i))
249    }
250
251    open spec fn spec_map_rev(&self, o: Self::Out) -> Self::In {
252        u24_le_to_bytes(o)@
253    }
254
255    open spec fn wf_in(&self, i: Self::In) -> bool {
256        i.len() == U24_BYTE_LEN
257    }
258
259    open spec fn wf_out(&self, o: Self::Out) -> bool {
260        o < 0x01000000
261    }
262}
263
264impl LossyMapper for U24LeMapper {
265    proof fn lemma_sound_mapper(&self, o: Self::Out) {
266        broadcast use lemma_array_from_seq_roundtrip;
267
268        lemma_u24_le_value_roundtrip(o);
269        assert(self.spec_map(self.spec_map_rev(o)) == o);
270    }
271
272    proof fn lemma_mapper_wf_out_in(&self, o: Self::Out) {
273    }
274}
275
276impl LosslessMapper for U24LeMapper {
277    proof fn lemma_lossless_mapper(&self, i: Self::In) {
278        broadcast use axiom_array_from_seq;
279        broadcast use lemma_u24_le_bytes_roundtrip;
280
281    }
282
283    proof fn lemma_mapper_wf_in_out(&self, i: Self::In) {
284        broadcast use axiom_array_from_seq;
285
286        lemma_u24_le_from_bytes_range(array_from_seq(i));
287    }
288}
289
290impl SpecMapper for U24BeMapper {
291    type In = Seq<u8>;
292
293    type Out = u32;
294
295    open spec fn spec_map(&self, i: Self::In) -> Self::Out {
296        u24_be_from_bytes(array_from_seq(i))
297    }
298
299    open spec fn spec_map_rev(&self, o: Self::Out) -> Self::In {
300        u24_be_to_bytes(o)@
301    }
302
303    open spec fn wf_in(&self, i: Self::In) -> bool {
304        i.len() == U24_BYTE_LEN
305    }
306
307    open spec fn wf_out(&self, o: Self::Out) -> bool {
308        o < 0x01000000
309    }
310}
311
312impl LossyMapper for U24BeMapper {
313    proof fn lemma_sound_mapper(&self, o: Self::Out) {
314        broadcast use lemma_array_from_seq_roundtrip;
315
316        lemma_u24_be_value_roundtrip(o);
317        assert(self.spec_map(self.spec_map_rev(o)) == o);
318    }
319
320    proof fn lemma_mapper_wf_out_in(&self, o: Self::Out) {
321    }
322}
323
324impl LosslessMapper for U24BeMapper {
325    proof fn lemma_lossless_mapper(&self, i: Self::In) {
326        broadcast use axiom_array_from_seq;
327        broadcast use lemma_u24_be_bytes_roundtrip;
328
329    }
330
331    proof fn lemma_mapper_wf_in_out(&self, i: Self::In) {
332        broadcast use axiom_array_from_seq;
333
334        lemma_u24_be_from_bytes_range(array_from_seq(i));
335    }
336}
337
338pub open spec fn u32_le_from_bytes(i: [u8; 4]) -> u32 {
339    (i[0] as u32) | (i[1] as u32) << 8 | (i[2] as u32) << 16 | (i[3] as u32) << 24
340}
341
342pub open spec fn u32_le_to_bytes(o: u32) -> [u8; 4] {
343    [(o & 0xff) as u8, ((o >> 8) & 0xff) as u8, ((o >> 16) & 0xff) as u8, ((o >> 24) & 0xff) as u8]
344}
345
346pub broadcast proof fn lemma_u32_le_bytes_roundtrip(i: [u8; 4])
347    ensures
348        #[trigger] u32_le_to_bytes(u32_le_from_bytes(i)) == i,
349{
350    let x = u32_le_from_bytes(i);
351    let i0 = i[0] as u32;
352    let i1 = i[1] as u32;
353    let i2 = i[2] as u32;
354    let i3 = i[3] as u32;
355    assert(((x == i0 | i1 << 8 | i2 << 16 | i3 << 24) && (i0 < 256) && (i1 < 256) && (i2 < 256) && (
356    i3 < 256)) ==> i0 == (x & 0xff) && i1 == ((x >> 8) & 0xff) && i2 == ((x >> 16) & 0xff) && i3
357        == ((x >> 24) & 0xff)) by (bit_vector);
358}
359
360pub broadcast proof fn lemma_u32_le_value_roundtrip(o: u32)
361    ensures
362        #[trigger] u32_le_from_bytes(u32_le_to_bytes(o)) == o,
363{
364    assert({
365        &&& o & 0xff < 256
366        &&& (o >> 8) & 0xff < 256
367        &&& (o >> 16) & 0xff < 256
368        &&& (o >> 24) & 0xff < 256
369    }) by (bit_vector);
370    assert(o == ((o & 0xff) | ((o >> 8) & 0xff) << 8 | ((o >> 16) & 0xff) << 16 | ((o >> 24) & 0xff)
371        << 24)) by (bit_vector);
372}
373
374pub open spec fn u32_be_from_bytes(i: [u8; 4]) -> u32 {
375    (i[0] as u32) << 24 | (i[1] as u32) << 16 | (i[2] as u32) << 8 | (i[3] as u32)
376}
377
378pub open spec fn u32_be_to_bytes(o: u32) -> [u8; 4] {
379    [((o >> 24) & 0xff) as u8, ((o >> 16) & 0xff) as u8, ((o >> 8) & 0xff) as u8, (o & 0xff) as u8]
380}
381
382pub broadcast proof fn lemma_u32_be_bytes_roundtrip(i: [u8; 4])
383    ensures
384        #[trigger] u32_be_to_bytes(u32_be_from_bytes(i)) == i,
385{
386    let x = u32_be_from_bytes(i);
387    let i0 = i[0] as u32;
388    let i1 = i[1] as u32;
389    let i2 = i[2] as u32;
390    let i3 = i[3] as u32;
391    assert(((x == i0 << 24 | i1 << 16 | i2 << 8 | i3) && (i0 < 256) && (i1 < 256) && (i2 < 256) && (
392    i3 < 256)) ==> i0 == ((x >> 24) & 0xff) && i1 == ((x >> 16) & 0xff) && i2 == ((x >> 8) & 0xff)
393        && i3 == (x & 0xff)) by (bit_vector);
394}
395
396pub broadcast proof fn lemma_u32_be_value_roundtrip(o: u32)
397    ensures
398        #[trigger] u32_be_from_bytes(u32_be_to_bytes(o)) == o,
399{
400    assert({
401        &&& o & 0xff < 256
402        &&& (o >> 8) & 0xff < 256
403        &&& (o >> 16) & 0xff < 256
404        &&& (o >> 24) & 0xff < 256
405    }) by (bit_vector);
406    assert(o == (((o >> 24) & 0xff) << 24 | ((o >> 16) & 0xff) << 16 | ((o >> 8) & 0xff) << 8 | (o
407        & 0xff))) by (bit_vector);
408}
409
410pub open spec fn u64_le_from_bytes(i: [u8; 8]) -> u64 {
411    (i[0] as u64) | (i[1] as u64) << 8 | (i[2] as u64) << 16 | (i[3] as u64) << 24 | (i[4] as u64)
412        << 32 | (i[5] as u64) << 40 | (i[6] as u64) << 48 | (i[7] as u64) << 56
413}
414
415pub open spec fn u64_le_to_bytes(o: u64) -> [u8; 8] {
416    [
417        (o & 0xff) as u8,
418        ((o >> 8) & 0xff) as u8,
419        ((o >> 16) & 0xff) as u8,
420        ((o >> 24) & 0xff) as u8,
421        ((o >> 32) & 0xff) as u8,
422        ((o >> 40) & 0xff) as u8,
423        ((o >> 48) & 0xff) as u8,
424        ((o >> 56) & 0xff) as u8,
425    ]
426}
427
428pub broadcast proof fn lemma_u64_le_bytes_roundtrip(i: [u8; 8])
429    ensures
430        #[trigger] u64_le_to_bytes(u64_le_from_bytes(i)) == i,
431{
432    let x = u64_le_from_bytes(i);
433    let i0 = i[0] as u64;
434    let i1 = i[1] as u64;
435    let i2 = i[2] as u64;
436    let i3 = i[3] as u64;
437    let i4 = i[4] as u64;
438    let i5 = i[5] as u64;
439    let i6 = i[6] as u64;
440    let i7 = i[7] as u64;
441    assert(((x == i0 | i1 << 8 | i2 << 16 | i3 << 24 | i4 << 32 | i5 << 40 | i6 << 48 | i7 << 56)
442        && (i0 < 256) && (i1 < 256) && (i2 < 256) && (i3 < 256) && (i4 < 256) && (i5 < 256) && (i6
443        < 256) && (i7 < 256)) ==> i0 == (x & 0xff) && i1 == ((x >> 8) & 0xff) && i2 == ((x >> 16)
444        & 0xff) && i3 == ((x >> 24) & 0xff) && i4 == ((x >> 32) & 0xff) && i5 == ((x >> 40) & 0xff)
445        && i6 == ((x >> 48) & 0xff) && i7 == ((x >> 56) & 0xff)) by (bit_vector);
446}
447
448pub broadcast proof fn lemma_u64_le_value_roundtrip(o: u64)
449    ensures
450        #[trigger] u64_le_from_bytes(u64_le_to_bytes(o)) == o,
451{
452    assert({
453        &&& o & 0xff < 256
454        &&& (o >> 8) & 0xff < 256
455        &&& (o >> 16) & 0xff < 256
456        &&& (o >> 24) & 0xff < 256
457        &&& (o >> 32) & 0xff < 256
458        &&& (o >> 40) & 0xff < 256
459        &&& (o >> 48) & 0xff < 256
460        &&& (o >> 56) & 0xff < 256
461    }) by (bit_vector);
462    assert(o == ((o & 0xff) | ((o >> 8) & 0xff) << 8 | ((o >> 16) & 0xff) << 16 | ((o >> 24) & 0xff)
463        << 24 | ((o >> 32) & 0xff) << 32 | ((o >> 40) & 0xff) << 40 | ((o >> 48) & 0xff) << 48 | ((o
464        >> 56) & 0xff) << 56)) by (bit_vector);
465}
466
467pub open spec fn u64_be_from_bytes(i: [u8; 8]) -> u64 {
468    (i[0] as u64) << 56 | (i[1] as u64) << 48 | (i[2] as u64) << 40 | (i[3] as u64) << 32 | (
469    i[4] as u64) << 24 | (i[5] as u64) << 16 | (i[6] as u64) << 8 | (i[7] as u64)
470}
471
472pub open spec fn u64_be_to_bytes(o: u64) -> [u8; 8] {
473    [
474        ((o >> 56) & 0xff) as u8,
475        ((o >> 48) & 0xff) as u8,
476        ((o >> 40) & 0xff) as u8,
477        ((o >> 32) & 0xff) as u8,
478        ((o >> 24) & 0xff) as u8,
479        ((o >> 16) & 0xff) as u8,
480        ((o >> 8) & 0xff) as u8,
481        (o & 0xff) as u8,
482    ]
483}
484
485pub broadcast proof fn lemma_u64_be_bytes_roundtrip(i: [u8; 8])
486    ensures
487        #[trigger] u64_be_to_bytes(u64_be_from_bytes(i)) == i,
488{
489    let x = u64_be_from_bytes(i);
490    let i0 = i[0] as u64;
491    let i1 = i[1] as u64;
492    let i2 = i[2] as u64;
493    let i3 = i[3] as u64;
494    let i4 = i[4] as u64;
495    let i5 = i[5] as u64;
496    let i6 = i[6] as u64;
497    let i7 = i[7] as u64;
498    assert(((x == i0 << 56 | i1 << 48 | i2 << 40 | i3 << 32 | i4 << 24 | i5 << 16 | i6 << 8 | i7)
499        && (i0 < 256) && (i1 < 256) && (i2 < 256) && (i3 < 256) && (i4 < 256) && (i5 < 256) && (i6
500        < 256) && (i7 < 256)) ==> i0 == ((x >> 56) & 0xff) && i1 == ((x >> 48) & 0xff) && i2 == ((x
501        >> 40) & 0xff) && i3 == ((x >> 32) & 0xff) && i4 == ((x >> 24) & 0xff) && i5 == ((x >> 16)
502        & 0xff) && i6 == ((x >> 8) & 0xff) && i7 == (x & 0xff)) by (bit_vector);
503}
504
505pub broadcast proof fn lemma_u64_be_value_roundtrip(o: u64)
506    ensures
507        #[trigger] u64_be_from_bytes(u64_be_to_bytes(o)) == o,
508{
509    assert({
510        &&& o & 0xff < 256
511        &&& (o >> 8) & 0xff < 256
512        &&& (o >> 16) & 0xff < 256
513        &&& (o >> 24) & 0xff < 256
514        &&& (o >> 32) & 0xff < 256
515        &&& (o >> 40) & 0xff < 256
516        &&& (o >> 48) & 0xff < 256
517        &&& (o >> 56) & 0xff < 256
518    }) by (bit_vector);
519    assert(o == (((o >> 56) & 0xff) << 56 | ((o >> 48) & 0xff) << 48 | ((o >> 40) & 0xff) << 40 | ((
520    o >> 32) & 0xff) << 32 | ((o >> 24) & 0xff) << 24 | ((o >> 16) & 0xff) << 16 | ((o >> 8) & 0xff)
521        << 8 | (o & 0xff))) by (bit_vector);
522}
523
524impl SpecParser for super::U8 {
525    type PVal = u8;
526
527    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, u8)> {
528        if ibuf.len() >= 1 {
529            Some((1, ibuf[0]))
530        } else {
531            None
532        }
533    }
534}
535
536impl Consistency for super::U8 {
537    type Val = u8;
538
539    open spec fn consistent(&self, _v: Self::Val) -> bool {
540        true
541    }
542}
543
544impl SpecSerializerDps for super::U8 {
545    type SValue = u8;
546
547    open spec fn spec_serialize_dps(&self, v: u8, obuf: Seq<u8>) -> Seq<u8> {
548        seq![v] + obuf
549    }
550}
551
552impl SpecSerializer for super::U8 {
553    type SVal = u8;
554
555    open spec fn spec_serialize(&self, v: u8) -> Seq<u8> {
556        seq![v]
557    }
558}
559
560impl SafeParser for super::U8 {
561    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
562    }
563}
564
565impl SoundParser for super::U8 {
566    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
567    }
568
569    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
570    }
571}
572
573impl NonTailFmt for super::U8 {
574    proof fn lemma_serialize_dps_prepend(&self, v: u8, obuf: Seq<u8>) {
575        assert(self.spec_serialize_dps(v, obuf) == seq![v] + obuf);
576    }
577
578    proof fn lemma_serialize_dps_len(&self, v: u8, obuf: Seq<u8>) {
579        assert(self.spec_serialize_dps(v, obuf).len() - obuf.len() == 1);
580    }
581}
582
583impl GoodSerializer for super::U8 {
584    proof fn lemma_serialize_len(&self, v: Self::SVal) {
585        assert(self.spec_serialize(v).len() == 1);
586    }
587}
588
589impl SpecByteLen for super::U8 {
590    type T = u8;
591
592    open spec fn byte_len(&self, _v: Self::T) -> nat {
593        U8_BYTE_LEN as nat
594    }
595}
596
597impl MinMaxByteLen for super::U8 {
598    open spec fn min(&self) -> nat {
599        U8_BYTE_LEN as nat
600    }
601
602    open spec fn max(&self) -> nat {
603        U8_BYTE_LEN as nat
604    }
605
606    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
607    }
608}
609
610impl StaticByteLen for super::U8 {
611    open spec fn static_byte_len() -> nat {
612        U8_BYTE_LEN as nat
613    }
614
615    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
616    }
617}
618
619impl ValueByteLen for super::U8 {
620    open spec fn value_byte_len(_v: Self::T) -> nat {
621        U8_BYTE_LEN as nat
622    }
623
624    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
625    }
626}
627
628impl SpecParser for super::U16Le {
629    type PVal = u16;
630
631    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, u16)> {
632        u16_le_fmt().spec_parse(ibuf)
633    }
634}
635
636impl Consistency for super::U16Le {
637    type Val = u16;
638
639    open spec fn consistent(&self, _v: Self::Val) -> bool {
640        true
641    }
642}
643
644impl SpecSerializerDps for super::U16Le {
645    type SValue = u16;
646
647    open spec fn spec_serialize_dps(&self, v: u16, obuf: Seq<u8>) -> Seq<u8> {
648        u16_le_fmt().spec_serialize_dps(v, obuf)
649    }
650}
651
652impl SpecSerializer for super::U16Le {
653    type SVal = u16;
654
655    open spec fn spec_serialize(&self, v: u16) -> Seq<u8> {
656        u16_le_fmt().spec_serialize(v)
657    }
658}
659
660impl SafeParser for super::U16Le {
661    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
662        u16_le_fmt().lemma_parse_safe(ibuf);
663    }
664}
665
666impl SoundParser for super::U16Le {
667    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
668        broadcast use lemma_u16_le_bytes_roundtrip;
669        broadcast use axiom_array_from_seq;
670
671        u16_le_fmt().lemma_parse_sound_consumption(ibuf);
672    }
673
674    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
675        broadcast use lemma_u16_le_bytes_roundtrip;
676        broadcast use axiom_array_from_seq;
677
678        u16_le_fmt().lemma_parse_sound_value(ibuf);
679    }
680}
681
682impl NonTailFmt for super::U16Le {
683    proof fn lemma_serialize_dps_prepend(&self, v: u16, obuf: Seq<u8>) {
684        u16_le_fmt().lemma_serialize_dps_prepend(v, obuf);
685    }
686
687    proof fn lemma_serialize_dps_len(&self, v: u16, obuf: Seq<u8>) {
688        u16_le_fmt().lemma_serialize_dps_len(v, obuf);
689    }
690}
691
692impl GoodSerializer for super::U16Le {
693    proof fn lemma_serialize_len(&self, v: u16) {
694        u16_le_fmt().lemma_serialize_len(v);
695    }
696}
697
698impl SpecByteLen for super::U16Le {
699    type T = u16;
700
701    open spec fn byte_len(&self, _v: Self::T) -> nat {
702        U16_BYTE_LEN as nat
703    }
704}
705
706impl MinMaxByteLen for super::U16Le {
707    open spec fn min(&self) -> nat {
708        U16_BYTE_LEN as nat
709    }
710
711    open spec fn max(&self) -> nat {
712        U16_BYTE_LEN as nat
713    }
714
715    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
716    }
717}
718
719impl StaticByteLen for super::U16Le {
720    open spec fn static_byte_len() -> nat {
721        U16_BYTE_LEN as nat
722    }
723
724    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
725    }
726}
727
728impl ValueByteLen for super::U16Le {
729    open spec fn value_byte_len(_v: Self::T) -> nat {
730        U16_BYTE_LEN as nat
731    }
732
733    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
734    }
735}
736
737impl SpecParser for super::U16Be {
738    type PVal = u16;
739
740    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, u16)> {
741        u16_be_fmt().spec_parse(ibuf)
742    }
743}
744
745impl Consistency for super::U16Be {
746    type Val = u16;
747
748    open spec fn consistent(&self, _v: Self::Val) -> bool {
749        true
750    }
751}
752
753impl SpecSerializerDps for super::U16Be {
754    type SValue = u16;
755
756    open spec fn spec_serialize_dps(&self, v: u16, obuf: Seq<u8>) -> Seq<u8> {
757        u16_be_fmt().spec_serialize_dps(v, obuf)
758    }
759}
760
761impl SpecSerializer for super::U16Be {
762    type SVal = u16;
763
764    open spec fn spec_serialize(&self, v: u16) -> Seq<u8> {
765        u16_be_fmt().spec_serialize(v)
766    }
767}
768
769impl SafeParser for super::U16Be {
770    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
771        u16_be_fmt().lemma_parse_safe(ibuf);
772    }
773}
774
775impl SoundParser for super::U16Be {
776    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
777        broadcast use lemma_u16_be_bytes_roundtrip;
778        broadcast use axiom_array_from_seq;
779
780        u16_be_fmt().lemma_parse_sound_consumption(ibuf);
781    }
782
783    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
784        broadcast use lemma_u16_be_bytes_roundtrip;
785        broadcast use axiom_array_from_seq;
786
787        u16_be_fmt().lemma_parse_sound_value(ibuf);
788    }
789}
790
791impl NonTailFmt for super::U16Be {
792    proof fn lemma_serialize_dps_prepend(&self, v: u16, obuf: Seq<u8>) {
793        u16_be_fmt().lemma_serialize_dps_prepend(v, obuf);
794    }
795
796    proof fn lemma_serialize_dps_len(&self, v: u16, obuf: Seq<u8>) {
797        u16_be_fmt().lemma_serialize_dps_len(v, obuf);
798    }
799}
800
801impl GoodSerializer for super::U16Be {
802    proof fn lemma_serialize_len(&self, v: u16) {
803        u16_be_fmt().lemma_serialize_len(v);
804    }
805}
806
807impl SpecByteLen for super::U16Be {
808    type T = u16;
809
810    open spec fn byte_len(&self, _v: Self::T) -> nat {
811        U16_BYTE_LEN as nat
812    }
813}
814
815impl MinMaxByteLen for super::U16Be {
816    open spec fn min(&self) -> nat {
817        U16_BYTE_LEN as nat
818    }
819
820    open spec fn max(&self) -> nat {
821        U16_BYTE_LEN as nat
822    }
823
824    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
825    }
826}
827
828impl StaticByteLen for super::U16Be {
829    open spec fn static_byte_len() -> nat {
830        U16_BYTE_LEN as nat
831    }
832
833    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
834    }
835}
836
837impl ValueByteLen for super::U16Be {
838    open spec fn value_byte_len(_v: Self::T) -> nat {
839        U16_BYTE_LEN as nat
840    }
841
842    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
843    }
844}
845
846impl SpecParser for super::U24Le {
847    type PVal = u32;
848
849    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, u32)> {
850        u24_le_fmt().spec_parse(ibuf)
851    }
852}
853
854impl Consistency for super::U24Le {
855    type Val = u32;
856
857    open spec fn consistent(&self, v: Self::Val) -> bool {
858        v < 0x01000000
859    }
860}
861
862impl SpecSerializerDps for super::U24Le {
863    type SValue = u32;
864
865    open spec fn spec_serialize_dps(&self, v: u32, obuf: Seq<u8>) -> Seq<u8> {
866        u24_le_fmt().spec_serialize_dps(v, obuf)
867    }
868}
869
870impl SpecSerializer for super::U24Le {
871    type SVal = u32;
872
873    open spec fn spec_serialize(&self, v: u32) -> Seq<u8> {
874        u24_le_fmt().spec_serialize(v)
875    }
876}
877
878impl SafeParser for super::U24Le {
879    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
880        u24_le_fmt().lemma_parse_safe(ibuf);
881    }
882}
883
884impl SoundParser for super::U24Le {
885    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
886        broadcast use axiom_array_from_seq;
887        broadcast use lemma_u24_le_bytes_roundtrip;
888
889        u24_le_fmt().lemma_parse_sound_consumption(ibuf);
890    }
891
892    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
893        broadcast use axiom_array_from_seq;
894        broadcast use lemma_u24_le_bytes_roundtrip;
895
896        u24_le_fmt().lemma_parse_sound_value(ibuf);
897    }
898}
899
900impl NonTailFmt for super::U24Le {
901    proof fn lemma_serialize_dps_prepend(&self, v: u32, obuf: Seq<u8>) {
902        u24_le_fmt().lemma_serialize_dps_prepend(v, obuf);
903    }
904
905    proof fn lemma_serialize_dps_len(&self, v: u32, obuf: Seq<u8>) {
906        u24_le_fmt().lemma_serialize_dps_len(v, obuf);
907    }
908}
909
910impl GoodSerializer for super::U24Le {
911    proof fn lemma_serialize_len(&self, v: u32) {
912        u24_le_fmt().lemma_serialize_len(v);
913    }
914}
915
916impl SpecByteLen for super::U24Le {
917    type T = u32;
918
919    open spec fn byte_len(&self, _v: Self::T) -> nat {
920        U24_BYTE_LEN as nat
921    }
922}
923
924impl MinMaxByteLen for super::U24Le {
925    open spec fn min(&self) -> nat {
926        U24_BYTE_LEN as nat
927    }
928
929    open spec fn max(&self) -> nat {
930        U24_BYTE_LEN as nat
931    }
932
933    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
934    }
935}
936
937impl StaticByteLen for super::U24Le {
938    open spec fn static_byte_len() -> nat {
939        U24_BYTE_LEN as nat
940    }
941
942    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
943    }
944}
945
946impl ValueByteLen for super::U24Le {
947    open spec fn value_byte_len(_v: Self::T) -> nat {
948        U24_BYTE_LEN as nat
949    }
950
951    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
952    }
953}
954
955impl SpecParser for super::U24Be {
956    type PVal = u32;
957
958    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, u32)> {
959        u24_be_fmt().spec_parse(ibuf)
960    }
961}
962
963impl Consistency for super::U24Be {
964    type Val = u32;
965
966    open spec fn consistent(&self, v: Self::Val) -> bool {
967        v < 0x01000000
968    }
969}
970
971impl SpecSerializerDps for super::U24Be {
972    type SValue = u32;
973
974    open spec fn spec_serialize_dps(&self, v: u32, obuf: Seq<u8>) -> Seq<u8> {
975        u24_be_fmt().spec_serialize_dps(v, obuf)
976    }
977}
978
979impl SpecSerializer for super::U24Be {
980    type SVal = u32;
981
982    open spec fn spec_serialize(&self, v: u32) -> Seq<u8> {
983        u24_be_fmt().spec_serialize(v)
984    }
985}
986
987impl SafeParser for super::U24Be {
988    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
989        u24_be_fmt().lemma_parse_safe(ibuf);
990    }
991}
992
993impl SoundParser for super::U24Be {
994    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
995        broadcast use axiom_array_from_seq;
996        broadcast use lemma_u24_be_bytes_roundtrip;
997
998        u24_be_fmt().lemma_parse_sound_consumption(ibuf);
999    }
1000
1001    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
1002        broadcast use axiom_array_from_seq;
1003        broadcast use lemma_u24_be_bytes_roundtrip;
1004
1005        u24_be_fmt().lemma_parse_sound_value(ibuf);
1006    }
1007}
1008
1009impl NonTailFmt for super::U24Be {
1010    proof fn lemma_serialize_dps_prepend(&self, v: u32, obuf: Seq<u8>) {
1011        u24_be_fmt().lemma_serialize_dps_prepend(v, obuf);
1012    }
1013
1014    proof fn lemma_serialize_dps_len(&self, v: u32, obuf: Seq<u8>) {
1015        u24_be_fmt().lemma_serialize_dps_len(v, obuf);
1016    }
1017}
1018
1019impl GoodSerializer for super::U24Be {
1020    proof fn lemma_serialize_len(&self, v: u32) {
1021        u24_be_fmt().lemma_serialize_len(v);
1022    }
1023}
1024
1025impl SpecByteLen for super::U24Be {
1026    type T = u32;
1027
1028    open spec fn byte_len(&self, _v: Self::T) -> nat {
1029        U24_BYTE_LEN as nat
1030    }
1031}
1032
1033impl MinMaxByteLen for super::U24Be {
1034    open spec fn min(&self) -> nat {
1035        U24_BYTE_LEN as nat
1036    }
1037
1038    open spec fn max(&self) -> nat {
1039        U24_BYTE_LEN as nat
1040    }
1041
1042    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
1043    }
1044}
1045
1046impl StaticByteLen for super::U24Be {
1047    open spec fn static_byte_len() -> nat {
1048        U24_BYTE_LEN as nat
1049    }
1050
1051    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
1052    }
1053}
1054
1055impl ValueByteLen for super::U24Be {
1056    open spec fn value_byte_len(_v: Self::T) -> nat {
1057        U24_BYTE_LEN as nat
1058    }
1059
1060    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
1061    }
1062}
1063
1064impl SpecParser for super::U32Le {
1065    type PVal = u32;
1066
1067    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, u32)> {
1068        u32_le_fmt().spec_parse(ibuf)
1069    }
1070}
1071
1072impl Consistency for super::U32Le {
1073    type Val = u32;
1074
1075    open spec fn consistent(&self, _v: Self::Val) -> bool {
1076        true
1077    }
1078}
1079
1080impl SpecSerializerDps for super::U32Le {
1081    type SValue = u32;
1082
1083    open spec fn spec_serialize_dps(&self, v: u32, obuf: Seq<u8>) -> Seq<u8> {
1084        u32_le_fmt().spec_serialize_dps(v, obuf)
1085    }
1086}
1087
1088impl SpecSerializer for super::U32Le {
1089    type SVal = u32;
1090
1091    open spec fn spec_serialize(&self, v: u32) -> Seq<u8> {
1092        u32_le_fmt().spec_serialize(v)
1093    }
1094}
1095
1096impl SafeParser for super::U32Le {
1097    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
1098        u32_le_fmt().lemma_parse_safe(ibuf);
1099    }
1100}
1101
1102impl SoundParser for super::U32Le {
1103    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
1104        broadcast use lemma_u32_le_bytes_roundtrip;
1105        broadcast use axiom_array_from_seq;
1106
1107        u32_le_fmt().lemma_parse_sound_consumption(ibuf);
1108    }
1109
1110    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
1111        broadcast use lemma_u32_le_bytes_roundtrip;
1112        broadcast use axiom_array_from_seq;
1113
1114        u32_le_fmt().lemma_parse_sound_value(ibuf);
1115    }
1116}
1117
1118impl NonTailFmt for super::U32Le {
1119    proof fn lemma_serialize_dps_prepend(&self, v: u32, obuf: Seq<u8>) {
1120        u32_le_fmt().lemma_serialize_dps_prepend(v, obuf);
1121    }
1122
1123    proof fn lemma_serialize_dps_len(&self, v: u32, obuf: Seq<u8>) {
1124        u32_le_fmt().lemma_serialize_dps_len(v, obuf);
1125    }
1126}
1127
1128impl GoodSerializer for super::U32Le {
1129    proof fn lemma_serialize_len(&self, v: u32) {
1130        u32_le_fmt().lemma_serialize_len(v);
1131    }
1132}
1133
1134impl SpecByteLen for super::U32Le {
1135    type T = u32;
1136
1137    open spec fn byte_len(&self, _v: Self::T) -> nat {
1138        U32_BYTE_LEN as nat
1139    }
1140}
1141
1142impl MinMaxByteLen for super::U32Le {
1143    open spec fn min(&self) -> nat {
1144        U32_BYTE_LEN as nat
1145    }
1146
1147    open spec fn max(&self) -> nat {
1148        U32_BYTE_LEN as nat
1149    }
1150
1151    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
1152    }
1153}
1154
1155impl StaticByteLen for super::U32Le {
1156    open spec fn static_byte_len() -> nat {
1157        U32_BYTE_LEN as nat
1158    }
1159
1160    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
1161    }
1162}
1163
1164impl ValueByteLen for super::U32Le {
1165    open spec fn value_byte_len(_v: Self::T) -> nat {
1166        U32_BYTE_LEN as nat
1167    }
1168
1169    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
1170    }
1171}
1172
1173impl SpecParser for super::U32Be {
1174    type PVal = u32;
1175
1176    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, u32)> {
1177        u32_be_fmt().spec_parse(ibuf)
1178    }
1179}
1180
1181impl Consistency for super::U32Be {
1182    type Val = u32;
1183
1184    open spec fn consistent(&self, _v: Self::Val) -> bool {
1185        true
1186    }
1187}
1188
1189impl SpecSerializerDps for super::U32Be {
1190    type SValue = u32;
1191
1192    open spec fn spec_serialize_dps(&self, v: u32, obuf: Seq<u8>) -> Seq<u8> {
1193        u32_be_fmt().spec_serialize_dps(v, obuf)
1194    }
1195}
1196
1197impl SpecSerializer for super::U32Be {
1198    type SVal = u32;
1199
1200    open spec fn spec_serialize(&self, v: u32) -> Seq<u8> {
1201        u32_be_fmt().spec_serialize(v)
1202    }
1203}
1204
1205impl SafeParser for super::U32Be {
1206    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
1207        u32_be_fmt().lemma_parse_safe(ibuf);
1208    }
1209}
1210
1211impl SoundParser for super::U32Be {
1212    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
1213        broadcast use lemma_u32_be_bytes_roundtrip;
1214        broadcast use axiom_array_from_seq;
1215
1216        u32_be_fmt().lemma_parse_sound_consumption(ibuf);
1217    }
1218
1219    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
1220        broadcast use lemma_u32_be_bytes_roundtrip;
1221        broadcast use axiom_array_from_seq;
1222
1223        u32_be_fmt().lemma_parse_sound_value(ibuf);
1224    }
1225}
1226
1227impl NonTailFmt for super::U32Be {
1228    proof fn lemma_serialize_dps_prepend(&self, v: u32, obuf: Seq<u8>) {
1229        u32_be_fmt().lemma_serialize_dps_prepend(v, obuf);
1230    }
1231
1232    proof fn lemma_serialize_dps_len(&self, v: u32, obuf: Seq<u8>) {
1233        u32_be_fmt().lemma_serialize_dps_len(v, obuf);
1234    }
1235}
1236
1237impl GoodSerializer for super::U32Be {
1238    proof fn lemma_serialize_len(&self, v: u32) {
1239        u32_be_fmt().lemma_serialize_len(v);
1240    }
1241}
1242
1243impl SpecByteLen for super::U32Be {
1244    type T = u32;
1245
1246    open spec fn byte_len(&self, _v: Self::T) -> nat {
1247        U32_BYTE_LEN as nat
1248    }
1249}
1250
1251impl MinMaxByteLen for super::U32Be {
1252    open spec fn min(&self) -> nat {
1253        U32_BYTE_LEN as nat
1254    }
1255
1256    open spec fn max(&self) -> nat {
1257        U32_BYTE_LEN as nat
1258    }
1259
1260    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
1261    }
1262}
1263
1264impl StaticByteLen for super::U32Be {
1265    open spec fn static_byte_len() -> nat {
1266        U32_BYTE_LEN as nat
1267    }
1268
1269    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
1270    }
1271}
1272
1273impl ValueByteLen for super::U32Be {
1274    open spec fn value_byte_len(_v: Self::T) -> nat {
1275        U32_BYTE_LEN as nat
1276    }
1277
1278    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
1279    }
1280}
1281
1282impl SpecParser for super::U64Le {
1283    type PVal = u64;
1284
1285    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, u64)> {
1286        u64_le_fmt().spec_parse(ibuf)
1287    }
1288}
1289
1290impl Consistency for super::U64Le {
1291    type Val = u64;
1292
1293    open spec fn consistent(&self, _v: Self::Val) -> bool {
1294        true
1295    }
1296}
1297
1298impl SpecSerializerDps for super::U64Le {
1299    type SValue = u64;
1300
1301    open spec fn spec_serialize_dps(&self, v: u64, obuf: Seq<u8>) -> Seq<u8> {
1302        u64_le_fmt().spec_serialize_dps(v, obuf)
1303    }
1304}
1305
1306impl SpecSerializer for super::U64Le {
1307    type SVal = u64;
1308
1309    open spec fn spec_serialize(&self, v: u64) -> Seq<u8> {
1310        u64_le_fmt().spec_serialize(v)
1311    }
1312}
1313
1314impl SafeParser for super::U64Le {
1315    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
1316        u64_le_fmt().lemma_parse_safe(ibuf);
1317    }
1318}
1319
1320impl SoundParser for super::U64Le {
1321    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
1322        broadcast use lemma_u64_le_bytes_roundtrip;
1323        broadcast use axiom_array_from_seq;
1324
1325        u64_le_fmt().lemma_parse_sound_consumption(ibuf);
1326    }
1327
1328    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
1329        broadcast use lemma_u64_le_bytes_roundtrip;
1330        broadcast use axiom_array_from_seq;
1331
1332        u64_le_fmt().lemma_parse_sound_value(ibuf);
1333    }
1334}
1335
1336impl NonTailFmt for super::U64Le {
1337    proof fn lemma_serialize_dps_prepend(&self, v: u64, obuf: Seq<u8>) {
1338        u64_le_fmt().lemma_serialize_dps_prepend(v, obuf);
1339    }
1340
1341    proof fn lemma_serialize_dps_len(&self, v: u64, obuf: Seq<u8>) {
1342        u64_le_fmt().lemma_serialize_dps_len(v, obuf);
1343    }
1344}
1345
1346impl GoodSerializer for super::U64Le {
1347    proof fn lemma_serialize_len(&self, v: u64) {
1348        u64_le_fmt().lemma_serialize_len(v);
1349    }
1350}
1351
1352impl SpecByteLen for super::U64Le {
1353    type T = u64;
1354
1355    open spec fn byte_len(&self, _v: Self::T) -> nat {
1356        U64_BYTE_LEN as nat
1357    }
1358}
1359
1360impl MinMaxByteLen for super::U64Le {
1361    open spec fn min(&self) -> nat {
1362        U64_BYTE_LEN as nat
1363    }
1364
1365    open spec fn max(&self) -> nat {
1366        U64_BYTE_LEN as nat
1367    }
1368
1369    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
1370    }
1371}
1372
1373impl StaticByteLen for super::U64Le {
1374    open spec fn static_byte_len() -> nat {
1375        U64_BYTE_LEN as nat
1376    }
1377
1378    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
1379    }
1380}
1381
1382impl ValueByteLen for super::U64Le {
1383    open spec fn value_byte_len(_v: Self::T) -> nat {
1384        U64_BYTE_LEN as nat
1385    }
1386
1387    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
1388    }
1389}
1390
1391impl SpecParser for super::U64Be {
1392    type PVal = u64;
1393
1394    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, u64)> {
1395        u64_be_fmt().spec_parse(ibuf)
1396    }
1397}
1398
1399impl Consistency for super::U64Be {
1400    type Val = u64;
1401
1402    open spec fn consistent(&self, _v: Self::Val) -> bool {
1403        true
1404    }
1405}
1406
1407impl SpecSerializerDps for super::U64Be {
1408    type SValue = u64;
1409
1410    open spec fn spec_serialize_dps(&self, v: u64, obuf: Seq<u8>) -> Seq<u8> {
1411        u64_be_fmt().spec_serialize_dps(v, obuf)
1412    }
1413}
1414
1415impl SpecSerializer for super::U64Be {
1416    type SVal = u64;
1417
1418    open spec fn spec_serialize(&self, v: u64) -> Seq<u8> {
1419        u64_be_fmt().spec_serialize(v)
1420    }
1421}
1422
1423impl SafeParser for super::U64Be {
1424    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
1425        u64_be_fmt().lemma_parse_safe(ibuf);
1426    }
1427}
1428
1429impl SoundParser for super::U64Be {
1430    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
1431        broadcast use lemma_u64_be_bytes_roundtrip;
1432        broadcast use axiom_array_from_seq;
1433
1434        u64_be_fmt().lemma_parse_sound_consumption(ibuf);
1435    }
1436
1437    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
1438        broadcast use lemma_u64_be_bytes_roundtrip;
1439        broadcast use axiom_array_from_seq;
1440
1441        u64_be_fmt().lemma_parse_sound_value(ibuf);
1442    }
1443}
1444
1445impl NonTailFmt for super::U64Be {
1446    proof fn lemma_serialize_dps_prepend(&self, v: u64, obuf: Seq<u8>) {
1447        u64_be_fmt().lemma_serialize_dps_prepend(v, obuf);
1448    }
1449
1450    proof fn lemma_serialize_dps_len(&self, v: u64, obuf: Seq<u8>) {
1451        u64_be_fmt().lemma_serialize_dps_len(v, obuf);
1452    }
1453}
1454
1455impl GoodSerializer for super::U64Be {
1456    proof fn lemma_serialize_len(&self, v: u64) {
1457        u64_be_fmt().lemma_serialize_len(v);
1458    }
1459}
1460
1461impl SpecByteLen for super::U64Be {
1462    type T = u64;
1463
1464    open spec fn byte_len(&self, _v: Self::T) -> nat {
1465        U64_BYTE_LEN as nat
1466    }
1467}
1468
1469impl MinMaxByteLen for super::U64Be {
1470    open spec fn min(&self) -> nat {
1471        U64_BYTE_LEN as nat
1472    }
1473
1474    open spec fn max(&self) -> nat {
1475        U64_BYTE_LEN as nat
1476    }
1477
1478    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
1479    }
1480}
1481
1482impl StaticByteLen for super::U64Be {
1483    open spec fn static_byte_len() -> nat {
1484        U64_BYTE_LEN as nat
1485    }
1486
1487    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
1488    }
1489}
1490
1491impl ValueByteLen for super::U64Be {
1492    open spec fn value_byte_len(_v: Self::T) -> nat {
1493        U64_BYTE_LEN as nat
1494    }
1495
1496    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
1497    }
1498}
1499
1500} // verus!
vest_lib/combinators/uints/spec.rs

vest_lib/combinators/uints/
spec.rs
