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")]
23const MAX_INITIAL_BYTES: usize = 16_384;
24
25/// Bound speculative reservation in bytes.
26#[cfg(feature = "alloc")]
27fn initial_capacity<T>(estimated: usize) -> (cap: usize)
28    ensures
29        cap <= estimated,
30{
31    let size = core::mem::size_of::<T>();
32    if size == 0 {
33        0
34    } else {
35        let limit = MAX_INITIAL_BYTES / size;
36        if estimated < limit {
37            estimated
38        } else {
39            limit
40        }
41    }
42}
43
44#[cfg(feature = "alloc")]
45impl<I, Inner> Parser<I> for super::Star<Inner> where I: InputBuf, Inner: Parser<I> + Productive {
46    type PT = Vec<Inner::PT>;
47
48    fn min_byte_len(&self) -> usize {
49        // A repetition may be empty.
50        0
51    }
52
53    open spec fn exec_inv(&self) -> bool {
54        &&& self.0.exec_inv()
55        &&& self.0.safe_inv()
56        &&& self.0.productive_inv()
57    }
58
59    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
60        reveal(<super::Star::<_> as SpecParser>::spec_parse);
61        broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
62
63        let total_len = ibuf.len();
64        let mut consumed: usize = 0;
65        let mut remaining = total_len;
66        let mut rest = ibuf.skip(0);
67        // Unlike RepeatN, Star does not know the actual element count.
68        // We reserve the `Vec` capacity based on the minimum byte length of the inner parser.
69        // Without reservation, the `Vec` is regrown several times per repetition,
70        // which dominates the cost of parsing `[u8; @len] >>= Vec<..>`.
71        let min_len = self.0.min_byte_len();
72        let per = if min_len == 0 {
73            1
74        } else {
75            min_len
76        };
77        let estimate = remaining / per;
78        let mut values = Vec::with_capacity(initial_capacity::<Inner::PT>(estimate));
79
80        while remaining > 0
81            invariant
82                self.exec_inv(),
83                consumed + remaining == total_len,
84                remaining == rest@.len(),
85                ({
86                    let prefix = values.deep_view();
87                    let (n, suffix) = self.parse_rec(rest@);
88                    self.parse_rec(ibuf@) == (consumed + n, prefix + suffix)
89                }),
90            decreases remaining,
91        {
92            broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
93
94            reveal(<super::Star::<_> as SpecParser>::spec_parse);
95
96            match self.0.parse(&rest) {
97                Ok((n, v)) => {
98                    proof {
99                        self.0.lemma_productive(rest@);
100                        assert(n > 0);
101                    }
102                    values.push(v);
103                    rest = rest.skip(n);
104                    consumed += n;
105                    remaining -= n;
106                },
107                Err(_) => return Ok((consumed, values)),
108            }
109        }
110        Ok((consumed, values))
111    }
112}
113
114#[cfg(feature = "alloc")]
115impl<I, A, B> Parser<I> for super::Repeat<A, B> where
116    I: InputBuf,
117    A: Parser<I> + SafeParser + Productive + Copy,
118    B: Parser<I> + SafeParser + Copy,
119 {
120    type PT = (Vec<A::PT>, B::PT);
121
122    fn min_byte_len(&self) -> usize {
123        // The repetition may be empty, so only the terminator is guaranteed.
124        self.1.min_byte_len()
125    }
126
127    open spec fn exec_inv(&self) -> bool {
128        &&& self.0.exec_inv()
129        &&& self.0.safe_inv()
130        &&& self.0.productive_inv()
131        &&& self.1.exec_inv()
132        &&& self.1.safe_inv()
133    }
134
135    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
136        crate::combinators::Pair(super::Star(self.0), self.1).parse(ibuf)
137    }
138}
139
140#[cfg(feature = "alloc")]
141impl<I, Inner, N> Parser<I> for super::RepeatN<Inner, N> where
142    I: InputBuf,
143    Inner: Parser<I> + SafeParser,
144    N: AsLen,
145 {
146    type PT = Vec<Inner::PT>;
147
148    fn min_byte_len(&self) -> usize {
149        // Exactly `count` elements.
150        self.0.get().saturating_mul(self.1.min_byte_len())
151    }
152
153    open spec fn exec_inv(&self) -> bool {
154        &&& self.1.exec_inv()
155        &&& self.1.safe_inv()
156    }
157
158    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
159        broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
160
161        let count = self.0.get();
162        let _total_len = ibuf.len();
163        let mut consumed: usize = 0;
164        let mut rest = ibuf.skip(0);
165        // The count may be attacker-controlled. Bound the initial allocation
166        // even when a short input claims many elements.
167        let reserve = if count < _total_len {
168            count
169        } else {
170            _total_len
171        };
172        let mut values = Vec::with_capacity(initial_capacity::<Inner::PT>(reserve));
173
174        for _i in 0..count
175            invariant
176                self.exec_inv(),
177                count as nat == self.0.as_nat(),
178                consumed + rest@.len() == _total_len,
179                ({
180                    let prefix = values.deep_view();
181                    let parsed = self.parse_n_rec(count as nat, ibuf@);
182                    match self.parse_n_rec((count - _i) as nat, rest@) {
183                        Some((n, suffix)) => parsed == Some((consumed + n, prefix + suffix)),
184                        None => parsed is None,
185                    }
186                }),
187        {
188            broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
189
190            let (n, v) = self.1.parse(&rest)?;
191            values.push(v);
192            rest = rest.skip(n);
193            consumed += n;
194        }
195        Ok((consumed, values))
196    }
197}
198
199// pub assume_specification<T, const N: usize, F: FnMut(usize) -> T>[ core::array::from_fn ](
200//     f: F,
201// ) -> (out: [T; N])
202//     requires
203//         forall|i: int| 0 <= i < N ==> #[trigger] call_requires(f, (i as usize,)),
204//     ensures
205//         forall|i: int| 0 <= i < N ==> call_ensures(f, (i as usize,), #[trigger] out[i]),
206// ;
207// pub assume_specification<T, const N: usize, F: FnMut(T) -> U, U>[ <[T; N]>::map ](
208//     arr: [T; N],
209//     f: F,
210// ) -> (out: [U; N])
211//     requires
212//         forall|i: int| 0 <= i < N ==> #[trigger] call_requires(f, (arr[i],)),
213//     ensures
214//         forall|i: int|
215//             #![trigger arr[i]]
216//             #![trigger out[i]]
217//             0 <= i < N ==> call_ensures(f, (arr[i],), out[i]),
218// ;
219#[inline(always)]
220#[verifier::external_body]
221pub fn array_of_none<T, const N: usize>() -> (out: [Option<T>; N])
222    ensures
223        forall|j: int| 0 <= j < N ==> #[trigger] out@[j] is None,
224{
225    core::array::from_fn(|_i| None)
226}
227
228#[inline(always)]
229#[verifier::external_body]
230pub fn array_option_unwrap<T: DeepView, const N: usize>(arr: [Option<T>; N]) -> (out: [T; N])
231    requires
232        forall|j: int| 0 <= j < N ==> #[trigger] arr@[j] is Some,
233    ensures
234        out.deep_view() == Seq::new(N as nat, |j| arr@[j]->0.deep_view()),
235{
236    arr.map(Option::<T>::unwrap)
237}
238
239impl<I, Inner, const N: usize> Parser<I> for super::Array<N, Inner> where
240    I: InputBuf,
241    Inner: Parser<I> + SafeParser,
242 {
243    type PT = [Inner::PT; N];
244
245    fn min_byte_len(&self) -> usize {
246        N.saturating_mul(self.0.min_byte_len())
247    }
248
249    open spec fn exec_inv(&self) -> bool {
250        &&& self.0.exec_inv()
251        &&& self.0.safe_inv()
252    }
253
254    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
255        broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
256
257        let mut consumed: usize = 0;
258        let _total_len = ibuf.len();
259        let mut rest = ibuf.skip(0);
260        let mut arr: [Option<Inner::PT>; N] = array_of_none();
261
262        for i in 0..N
263            invariant
264                self.exec_inv(),
265                consumed + rest@.len() == _total_len,
266                forall|j: int| 0 <= j < i ==> #[trigger] arr@[j] is Some,
267                forall|j: int| i <= j < N ==> #[trigger] arr@[j] is None,
268                ({
269                    let prefix = Seq::new(i as nat, |j| arr@[j]->0.deep_view());
270                    match super::RepeatN(N, self.0).parse_n_rec((N - i) as nat, rest@) {
271                        Some((n, suffix)) => self.spec_parse(ibuf@) == Some(
272                            (consumed + n, prefix + suffix),
273                        ),
274                        None => self.spec_parse(ibuf@) is None,
275                    }
276                }),
277        {
278            broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
279
280            let (n, v) = self.0.parse(&rest)?;
281            let elem = Some(v);
282            arr[i] = elem;
283            rest = rest.skip(n);
284            consumed += n;
285        }
286
287        let arr = array_option_unwrap(arr);
288
289        Ok((consumed, arr))
290    }
291}
292
293#[verifier::loop_isolation(false)]
294pub fn serialize_slice<Output, Inner, T>(inner: &Inner, values: &[T], obuf: &mut Output) where
295    Output: OutputBuf,
296    T: DeepView,
297    Inner: Serializer<Output, T>,
298
299    requires
300        inner.exec_inv(),
301        (super::Star(*inner)).consistent(values.deep_view()),
302        old(obuf).fits((super::Star(*inner)).byte_len(values.deep_view())),
303    ensures
304        final(obuf)@ == old(obuf)@ + spec_serialize_seq(inner, values.deep_view()),
305        forall|n|
306            old(obuf).fits((super::Star(*inner)).byte_len(values.deep_view()) + n)
307                <==> #[trigger] final(obuf).fits(n),
308        old(obuf).same_destination(final(obuf)),
309{
310    broadcast use crate::core::exec::output::outbuf_lemmas;
311
312    reveal(<super::Star::<_> as SpecByteLen>::byte_len);
313    reveal(<super::Star::<_> as Consistency>::consistent);
314
315    let ghost vs = values.deep_view();
316    let ghost star = super::Star(*inner);
317    let ghost mut consumed: nat = 0;
318
319    for value in iter: values.iter()
320        invariant
321            consumed + star.byte_len(vs[iter.index()..]) == star.byte_len(vs),
322            obuf@ == old(obuf)@ + spec_serialize_seq(inner, vs[0..iter.index()]),
323            forall|n| old(obuf).fits(consumed + n) <==> #[trigger] obuf.fits(n),
324            old(obuf).same_destination(obuf),
325    {
326        proof {
327            let i = iter.index();
328            let elem_len = inner.byte_len(vs[i as int]);
329            assert(vs[i..] == seq![vs[i]] + vs[i + 1..]);
330            star.lemma_byte_len_cons(vs[i], vs[i + 1..]);
331            assert(vs[0..i + 1] == vs[0..i].push(vs[i]));
332            assert(vs[0..i].push(vs[i]).drop_last() == vs[0..i]);
333            consumed = consumed + elem_len;
334        }
335        inner.serialize_into(value, obuf);
336    }
337}
338
339#[verifier::loop_isolation(false)]
340pub fn length_slice<Inner, T>(fmt: &Inner, values: &[T]) -> (len: usize) where
341    Inner: ByteLen<T>,
342    T: DeepView,
343
344    requires
345        fmt.exec_inv(),
346        (super::Star(*fmt)).byte_len(values.deep_view()) <= usize::MAX,
347    ensures
348        len == (super::Star(*fmt)).byte_len(values.deep_view()),
349{
350    reveal(<super::Star::<_> as SpecByteLen>::byte_len);
351    let ghost vs = values.deep_view();
352    let ghost star = super::Star(*fmt);
353
354    let mut len = 0usize;
355    for value in iter: values.iter()
356        invariant
357            len + star.byte_len(vs[iter.index()..]) == star.byte_len(vs),
358    {
359        proof {
360            let i = iter.index();
361            assert(vs[i..] == seq![vs[i]] + vs[i + 1..]);
362            star.lemma_byte_len_cons(vs[i], vs[i + 1..]);
363        }
364        let l = fmt.length(value);
365        len += l;
366    }
367    len
368}
369
370#[verifier::loop_isolation(false)]
371pub fn prepare_slice<Inner, T>(fmt: &Inner, values: &[T]) -> (checked: Result<
372    usize,
373    PreSerializeError,
374>) where Inner: Prepare<T>, T: DeepView
375    requires
376        fmt.exec_inv(),
377    ensures
378        checked matches Ok(len) ==> {
379            &&& (super::Star(*fmt)).consistent(values.deep_view())
380            &&& len == (super::Star(*fmt)).byte_len(values.deep_view())
381        },
382{
383    reveal(<super::Star::<_> as Consistency>::consistent);
384    reveal(<super::Star::<_> as SpecByteLen>::byte_len);
385    let ghost vs = values.deep_view();
386    let ghost star = super::Star(*fmt);
387
388    let mut len = 0usize;
389    for value in iter: values.iter()
390        invariant
391            forall|j: int| 0 <= j < iter.index() ==> fmt.consistent(#[trigger] vs[j]),
392            len + star.byte_len(vs[iter.index()..]) == star.byte_len(vs),
393    {
394        proof {
395            let i = iter.index();
396            assert(vs[i..] == seq![vs[i]] + vs[i + 1..]);
397            star.lemma_byte_len_cons(vs[i], vs[i + 1..]);
398        }
399        let elem_len = fmt.prepare(value)?;
400        match len.checked_add(elem_len) {
401            Some(total) => len = total,
402            None => return Err(PreSerializeError::length_too_large()),
403        }
404    }
405    Ok(len)
406}
407
408impl<Output: OutputBuf, Inner, T> Serializer<Output, [T]> for super::Star<Inner> where
409    T: DeepView,
410    Inner: Serializer<Output, T>,
411 {
412    #[verifier::prophetic]
413    open spec fn exec_inv(&self) -> bool {
414        self.0.exec_inv()
415    }
416
417    fn serialize_into(&self, v: &[T], obuf: &mut Output) {
418        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
419        serialize_slice(&self.0, v, obuf);
420    }
421}
422
423impl<Inner, T> ByteLen<[T]> for super::Star<Inner> where Inner: ByteLen<T>, T: DeepView {
424    open spec fn exec_inv(&self) -> bool {
425        self.0.exec_inv()
426    }
427
428    fn length(&self, v: &[T]) -> (len: usize) {
429        length_slice(&self.0, v)
430    }
431}
432
433impl<Inner, T> Prepare<[T]> for super::Star<Inner> where Inner: Prepare<T>, T: DeepView {
434    open spec fn exec_inv(&self) -> bool {
435        self.0.exec_inv()
436    }
437
438    fn prepare(&self, v: &[T]) -> (checked: Result<usize, PreSerializeError>) {
439        prepare_slice(&self.0, v)
440    }
441}
442
443impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (&[TA], TB)> for super::Repeat<A, B> where
444    TA: DeepView,
445    TB: DeepView,
446    A: Serializer<Output, TA> + Copy,
447    B: Serializer<Output, TB>,
448 {
449    #[verifier::prophetic]
450    open spec fn exec_inv(&self) -> bool {
451        &&& self.0.exec_inv()
452        &&& self.1.exec_inv()
453    }
454
455    fn serialize_into(&self, v: &(&[TA], TB), obuf: &mut Output) {
456        broadcast use crate::core::exec::output::outbuf_lemmas;
457
458        reveal(<super::Star<_> as SpecSerializer>::spec_serialize);
459
460        super::Star(self.0).serialize_into(v.0, obuf);
461        assert(obuf.fits(self.1.byte_len(v.deep_view().1)));
462        self.1.serialize_into(&v.1, obuf);
463    }
464}
465
466impl<A, B, TA, TB> ByteLen<(&[TA], TB)> for super::Repeat<A, B> where
467    A: ByteLen<TA> + Copy,
468    B: ByteLen<TB>,
469    TA: DeepView,
470    TB: DeepView,
471 {
472    open spec fn exec_inv(&self) -> bool {
473        &&& self.0.exec_inv()
474        &&& self.1.exec_inv()
475    }
476
477    fn length(&self, v: &(&[TA], TB)) -> (len: usize) {
478        let la = super::Star(self.0).length(v.0);
479        let lb = self.1.length(&v.1);
480        la + lb
481    }
482}
483
484impl<A, B, TA, TB> Prepare<(&[TA], TB)> for super::Repeat<A, B> where
485    A: Prepare<TA> + Copy,
486    B: Prepare<TB>,
487    TA: DeepView,
488    TB: DeepView,
489 {
490    open spec fn exec_inv(&self) -> bool {
491        &&& self.0.exec_inv()
492        &&& self.1.exec_inv()
493    }
494
495    fn prepare(&self, v: &(&[TA], TB)) -> (checked: Result<usize, PreSerializeError>) {
496        let la = super::Star(self.0).prepare(v.0)?;
497        let lb = self.1.prepare(&v.1)?;
498        match la.checked_add(lb) {
499            Some(total) => Ok(total),
500            None => Err(PreSerializeError::length_too_large()),
501        }
502    }
503}
504
505impl<Output: OutputBuf, Inner, N, T> Serializer<Output, [T]> for super::RepeatN<Inner, N> where
506    T: DeepView,
507    Inner: Serializer<Output, T>,
508    N: AsLen,
509 {
510    #[verifier::prophetic]
511    open spec fn exec_inv(&self) -> bool {
512        self.1.exec_inv()
513    }
514
515    fn serialize_into(&self, v: &[T], obuf: &mut Output) {
516        broadcast use crate::core::exec::output::outbuf_lemmas;
517
518        serialize_slice(&self.1, v, obuf);
519    }
520}
521
522impl<Inner, N, T> ByteLen<[T]> for super::RepeatN<Inner, N> where
523    Inner: ByteLen<T>,
524    T: DeepView,
525    N: AsLen,
526 {
527    open spec fn exec_inv(&self) -> bool {
528        self.1.exec_inv()
529    }
530
531    fn length(&self, v: &[T]) -> (len: usize) {
532        length_slice(&self.1, v)
533    }
534}
535
536impl<Inner, N, T> Prepare<[T]> for super::RepeatN<Inner, N> where
537    Inner: Prepare<T>,
538    T: DeepView,
539    N: AsLen,
540 {
541    open spec fn exec_inv(&self) -> bool {
542        self.1.exec_inv()
543    }
544
545    fn prepare(&self, v: &[T]) -> (checked: Result<usize, PreSerializeError>) {
546        if v.len() == self.0.get() {
547            prepare_slice(&self.1, v)
548        } else {
549            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
550        }
551    }
552}
553
554impl<Output: OutputBuf, Inner, T, const N: usize> Serializer<Output, [T; N]> for super::Array<
555    N,
556    Inner,
557> where T: DeepView, Inner: Serializer<Output, T> {
558    #[verifier::prophetic]
559    open spec fn exec_inv(&self) -> bool {
560        self.0.exec_inv()
561    }
562
563    fn serialize_into(&self, v: &[T; N], obuf: &mut Output) {
564        broadcast use crate::core::exec::output::outbuf_lemmas;
565
566        serialize_slice(&self.0, v, obuf);
567    }
568}
569
570impl<Inner, T, const N: usize> ByteLen<[T; N]> for super::Array<N, Inner> where
571    Inner: ByteLen<T>,
572    T: DeepView,
573 {
574    open spec fn exec_inv(&self) -> bool {
575        self.0.exec_inv()
576    }
577
578    fn length(&self, v: &[T; N]) -> (len: usize) {
579        length_slice(&self.0, v.as_slice())
580    }
581}
582
583impl<Inner, T, const N: usize> Prepare<[T; N]> for super::Array<N, Inner> where
584    Inner: Prepare<T>,
585    T: DeepView,
586 {
587    open spec fn exec_inv(&self) -> bool {
588        self.0.exec_inv()
589    }
590
591    fn prepare(&self, v: &[T; N]) -> (checked: Result<usize, PreSerializeError>) {
592        prepare_slice(&self.0, v.as_slice())
593    }
594}
595
596} // verus!
597#[cfg(all(test, feature = "alloc"))]
598mod reservation_tests {
599    use super::initial_capacity;
600
601    #[test]
602    fn speculative_reservation_is_bounded_in_bytes() {
603        assert_eq!(initial_capacity::<u8>(32), 32);
604        assert_eq!(initial_capacity::<u8>(usize::MAX), 16_384);
605        assert_eq!(initial_capacity::<[u8; 832]>(309_417), 19);
606        assert_eq!(initial_capacity::<[u8; 32_768]>(usize::MAX), 0);
607        assert_eq!(initial_capacity::<()>(usize::MAX), 0);
608        assert_eq!(initial_capacity::<u64>(0), 0);
609    }
610}
vest_lib/combinators/star/exec.rs

vest_lib/combinators/star/
exec.rs
