vest_lib/combinators/cond/
mod.rs

1//! Conditional format controlled by a boolean flag.
2//!
3//! A disabled [`Cond`] accepts and serializes no values; an enabled one
4//! delegates its specifications, executable operations, and proofs to its child.
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/// Conditionally apply `Inner` depending on a boolean flag.
17///
18/// Parsing semantics: if the flag is `true`, parse with `Inner` and return its value; if the flag is `false`, fail.
19///
20/// ## Consistency
21///
22/// A value `v` is consistent with `Cond(true, Inner)` iff it is consistent with `Inner`. No value is consistent with `Cond(false, Inner)`.
23#[derive(Copy)]
24pub struct Cond<Inner>(pub bool, pub Inner);
25
26impl<Inner: Clone> Clone for Cond<Inner> {
27    fn clone(&self) -> (cloned: Self)
28        ensures
29            call_ensures(Inner::clone, (&self.1,), cloned.1),
30    {
31        Cond(self.0, self.1.clone())
32    }
33}
34
35} // verus!
vest_lib/combinators/cond/mod.rs

vest_lib/combinators/cond/
mod.rs
