vest_lib/combinators/star/
mod.rs

1//! Repetition into vectors/sequences.
2//!
3//! [`Star`] stops when its child no longer matches;
4//! [`RepeatTillEnd`](crate::combinators::RepeatTillEnd) requires a
5//! bounded region to be exhausted. Their child must be productive so every
6//! successful iteration consumes input.
7/// Executable trait implementations for this combinator.
8pub mod exec;
9/// Correctness proofs for this combinator.
10pub mod proof;
11/// Specification trait implementations for this combinator.
12pub mod spec;
13
14use vstd::prelude::*;
15
16verus! {
17
18/// Kleene star combinator: greedy zero-or-more repetition, consuming/producing `Seq<A::PVal>`.
19///
20/// Parsing semantics: always succeeds (may return an empty sequence). Stops when `A` fails or
21/// consumes zero bytes.
22///
23/// ## Consistency
24///
25/// A sequence `s` is consistent with `Star<A>` iff every element of `s` is consistent with `A`.
26///
27/// ## Note
28///
29/// This combinator is mostly used *internally* to specify [`Repeat<A, B>`], which is
30/// able to disambiguate `A` and `B` and hence more compositional.
31#[derive(Copy)]
32pub struct Star<A>(pub A);
33
34impl<A: Clone> Clone for Star<A> {
35    fn clone(&self) -> (cloned: Self)
36        ensures
37            call_ensures(A::clone, (&self.0,), cloned.0),
38    {
39        Star(self.0.clone())
40    }
41}
42
43/// Zero-or-more `A` followed by terminator `B`: sugar for `Pair(Star<A>, B)`.
44///
45/// ## Unambiguity
46///
47/// Requires `disjoint_domains(A, B)`.
48#[derive(Copy)]
49pub struct Repeat<A, B>(pub A, pub B);
50
51impl<A: Clone, B: Clone> Clone for Repeat<A, B> {
52    fn clone(&self) -> (cloned: Self)
53        ensures
54            call_ensures(A::clone, (&self.0,), cloned.0),
55            call_ensures(B::clone, (&self.1,), cloned.1),
56    {
57        Repeat(self.0.clone(), self.1.clone())
58    }
59}
60
61/// Exactly `N` repetitions of combinator `C` (`N` is a runtime value).
62#[derive(Copy)]
63pub struct RepeatN<C, N = u8>(pub N, pub C);
64
65impl<C: Clone, N: Clone> Clone for RepeatN<C, N> {
66    fn clone(&self) -> (cloned: Self)
67        ensures
68            call_ensures(N::clone, (&self.0,), cloned.0),
69            call_ensures(C::clone, (&self.1,), cloned.1),
70    {
71        RepeatN(self.0.clone(), self.1.clone())
72    }
73}
74
75/// Exactly `N` repetitions of combinator `C` (`N` is a compile-time constant).
76#[derive(Copy)]
77pub struct Array<const N: usize, C>(pub C);
78
79impl<const N: usize, C: Clone> Clone for Array<N, C> {
80    fn clone(&self) -> (cloned: Self)
81        ensures
82            call_ensures(C::clone, (&self.0,), cloned.0),
83    {
84        Array(self.0.clone())
85    }
86}
87
88} // verus!
vest_lib/combinators/star/mod.rs

vest_lib/combinators/star/
mod.rs
