vest_lib/combinators/star/
exec.rs

1//! Executable zero-or-more repetition.
2use super::spec::*;
3use crate::combinators::length::AsLen;
4use crate::core::exec::output::*;
5use crate::core::{
6    exec::{
7        input::InputBuf,
8        parser::{PResult, Parser},
9        serializer::{ByteLen, ComplianceErrorKind, PreSerializeError, Prepare, Serializer},
10        ParseError,
11    },
12    proof::Productive,
13    spec::{Consistency, SafeParser, SpecByteLen, SpecParser, SpecSerializer},
14};
15#[cfg(feature = "alloc")]
16use alloc::vec::Vec;
17use vstd::prelude::*;
18use OutputBuf;
19
20verus! {
21
22#[cfg(feature = "alloc")]
23impl<I, Inner> Parser<I> for super::Star<Inner> where I: InputBuf, Inner: Parser<I> + Productive {
24    type PT = Vec<Inner::PT>;
25
26    open spec fn exec_inv(&self) -> bool {
27        &&& self.0.exec_inv()
28        &&& self.0.safe_inv()
29        &&& self.0.productive_inv()
30    }
31
32    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
33        reveal(<super::Star::<_> as SpecParser>::spec_parse);
34        broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
35
36        let total_len = ibuf.len();
37        let mut consumed: usize = 0;
38        let mut remaining = total_len;
39        let mut rest = ibuf.skip(0);
40        let mut values = Vec::new();
41
42        while remaining > 0
43            invariant
44                self.exec_inv(),
45                consumed + remaining == total_len,
46                remaining == rest@.len(),
47                ({
48                    let prefix = values.deep_view();
49                    let (n, suffix) = self.parse_rec(rest@);
50                    self.parse_rec(ibuf@) == (consumed + n, prefix + suffix)
51                }),
52            decreases remaining,
53        {
54            broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
55
56            reveal(<super::Star::<_> as SpecParser>::spec_parse);
57
58            match self.0.parse(&rest) {
59                Ok((n, v)) => {
60                    proof {
61                        self.0.lemma_productive(rest@);
62                        assert(n > 0);
63                    }
64                    values.push(v);
65                    rest = rest.skip(n);
66                    consumed += n;
67                    remaining -= n;
68                },
69                Err(_) => return Ok((consumed, values)),
70            }
71        }
72        Ok((consumed, values))
73    }
74}
75
76#[cfg(feature = "alloc")]
77impl<I, A, B> Parser<I> for super::Repeat<A, B> where
78    I: InputBuf,
79    A: Parser<I> + SafeParser + Productive + Copy,
80    B: Parser<I> + SafeParser + Copy,
81 {
82    type PT = (Vec<A::PT>, B::PT);
83
84    open spec fn exec_inv(&self) -> bool {
85        &&& self.0.exec_inv()
86        &&& self.0.safe_inv()
87        &&& self.0.productive_inv()
88        &&& self.1.exec_inv()
89        &&& self.1.safe_inv()
90    }
91
92    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
93        crate::combinators::Pair(super::Star(self.0), self.1).parse(ibuf)
94    }
95}
96
97#[cfg(feature = "alloc")]
98impl<I, Inner, N> Parser<I> for super::RepeatN<Inner, N> where
99    I: InputBuf,
100    Inner: Parser<I> + SafeParser,
101    N: AsLen,
102 {
103    type PT = Vec<Inner::PT>;
104
105    open spec fn exec_inv(&self) -> bool {
106        &&& self.1.exec_inv()
107        &&& self.1.safe_inv()
108    }
109
110    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
111        broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
112
113        let count = self.0.get();
114        let _total_len = ibuf.len();
115        let mut consumed: usize = 0;
116        let mut rest = ibuf.skip(0);
117        let mut values = Vec::new();
118
119        for _i in 0..count
120            invariant
121                self.exec_inv(),
122                count as nat == self.0.as_nat(),
123                consumed + rest@.len() == _total_len,
124                ({
125                    let prefix = values.deep_view();
126                    let parsed = self.parse_n_rec(count as nat, ibuf@);
127                    match self.parse_n_rec((count - _i) as nat, rest@) {
128                        Some((n, suffix)) => parsed == Some((consumed + n, prefix + suffix)),
129                        None => parsed is None,
130                    }
131                }),
132        {
133            broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
134
135            let (n, v) = self.1.parse(&rest)?;
136            values.push(v);
137            rest = rest.skip(n);
138            consumed += n;
139        }
140        Ok((consumed, values))
141    }
142}
143
144// pub assume_specification<T, const N: usize, F: FnMut(usize) -> T>[ core::array::from_fn ](
145//     f: F,
146// ) -> (out: [T; N])
147//     requires
148//         forall|i: int| 0 <= i < N ==> #[trigger] call_requires(f, (i as usize,)),
149//     ensures
150//         forall|i: int| 0 <= i < N ==> call_ensures(f, (i as usize,), #[trigger] out[i]),
151// ;
152// pub assume_specification<T, const N: usize, F: FnMut(T) -> U, U>[ <[T; N]>::map ](
153//     arr: [T; N],
154//     f: F,
155// ) -> (out: [U; N])
156//     requires
157//         forall|i: int| 0 <= i < N ==> #[trigger] call_requires(f, (arr[i],)),
158//     ensures
159//         forall|i: int|
160//             #![trigger arr[i]]
161//             #![trigger out[i]]
162//             0 <= i < N ==> call_ensures(f, (arr[i],), out[i]),
163// ;
164#[inline(always)]
165#[verifier::external_body]
166pub fn array_of_none<T, const N: usize>() -> (out: [Option<T>; N])
167    ensures
168        forall|j: int| 0 <= j < N ==> #[trigger] out@[j] is None,
169{
170    core::array::from_fn(|_i| None)
171}
172
173#[inline(always)]
174#[verifier::external_body]
175pub fn array_option_unwrap<T: DeepView, const N: usize>(arr: [Option<T>; N]) -> (out: [T; N])
176    requires
177        forall|j: int| 0 <= j < N ==> #[trigger] arr@[j] is Some,
178    ensures
179        out.deep_view() == Seq::new(N as nat, |j| arr@[j]->0.deep_view()),
180{
181    arr.map(Option::<T>::unwrap)
182}
183
184impl<I, Inner, const N: usize> Parser<I> for super::Array<N, Inner> where
185    I: InputBuf,
186    Inner: Parser<I> + SafeParser,
187 {
188    type PT = [Inner::PT; N];
189
190    open spec fn exec_inv(&self) -> bool {
191        &&& self.0.exec_inv()
192        &&& self.0.safe_inv()
193    }
194
195    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
196        broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
197
198        let mut consumed: usize = 0;
199        let _total_len = ibuf.len();
200        let mut rest = ibuf.skip(0);
201        let mut arr: [Option<Inner::PT>; N] = array_of_none();
202
203        for i in 0..N
204            invariant
205                self.exec_inv(),
206                consumed + rest@.len() == _total_len,
207                forall|j: int| 0 <= j < i ==> #[trigger] arr@[j] is Some,
208                forall|j: int| i <= j < N ==> #[trigger] arr@[j] is None,
209                ({
210                    let prefix = Seq::new(i as nat, |j| arr@[j]->0.deep_view());
211                    match super::RepeatN(N, self.0).parse_n_rec((N - i) as nat, rest@) {
212                        Some((n, suffix)) => self.spec_parse(ibuf@) == Some(
213                            (consumed + n, prefix + suffix),
214                        ),
215                        None => self.spec_parse(ibuf@) is None,
216                    }
217                }),
218        {
219            broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
220
221            let (n, v) = self.0.parse(&rest)?;
222            let elem = Some(v);
223            arr[i] = elem;
224            rest = rest.skip(n);
225            consumed += n;
226        }
227
228        let arr = array_option_unwrap(arr);
229
230        Ok((consumed, arr))
231    }
232}
233
234#[verifier::loop_isolation(false)]
235pub fn serialize_slice<Output, Inner, T>(inner: &Inner, values: &[T], obuf: &mut Output) where
236    Output: OutputBuf,
237    T: DeepView,
238    Inner: Serializer<Output, T>,
239
240    requires
241        inner.exec_inv(),
242        (super::Star(*inner)).consistent(values.deep_view()),
243        old(obuf).fits((super::Star(*inner)).byte_len(values.deep_view())),
244    ensures
245        final(obuf)@ == old(obuf)@ + spec_serialize_seq(inner, values.deep_view()),
246        forall|n|
247            old(obuf).fits((super::Star(*inner)).byte_len(values.deep_view()) + n)
248                <==> #[trigger] final(obuf).fits(n),
249        old(obuf).same_destination(final(obuf)),
250{
251    broadcast use crate::core::exec::output::outbuf_lemmas;
252
253    reveal(<super::Star::<_> as SpecByteLen>::byte_len);
254    reveal(<super::Star::<_> as Consistency>::consistent);
255
256    let ghost vs = values.deep_view();
257    let ghost star = super::Star(*inner);
258    let ghost mut consumed: nat = 0;
259
260    for i in 0..values.len()
261        invariant
262            consumed + star.byte_len(vs.skip(i as int)) == star.byte_len(vs),
263            obuf@ == old(obuf)@ + spec_serialize_seq(inner, vs.take(i as int)),
264            forall|n| old(obuf).fits(consumed + n) <==> #[trigger] obuf.fits(n),
265            old(obuf).same_destination(obuf),
266    {
267        proof {
268            let elem_len = inner.byte_len(vs[i as int]);
269            assert(vs.skip(i as int) == seq![vs[i as int]] + vs.skip(i + 1));
270            star.lemma_byte_len_cons(vs[i as int], vs.skip(i + 1));
271            assert(vs.take(i + 1) == vs.take(i as int).push(vs[i as int]));
272            assert(vs.take(i as int).push(vs[i as int]).drop_last() == vs.take(i as int));
273            consumed = consumed + elem_len;
274        }
275        inner.serialize_into(&values[i], obuf);
276    }
277}
278
279#[verifier::loop_isolation(false)]
280pub fn length_slice<Inner, T>(fmt: &Inner, values: &[T]) -> (len: usize) where
281    Inner: ByteLen<T>,
282    T: DeepView,
283
284    requires
285        fmt.exec_inv(),
286        (super::Star(*fmt)).byte_len(values.deep_view()) <= usize::MAX,
287    ensures
288        len == (super::Star(*fmt)).byte_len(values.deep_view()),
289{
290    reveal(<super::Star::<_> as SpecByteLen>::byte_len);
291    let ghost vs = values.deep_view();
292    let ghost star = super::Star(*fmt);
293
294    let mut len = 0usize;
295    for i in 0..values.len()
296        invariant
297            len + star.byte_len(vs.skip(i as int)) == star.byte_len(vs),
298    {
299        proof {
300            assert(vs.skip(i as int) == seq![vs[i as int]] + vs.skip(i + 1));
301            star.lemma_byte_len_cons(vs[i as int], vs.skip(i + 1));
302        }
303        let l = fmt.length(&values[i]);
304        len += l;
305    }
306    len
307}
308
309#[verifier::loop_isolation(false)]
310pub fn prepare_slice<Inner, T>(fmt: &Inner, values: &[T]) -> (checked: Result<
311    usize,
312    PreSerializeError,
313>) where Inner: Prepare<T>, T: DeepView
314    requires
315        fmt.exec_inv(),
316    ensures
317        checked matches Ok(len) ==> {
318            &&& (super::Star(*fmt)).consistent(values.deep_view())
319            &&& len == (super::Star(*fmt)).byte_len(values.deep_view())
320        },
321{
322    reveal(<super::Star::<_> as Consistency>::consistent);
323    reveal(<super::Star::<_> as SpecByteLen>::byte_len);
324    let ghost vs = values.deep_view();
325    let ghost star = super::Star(*fmt);
326
327    let mut len = 0usize;
328    for i in 0..values.len()
329        invariant
330            forall|j: int| 0 <= j < i ==> fmt.consistent(#[trigger] vs[j]),
331            len + star.byte_len(vs.skip(i as int)) == star.byte_len(vs),
332    {
333        proof {
334            assert(vs.skip(i as int) == seq![vs[i as int]] + vs.skip(i + 1));
335            star.lemma_byte_len_cons(vs[i as int], vs.skip(i + 1));
336        }
337        let elem_len = fmt.prepare(&values[i])?;
338        match len.checked_add(elem_len) {
339            Some(total) => len = total,
340            None => return Err(PreSerializeError::length_too_large()),
341        }
342    }
343    Ok(len)
344}
345
346impl<Output: OutputBuf, Inner, T> Serializer<Output, [T]> for super::Star<Inner> where
347    T: DeepView,
348    Inner: Serializer<Output, T>,
349 {
350    #[verifier::prophetic]
351    open spec fn exec_inv(&self) -> bool {
352        self.0.exec_inv()
353    }
354
355    fn serialize_into(&self, v: &[T], obuf: &mut Output) {
356        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
357        serialize_slice(&self.0, v, obuf);
358    }
359}
360
361impl<Inner, T> ByteLen<[T]> for super::Star<Inner> where Inner: ByteLen<T>, T: DeepView {
362    open spec fn exec_inv(&self) -> bool {
363        self.0.exec_inv()
364    }
365
366    fn length(&self, v: &[T]) -> (len: usize) {
367        length_slice(&self.0, v)
368    }
369}
370
371impl<Inner, T> Prepare<[T]> for super::Star<Inner> where Inner: Prepare<T>, T: DeepView {
372    open spec fn exec_inv(&self) -> bool {
373        self.0.exec_inv()
374    }
375
376    fn prepare(&self, v: &[T]) -> (checked: Result<usize, PreSerializeError>) {
377        prepare_slice(&self.0, v)
378    }
379}
380
381impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (&[TA], TB)> for super::Repeat<A, B> where
382    TA: DeepView,
383    TB: DeepView,
384    A: Serializer<Output, TA> + Copy,
385    B: Serializer<Output, TB>,
386 {
387    #[verifier::prophetic]
388    open spec fn exec_inv(&self) -> bool {
389        &&& self.0.exec_inv()
390        &&& self.1.exec_inv()
391    }
392
393    fn serialize_into(&self, v: &(&[TA], TB), obuf: &mut Output) {
394        broadcast use crate::core::exec::output::outbuf_lemmas;
395
396        reveal(<super::Star<_> as SpecSerializer>::spec_serialize);
397
398        super::Star(self.0).serialize_into(v.0, obuf);
399        assert(obuf.fits(self.1.byte_len(v.deep_view().1)));
400        self.1.serialize_into(&v.1, obuf);
401    }
402}
403
404impl<A, B, TA, TB> ByteLen<(&[TA], TB)> for super::Repeat<A, B> where
405    A: ByteLen<TA> + Copy,
406    B: ByteLen<TB>,
407    TA: DeepView,
408    TB: DeepView,
409 {
410    open spec fn exec_inv(&self) -> bool {
411        &&& self.0.exec_inv()
412        &&& self.1.exec_inv()
413    }
414
415    fn length(&self, v: &(&[TA], TB)) -> (len: usize) {
416        let la = super::Star(self.0).length(v.0);
417        let lb = self.1.length(&v.1);
418        la + lb
419    }
420}
421
422impl<A, B, TA, TB> Prepare<(&[TA], TB)> for super::Repeat<A, B> where
423    A: Prepare<TA> + Copy,
424    B: Prepare<TB>,
425    TA: DeepView,
426    TB: DeepView,
427 {
428    open spec fn exec_inv(&self) -> bool {
429        &&& self.0.exec_inv()
430        &&& self.1.exec_inv()
431    }
432
433    fn prepare(&self, v: &(&[TA], TB)) -> (checked: Result<usize, PreSerializeError>) {
434        let la = super::Star(self.0).prepare(v.0)?;
435        let lb = self.1.prepare(&v.1)?;
436        match la.checked_add(lb) {
437            Some(total) => Ok(total),
438            None => Err(PreSerializeError::length_too_large()),
439        }
440    }
441}
442
443impl<Output: OutputBuf, Inner, N, T> Serializer<Output, [T]> for super::RepeatN<Inner, N> where
444    T: DeepView,
445    Inner: Serializer<Output, T>,
446    N: AsLen,
447 {
448    #[verifier::prophetic]
449    open spec fn exec_inv(&self) -> bool {
450        self.1.exec_inv()
451    }
452
453    fn serialize_into(&self, v: &[T], obuf: &mut Output) {
454        broadcast use crate::core::exec::output::outbuf_lemmas;
455
456        serialize_slice(&self.1, v, obuf);
457    }
458}
459
460impl<Inner, N, T> ByteLen<[T]> for super::RepeatN<Inner, N> where
461    Inner: ByteLen<T>,
462    T: DeepView,
463    N: AsLen,
464 {
465    open spec fn exec_inv(&self) -> bool {
466        self.1.exec_inv()
467    }
468
469    fn length(&self, v: &[T]) -> (len: usize) {
470        length_slice(&self.1, v)
471    }
472}
473
474impl<Inner, N, T> Prepare<[T]> for super::RepeatN<Inner, N> where
475    Inner: Prepare<T>,
476    T: DeepView,
477    N: AsLen,
478 {
479    open spec fn exec_inv(&self) -> bool {
480        self.1.exec_inv()
481    }
482
483    fn prepare(&self, v: &[T]) -> (checked: Result<usize, PreSerializeError>) {
484        if v.len() == self.0.get() {
485            prepare_slice(&self.1, v)
486        } else {
487            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
488        }
489    }
490}
491
492impl<Output: OutputBuf, Inner, T, const N: usize> Serializer<Output, [T; N]> for super::Array<
493    N,
494    Inner,
495> where T: DeepView, Inner: Serializer<Output, T> {
496    #[verifier::prophetic]
497    open spec fn exec_inv(&self) -> bool {
498        self.0.exec_inv()
499    }
500
501    fn serialize_into(&self, v: &[T; N], obuf: &mut Output) {
502        broadcast use crate::core::exec::output::outbuf_lemmas;
503
504        serialize_slice(&self.0, v, obuf);
505    }
506}
507
508impl<Inner, T, const N: usize> ByteLen<[T; N]> for super::Array<N, Inner> where
509    Inner: ByteLen<T>,
510    T: DeepView,
511 {
512    open spec fn exec_inv(&self) -> bool {
513        self.0.exec_inv()
514    }
515
516    fn length(&self, v: &[T; N]) -> (len: usize) {
517        length_slice(&self.0, v.as_slice())
518    }
519}
520
521impl<Inner, T, const N: usize> Prepare<[T; N]> for super::Array<N, Inner> where
522    Inner: Prepare<T>,
523    T: DeepView,
524 {
525    open spec fn exec_inv(&self) -> bool {
526        self.0.exec_inv()
527    }
528
529    fn prepare(&self, v: &[T; N]) -> (checked: Result<usize, PreSerializeError>) {
530        prepare_slice(&self.0, v.as_slice())
531    }
532}
533
534} // verus!
vest_lib/combinators/star/exec.rs

vest_lib/combinators/star/
exec.rs
