vest_lib/combinators/tail/
mod.rs

1//! Formats that consume the remaining input.
2//!
3//! [`Tail`] borrows all remaining bytes. [`Eof`] accepts only an empty input
4//! and is used to make complete-consumption requirements explicit.
5/// Executable trait implementations for this combinator.
6pub mod exec;
7/// Correctness proofs for this combinator.
8pub mod proof;
9/// Specification trait implementations for this combinator.
10pub mod spec;
11
12use vstd::prelude::*;
13
14verus! {
15
16/// Tail combinator: denotes the "tail" of the format, useful for under-specification.
17///
18/// Parsing semantics: consumes and return all remaining bytes (even if the input is empty).
19///
20/// ## Note
21///
22/// The DPS serialization replaces (not prepends to) the output buffer,
23/// so `Tail` should only appear at the end of a format (and the trait system enforces this).
24#[derive(Clone, Copy)]
25pub struct Tail;
26
27/// End-of-file combinator: denotes the "EOF".
28///
29/// Parsing semantics: succeeds only if the input is empty, producing `()`.
30///
31/// Implements [`AdmitsUniqueVal`](crate::core::spec::AdmitsUniqueVal).
32///
33/// ## Note
34///
35/// The DPS serialization always replaces the output buffer with the empty sequence, so `Eof`
36/// should only appear at the end of a format (and the trait system enforces this).
37#[derive(Clone, Copy)]
38pub struct Eof;
39
40/// Sequential composition of formats `A` and `B`, where the direction of parsing is reversed compared to [`super::Pair`].
41///
42/// Parsing semantics: parses `B` from the back, consumes the tail part of the input, then parses `A`.
43#[derive(Copy)]
44pub struct PairRev<A, B>(pub B, pub A);
45
46impl<A: Clone, B: Clone> Clone for PairRev<A, B> {
47    fn clone(&self) -> (cloned: Self)
48        ensures
49            call_ensures(B::clone, (&self.0,), cloned.0),
50            call_ensures(A::clone, (&self.1,), cloned.1),
51    {
52        PairRev(self.0.clone(), self.1.clone())
53    }
54}
55
56/// Sugar for `Optional(C, Eof)`.
57#[derive(Copy)]
58pub struct OptionalEnd<C>(pub C);
59
60impl<C: Clone> Clone for OptionalEnd<C> {
61    fn clone(&self) -> (cloned: Self)
62        ensures
63            call_ensures(C::clone, (&self.0,), cloned.0),
64    {
65        OptionalEnd(self.0.clone())
66    }
67}
68
69/// Sugar for `Repeat(C, Eof)`.
70#[derive(Copy)]
71pub struct RepeatTillEnd<C>(pub C);
72
73impl<C: Clone> Clone for RepeatTillEnd<C> {
74    fn clone(&self) -> (cloned: Self)
75        ensures
76            call_ensures(C::clone, (&self.0,), cloned.0),
77    {
78        RepeatTillEnd(self.0.clone())
79    }
80}
81
82} // verus!
vest_lib/combinators/tail/mod.rs

vest_lib/combinators/tail/
mod.rs
