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    open spec fn exec_inv(&self) -> bool {
130        true
131    }
132
133    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
134        if ibuf.len() < 1 {
135            Err(ParseError::unexpected_eof())
136        } else {
137            Ok((1, ibuf[0] as i8))
138        }
139    }
140}
141
142impl<Output: OutputBuf> Serializer<Output, i8> for super::I8 {
143    fn serialize_into(&self, v: &i8, obuf: &mut Output) {
144        obuf.write_byte(*v as u8);
145    }
146}
147
148impl ByteLen<i8> for super::I8 {
149    fn length(&self, _v: &i8) -> (len: usize) {
150        U8_BYTE_LEN
151    }
152}
153
154impl Prepare<i8> for super::I8 {
155    fn prepare(&self, _v: &i8) -> (checked: Result<usize, PreSerializeError>) {
156        Ok(U8_BYTE_LEN)
157    }
158}
159
160impl Parser<&[u8]> for super::I16Le {
161    type PT = i16;
162
163    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
164        broadcast use lemma_array_from_seq_roundtrip;
165
166        let (n, chunk) = Fixed::<U16_BYTE_LEN>.parse(ibuf)?;
167        assert(chunk@ == ibuf@.take(U16_BYTE_LEN as int));
168
169        let bytes = [chunk[0], chunk[1]];
170        let value = i16_from_le_bytes(bytes);
171
172        assert(bytes@ == chunk@);
173
174        Ok((n, value))
175    }
176}
177
178impl<Output: OutputBuf> Serializer<Output, i16> for super::I16Le {
179    fn serialize_into(&self, v: &i16, obuf: &mut Output) {
180        let bytes = i16_to_le_bytes(*v);
181        obuf.write_bytes(&bytes);
182    }
183}
184
185impl ByteLen<i16> for super::I16Le {
186    fn length(&self, _v: &i16) -> (len: usize) {
187        U16_BYTE_LEN
188    }
189}
190
191impl Prepare<i16> for super::I16Le {
192    fn prepare(&self, _v: &i16) -> (checked: Result<usize, PreSerializeError>) {
193        Ok(U16_BYTE_LEN)
194    }
195}
196
197impl Parser<&[u8]> for super::I16Be {
198    type PT = i16;
199
200    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
201        broadcast use lemma_array_from_seq_roundtrip;
202
203        let (n, chunk) = Fixed::<U16_BYTE_LEN>.parse(ibuf)?;
204        assert(chunk@ == ibuf@.take(U16_BYTE_LEN as int));
205
206        let bytes = [chunk[0], chunk[1]];
207        let value = i16_from_be_bytes(bytes);
208
209        assert(bytes@ == chunk@);
210
211        Ok((n, value))
212    }
213}
214
215impl<Output: OutputBuf> Serializer<Output, i16> for super::I16Be {
216    fn serialize_into(&self, v: &i16, obuf: &mut Output) {
217        let bytes = i16_to_be_bytes(*v);
218        obuf.write_bytes(&bytes);
219    }
220}
221
222impl ByteLen<i16> for super::I16Be {
223    fn length(&self, _v: &i16) -> (len: usize) {
224        U16_BYTE_LEN
225    }
226}
227
228impl Prepare<i16> for super::I16Be {
229    fn prepare(&self, _v: &i16) -> (checked: Result<usize, PreSerializeError>) {
230        Ok(U16_BYTE_LEN)
231    }
232}
233
234impl Parser<&[u8]> for super::I32Le {
235    type PT = i32;
236
237    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
238        broadcast use lemma_array_from_seq_roundtrip;
239
240        let (n, chunk) = Fixed::<U32_BYTE_LEN>.parse(ibuf)?;
241        assert(chunk@ == ibuf@.take(U32_BYTE_LEN as int));
242
243        let bytes = [chunk[0], chunk[1], chunk[2], chunk[3]];
244        let value = i32_from_le_bytes(bytes);
245
246        assert(bytes@ == chunk@);
247
248        Ok((n, value))
249    }
250}
251
252impl<Output: OutputBuf> Serializer<Output, i32> for super::I32Le {
253    fn serialize_into(&self, v: &i32, obuf: &mut Output) {
254        let bytes = i32_to_le_bytes(*v);
255        obuf.write_bytes(&bytes);
256    }
257}
258
259impl ByteLen<i32> for super::I32Le {
260    fn length(&self, _v: &i32) -> (len: usize) {
261        U32_BYTE_LEN
262    }
263}
264
265impl Prepare<i32> for super::I32Le {
266    fn prepare(&self, _v: &i32) -> (checked: Result<usize, PreSerializeError>) {
267        Ok(U32_BYTE_LEN)
268    }
269}
270
271impl Parser<&[u8]> for super::I32Be {
272    type PT = i32;
273
274    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
275        broadcast use lemma_array_from_seq_roundtrip;
276
277        let (n, chunk) = Fixed::<U32_BYTE_LEN>.parse(ibuf)?;
278        assert(chunk@ == ibuf@.take(U32_BYTE_LEN as int));
279
280        let bytes = [chunk[0], chunk[1], chunk[2], chunk[3]];
281        let value = i32_from_be_bytes(bytes);
282
283        assert(bytes@ == chunk@);
284
285        Ok((n, value))
286    }
287}
288
289impl<Output: OutputBuf> Serializer<Output, i32> for super::I32Be {
290    fn serialize_into(&self, v: &i32, obuf: &mut Output) {
291        let bytes = i32_to_be_bytes(*v);
292        obuf.write_bytes(&bytes);
293    }
294}
295
296impl ByteLen<i32> for super::I32Be {
297    fn length(&self, _v: &i32) -> (len: usize) {
298        U32_BYTE_LEN
299    }
300}
301
302impl Prepare<i32> for super::I32Be {
303    fn prepare(&self, _v: &i32) -> (checked: Result<usize, PreSerializeError>) {
304        Ok(U32_BYTE_LEN)
305    }
306}
307
308impl Parser<&[u8]> for super::I64Le {
309    type PT = i64;
310
311    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
312        broadcast use lemma_array_from_seq_roundtrip;
313
314        let (n, chunk) = Fixed::<U64_BYTE_LEN>.parse(ibuf)?;
315        assert(chunk@ == ibuf@.take(U64_BYTE_LEN as int));
316
317        let bytes = [
318            chunk[0],
319            chunk[1],
320            chunk[2],
321            chunk[3],
322            chunk[4],
323            chunk[5],
324            chunk[6],
325            chunk[7],
326        ];
327        let value = i64_from_le_bytes(bytes);
328
329        assert(bytes@ == chunk@);
330
331        Ok((n, value))
332    }
333}
334
335impl<Output: OutputBuf> Serializer<Output, i64> for super::I64Le {
336    fn serialize_into(&self, v: &i64, obuf: &mut Output) {
337        let bytes = i64_to_le_bytes(*v);
338        obuf.write_bytes(&bytes);
339    }
340}
341
342impl ByteLen<i64> for super::I64Le {
343    fn length(&self, _v: &i64) -> (len: usize) {
344        U64_BYTE_LEN
345    }
346}
347
348impl Prepare<i64> for super::I64Le {
349    fn prepare(&self, _v: &i64) -> (checked: Result<usize, PreSerializeError>) {
350        Ok(U64_BYTE_LEN)
351    }
352}
353
354impl Parser<&[u8]> for super::I64Be {
355    type PT = i64;
356
357    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
358        broadcast use lemma_array_from_seq_roundtrip;
359
360        let (n, chunk) = Fixed::<U64_BYTE_LEN>.parse(ibuf)?;
361        assert(chunk@ == ibuf@.take(U64_BYTE_LEN as int));
362
363        let bytes = [
364            chunk[0],
365            chunk[1],
366            chunk[2],
367            chunk[3],
368            chunk[4],
369            chunk[5],
370            chunk[6],
371            chunk[7],
372        ];
373        let value = i64_from_be_bytes(bytes);
374
375        assert(bytes@ == chunk@);
376
377        Ok((n, value))
378    }
379}
380
381impl<Output: OutputBuf> Serializer<Output, i64> for super::I64Be {
382    fn serialize_into(&self, v: &i64, obuf: &mut Output) {
383        let bytes = i64_to_be_bytes(*v);
384        obuf.write_bytes(&bytes);
385    }
386}
387
388impl ByteLen<i64> for super::I64Be {
389    fn length(&self, _v: &i64) -> (len: usize) {
390        U64_BYTE_LEN
391    }
392}
393
394impl Prepare<i64> for super::I64Be {
395    fn prepare(&self, _v: &i64) -> (checked: Result<usize, PreSerializeError>) {
396        Ok(U64_BYTE_LEN)
397    }
398}
399
400} // verus!
vest_lib/combinators/sints/exec.rs

vest_lib/combinators/sints/
exec.rs
