vest_lib/combinators/recursive/
exec.rs

1//! Executable interfaces for bounded recursive format bodies.
2use super::{ParamRecSpecs, ProductiveRecBody, SafeParserRecBody, SpecRecBody};
3use crate::core::exec::output::*;
4use crate::core::exec::parser::*;
5use crate::core::exec::serializer::{
6    ByteLen, ComplianceErrorKind, PreSerializeError, Prepare, Serializer,
7};
8use crate::core::exec::{input::InputBuf, output::OutputBuf, ParseError};
9use crate::core::proof::Productive;
10use crate::core::spec::{
11    Consistency, GoodSerializer, SafeParser, SpecByteLen, SpecParser, SpecSerializer,
12};
13use vstd::prelude::*;
14
15verus! {
16
17/// Executable parsing for one recursive unfolding.
18pub trait ParserRecBody<I: InputBuf>: SpecRecBody {
19    type EP: DeepView<V = Self::Param>;
20
21    type O: DeepView<V = Self::T>;
22
23    /// Execute one recursive unfolding, using `exec_rec` for all recursive positions in the body.
24    ///
25    /// `spec_rec` is the ghost/spec callback bundle corresponding to `exec_rec`.
26    fn parse_body<Exec>(
27        &self,
28        param: &Self::EP,
29        Ghost(spec_rec): Ghost<ParamRecSpecs<Self::Param, Self::T>>,
30        exec_rec: Exec,
31        ibuf: &I,
32    ) -> (r: PResult<Self::O>) where Exec: Fn(&Self::EP, &I) -> PResult<Self::O>
33        requires
34            forall|p: Self::Param| #[trigger] spec_rec(p).safe_inv(),
35            forall|p: Self::Param| #[trigger] spec_rec(p).productive_inv(),
36            forall|pp: &Self::EP, i: &I| call_requires(exec_rec, (pp, i)),
37            forall|pp: &Self::EP, i: &I, rr: PResult<Self::O>|
38                call_ensures(exec_rec, (pp, i), rr) ==> parse_matches_spec(
39                    rr,
40                    spec_rec(pp.deep_view()).2(i@),
41                ),
42        ensures
43            parse_matches_spec(r, self.spec_body(param.deep_view(), spec_rec).spec_parse(ibuf@)),
44    ;
45}
46
47/// Executable serialization for one recursive unfolding.
48pub trait SerializerRecBody<Output, T>: SpecRecBody where
49    Output: OutputBuf,
50    T: DeepView<V = Self::T>,
51 {
52    type EP: DeepView<V = Self::Param>;
53
54    /// Execute one recursive unfolding, using `exec_rec` for all recursive positions in the body.
55    ///
56    /// `spec_rec` is the ghost/spec callback bundle corresponding to `exec_rec`.
57    fn serialize_body<Exec>(
58        &self,
59        param: &Self::EP,
60        Ghost(spec_rec): Ghost<ParamRecSpecs<Self::Param, Self::T>>,
61        exec_rec: Exec,
62        v: &T,
63        obuf: &mut Output,
64    ) where Exec: Fn(&Self::EP, &T, &mut Output)
65        requires
66            self.spec_body(param.deep_view(), spec_rec).consistent(v.deep_view()),
67            old(obuf).fits(self.spec_body(param.deep_view(), spec_rec).byte_len(v.deep_view())),
68            forall|pp: &Self::EP, vv: &T, out: &mut Output|
69                {
70                    &&& spec_rec(pp.deep_view()).0(vv.deep_view())
71                    &&& out.fits(spec_rec(pp.deep_view()).1(vv.deep_view()))
72                } ==> call_requires(exec_rec, (pp, vv, out)),
73            forall|pp: &Self::EP, vv: &T, out: &mut Output|
74                call_ensures(exec_rec, (pp, vv, out), ()) ==> {
75                    &&& final(out)@ == out@ + spec_rec(pp.deep_view()).3(vv.deep_view())
76                    &&& forall|n|
77                        out.fits(spec_rec(pp.deep_view()).1(vv.deep_view()) + n)
78                            <==> #[trigger] final(out).fits(n)
79                    &&& out.same_destination(final(out))
80                },
81        ensures
82            final(obuf)@ == old(obuf)@ + self.spec_body(param.deep_view(), spec_rec).spec_serialize(
83                v.deep_view(),
84            ),
85            forall|n|
86                old(obuf).fits(
87                    self.spec_body(param.deep_view(), spec_rec).byte_len(v.deep_view()) + n,
88                ) <==> #[trigger] final(obuf).fits(n),
89            old(obuf).same_destination(final(obuf)),
90    ;
91}
92
93/// Executable pre-serialization analysis for one recursive unfolding.
94pub trait PrepareRecBody<T>: SpecRecBody where T: DeepView<V = Self::T> {
95    type EP: DeepView<V = Self::Param>;
96
97    /// Execute one recursive unfolding, using `exec_rec` for all recursive positions in the body.
98    ///
99    /// `spec_rec` is the ghost/spec callback bundle corresponding to `exec_rec`.
100    fn prepare_body<Exec>(
101        &self,
102        param: &Self::EP,
103        Ghost(spec_rec): Ghost<ParamRecSpecs<Self::Param, Self::T>>,
104        exec_rec: Exec,
105        v: &T,
106    ) -> (checked: Result<usize, PreSerializeError>) where
107        Exec: Fn(&Self::EP, &T) -> Result<usize, PreSerializeError>,
108
109        requires
110            forall|pp: &Self::EP, vv: &T| call_requires(exec_rec, (pp, vv)),
111            forall|pp: &Self::EP, vv: &T, rr: Result<usize, PreSerializeError>|
112                call_ensures(exec_rec, (pp, vv), rr) ==> (rr matches Ok(len) ==> {
113                    &&& spec_rec(pp.deep_view()).0(vv.deep_view())
114                    &&& len == spec_rec(pp.deep_view()).1(vv.deep_view())
115                }),
116        ensures
117            checked matches Ok(len) ==> {
118                &&& self.spec_body(param.deep_view(), spec_rec).consistent(v.deep_view())
119                &&& len == self.spec_body(param.deep_view(), spec_rec).byte_len(v.deep_view())
120            },
121    ;
122}
123
124impl<const LIMIT: usize, Body, Param> super::FixWith<LIMIT, Body, Param> where
125    Body: SpecRecBody,
126    Param: DeepView<V = Body::Param>,
127 {
128    fn parse_gas<I>(&self, gas: usize, param: &Param, ibuf: &I) -> (r: PResult<Body::O>) where
129        I: InputBuf,
130        Param: DeepView<V = Body::Param>,
131        Body: ParserRecBody<I, EP = Param> + ProductiveRecBody,
132        Body::Body: Productive,
133
134        ensures
135            parse_matches_spec(
136                r,
137                Self::spec_parse_gas(&self.0, gas as nat, param.deep_view(), ibuf@),
138            ),
139        decreases gas,
140    {
141        let ghost body = self.0;
142        let exec_callback = |pp: &Param, i: &I| -> (rr: PResult<Body::O>)
143            ensures
144                parse_matches_spec(
145                    rr,
146                    Self::spec_parse_callback(&body, gas as nat, pp.deep_view())(i@),
147                ),
148            {
149                if gas > 0 {
150                    self.parse_gas((gas - 1) as usize, pp, i)
151                } else {
152                    Err(ParseError::recursion_limit_exceeded())
153                }
154            };
155
156        let ghost spec_callback = Self::specs_callback(&body, gas as nat);
157        proof {
158            assert forall|p: Body::Param, input: Seq<u8>| #[trigger]
159                spec_callback(p).2(input) matches Some((n, _v)) ==> 0 <= n <= input.len() by {
160                if let Some((n, v)) = spec_callback(p).2(input) {
161                    if gas > 0 {
162                        self.safe_parser_by_induction((gas - 1) as nat, p, input, n, v);
163                    }
164                }
165            }
166            assert forall|p: Body::Param| #[trigger] spec_callback(p).safe_inv() by {
167                assert(spec_callback(p).safe_inv());
168            }
169            assert forall|p: Body::Param| #[trigger] spec_callback(p).productive_inv() by {
170                assert forall|input: Seq<u8>| #[trigger]
171                    spec_callback(p).2(input) matches Some((n, _v)) ==> n > 0 by {
172                    if let Some((n, v)) = spec_callback(p).2(input) {
173                        if gas > 0 {
174                            self.productive_by_induction((gas - 1) as nat, p, input, n, v);
175                        }
176                    }
177                }
178                assert(spec_callback(p).productive_inv());
179            }
180        }
181
182        self.0.parse_body(param, Ghost(spec_callback), exec_callback, ibuf)
183    }
184
185    fn serialize_gas<Output, T>(&self, gas: usize, param: &Param, v: &T, obuf: &mut Output) where
186        Output: OutputBuf,
187        T: DeepView<V = Body::T>,
188        Param: DeepView<V = Body::Param>,
189        Body: SerializerRecBody<Output, T, EP = Param>,
190
191        requires
192            Self::consistent_gas(&self.0, gas as nat, param.deep_view(), v.deep_view()),
193            old(obuf).fits(
194                Self::byte_len_gas(&self.0, gas as nat, param.deep_view(), v.deep_view()),
195            ),
196        ensures
197            final(obuf)@ == old(obuf)@ + Self::spec_serialize_gas(
198                &self.0,
199                gas as nat,
200                param.deep_view(),
201                v.deep_view(),
202            ),
203            forall|n|
204                old(obuf).fits(
205                    Self::byte_len_gas(&self.0, gas as nat, param.deep_view(), v.deep_view()) + n,
206                ) <==> #[trigger] final(obuf).fits(n),
207            old(obuf).same_destination(final(obuf)),
208        decreases gas,
209    {
210        let ghost body = self.0;
211        let exec_callback = |pp: &Param, vv: &T, oo: &mut Output| -> ()
212            requires
213                Self::consistent_callback(&body, gas as nat, pp.deep_view())(vv.deep_view()),
214                old(oo).fits(
215                    Self::byte_len_callback(&body, gas as nat, pp.deep_view())(vv.deep_view()),
216                ),
217            ensures
218                final(oo)@ == old(oo)@ + Self::spec_serialize_callback(
219                    &body,
220                    gas as nat,
221                    pp.deep_view(),
222                )(vv.deep_view()),
223                forall|n|
224                    old(oo).fits(
225                        Self::byte_len_callback(&body, gas as nat, pp.deep_view())(vv.deep_view())
226                            + n,
227                    ) <==> #[trigger] final(oo).fits(n),
228                old(oo).same_destination(final(oo)),
229            {
230                if gas > 0 {
231                    self.serialize_gas((gas - 1) as usize, pp, vv, oo);
232                }
233            };
234
235        let ghost spec_callback = Self::specs_callback(&body, gas as nat);
236        self.0.serialize_body(param, Ghost(spec_callback), exec_callback, v, obuf)
237    }
238
239    fn prepare_gas<T>(&self, gas: usize, param: &Param, v: &T) -> (checked: Result<
240        usize,
241        PreSerializeError,
242    >) where
243        T: DeepView<V = Body::T>,
244        Param: DeepView<V = Body::Param>,
245        Body: PrepareRecBody<T, EP = Param>,
246
247        ensures
248            checked matches Ok(len) ==> {
249                &&& Self::consistent_gas(&self.0, gas as nat, param.deep_view(), v.deep_view())
250                &&& len == Self::byte_len_gas(&self.0, gas as nat, param.deep_view(), v.deep_view())
251            },
252        decreases gas,
253    {
254        let ghost body = self.0;
255        let exec_callback = |pp: &Param, vv: &T| -> (rr: Result<usize, PreSerializeError>)
256            ensures
257                rr matches Ok(len) ==> {
258                    &&& Self::consistent_callback(&body, gas as nat, pp.deep_view())(vv.deep_view())
259                    &&& len == Self::byte_len_callback(&body, gas as nat, pp.deep_view())(
260                        vv.deep_view(),
261                    )
262                },
263            {
264                if gas > 0 {
265                    self.prepare_gas((gas - 1) as usize, pp, vv)
266                } else {
267                    Err(
268                        PreSerializeError::not_compliant(
269                            ComplianceErrorKind::RecursionLimitExceeded,
270                        ),
271                    )
272                }
273            };
274
275        let ghost spec_callback = Self::specs_callback(&body, gas as nat);
276        self.0.prepare_body(param, Ghost(spec_callback), exec_callback, v)
277    }
278}
279
280impl<const LIMIT: usize, Body, Param, I> Parser<I> for super::FixWith<LIMIT, Body, Param> where
281    I: InputBuf,
282    Param: DeepView<V = Body::Param>,
283    Body: ParserRecBody<I, EP = Param> + ProductiveRecBody,
284    Body::Body: Productive,
285 {
286    type PT = Body::O;
287
288    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
289        self.parse_gas(LIMIT, &self.1, ibuf)
290    }
291}
292
293impl<Output: OutputBuf, T, const LIMIT: usize, Body, Param> Serializer<
294    Output,
295    T,
296> for super::FixWith<LIMIT, Body, Param> where
297    T: DeepView<V = Body::T>,
298    Param: DeepView<V = Body::Param>,
299    Body: SerializerRecBody<Output, T, EP = Param>,
300 {
301    fn serialize_into(&self, v: &T, obuf: &mut Output) {
302        self.serialize_gas(LIMIT, &self.1, v, obuf)
303    }
304}
305
306impl<T, const LIMIT: usize, Body, Param> Prepare<T> for super::FixWith<LIMIT, Body, Param> where
307    T: DeepView<V = Body::T>,
308    Param: DeepView<V = Body::Param>,
309    Body: PrepareRecBody<T, EP = Param>,
310 {
311    open spec fn exec_inv(&self) -> bool {
312        true
313    }
314
315    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
316        self.prepare_gas(LIMIT, &self.1, v)
317    }
318}
319
320} // verus!
vest_lib/combinators/recursive/exec.rs

vest_lib/combinators/recursive/
exec.rs
