vest_lib/combinators/implicit/
mod.rs

1//! Dependent sequencing that omits a parsed header from the public value.
2//!
3//! [`Implicit`] selects a body from a header like [`Bind`](crate::combinators::Bind),
4//! but reconstructs that header from the body during serialization.
5/// Correctness proofs for this combinator.
6pub mod proof;
7/// Specification trait implementations for this combinator.
8pub mod spec;
9
10use crate::core::spec::Consistency;
11use vstd::prelude::*;
12
13verus! {
14
15/// A family of dependent combinators indexed by a key type.
16///
17/// Used to constrain the `Tail` combinator in a [`Implicit<Head, Tail>`].
18pub trait DepCombinator {
19    /// The type of keys parsed by the head combinator/to be recovered during serialization.
20    type Key;
21
22    /// The type of values consumed/produced by the body combinator.
23    type Val;
24
25    /// The type of the body combinator produced by `apply`.
26    type Body: Consistency<Val = Self::Val>;
27
28    /// Given a key, produce the body combinator for that key.
29    spec fn apply(&self, key: Self::Key) -> Self::Body;
30
31    /// Given a body value, recover the key used to produce the body combinator.
32    spec fn recover(&self, value: Self::Val) -> Self::Key;
33
34    open spec fn recover_inv(&self) -> bool {
35        true
36    }
37
38    /// Recover must agree with any key that makes the body's value consistent.
39    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val)
40        requires
41            self.recover_inv(),
42        ensures
43            self.apply(key).consistent(value) ==> self.recover(value) == key,
44    ;
45}
46
47/// Dependent family encoded by a pair of pure spec closures `(apply, recover)`.
48pub type KVFormat<Key, Value, Fmt> = (spec_fn(Key) -> Fmt, spec_fn(Value) -> Key);
49
50/// Dependent sequential combinator with deterministic key recovery.
51///
52/// Parsing semantics: parse `Head` to get a key, then parse the
53/// body via `Tail::apply(key)`. Only the body value is returned.
54///
55/// The key is recovered via `Tail::recover(value)` during serialization.
56///
57/// ## Consistency
58///
59/// A value `v: Tail::Val` is consistent with `Implicit(Head, Tail)` iff
60/// ```text
61/// let key = self.1.recover(v);
62/// self.0.consistent(key) && self.1.apply(key).consistent(v)
63/// ```
64///
65/// ## Unambiguity
66///
67/// ```text
68/// self.0.unambiguous() &&
69/// forall|key: Head::PVal| #[trigger] (self.1.apply(key)).unambiguous()
70/// ```
71#[derive(Copy)]
72pub struct Implicit<Head, Tail>(pub Head, pub Tail);
73
74impl<Head: Clone, Tail: Clone> Clone for Implicit<Head, Tail> {
75    fn clone(&self) -> (cloned: Self)
76        ensures
77            call_ensures(Head::clone, (&self.0,), cloned.0),
78            call_ensures(Tail::clone, (&self.1,), cloned.1),
79    {
80        Implicit(self.0.clone(), self.1.clone())
81    }
82}
83
84/// One of the [dependent family of combinators](DepCombinator)
85///
86/// Typically used as `Implicit(U8, VLData())`.
87pub struct VariedLen<Len = u8>(pub core::marker::PhantomData<Len>);
88
89/// Convenience constructor for [`VariedLen`].
90#[allow(non_snake_case)]
91pub open spec fn VLData<Len>() -> VariedLen<Len> {
92    VariedLen(core::marker::PhantomData)
93}
94
95/// One of the [dependent family of combinators](DepCombinator)
96///
97/// Typically used as `Implicit(U16Le, NBytesOf(inner_fmt))`.
98pub struct NBytesOf<Len, Then>(pub core::marker::PhantomData<Len>, pub Then);
99
100/// Convenience constructor for [`NBytesOf`].
101#[allow(non_snake_case)]
102pub open spec fn VLDataOf<Len, C>(c: C) -> NBytesOf<Len, C> {
103    NBytesOf(core::marker::PhantomData, c)
104}
105
106/// One of the [dependent family of combinators](DepCombinator)
107///
108/// Typically used to build linear chains of tagged unions: `TVOr(0x01u8, fmt1, TVOr(0x02u8, fmt2, Uninhabited()))`
109pub struct TVOr<Tag, C, Rest>(pub Tag, pub C, pub Rest);
110
111/// One of the [dependent family of combinators](DepCombinator)
112///
113/// Typically used in the "uninhabited" branch of a [`TVOr`] chain.
114pub struct VoidTag<Tag>(pub core::marker::PhantomData<Tag>);
115
116/// Convenience constructor for [`VoidTag`].
117#[allow(non_snake_case)]
118pub open spec fn Uninhabited<Tag>() -> VoidTag<Tag> {
119    VoidTag(core::marker::PhantomData)
120}
121
122/// One of the [dependent family of combinators](DepCombinator)
123///
124/// Typically used as `Implicit((U8, U16Le), TLVOf(body))`.
125pub struct TLVal<Tag, Len, Body>(pub Body, pub core::marker::PhantomData<(Tag, Len)>);
126
127/// Convenience constructor for [`TLVal`].
128#[allow(non_snake_case)]
129pub open spec fn TLVOf<Tag, Len, Body>(body: Body) -> TLVal<Tag, Len, Body> {
130    TLVal(body, core::marker::PhantomData)
131}
132
133/// One of the [dependent family of combinators](DepCombinator)
134///
135/// Balanced binary tree node for tag-value choices.
136pub struct TagValNode<Tag, Left, Right>(pub Left, pub Right, pub core::marker::PhantomData<Tag>);
137
138/// One of the [dependent family of combinators](DepCombinator)
139///
140/// Leaf node for tag-value tree.
141#[derive(Copy)]
142pub struct TVLeaf<Tag, C>(pub Tag, pub C);
143
144impl<Tag: Clone, C: Clone> Clone for TVLeaf<Tag, C> {
145    fn clone(&self) -> (cloned: Self)
146        ensures
147            call_ensures(Tag::clone, (&self.0,), cloned.0),
148            call_ensures(C::clone, (&self.1,), cloned.1),
149    {
150        TVLeaf(self.0.clone(), self.1.clone())
151    }
152}
153
154/// Convenience constructor for [`TagValNode`].
155#[allow(non_snake_case)]
156pub open spec fn TVNode<Tag, Left, Right>(left: Left, right: Right) -> TagValNode<
157    Tag,
158    Left,
159    Right,
160> {
161    TagValNode(left, right, core::marker::PhantomData)
162}
163
164} // verus!
vest_lib/combinators/implicit/mod.rs

vest_lib/combinators/implicit/
mod.rs
