vest_lib/combinators/refined/
mod.rs

1//! Predicate refinement and constant-value formats.
2//!
3//! [`Refined`] keeps only values satisfying a predicate. [`Const`] fixes that value and is commonly used for static tags or discriminants.
4/// Executable trait implementations for this combinator.
5pub mod exec;
6/// Correctness proofs for this combinator.
7pub mod proof;
8/// Specification trait implementations for this combinator.
9pub mod spec;
10
11use vstd::prelude::*;
12
13use super::{Preceded, Terminated};
14
15verus! {
16
17/// Value refinement combinator: filters values through a predicate.
18///
19/// ## Consistency
20///
21/// `inner.consistent(v) && predicate.apply(v)`.
22#[derive(Copy)]
23pub struct Refined<Inner, Predicate>(pub Inner, pub Predicate);
24
25impl<Inner: Clone, Predicate: Clone> Clone for Refined<Inner, Predicate> {
26    fn clone(&self) -> (cloned: Self)
27        ensures
28            call_ensures(Inner::clone, (&self.0,), cloned.0),
29            call_ensures(Predicate::clone, (&self.1,), cloned.1),
30    {
31        Refined(self.0.clone(), self.1.clone())
32    }
33}
34
35/// Constant-value combinator: matches a specific constant value.
36///
37/// Parsing semantics: parses with `inner` and succeeds only if the result equals the expected value.
38/// The matched constant value itself is returned.
39///
40/// Implements [`AdmitsUniqueVal`](crate::core::spec::AdmitsUniqueVal).
41#[derive(Copy)]
42pub struct Const<Inner, Value>(pub Inner, pub Value);
43
44impl<Inner: Clone, Value: Clone> Clone for Const<Inner, Value> {
45    fn clone(&self) -> (cloned: Self)
46        ensures
47            call_ensures(Inner::clone, (&self.0,), cloned.0),
48            call_ensures(Value::clone, (&self.1,), cloned.1),
49    {
50        Const(self.0.clone(), self.1.clone())
51    }
52}
53
54// #[allow(type_alias_bounds)]
55// pub type PrefixTagged<TagFmt: SpecByteLen, Of, Tag = <TagFmt as SpecByteLen>::T> = Preceded<
56//     Const<TagFmt, Tag>,
57//     Tag,
58//     Of,
59//     false,
60// >;
61// #[allow(type_alias_bounds)]
62// pub type SuffixTagged<Of, TagFmt: SpecByteLen, Tag = <TagFmt as SpecByteLen>::T> = Terminated<
63//     Of,
64//     Const<TagFmt, Tag>,
65//     Tag,
66//     false,
67// >;
68// #[allow(non_snake_case)]
69// #[verifier::allow_in_spec]
70// pub fn PrefixTagged<TagFmt, Of, Tag>(tag_fmt: TagFmt, tag: Tag, body: Of) -> PrefixTagged<
71//     TagFmt,
72//     Of,
73//     Tag,
74// > where TagFmt: SpecByteLen, Tag: Copy
75//     returns
76//         (Preceded::<Const<TagFmt, Tag>, Tag, Of, false> {
77//             a: Const(tag_fmt, tag),
78//             a_val: tag,
79//             b: body,
80//         }),
81// {
82//     let a = Const(tag_fmt, tag);
83//     let b = body;
84//     let a_val = tag;
85//     Preceded { a, a_val, b }
86// }
87// #[allow(non_snake_case)]
88// #[verifier::allow_in_spec]
89// pub fn SuffixTagged<Of, TagFmt, Tag>(body: Of, tag_fmt: TagFmt, tag: Tag) -> SuffixTagged<
90//     Of,
91//     TagFmt,
92//     Tag,
93// > where TagFmt: SpecByteLen, Tag: Copy
94//     returns
95//         (Terminated::<Of, Const<TagFmt, Tag>, Tag, false> {
96//             a: body,
97//             b: Const(tag_fmt, tag),
98//             b_val: tag,
99//         }),
100// {
101//     let a = body;
102//     let b = Const(tag_fmt, tag);
103//     let b_val = tag;
104//     Terminated { a, b, b_val }
105// }
106/// Sugar for `Preceded { a: Const(inner, tag), a_val: tag, b: body }`.
107#[derive(Copy)]
108pub struct PrefixTagged<Tg, Tag, Of>(pub Tg, pub Tag, pub Of);
109
110impl<Tg: Clone, Tag: Clone, Of: Clone> Clone for PrefixTagged<Tg, Tag, Of> {
111    fn clone(&self) -> (cloned: Self)
112        ensures
113            call_ensures(Tg::clone, (&self.0,), cloned.0),
114            call_ensures(Tag::clone, (&self.1,), cloned.1),
115            call_ensures(Of::clone, (&self.2,), cloned.2),
116    {
117        PrefixTagged(self.0.clone(), self.1.clone(), self.2.clone())
118    }
119}
120
121/// Sugar for `Terminated { a: body, b: Const(inner, tag), b_val: tag }`.
122#[derive(Copy)]
123pub struct SuffixTagged<Of, Tg, Tag>(pub Of, pub Tg, pub Tag);
124
125impl<Of: Clone, Tg: Clone, Tag: Clone> Clone for SuffixTagged<Of, Tg, Tag> {
126    fn clone(&self) -> (cloned: Self)
127        ensures
128            call_ensures(Of::clone, (&self.0,), cloned.0),
129            call_ensures(Tg::clone, (&self.1,), cloned.1),
130            call_ensures(Tag::clone, (&self.2,), cloned.2),
131    {
132        SuffixTagged(self.0.clone(), self.1.clone(), self.2.clone())
133    }
134}
135
136} // verus!
vest_lib/combinators/refined/mod.rs

vest_lib/combinators/refined/
mod.rs
