vest_lib/combinators/terminated/
exec.rs

1//! Executable implementation for sequential formats discarding their suffix.
2use crate::core::exec::output::*;
3use crate::{
4    combinators::Pair,
5    core::{
6        exec::{
7            input::InputBuf,
8            parser::{PResult, Parser},
9            serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
10            ParseError,
11        },
12        spec::{SafeParser, SpecByteLen, SpecParser, SpecSerializer},
13    },
14};
15use vstd::prelude::*;
16use OutputBuf;
17
18verus! {
19
20// Malleable version
21impl<I, A, B, BVal> Parser<I> for super::Terminated<A, B, BVal, false> where
22    I: InputBuf,
23    A: Parser<I> + SafeParser,
24    B: Parser<I, PT = BVal> + SafeParser<PVal = BVal>,
25    BVal: DeepView<V = BVal>,
26 {
27    type PT = A::PT;
28
29    fn min_byte_len(&self) -> usize {
30        self.a.min_byte_len().saturating_add(self.b.min_byte_len())
31    }
32
33    open spec fn exec_inv(&self) -> bool {
34        Pair(&self.a, &self.b).exec_inv()
35    }
36
37    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
38        let (n, (v, _)) = Pair(&self.a, &self.b).parse(ibuf)?;
39        Ok((n, v))
40    }
41}
42
43// Non-malleable version
44impl<I, A, B, BVal> Parser<I> for super::Terminated<A, B, BVal, true> where
45    I: InputBuf,
46    A: Parser<I> + SafeParser,
47    B: Parser<I, PT = BVal> + SafeParser<PVal = BVal>,
48    BVal: DeepView<V = BVal> + PartialEq + Structural,
49 {
50    type PT = A::PT;
51
52    fn min_byte_len(&self) -> usize {
53        self.a.min_byte_len().saturating_add(self.b.min_byte_len())
54    }
55
56    open spec fn exec_inv(&self) -> bool {
57        &&& Pair(&self.a, &self.b).exec_inv()
58        &&& forall|v: BVal| v.deep_view() == v
59    }
60
61    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
62        let (n, (v, vb)) = Pair(&self.a, &self.b).parse(ibuf)?;
63        if vb == self.b_val {
64            Ok((n, v))
65        } else {
66            Err(ParseError::non_canonical())
67        }
68    }
69}
70
71impl<Output: OutputBuf, A, B, BVal, T, const CHECK: bool> Serializer<
72    Output,
73    T,
74> for super::Terminated<A, B, BVal, CHECK> where
75    T: DeepView,
76    BVal: DeepView<V = BVal>,
77    A: Serializer<Output, T>,
78    B: Serializer<Output, BVal>,
79 {
80    #[verifier::prophetic]
81    open spec fn exec_inv(&self) -> bool {
82        &&& self.a.exec_inv()
83        &&& self.b.exec_inv()
84        &&& forall|v: BVal| v.deep_view() == v
85    }
86
87    fn serialize_into(&self, v: &T, obuf: &mut Output) {
88        broadcast use crate::core::exec::output::outbuf_lemmas;
89
90        self.a.serialize_into(v, obuf);
91        self.b.serialize_into(&self.b_val, obuf);
92    }
93}
94
95impl<A, B, BVal, T, const CHECK: bool> ByteLen<T> for super::Terminated<A, B, BVal, CHECK> where
96    T: DeepView,
97    BVal: DeepView<V = BVal>,
98    A: ByteLen<T>,
99    B: ByteLen<BVal>,
100 {
101    open spec fn exec_inv(&self) -> bool {
102        &&& self.a.exec_inv()
103        &&& self.b.exec_inv()
104        &&& forall|v: BVal| v.deep_view() == v
105    }
106
107    fn length(&self, v: &T) -> (len: usize) {
108        self.a.length(v) + self.b.length(&self.b_val)
109    }
110}
111
112impl<A, B, BVal, T, const CHECK: bool> Prepare<T> for super::Terminated<A, B, BVal, CHECK> where
113    T: DeepView,
114    BVal: DeepView<V = BVal>,
115    A: Prepare<T>,
116    B: Prepare<BVal>,
117 {
118    open spec fn exec_inv(&self) -> bool {
119        &&& self.a.exec_inv()
120        &&& self.b.exec_inv()
121        &&& forall|v: BVal| v.deep_view() == v
122    }
123
124    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
125        let la = self.a.prepare(v)?;
126        let lb = self.b.prepare(&self.b_val)?;
127        if let Some(total) = la.checked_add(lb) {
128            Ok(total)
129        } else {
130            Err(PreSerializeError::length_too_large())
131        }
132    }
133}
134
135} // verus!
vest_lib/combinators/terminated/exec.rs

vest_lib/combinators/terminated/
exec.rs
