vest_lib/combinators/sints/
exec.rs

1//! Executable fixed-width signed integer formats.
2use crate::combinators::sints::spec::*;
3use crate::combinators::Fixed;
4use crate::core::exec::input::InputSlice;
5use crate::core::exec::output::*;
6use crate::core::exec::{
7    parser::{PResult, Parser},
8    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
9    ParseError,
10};
11use vstd::prelude::*;
12use OutputBuf;
13
14verus! {
15
16use crate::combinators::bytes::spec::*;
17
18#[verifier::external_body]
19#[inline(always)]
20pub fn i16_from_le_bytes(bytes: [u8; 2]) -> (out: i16)
21    ensures
22        out == i16_le_from_bytes(bytes),
23{
24    i16::from_le_bytes(bytes)
25}
26
27#[verifier::external_body]
28#[inline(always)]
29pub fn i16_from_be_bytes(bytes: [u8; 2]) -> (out: i16)
30    ensures
31        out == i16_be_from_bytes(bytes),
32{
33    i16::from_be_bytes(bytes)
34}
35
36#[verifier::external_body]
37#[inline(always)]
38pub fn i16_to_le_bytes(value: i16) -> (bytes: [u8; 2])
39    ensures
40        bytes == i16_le_to_bytes(value),
41{
42    value.to_le_bytes()
43}
44
45#[verifier::external_body]
46#[inline(always)]
47pub fn i16_to_be_bytes(value: i16) -> (bytes: [u8; 2])
48    ensures
49        bytes == i16_be_to_bytes(value),
50{
51    value.to_be_bytes()
52}
53
54#[verifier::external_body]
55#[inline(always)]
56pub fn i32_from_le_bytes(bytes: [u8; 4]) -> (out: i32)
57    ensures
58        out == i32_le_from_bytes(bytes),
59{
60    i32::from_le_bytes(bytes)
61}
62
63#[verifier::external_body]
64#[inline(always)]
65pub fn i32_from_be_bytes(bytes: [u8; 4]) -> (out: i32)
66    ensures
67        out == i32_be_from_bytes(bytes),
68{
69    i32::from_be_bytes(bytes)
70}
71
72#[verifier::external_body]
73#[inline(always)]
74pub fn i32_to_le_bytes(value: i32) -> (bytes: [u8; 4])
75    ensures
76        bytes == i32_le_to_bytes(value),
77{
78    value.to_le_bytes()
79}
80
81#[verifier::external_body]
82#[inline(always)]
83pub fn i32_to_be_bytes(value: i32) -> (bytes: [u8; 4])
84    ensures
85        bytes == i32_be_to_bytes(value),
86{
87    value.to_be_bytes()
88}
89
90#[verifier::external_body]
91#[inline(always)]
92pub fn i64_from_le_bytes(bytes: [u8; 8]) -> (out: i64)
93    ensures
94        out == i64_le_from_bytes(bytes),
95{
96    i64::from_le_bytes(bytes)
97}
98
99#[verifier::external_body]
100#[inline(always)]
101pub fn i64_from_be_bytes(bytes: [u8; 8]) -> (out: i64)
102    ensures
103        out == i64_be_from_bytes(bytes),
104{
105    i64::from_be_bytes(bytes)
106}
107
108#[verifier::external_body]
109#[inline(always)]
110pub fn i64_to_le_bytes(value: i64) -> (bytes: [u8; 8])
111    ensures
112        bytes == i64_le_to_bytes(value),
113{
114    value.to_le_bytes()
115}
116
117#[verifier::external_body]
118#[inline(always)]
119pub fn i64_to_be_bytes(value: i64) -> (bytes: [u8; 8])
120    ensures
121        bytes == i64_be_to_bytes(value),
122{
123    value.to_be_bytes()
124}
125
126impl Parser<&[u8]> for super::I8 {
127    type PT = i8;
128
129    fn min_byte_len(&self) -> usize {
130        U8_BYTE_LEN
131    }
132
133    open spec fn exec_inv(&self) -> bool {
134        true
135    }
136
137    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
138        if ibuf.len() < 1 {
139            Err(ParseError::unexpected_eof())
140        } else {
141            Ok((1, ibuf[0] as i8))
142        }
143    }
144}
145
146impl<Output: OutputBuf> Serializer<Output, i8> for super::I8 {
147    fn serialize_into(&self, v: &i8, obuf: &mut Output) {
148        obuf.write_byte(*v as u8);
149    }
150}
151
152impl ByteLen<i8> for super::I8 {
153    fn length(&self, _v: &i8) -> (len: usize) {
154        U8_BYTE_LEN
155    }
156}
157
158impl Prepare<i8> for super::I8 {
159    fn prepare(&self, _v: &i8) -> (checked: Result<usize, PreSerializeError>) {
160        Ok(U8_BYTE_LEN)
161    }
162}
163
164impl Parser<&[u8]> for super::I16Le {
165    type PT = i16;
166
167    fn min_byte_len(&self) -> usize {
168        U16_BYTE_LEN
169    }
170
171    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
172        broadcast use lemma_array_from_seq_roundtrip;
173
174        let (n, chunk) = Fixed::<U16_BYTE_LEN>.parse(ibuf)?;
175        assert(chunk@ == ibuf@[0..U16_BYTE_LEN]);
176
177        let bytes = [chunk[0], chunk[1]];
178        let value = i16_from_le_bytes(bytes);
179
180        assert(bytes@ == chunk@);
181
182        Ok((n, value))
183    }
184}
185
186impl<Output: OutputBuf> Serializer<Output, i16> for super::I16Le {
187    fn serialize_into(&self, v: &i16, obuf: &mut Output) {
188        let bytes = i16_to_le_bytes(*v);
189        obuf.write_bytes(&bytes);
190    }
191}
192
193impl ByteLen<i16> for super::I16Le {
194    fn length(&self, _v: &i16) -> (len: usize) {
195        U16_BYTE_LEN
196    }
197}
198
199impl Prepare<i16> for super::I16Le {
200    fn prepare(&self, _v: &i16) -> (checked: Result<usize, PreSerializeError>) {
201        Ok(U16_BYTE_LEN)
202    }
203}
204
205impl Parser<&[u8]> for super::I16Be {
206    type PT = i16;
207
208    fn min_byte_len(&self) -> usize {
209        U16_BYTE_LEN
210    }
211
212    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
213        broadcast use lemma_array_from_seq_roundtrip;
214
215        let (n, chunk) = Fixed::<U16_BYTE_LEN>.parse(ibuf)?;
216        assert(chunk@ == ibuf@[0..U16_BYTE_LEN]);
217
218        let bytes = [chunk[0], chunk[1]];
219        let value = i16_from_be_bytes(bytes);
220
221        assert(bytes@ == chunk@);
222
223        Ok((n, value))
224    }
225}
226
227impl<Output: OutputBuf> Serializer<Output, i16> for super::I16Be {
228    fn serialize_into(&self, v: &i16, obuf: &mut Output) {
229        let bytes = i16_to_be_bytes(*v);
230        obuf.write_bytes(&bytes);
231    }
232}
233
234impl ByteLen<i16> for super::I16Be {
235    fn length(&self, _v: &i16) -> (len: usize) {
236        U16_BYTE_LEN
237    }
238}
239
240impl Prepare<i16> for super::I16Be {
241    fn prepare(&self, _v: &i16) -> (checked: Result<usize, PreSerializeError>) {
242        Ok(U16_BYTE_LEN)
243    }
244}
245
246impl Parser<&[u8]> for super::I32Le {
247    type PT = i32;
248
249    fn min_byte_len(&self) -> usize {
250        U32_BYTE_LEN
251    }
252
253    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
254        broadcast use lemma_array_from_seq_roundtrip;
255
256        let (n, chunk) = Fixed::<U32_BYTE_LEN>.parse(ibuf)?;
257        assert(chunk@ == ibuf@[0..U32_BYTE_LEN]);
258
259        let bytes = [chunk[0], chunk[1], chunk[2], chunk[3]];
260        let value = i32_from_le_bytes(bytes);
261
262        assert(bytes@ == chunk@);
263
264        Ok((n, value))
265    }
266}
267
268impl<Output: OutputBuf> Serializer<Output, i32> for super::I32Le {
269    fn serialize_into(&self, v: &i32, obuf: &mut Output) {
270        let bytes = i32_to_le_bytes(*v);
271        obuf.write_bytes(&bytes);
272    }
273}
274
275impl ByteLen<i32> for super::I32Le {
276    fn length(&self, _v: &i32) -> (len: usize) {
277        U32_BYTE_LEN
278    }
279}
280
281impl Prepare<i32> for super::I32Le {
282    fn prepare(&self, _v: &i32) -> (checked: Result<usize, PreSerializeError>) {
283        Ok(U32_BYTE_LEN)
284    }
285}
286
287impl Parser<&[u8]> for super::I32Be {
288    type PT = i32;
289
290    fn min_byte_len(&self) -> usize {
291        U32_BYTE_LEN
292    }
293
294    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
295        broadcast use lemma_array_from_seq_roundtrip;
296
297        let (n, chunk) = Fixed::<U32_BYTE_LEN>.parse(ibuf)?;
298        assert(chunk@ == ibuf@[0..U32_BYTE_LEN]);
299
300        let bytes = [chunk[0], chunk[1], chunk[2], chunk[3]];
301        let value = i32_from_be_bytes(bytes);
302
303        assert(bytes@ == chunk@);
304
305        Ok((n, value))
306    }
307}
308
309impl<Output: OutputBuf> Serializer<Output, i32> for super::I32Be {
310    fn serialize_into(&self, v: &i32, obuf: &mut Output) {
311        let bytes = i32_to_be_bytes(*v);
312        obuf.write_bytes(&bytes);
313    }
314}
315
316impl ByteLen<i32> for super::I32Be {
317    fn length(&self, _v: &i32) -> (len: usize) {
318        U32_BYTE_LEN
319    }
320}
321
322impl Prepare<i32> for super::I32Be {
323    fn prepare(&self, _v: &i32) -> (checked: Result<usize, PreSerializeError>) {
324        Ok(U32_BYTE_LEN)
325    }
326}
327
328impl Parser<&[u8]> for super::I64Le {
329    type PT = i64;
330
331    fn min_byte_len(&self) -> usize {
332        U64_BYTE_LEN
333    }
334
335    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
336        broadcast use lemma_array_from_seq_roundtrip;
337
338        let (n, chunk) = Fixed::<U64_BYTE_LEN>.parse(ibuf)?;
339        assert(chunk@ == ibuf@[0..U64_BYTE_LEN]);
340
341        let bytes = [
342            chunk[0],
343            chunk[1],
344            chunk[2],
345            chunk[3],
346            chunk[4],
347            chunk[5],
348            chunk[6],
349            chunk[7],
350        ];
351        let value = i64_from_le_bytes(bytes);
352
353        assert(bytes@ == chunk@);
354
355        Ok((n, value))
356    }
357}
358
359impl<Output: OutputBuf> Serializer<Output, i64> for super::I64Le {
360    fn serialize_into(&self, v: &i64, obuf: &mut Output) {
361        let bytes = i64_to_le_bytes(*v);
362        obuf.write_bytes(&bytes);
363    }
364}
365
366impl ByteLen<i64> for super::I64Le {
367    fn length(&self, _v: &i64) -> (len: usize) {
368        U64_BYTE_LEN
369    }
370}
371
372impl Prepare<i64> for super::I64Le {
373    fn prepare(&self, _v: &i64) -> (checked: Result<usize, PreSerializeError>) {
374        Ok(U64_BYTE_LEN)
375    }
376}
377
378impl Parser<&[u8]> for super::I64Be {
379    type PT = i64;
380
381    fn min_byte_len(&self) -> usize {
382        U64_BYTE_LEN
383    }
384
385    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
386        broadcast use lemma_array_from_seq_roundtrip;
387
388        let (n, chunk) = Fixed::<U64_BYTE_LEN>.parse(ibuf)?;
389        assert(chunk@ == ibuf@[0..U64_BYTE_LEN]);
390
391        let bytes = [
392            chunk[0],
393            chunk[1],
394            chunk[2],
395            chunk[3],
396            chunk[4],
397            chunk[5],
398            chunk[6],
399            chunk[7],
400        ];
401        let value = i64_from_be_bytes(bytes);
402
403        assert(bytes@ == chunk@);
404
405        Ok((n, value))
406    }
407}
408
409impl<Output: OutputBuf> Serializer<Output, i64> for super::I64Be {
410    fn serialize_into(&self, v: &i64, obuf: &mut Output) {
411        let bytes = i64_to_be_bytes(*v);
412        obuf.write_bytes(&bytes);
413    }
414}
415
416impl ByteLen<i64> for super::I64Be {
417    fn length(&self, _v: &i64) -> (len: usize) {
418        U64_BYTE_LEN
419    }
420}
421
422impl Prepare<i64> for super::I64Be {
423    fn prepare(&self, _v: &i64) -> (checked: Result<usize, PreSerializeError>) {
424        Ok(U64_BYTE_LEN)
425    }
426}
427
428} // verus!
vest_lib/combinators/sints/exec.rs

vest_lib/combinators/sints/
exec.rs
