vest_lib/core/
proof.rs

1//! Correctness and security proof traits for Vest combinators.
2
3use crate::core::spec::SpecParser;
4
5use super::spec::*;
6use vstd::prelude::*;
7
8verus! {
9
10/// Serialize-parse roundtrip (DPS).
11///
12/// Serializing a consistent value in DPS style and parsing the result recovers the
13/// original value, consuming exactly `byte_len(v)` bytes.
14///
15/// This is a low-level trait. Individual combinators in the library prove this directly;
16/// the higher-level property [`SPRoundTrip`] is derived via a blanket impl composing this with
17/// [`GoodSerializer`] and [`EquivSerializers`].
18///
19/// ## Note on user-defined combinators
20///
21/// User-defined combinators should prefer proving this trait to proving [`SPRoundTrip`], as
22/// 1. it's a stronger property and proving and implementing this trait would make Rust/Verus auto-derive a proof for [`SPRoundTrip`];
23/// 2. it makes the combinator composable with the rest of the library, which are all built on this stronger property.
24pub trait SPRoundTripDps where
25    Self: SpecByteLen +
26          Consistency<Val = Self::T> +
27          SpecParser<PVal = Self::T> +
28          SpecSerializerDps<SValue = Self::T>,
29 {
30    open spec fn unambiguous(&self) -> bool {
31        true
32    }
33
34    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>)
35        requires
36            self.unambiguous(),
37            self.consistent(v),
38        ensures
39            ({
40                let ibuf = self.spec_serialize_dps(v, obuf);
41                let n = self.byte_len(v) as int;
42                self.spec_parse(ibuf) == Some((n, v))
43            }),
44    ;
45}
46
47/// Serialize-parse roundtrip.
48///
49/// Serializing a consistent value and parsing the result recovers `v`, consuming
50/// the entire serialized buffer. Automatically derived for combinators implementing
51/// [`SPRoundTripDps`] + [`GoodSerializer`] + [`EquivSerializers`].
52///
53/// ## Note on user-defined combinators
54///
55/// User-defined combinators should prefer proving [`SPRoundTripDps`] to proving this trait. See the note on [`SPRoundTripDps`] for details.
56pub trait SPRoundTrip where
57    Self: SpecByteLen +
58          SpecParser<PVal = Self::T> +
59          SpecSerializer<SVal = Self::T> +
60          Consistency<Val = Self::T> +
61{
62    open spec fn sp_roundtrip_inv(&self) -> bool {
63        true
64    }
65
66    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::T)
67        requires
68            self.sp_roundtrip_inv(),
69            self.consistent(v),
70        ensures
71            ({
72                let bytes = self.spec_serialize(v);
73                self.spec_parse(bytes) == Some((bytes.len() as int, v))
74            }),
75    ;
76}
77
78impl<C: SPRoundTripDps + GoodSerializer + EquivSerializers> SPRoundTrip for C {
79    open spec fn sp_roundtrip_inv(&self) -> bool {
80        self.serialize_inv() && self.equiv_inv() && self.unambiguous()
81    }
82
83    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::T) {
84        let empty = Seq::empty();
85        self.theorem_serialize_dps_parse_roundtrip(v, empty);
86        self.lemma_serialize_equiv_on_empty(v);
87        self.lemma_serialize_len(v);
88    }
89}
90
91
92/// Serializer unambiguity (injectivity on consistent values).
93///
94/// Two different consistent values cannot serialize to the same bytes. This
95/// rules out ambiguity in the value-to-wire direction and follows
96/// automatically from [`SPRoundTrip`].
97pub trait NonAmbiguous where
98    Self: Consistency + SpecSerializer<SVal = Self::Val>
99{
100    /// Side conditions needed by the injectivity proof.
101    open spec fn nonamb_inv(&self) -> bool {
102        true
103    }
104
105    /// Proves that equal serializations imply equal values.
106    proof fn lemma_serialize_injective(&self, v1: Self::Val, v2: Self::Val)
107        requires
108            self.nonamb_inv(),
109            self.consistent(v1),
110            self.consistent(v2),
111        ensures
112            self.spec_serialize(v1) == self.spec_serialize(v2) ==> v1 == v2
113    ;
114
115    /// Equivalent contrapositive: distinct values have distinct serializations.
116    proof fn corollary_serialize_injective_contrapositive(&self, v1: Self::Val, v2: Self::Val)
117        requires
118            self.nonamb_inv(),
119            self.consistent(v1),
120            self.consistent(v2),
121        ensures
122            v1 != v2 ==> self.spec_serialize(v1) != self.spec_serialize(v2),
123    {
124        self.lemma_serialize_injective(v1, v2);
125    }
126}
127
128impl<C: SPRoundTrip> NonAmbiguous for C {
129    open spec fn nonamb_inv(&self) -> bool {
130        self.sp_roundtrip_inv()
131    }
132
133    proof fn lemma_serialize_injective(&self, v1: Self::Val, v2: Self::Val) {
134        self.theorem_serialize_parse_roundtrip(v1);
135        self.theorem_serialize_parse_roundtrip(v2);
136    }
137}
138
139
140/// Parse-serialize roundtrip.
141///
142/// Parsing a buffer and serializing the result reproduces the consumed bytes.
143///
144/// Automatically derived for combinators implementing [`SPRoundTrip`] + [`NonMalleable`].
145///
146/// User-defined combinators can also prove this directly.
147pub trait PSRoundTrip where
148    Self: SpecByteLen +
149          SpecParser<PVal = Self::T> +
150          SpecSerializer<SVal = Self::T> +
151{
152    open spec fn ps_roundtrip_inv(&self) -> bool {
153        true
154    }
155
156    proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>)
157        requires
158            self.ps_roundtrip_inv(),
159        ensures
160            self.spec_parse(ibuf) matches Some((n, v)) ==> self.spec_serialize(v) == ibuf.take(n),
161    ;
162
163    proof fn corollary_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)
164        requires
165            self.ps_roundtrip_inv(),
166        ensures
167            self.spec_parse(buf1) matches Some((n1, v1)) ==>
168            self.spec_parse(buf2) matches Some((n2, v2)) ==>
169            v1 == v2 ==> buf1.take(n1) == buf2.take(n2),
170    {
171        self.theorem_parse_serialize_roundtrip(buf1);
172        self.theorem_parse_serialize_roundtrip(buf2);
173    }
174}
175
176impl<C: SPRoundTrip + NonMalleable + SoundParser> PSRoundTrip for C {
177    open spec fn ps_roundtrip_inv(&self) -> bool {
178        self.safe_inv() && self.sound_inv() && self.nonmal_inv() && self.sp_roundtrip_inv()
179    }
180
181    proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>) {
182        let c = self;
183        if let Some((n, v)) = c.spec_parse(ibuf) {
184            c.lemma_parse_sound_value(ibuf);
185            c.theorem_serialize_parse_roundtrip(v);
186
187            let serialized = c.spec_serialize(v);
188            assert((c.spec_parse(serialized)->0).1 == v);
189
190            // By non-malleability: both parses return v, so serialized is equal to the input prefix
191            c.lemma_parse_non_malleable(ibuf, serialized);
192            assert(ibuf.take(n) == serialized);
193        }
194    }
195}
196
197/// Parser non-malleability.
198///
199/// If two buffers parse to equal values, their consumed bytes are identical—i.e.,
200/// each semantic value has a unique byte-level representation.
201pub trait NonMalleable: SafeParser {
202    /// Optional invariant (used by spec-function combinators; struct-based combinators
203    /// typically leave this as `true`)
204    open spec fn nonmal_inv(&self) -> bool {
205        true
206    }
207
208    #[verusfmt::skip]
209    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)
210        requires
211            self.safe_inv(),
212            self.nonmal_inv(),
213        ensures
214            self.spec_parse(buf1) matches Some((n1, v1)) ==>
215            self.spec_parse(buf2) matches Some((n2, v2)) ==>
216            v1 == v2 ==> buf1.take(n1) == buf2.take(n2),
217    ;
218}
219
220/// No-lookahead property for parsers.
221///
222/// Intuitively: the parser's behavior does not depend on "future" bytes beyond the consumed prefix
223/// (i.e., it does not need to "look ahead"/"peek" at them to decide how to parse the prefix).
224///
225/// Formally: if two buffers share a common prefix that successfully parses, then they parse to the same value.
226pub trait NoLookAhead: SafeParser {
227    open spec fn no_lookahead_inv(&self) -> bool {
228        true
229    }
230
231    #[verusfmt::skip]
232    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)
233        requires
234            self.safe_inv(),
235            self.no_lookahead_inv(),
236        ensures
237            self.spec_parse(i1) matches Some((n, v)) ==>
238            0 <= n <= i2.len() ==> i2.take(n) == i1.take(n) ==>
239            self.spec_parse(i2) == Some((n, v)),
240    ;
241
242    proof fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)
243        requires
244            self.safe_inv(),
245            self.no_lookahead_inv(),
246        ensures
247            self.spec_parse(i1) matches Some((n, v)) ==> self.spec_parse(i1 + i2) == Some((n, v)),
248    {
249        self.lemma_no_lookahead(i1, i1 + i2);
250        if let Some((n, v)) = self.spec_parse(i1) {
251            self.lemma_parse_safe(i1);
252            assert(0 <= n <= (i1 + i2).len());
253            assert(i1.take(n) == (i1 + i2).take(n));
254        }
255    }
256}
257
258/// Productivity for parsers.
259///
260/// A productive parser always consumes at least one byte when it succeeds.
261///
262/// Inherently unproductive combinators are:
263/// *   **`Empty`**: Always succeeds and never consumes any bytes.
264/// *   **`Eof`**: Asserts the end of the input. It only succeeds if the buffer is entirely empty, thus always consuming 0 bytes.
265/// *   **`Tail`**: Consumes all remaining bytes in the buffer. If the buffer is already empty, it successfully consumes 0 bytes.
266/// *   **`Opt<A>`**: Evaluates an optional field. If `A` fails, `Opt<A>` successfully returns `None` while consuming 0 bytes.
267/// *   **`Star<A>`**: The Kleene star for zero-or-more repetitions. It can successfully parse zero occurrences of `A`, consuming 0 bytes.
268/// *   **`OptionalEnd<C>` & `RepeatTillEnd<C>`**: These are syntax sugar for `Optional<C, Eof>` and `Repeat<C, Eof>`.
269///
270/// The above combinators still implement the `Productive` trait in order for sequencing combinators
271/// like `Pair` to remain productive, but their `productive_inv` would return `false` (so `lemma_productive` would not apply to them).
272pub trait Productive: SafeParser {
273    open spec fn productive_inv(&self) -> bool {
274        true
275    }
276
277    broadcast proof fn lemma_productive(&self, s: Seq<u8>)
278        requires
279            self.safe_inv(),
280            self.productive_inv(),
281        ensures
282            #[trigger] self.spec_parse(s) matches Some((n, _)) ==> n > 0,
283    ;
284}
285
286/// Full DPS ↔ non-DPS serializer equivalence for *any* output buffer.
287///
288/// See [`EquivSerializers`] for the weaker empty-buffer variant.
289pub trait EquivSerializersGeneral: SpecSerializer + SpecSerializerDps<SValue = Self::SVal> {
290    open spec fn equiv_general_inv(&self) -> bool {
291        true
292    }
293
294    /// `spec_serialize_dps(v, obuf) == spec_serialize(v) + obuf`.
295    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>)
296        requires
297            self.equiv_general_inv(),
298        ensures
299            self.spec_serialize_dps(v, obuf) == self.spec_serialize(v) + obuf,
300    ;
301}
302
303/// DPS ↔ non-DPS serializer equivalence on the empty buffer.
304///
305/// Sufficient for deriving [`SPRoundTrip`] from [`SPRoundTripDps`].
306pub trait EquivSerializers: SpecSerializer + SpecSerializerDps<SValue = Self::SVal> {
307    open spec fn equiv_inv(&self) -> bool {
308        true
309    }
310
311    /// `spec_serialize_dps(v, []) == spec_serialize(v)`.
312    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal)
313        requires
314            self.equiv_inv(),
315        ensures
316            self.spec_serialize_dps(v, seq![]) == self.spec_serialize(v),
317    ;
318}
319
320/// A "strict" combinator that satisfies all the core correctness and security properties proven by the library's combinators.
321pub trait StrictCombinator:
322    SafeParser +
323    Productive +
324    SoundParser +
325    NonMalleable +
326    GoodSerializer +
327    NonTailFmt +
328    SPRoundTripDps +
329    EquivSerializersGeneral {
330
331}
332
333impl<Body> StrictCombinator for Body where
334    Body:
335        SafeParser +
336        Productive +
337        SoundParser +
338        NonMalleable +
339        GoodSerializer +
340        NonTailFmt +
341        SPRoundTripDps +
342        EquivSerializersGeneral,
343 {
344
345}
346
347/// This is a marker trait for combinators that are "leaves" in the combinator hierarchy.
348///
349/// A "leaf" combinator does not expose any non-trivial preconditions on its correctness and security properties.
350///
351/// Built-in combinators that are "leaves" include [Fixed](crate::combinators::bytes::Fixed), [Varied](crate::combinators::bytes::Varied),
352/// [U8](crate::combinators::uints::U8)/[U16Le](crate::combinators::uints::U16Le)/[U32Le](crate::combinators::uints::U32Le),
353/// [FixWith](crate::combinators::recursive::FixWith), [Empty](crate::combinators::marker::Empty), and [Void](crate::combinators::marker::Void).
354///
355/// In addition, any derived/composed combinator proven to satisfy `Leaf::leaf_inv` can also be marked as a leaf combinator.
356pub trait Leaf:
357    SafeParser +
358    GoodSerializer +
359    NonTailFmt +
360    SPRoundTripDps +
361    EquivSerializersGeneral {
362    proof fn leaf_inv(&self)
363        ensures
364            self.unambiguous(),
365            self.safe_inv(),
366            self.serialize_inv(),
367            self.serialize_dps_inv(),
368            self.equiv_general_inv(),
369    ;
370}
371
372/// Similar to [`Leaf`], but also includes the parser soundness and non-malleability properties.
373pub trait LeafNonMalleable:
374    Leaf +
375    SoundParser +
376    NonMalleable {
377    proof fn nonmal_leaf_inv(&self)
378        ensures
379            self.unambiguous(),
380            self.safe_inv(),
381            self.sound_inv(),
382            self.nonmal_inv(),
383            self.serialize_inv(),
384            self.serialize_dps_inv(),
385            self.equiv_general_inv(),
386    ;
387}
388
389impl<Fmt: LeafNonMalleable> Leaf for Fmt {
390    proof fn leaf_inv(&self) {
391        self.nonmal_leaf_inv();
392    }
393}
394
395} // verus!
vest_lib/core/proof.rs

vest_lib/core/
proof.rs
