vest_lib/combinators/recursive/
mod.rs

1//! Bounded fixpoint combinator for recursive and mutually recursive formats.
2//!
3//! Body proof traits state preservation of
4//! each invariant under the inductive hypothesis.
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 crate::core::proof::LeafNonMalleable;
13use crate::core::proof::StrictCombinator;
14use vstd::prelude::*;
15
16pub use exec::{ParserRecBody, PrepareRecBody, SerializerRecBody};
17pub use proof::{
18    EquivSerializersGeneralRecBody, NoLookAheadRecBody, NonMalleableRecBody, SPRoundTripDpsRecBody,
19    StrictRecBody,
20};
21pub use spec::{
22    BundledSpecs, GoodSerializerRecBody, NonTailFmtRecBody, ParamRecSpecs, ProductiveRecBody,
23    SafeParserRecBody, SoundParserRecBody, SpecRecBody,
24};
25
26use crate::core::{proof::*, spec::*};
27
28verus! {
29
30/// Bounded fixpoint combinator for parameterized recursive formats.
31///
32/// `Param` is the starting parameter for the recursive `Body`.
33/// Context-free recursive formats use `Param = ()`.
34#[derive(Copy)]
35pub struct FixWith<const LIMIT: usize, Body, Param>(pub Body, pub Param);
36
37// spec fn fix_<T>(r: spec_fn(ParserFnSpec<T>) -> impl SpecParser<PVal = T>, input: Seq<u8>) -> impl SpecParser<PVal = T>
38spec fn fix_<T>(r: spec_fn(ParserFnSpec<T>) -> impl SpecParser<PVal = T>, input: Seq<u8>) -> Option<
39    (int, T),
40>
41    decreases input.len(),
42{
43    let f = r;
44    let call_back = |buf: Seq<u8>|
45        if buf.len() < input.len() {
46            fix_(r, buf)
47        } else {
48            None
49        };
50    f(call_back).spec_parse(input)
51}
52
53impl<const LIMIT: usize, Body: Clone, Param: Clone> Clone for FixWith<LIMIT, Body, Param> {
54    fn clone(&self) -> (cloned: Self)
55        ensures
56            call_ensures(Body::clone, (&self.0,), cloned.0),
57            call_ensures(Param::clone, (&self.1,), cloned.1),
58    {
59        FixWith(self.0.clone(), self.1.clone())
60    }
61}
62
63impl<const N: usize, Body, Param> LeafNonMalleable for FixWith<N, Body, Param> where
64    Param: DeepView<V = Body::Param>,
65    Body: StrictRecBody,
66    Body::Body: StrictCombinator,
67 {
68    proof fn nonmal_leaf_inv(&self) {
69    }
70}
71
72} // verus!
vest_lib/combinators/recursive/mod.rs

vest_lib/combinators/recursive/
mod.rs
