vest/regular/
refined.rs

1use crate::properties::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// The spec version of [`Pred`].
7pub trait SpecPred {
8    /// The input type of the predicate.
9    type Input;
10
11    /// Applies the predicate to the input.
12    spec fn spec_apply(&self, i: &Self::Input) -> bool;
13}
14
15/// All predicates to be used in [`Refined`] combinator must implement this trait.
16pub trait Pred: View where Self::V: SpecPred<Input = <Self::InputOwned as View>::V> {
17    /// The input type of the predicate.
18    type Input<'a>: View<V = <Self::InputOwned as View>::V>;
19
20    /// The owned version of the input type.
21    type InputOwned: View;
22
23    /// Applies the predicate to the input.
24    fn apply(&self, i: &Self::Input<'_>) -> (res: bool)
25        ensures
26            res == self@.spec_apply(&i@),
27    ;
28}
29
30/// Combinator that refines the result of an `inner` combinator with a predicate that implements
31/// [`Pred`].
32pub struct Refined<Inner, P> {
33    /// The inner combinator.
34    pub inner: Inner,
35    /// The predicate.
36    pub predicate: P,
37}
38
39impl<Inner: View, P: View> View for Refined<Inner, P> where  {
40    type V = Refined<Inner::V, P::V>;
41
42    open spec fn view(&self) -> Self::V {
43        Refined { inner: self.inner@, predicate: self.predicate@ }
44    }
45}
46
47impl<Inner, P> SpecCombinator for Refined<Inner, P> where
48    Inner: SpecCombinator,
49    P: SpecPred<Input = Inner::SpecResult>,
50 {
51    type SpecResult = Inner::SpecResult;
52
53    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
54        match self.inner.spec_parse(s) {
55            Ok((n, v)) if self.predicate.spec_apply(&v) => Ok((n, v)),
56            _ => Err(()),
57        }
58    }
59
60    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
61        if self.predicate.spec_apply(&v) {
62            self.inner.spec_serialize(v)
63        } else {
64            Err(())
65        }
66    }
67
68    proof fn spec_parse_wf(&self, s: Seq<u8>) {
69        self.inner.spec_parse_wf(s);
70    }
71}
72
73impl<Inner, P> SecureSpecCombinator for Refined<Inner, P> where
74    Inner: SecureSpecCombinator,
75    P: SpecPred<Input = Inner::SpecResult>,
76 {
77    open spec fn is_prefix_secure() -> bool {
78        Inner::is_prefix_secure()
79    }
80
81    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
82        self.inner.theorem_serialize_parse_roundtrip(v);
83    }
84
85    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
86        self.inner.theorem_parse_serialize_roundtrip(buf);
87    }
88
89    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
90        self.inner.lemma_prefix_secure(s1, s2);
91        assert(Self::is_prefix_secure() ==> self.spec_parse(s1).is_ok() ==> self.spec_parse(
92            s1.add(s2),
93        ) == self.spec_parse(s1));
94    }
95}
96
97impl<Inner, P> Combinator for Refined<
98    Inner,
99    P,
100> where
101    Inner: Combinator,
102    Inner::V: SecureSpecCombinator<SpecResult = <Inner::Owned as View>::V>,
103    P: for <'a>Pred<Input<'a> = Inner::Result<'a>, InputOwned = Inner::Owned>,
104    P::V: SpecPred<Input = <Inner::Owned as View>::V>,
105 {
106    type Result<'a> = Inner::Result<'a>;
107
108    type Owned = Inner::Owned;
109
110    open spec fn spec_length(&self) -> Option<usize> {
111        self.inner.spec_length()
112    }
113
114    fn length(&self) -> Option<usize> {
115        self.inner.length()
116    }
117
118    open spec fn parse_requires(&self) -> bool {
119        self.inner.parse_requires()
120    }
121
122    fn parse<'a>(&self, s: &'a [u8]) -> Result<(usize, Self::Result<'a>), ParseError> {
123        match self.inner.parse(s) {
124            Ok((n, v)) => if self.predicate.apply(&v) {
125                Ok((n, v))
126            } else {
127                Err(ParseError::RefinedPredicateFailed)
128            },
129            Err(e) => Err(e),
130        }
131    }
132
133    open spec fn serialize_requires(&self) -> bool {
134        self.inner.serialize_requires()
135    }
136
137    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> Result<
138        usize,
139        SerializeError,
140    > {
141        if self.predicate.apply(&v) {
142            self.inner.serialize(v, data, pos)
143        } else {
144            Err(SerializeError::RefinedPredicateFailed)
145        }
146    }
147}
148
149} // verus!
vest/regular/refined.rs

vest/regular/
refined.rs
