vest_lib/regular/
repetition.rs

1use alloc::vec::Vec;
2
3use crate::properties::*;
4use vstd::prelude::*;
5
6verus! {
7
8/// Combinator that repeats [C] combinator [self.1] times.
9pub struct RepeatN<C>(pub C, pub usize);
10
11impl<C: View> View for RepeatN<C> {
12    type V = RepeatN<<C as View>::V>;
13
14    open spec fn view(&self) -> Self::V {
15        RepeatN(self.0@, self.1)
16    }
17}
18
19impl<C: SecureSpecCombinator> RepeatN<C> {
20    /// Helper function for parsing [n] instances of [C] from [s].
21    pub closed spec fn spec_parse_helper(&self, s: Seq<u8>, n: usize) -> Option<(int, Seq<C::Type>)>
22        decreases n,
23    {
24        if n == 0 {
25            Some((0, seq![]))
26        } else {
27            match self.spec_parse_helper(s, (n - 1) as usize) {
28                Some((m, vs)) => match self.0.spec_parse(s.skip(m as int)) {
29                    Some((k, v)) => Some((m + k, vs.push(v))),
30                    None => None,
31                },
32                None => None,
33            }
34        }
35    }
36
37    proof fn lemma_spec_parse_err_unrecoverable(&self, s: Seq<u8>, n1: usize, n2: usize)
38        ensures
39            n1 <= n2 ==> self.spec_parse_helper(s, n1) is None ==> self.spec_parse_helper(
40                s,
41                n2,
42            ) is None,
43        decreases n2,
44    {
45        if n2 == n1 {
46        } else if n2 > n1 {
47            self.lemma_spec_parse_err_unrecoverable(s, n1, (n2 - 1) as usize);
48        }
49    }
50}
51
52impl<C: SecureSpecCombinator> RepeatN<C> {
53    spec fn wf_helper(&self, vs: Seq<C::Type>, n: usize) -> bool {
54        &&& vs.len() == n
55        &&& forall|i: int| 0 <= i < vs.len() ==> #[trigger] self.0.wf(vs[i])
56    }
57
58    proof fn theorem_serialize_parse_roundtrip_helper(&self, vs: Seq<C::Type>, n: usize)
59        requires
60            self.requires(),
61        ensures
62            self.wf_helper(vs, n) ==> self.spec_parse_helper(self.spec_serialize(vs), n) == Some(
63                (self.spec_serialize(vs).len() as int, vs),
64            ),
65        decreases vs.len(), n,
66    {
67        if self.wf_helper(vs, n) {
68            if vs.len() == 0 {
69                assert(self.spec_parse_helper(self.spec_serialize(vs), n) == Some(
70                    (self.spec_serialize(vs).len() as int, vs),
71                ));
72            } else {
73                assert(n != 0);
74                let (v_, vs_) = (vs.last(), vs.drop_last());
75                self.0.theorem_serialize_parse_roundtrip(v_);  // <-- Base
76                self.theorem_serialize_parse_roundtrip_helper(vs_, (n - 1) as usize);  // <-- I.H.
77                let buf0 = self.0.spec_serialize(v_);
78                let buf1 = self.spec_serialize(vs_);
79                let (n0, n1) = (buf0.len() as int, buf1.len() as int);
80                assert(vs_.push(v_) == vs);  // <-- (1).
81                assert(self.spec_serialize(vs) == buf1 + buf0);  // <-- from (0) and (1)
82                assert(self.0.spec_parse(buf0) == Some((n0, v_)));  // <-- from Base
83                assert(self.spec_parse_helper(buf1, (n - 1) as usize) == Some((n1, vs_)));  // <-- from I.H.
84                self.lemma_prefix_secure_helper(buf1, buf0, (n - 1) as usize);
85                assert((buf1 + buf0).skip(n1) == buf0);
86                assert(self.spec_parse_helper(buf1 + buf0, n) == Some((n0 + n1, vs)));
87            }
88        }
89    }
90
91    proof fn theorem_parse_serialize_roundtrip_helper(&self, buf: Seq<u8>, n: usize)
92        requires
93            self.requires(),
94        ensures
95            self.spec_parse_helper(buf, n) matches Some((m, vs)) ==> {
96                &&& self.wf_helper(vs, n)
97                &&& self.spec_serialize(vs) == buf.take(m)
98            },
99        decreases n,
100    {
101        if n == 0 {
102            assert(buf.take(0) == Seq::<u8>::empty());
103        } else {
104            self.lemma_parse_length_helper(buf, n);  // <-- key
105            self.lemma_parse_length_helper(buf, (n - 1) as usize);  // <-- key
106            self.theorem_parse_serialize_roundtrip_helper(buf, (n - 1) as usize);  // <-- I.H.
107            if let Some((m, vs)) = self.spec_parse_helper(buf, (n - 1) as usize) {
108                self.0.lemma_parse_length(buf.skip(m as int));  // <-- key
109                if let Some((k, v)) = self.0.spec_parse(buf.skip(m as int)) {
110                    assert(vs.push(v).drop_last() == vs);
111                    self.0.theorem_parse_serialize_roundtrip(buf.skip(m as int));  // <-- Base
112                    assert(vs.push(v).last() == v);
113                    assert(buf.take(m + k) == buf.take(m) + buf.skip(m).take(k));
114                }
115            }
116        }
117    }
118
119    proof fn lemma_prefix_secure_helper(&self, s1: Seq<u8>, s2: Seq<u8>, n: usize)
120        requires
121            self.requires(),
122        ensures
123            self.spec_parse_helper(s1, n) is Some ==> self.spec_parse_helper(s1.add(s2), n)
124                == self.spec_parse_helper(s1, n),
125        decreases n,
126    {
127        if n == 0 {
128        } else {
129            self.lemma_prefix_secure_helper(s1, s2, (n - 1) as usize);
130            self.lemma_parse_length_helper(s1, (n - 1) as usize);
131            self.lemma_parse_length_helper(s1.add(s2), (n - 1) as usize);
132            if let Some((m1, vs1)) = self.spec_parse_helper(s1, (n - 1) as usize) {
133                self.0.lemma_prefix_secure(s1.skip(m1 as int), s2);
134                if let Some((m2, vs2)) = self.spec_parse_helper(s1.add(s2), (n - 1) as usize) {
135                    assert(s1.skip(m1 as int).add(s2) == s1.add(s2).skip(m2 as int));
136                }
137            }
138        }
139    }
140
141    proof fn lemma_parse_length_helper(&self, s: Seq<u8>, n: usize)
142        requires
143            self.requires(),
144        ensures
145            self.spec_parse_helper(s, n) matches Some((m, _)) ==> 0 <= m <= s.len(),
146        decreases n,
147    {
148        if n == 0 {
149        } else {
150            self.lemma_parse_length_helper(s, (n - 1) as usize);
151            match self.spec_parse_helper(s, (n - 1) as usize) {
152                Some((m, vs)) => {
153                    self.0.lemma_parse_length(s.skip(m as int));
154                },
155                None => {},
156            }
157        }
158    }
159
160    proof fn lemma_parse_productive_helper(&self, s: Seq<u8>, n: usize)
161        requires
162            self.requires(),
163            self.1 > 0,
164            self.0.is_productive(),
165        ensures
166            n > 0 ==> (self.spec_parse_helper(s, n) matches Some((consumed, _)) ==> consumed > 0),
167        decreases n,
168    {
169        if n == 0 {
170        } else {
171            self.lemma_parse_productive_helper(s, (n - 1) as usize);
172            match self.spec_parse_helper(s, (n - 1) as usize) {
173                Some((m, vs)) => {
174                    self.0.lemma_parse_productive(s.skip(m as int));
175                },
176                None => {},
177            }
178        }
179    }
180}
181
182impl<C: SecureSpecCombinator> SpecCombinator for RepeatN<C> {
183    type Type = Seq<C::Type>;
184
185    open spec fn requires(&self) -> bool {
186        &&& self.0.requires()
187        &&& C::is_prefix_secure()
188    }
189
190    open spec fn wf(&self, vs: Self::Type) -> bool {
191        &&& vs.len() == self.1
192        &&& forall|i: int| 0 <= i < vs.len() ==> #[trigger] self.0.wf(vs[i])
193    }
194
195    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
196        self.spec_parse_helper(s, self.1)
197    }
198
199    open spec fn spec_serialize(&self, vs: Self::Type) -> Seq<u8> {
200        vs.fold_left(Seq::empty(), |acc: Seq<u8>, v| acc + self.0.spec_serialize(v))
201    }
202}
203
204impl<C: SecureSpecCombinator> SecureSpecCombinator for RepeatN<C> {
205    open spec fn is_prefix_secure() -> bool {
206        C::is_prefix_secure()
207    }
208
209    open spec fn is_productive(&self) -> bool {
210        self.1 > 0 && self.0.is_productive()
211    }
212
213    proof fn theorem_serialize_parse_roundtrip(&self, vs: Self::Type) {
214        if self.wf(vs) {
215            self.theorem_serialize_parse_roundtrip_helper(vs, self.1)
216        }
217    }
218
219    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
220        self.theorem_parse_serialize_roundtrip_helper(buf, self.1)
221    }
222
223    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
224        if C::is_prefix_secure() {
225            self.lemma_prefix_secure_helper(s1, s2, self.1)
226        }
227    }
228
229    proof fn lemma_parse_length(&self, s: Seq<u8>) {
230        self.lemma_parse_length_helper(s, self.1)
231    }
232
233    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
234        if self.is_productive() {
235            self.lemma_parse_productive_helper(s, self.1)
236        }
237    }
238}
239
240impl<C: SecureSpecCombinator> RepeatN<C> {
241    spec fn parse_correct(
242        &self,
243        s: Seq<u8>,
244        n: usize,
245        res: Result<(usize, Seq<C::Type>), ParseError>,
246    ) -> bool {
247        &&& res matches Ok((k, v)) ==> self.spec_parse_helper(s, n) == Some((k as int, v))
248        &&& self.spec_parse_helper(s, n) matches Some((k, v)) ==> res == Ok::<_, ParseError>(
249            (k as usize, v),
250        )
251        &&& res is Err ==> self.spec_parse_helper(s, n) is None
252        &&& self.spec_parse_helper(s, n) is None ==> res is Err
253    }
254
255    proof fn lemma_spec_serialize_max_length(&self, vs: Seq<C::Type>, n: usize)
256        requires
257            self.requires(),
258            self.wf_helper(vs, n),
259            self.spec_serialize(vs).len() <= usize::MAX,
260        ensures
261            forall|i: int|
262                #![auto]
263                0 <= i < vs.len() ==> self.0.spec_serialize(vs[i]).len() <= usize::MAX,
264            forall|i: int|
265                #![auto]
266                0 <= i < vs.len() ==> self.spec_serialize(vs.take(i as int)).len() <= usize::MAX,
267        decreases vs.len(),
268    {
269        if vs.len() == 0 {
270            assert(vs == Seq::<C::Type>::empty());
271        } else {
272            let (v_, vs_) = (vs.last(), vs.drop_last());
273            assert(vs_ =~= vs.take(vs_.len() as int));
274            self.lemma_spec_serialize_max_length(vs_, (n - 1) as usize);
275            assert forall|i: int| #![auto] 0 <= i < vs.len() implies {
276                self.0.spec_serialize(vs[i]).len() <= usize::MAX
277            } by {
278                assert forall|i: int| #![auto] 0 <= i < vs.len() - 1 implies {
279                    self.0.spec_serialize(vs.drop_last()[i]).len() <= usize::MAX
280                } by {}
281                assert(forall|i: int|
282                    #![auto]
283                    0 <= i < vs.len() - 1 ==> vs.drop_last()[i] == vs[i]);
284                assert(forall|i: int|
285                    #![auto]
286                    0 <= i < vs.len() - 1 ==> vs.drop_last().take(i as int) == vs.take(i as int));
287                assert(self.spec_serialize(vs_).len() <= usize::MAX);
288                assert(self.spec_serialize(vs) == self.spec_serialize(vs_) + self.0.spec_serialize(
289                    v_,
290                ));
291                let last_len = self.0.spec_serialize(v_).len();
292                if last_len > usize::MAX {
293                    assert(self.spec_serialize(vs).len() > usize::MAX);
294                    assert(false);
295                }
296                assert(last_len <= usize::MAX);
297            }
298            assert forall|i: int| #![auto] 0 <= i < vs.len() implies {
299                self.spec_serialize(vs.take(i as int)).len() <= usize::MAX
300            } by {
301                assert forall|i: int| #![auto] 0 <= i < vs.len() - 1 implies {
302                    self.spec_serialize(vs.drop_last().take(i as int)).len() <= usize::MAX
303                } by {}
304                assert(forall|i: int|
305                    #![auto]
306                    0 <= i < vs.len() - 1 ==> vs.drop_last()[i] == vs[i]);
307                assert(forall|i: int|
308                    #![auto]
309                    0 <= i < vs.len() - 1 ==> vs.drop_last().take(i as int) == vs.take(i as int));
310            }
311        }
312    }
313
314    proof fn lemma_spec_serialize_max_length_2(&self, vs: Seq<C::Type>, n: usize)
315        requires
316            self.requires(),
317            self.wf_helper(vs, n),
318            self.spec_serialize(vs).len() <= usize::MAX,
319        ensures
320            forall|i: int|
321                #![auto]
322                0 <= i <= vs.len() ==> {
323                    &&& self.spec_serialize(vs.take(i as int)).len() <= usize::MAX
324                },
325    {
326        self.lemma_spec_serialize_max_length(vs, n);
327        assert(vs.take(vs.len() as int) == vs);
328    }
329}
330
331impl<I, O, C, 'x> Combinator<'x, I, O> for RepeatN<C> where
332    I: VestInput,
333    O: VestOutput<I>,
334    C: Combinator<'x, I, O, SType = &'x <C as Combinator<'x, I, O>>::Type>,
335    C::V: SecureSpecCombinator<Type = <C::Type as View>::V>,
336    <C as Combinator<'x, I, O>>::Type: 'x,
337 {
338    type Type = RepeatResult<C::Type>;
339
340    type SType = &'x RepeatResult<C::Type>;
341
342    fn length(&self, vs: Self::SType) -> usize {
343        let mut len = 0;
344        proof {
345            self@.lemma_spec_serialize_max_length(vs@, self.1);
346            self@.lemma_spec_serialize_max_length_2(vs@, self.1);
347        }
348        for i in 0..vs.0.len()
349            invariant
350                0 <= i <= vs.0.len(),
351                self@.wf(vs@),
352                self.ex_requires(),
353                self@.requires(),
354                self@.spec_serialize(vs@).len() <= usize::MAX,
355                forall|i: int|
356                    0 <= i < vs@.len() ==> self@.0.spec_serialize(#[trigger] vs@[i]).len()
357                        <= usize::MAX,
358                forall|i: int|
359                    0 <= i <= vs@.len() ==> self@.spec_serialize(
360                        #[trigger] vs@.take(i as int),
361                    ).len() <= usize::MAX,
362                len == self@.spec_serialize(vs@.take(i as int)).len(),
363            decreases vs.0.len() - i,
364        {
365            let v = &vs.0[i];
366            assert(v@ == vs@[i as int]);
367            assert(vs@.take((i + 1) as int).drop_last() == vs@.take(i as int));
368            len += self.0.length(v);
369        }
370        assert(vs@.take(vs.0.len() as int) == vs@);
371        len
372    }
373
374    open spec fn ex_requires(&self) -> bool {
375        self.0.ex_requires()
376    }
377
378    fn parse(&self, input: I) -> (res: Result<(usize, Self::Type), ParseError>) {
379        let (mut s, mut len, mut vs) = (input, 0usize, Vec::new());
380        assert(RepeatResult(vs)@ =~= seq![]);
381
382        for i in 0..self.1
383            invariant
384                0 <= i <= self.1,
385                self.ex_requires(),
386                self@.requires(),
387                0 <= len <= input@.len() <= usize::MAX,
388                s@ =~= input@.skip(len as int),  // <-- this is the key
389                self@.parse_correct(input@, i, Ok::<_, ParseError>((len, RepeatResult(vs)@))),
390            decreases self.1 - i,
391        {
392            match self.0.parse(s.clone()) {
393                Ok((n, v)) => {
394                    assert(0 <= n <= input@.skip(len as int).len()) by {
395                        self@.0.lemma_parse_length(s@);
396                    }
397                    let ghost old_vs = RepeatResult(vs)@;
398                    vs.push(v);
399                    len += n;
400                    s = s.subrange(n, s.len());
401                    assert(RepeatResult(vs)@ == old_vs.push(v@));
402                },
403                Err(e) => {
404                    proof {
405                        self@.lemma_spec_parse_err_unrecoverable(input@, (i + 1) as usize, self.1);
406                    }
407                    return Err(e);
408                },
409            }
410        }
411        Ok((len, RepeatResult(vs)))
412    }
413
414    fn serialize(&self, vs: Self::SType, data: &mut O, mut pos: usize) -> (res: Result<
415        usize,
416        SerializeError,
417    >) {
418        let ghost old_data = old(data)@;
419        let old_pos = pos;
420        assert(data@ == seq_splice(old(data)@, pos, Seq::<u8>::empty()));
421        let ghost _vs = vs@;
422        for i in 0..vs.0.len()
423            invariant
424                data@.len() == old_data.len(),
425                pos <= data@.len() <= usize::MAX,
426                _vs == vs@,
427                self@.wf(_vs),
428                self.ex_requires(),
429                self@.requires(),
430                (pos - old_pos) == self@.spec_serialize(_vs.take(i as int)).len(),
431                data@ == seq_splice(old_data, old_pos, self@.spec_serialize(_vs.take(i as int))),
432        {
433            let v = &vs.0[i];
434            assert(v@ == _vs[i as int]);
435            assert(_vs.take((i + 1) as int).drop_last() == _vs.take(i as int));  // <-- this is the key
436            let l = self.0.serialize(v, data, pos)?;
437            pos += l;
438            assert(data@ == seq_splice(
439                old_data,
440                old_pos,
441                self@.spec_serialize(_vs.take((i + 1) as int)),
442            ));
443        }
444        assert(_vs == _vs.take(vs.0.len() as int));
445        Ok(pos - old_pos)
446    }
447}
448
449/// A combinator to repeatedly parse/serialize the inner combinator C
450/// until the end of the buffer.
451///
452/// If the inner combinator fails before the end of the buffer, Repeat fails
453pub struct Repeat<C>(pub C);
454
455/// Wrappers around Vec so that their View's can be implemented as DeepView
456#[derive(Debug, PartialEq, Eq)]
457pub struct RepeatResult<T>(pub Vec<T>);
458
459impl<T: Clone> Clone for RepeatResult<T> {
460    fn clone(&self) -> Self {
461        RepeatResult(self.0.clone())
462    }
463}
464
465impl<'x, C: View> Repeat<C> where C::V: SecureSpecCombinator {
466    /// Constructs a new `Repeat` combinator, only if the inner combinator is productive.
467    pub fn new(c: C) -> (o: Self)
468        requires
469            c@.is_productive(),
470        ensures
471            o == Self(c),
472    {
473        Repeat(c)
474    }
475}
476
477impl<C: View> View for Repeat<C> {
478    type V = Repeat<<C as View>::V>;
479
480    open spec fn view(&self) -> Self::V {
481        Repeat(self.0@)
482    }
483}
484
485impl<T: View> View for RepeatResult<T> {
486    type V = Seq<T::V>;
487
488    open spec fn view(&self) -> Self::V {
489        Seq::new(self.0.len() as nat, |i: int| self.0@[i]@)
490    }
491}
492
493impl<C: SecureSpecCombinator> Repeat<C> {
494    #[verusfmt::skip]
495    proof fn lemma_serialize_add(&self, v: C::Type, vs: Seq<C::Type>)
496        ensures
497            self.spec_serialize(seq![v] + vs) == self.0.spec_serialize(v) + self.spec_serialize(vs)
498        decreases vs.len(),
499    {
500        if vs.len() == 0 {
501            assert(vs == Seq::<C::Type>::empty());
502            assert(seq![v].drop_last() == Seq::<C::Type>::empty());
503        } else {
504            let vs_ = vs.drop_last();
505            let v_ = vs.last();
506            self.lemma_serialize_add(v, vs_);
507             // (1) I.H.
508            assert(self.spec_serialize(seq![v] + vs_) == self.0.spec_serialize(v) + self.spec_serialize(vs_));
509             // (2) "expand" `fold_left`
510            assert(self.spec_serialize(vs) == self.spec_serialize(vs_) + self.0.spec_serialize((v_)));
511             // by (1) and (2)
512            assert(self.spec_serialize(seq![v] + vs_) + self.0.spec_serialize((v_))
513                == self.0.spec_serialize(v) + self.spec_serialize(vs));
514            assert(seq![v] + vs == (seq![v] + vs_).push(v_));
515            assert(self.spec_serialize((seq![v] + vs_).push(v_))
516                == self.spec_serialize(seq![v] + vs_) + self.0.spec_serialize((v_)))
517            by { assert((seq![v] + vs_).push(v_).drop_last() == seq![v] + vs_); }
518        }
519    }
520}
521
522impl<C: SecureSpecCombinator> SpecCombinator for Repeat<C> {
523    type Type = Seq<C::Type>;
524
525    open spec fn requires(&self) -> bool {
526        &&& self.0.requires()
527        &&& C::is_prefix_secure()
528        &&& self.0.is_productive()
529    }
530
531    open spec fn wf(&self, vs: Self::Type) -> bool {
532        forall|i: int| 0 <= i < vs.len() ==> #[trigger] self.0.wf(vs[i])
533    }
534
535    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
536        decreases s.len(),
537    {
538        if s.len() == 0 {
539            Some((0, seq![]))
540        } else {
541            match self.0.spec_parse(s) {
542                Some((n, v)) => if 0 < n <= s.len() {
543                    match self.spec_parse(s.skip(n)) {
544                        Some((_, vs)) => Some((s.len() as int, seq![v] + vs)),
545                        None => None,
546                    }
547                } else {
548                    None
549                },
550                None => None,
551            }
552        }
553    }
554
555    open spec fn spec_serialize(&self, vs: Self::Type) -> Seq<u8> {
556        RepeatN(self.0, vs.len() as usize).spec_serialize(vs)
557    }
558}
559
560impl<C: SecureSpecCombinator> SecureSpecCombinator for Repeat<C> {
561    open spec fn is_prefix_secure() -> bool {
562        false
563    }
564
565    open spec fn is_productive(&self) -> bool {
566        false
567    }
568
569    proof fn theorem_serialize_parse_roundtrip(&self, vs: Self::Type)
570        decreases vs.len(),
571    {
572        if self.wf(vs) {
573            if vs.len() == 0 {
574                assert(vs == <Seq<C::Type>>::empty());
575            } else {
576                let (v_, vs_) = (vs.first(), vs.drop_first());
577                self.lemma_serialize_add(v_, vs_);  // (0). "re-order" the I.H.
578                self.0.theorem_serialize_parse_roundtrip(v_);  // <-- Base
579                self.theorem_serialize_parse_roundtrip(vs_);  // <-- I.H.
580                let buf0 = self.0.spec_serialize(v_);
581                assert(buf0.len() > 0) by {
582                    self.0.lemma_serialize_productive(v_);
583                }
584                let buf1 = self.spec_serialize(vs_);
585                let (n0, n1) = (buf0.len() as int, buf1.len() as int);
586                assert(seq![v_] + vs_ == vs);  // <-- (1).
587                assert(self.spec_serialize(vs) == buf0 + buf1);  // <-- from (0) and (1)
588                assert(self.0.spec_parse(buf0) == Some((n0, v_)));  // <-- from Base
589                assert(self.spec_parse(buf1) == Some((n1, vs_)));  // <-- from I.H.
590                self.0.lemma_prefix_secure(buf0, buf1);
591                assert((buf0 + buf1).skip(n0) == buf1);
592                assert(self.spec_parse(buf0 + buf1) == Some((n0 + n1, vs)));
593            }
594        }
595    }
596
597    proof fn theorem_parse_serialize_roundtrip(&self, input: Seq<u8>)
598        decreases input.len(),
599    {
600        if input.len() == 0 {
601            assert(input.take(0) == Seq::<u8>::empty());
602        } else {
603            self.0.theorem_parse_serialize_roundtrip(input);
604            match self.0.spec_parse(input) {
605                Some((n, v)) => if 0 < n <= input.len() {
606                    self.theorem_parse_serialize_roundtrip(input.skip(n));
607                    match self.spec_parse(input.skip(n)) {
608                        Some((len, vs)) => {
609                            assert(self.0.spec_serialize(v) == input.take(n));  // <-- Base
610                            assert(self.spec_serialize(vs) == input.skip(n).take(len));  // <-- I.H.
611                            self.lemma_serialize_add(v, vs);
612                            assert(input.take(n + len) == input.take(n) + input.skip(n).take(len));
613                        },
614                        None => {},
615                    }
616                },
617                None => {},
618            }
619        }
620    }
621
622    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
623    }
624
625    proof fn lemma_parse_length(&self, s: Seq<u8>) {
626    }
627
628    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
629    }
630}
631
632impl<I, O, C, 'x> Combinator<'x, I, O> for Repeat<C> where
633    I: VestInput,
634    O: VestOutput<I>,
635    C: Combinator<'x, I, O, SType = &'x <C as Combinator<'x, I, O>>::Type>,
636    C::V: SecureSpecCombinator<Type = <C::Type as View>::V>,
637    <C as Combinator<'x, I, O>>::Type: 'x,
638 {
639    type Type = RepeatResult<C::Type>;
640
641    type SType = &'x RepeatResult<C::Type>;
642
643    fn length(&self, vs: Self::SType) -> usize {
644        RepeatN(&self.0, vs.0.len()).length(vs)
645    }
646
647    open spec fn ex_requires(&self) -> bool {
648        self.0.ex_requires()
649    }
650
651    fn parse(&self, input: I) -> (res: Result<(usize, Self::Type), ParseError>) {
652        let mut vs = Vec::new();
653        let mut len: usize = 0;
654
655        assert(input@.take(input@.len() as int) == input@);
656
657        while len < input.len()
658            invariant
659                0 <= len <= input@.len(),
660                self.ex_requires(),
661                self@.requires(),
662                self@.spec_parse(input@.skip(len as int)) matches Some((_, rest)) ==> {
663                    &&& self@.spec_parse(input@) matches Some((_, correct_vs))
664                    &&& RepeatResult(vs)@ + rest =~= correct_vs
665                },
666                len < input@.len() ==> (self@.spec_parse(input@.skip(len as int)) is None
667                    ==> self@.spec_parse(input@) is None),
668            decreases input@.len() - len,
669        {
670            let (n, v) = self.0.parse(input.subrange(len, input.len()))?;
671
672            assert(0 < n <= input@.skip(len as int).len()) by {
673                self.0@.lemma_parse_productive(input@.skip(len as int));
674                self.0@.lemma_parse_length(input@.skip(len as int));
675            }
676
677            let ghost prev_len = len;
678
679            vs.push(v);
680            len += n;
681
682            assert(input@.skip(prev_len as int).skip(n as int) == input@.skip(len as int));
683        }
684
685        Ok((input.len(), RepeatResult(vs)))
686    }
687
688    fn serialize(&self, vs: Self::SType, data: &mut O, pos: usize) -> (res: Result<
689        usize,
690        SerializeError,
691    >) {
692        RepeatN(&self.0, vs.0.len()).serialize(vs, data, pos)
693    }
694}
695
696} // verus!
vest_lib/regular/repetition.rs

vest_lib/regular/
repetition.rs
