vest_lib/combinators/preceded/
mod.rs

1//! Sequential composition that discards a prefix value.
2//!
3//! [`Preceded`] has the same wire order as a pair but exposes only the second
4//! semantic value. The prefix must still be reconstructible for serialization.
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/// Parsing semantics: like `(A, B)`, but discards the value parsed by `A` and returns only the value parsed by `B`.
17///
18/// Serialization semantics: reuses `a_val` as the serialized witness for `A`, then serializes `B`.
19///
20/// When `CHECK` is `false`, parsing is malleable in the discarded prefix unless `A` admits a unique consistent value.
21/// When `CHECK` is `true`, parsing additionally checks that the parsed prefix equals `a_val`.
22#[derive(Copy)]
23pub struct Preceded<A, AVal, B, const CHECK: bool = false> {
24    pub a: A,
25    pub b: B,
26    pub a_val: AVal,
27}
28
29impl<A: Clone, AVal: Clone, B: Clone, const CHECK: bool> Clone for Preceded<A, AVal, B, CHECK> {
30    fn clone(&self) -> (cloned: Self)
31        ensures
32            call_ensures(A::clone, (&self.a,), cloned.a),
33            call_ensures(B::clone, (&self.b,), cloned.b),
34            call_ensures(AVal::clone, (&self.a_val,), cloned.a_val),
35    {
36        Preceded { a: self.a.clone(), b: self.b.clone(), a_val: self.a_val.clone() }
37    }
38}
39
40} // verus!
vest_lib/combinators/preceded/mod.rs

vest_lib/combinators/preceded/
mod.rs
