vest/regular/
disjoint.rs

1use super::bytes::Bytes;
2use super::bytes_n::BytesN;
3use super::choice::OrdChoice;
4use super::cond::Cond;
5use super::depend::SpecDepend;
6use super::fail::Fail;
7use super::map::{Mapped, SpecIso};
8use super::preceded::Preceded;
9use super::refined::Refined;
10use super::tag::{Tag, TagPred};
11use super::uints::{U16, U32, U64, U8};
12use crate::properties::*;
13use vstd::prelude::*;
14
15verus! {
16
17/// A helper trait for [`OrdChoice`] combinator.
18pub trait DisjointFrom<Other> where Self: SpecCombinator, Other: SpecCombinator {
19    /// pre-condition that must be held for [`Self`] and [`Other`] to be disjoint
20    spec fn disjoint_from(&self, other: &Other) -> bool;
21
22    /// The combinator [`Self`] is disjoint from the combinator [`Other`] if the bytes `buf` can be
23    /// parsed by [`Self`] but not by [`Other`]
24    proof fn parse_disjoint_on(&self, other: &Other, buf: Seq<u8>)
25        requires
26            self.disjoint_from(
27                other,
28            ),
29    // just one direction is enough for the proofs of `OrdChoice`
30
31        ensures
32            self.spec_parse(buf).is_ok() ==> other.spec_parse(buf).is_err(),
33    ;
34}
35
36macro_rules! impl_disjoint_for_int_tag {
37    ($combinator:ty) => {
38        ::builtin_macros::verus! {
39            impl DisjointFrom<$combinator> for $combinator {
40                // two `Tag(T, value)`s are disjoint if their bytes `value`s are different
41                open spec fn disjoint_from(&self, other: &$combinator) -> bool {
42                    self.0.predicate.0 != other.0.predicate.0
43                }
44
45                proof fn parse_disjoint_on(&self, other: &$combinator, buf: Seq<u8>) {
46                }
47            }
48        }
49    };
50}
51
52macro_rules! impl_disjoint_for_refined_int {
53    ($combinator:ty) => {
54        ::builtin_macros::verus! {
55            impl DisjointFrom<$combinator> for $combinator {
56                // two `Tag(T, value)`s are disjoint if their bytes `value`s are different
57                open spec fn disjoint_from(&self, other: &$combinator) -> bool {
58                    self.predicate.0 != other.predicate.0
59                }
60
61                proof fn parse_disjoint_on(&self, other: &$combinator, buf: Seq<u8>) {
62                }
63            }
64        }
65    };
66}
67
68impl_disjoint_for_int_tag!(Tag<U8, u8>);
69
70impl_disjoint_for_int_tag!(Tag<U16, u16>);
71
72impl_disjoint_for_int_tag!(Tag<U32, u32>);
73
74impl_disjoint_for_int_tag!(Tag<U64, u64>);
75
76impl_disjoint_for_refined_int!(Refined<U8, TagPred<u8>>);
77
78impl_disjoint_for_refined_int!(Refined<U16, TagPred<u16>>);
79
80impl_disjoint_for_refined_int!(Refined<U32, TagPred<u32>>);
81
82impl_disjoint_for_refined_int!(Refined<U64, TagPred<u64>>);
83
84// two `Tag(T, value)`s are disjoint if their bytes `value`s are different
85impl<const N: usize> DisjointFrom<Tag<BytesN<N>, Seq<u8>>> for Tag<BytesN<N>, Seq<u8>> {
86    open spec fn disjoint_from(&self, other: &Tag<BytesN<N>, Seq<u8>>) -> bool {
87        self.0.predicate.0 != other.0.predicate.0
88    }
89
90    proof fn parse_disjoint_on(&self, other: &Tag<BytesN<N>, Seq<u8>>, buf: Seq<u8>) {
91    }
92}
93
94// two `Tag(T, value)`s are disjoint if their bytes `value`s are different
95impl DisjointFrom<Tag<Bytes, Seq<u8>>> for Tag<Bytes, Seq<u8>> {
96    open spec fn disjoint_from(&self, other: &Tag<Bytes, Seq<u8>>) -> bool {
97        // must also say that two `Bytes` combinators are of the same length
98        self.0.predicate.0 != other.0.predicate.0 && self.0.inner.0 == other.0.inner.0
99    }
100
101    proof fn parse_disjoint_on(&self, other: &Tag<Bytes, Seq<u8>>, buf: Seq<u8>) {
102    }
103}
104
105impl<const N: usize> DisjointFrom<Refined<BytesN<N>, TagPred<Seq<u8>>>> for Refined<BytesN<N>, TagPred<Seq<u8>>> {
106    open spec fn disjoint_from(&self, other: &Refined<BytesN<N>, TagPred<Seq<u8>>>) -> bool {
107        self.predicate.0 != other.predicate.0
108    }
109
110    proof fn parse_disjoint_on(&self, other: &Refined<BytesN<N>, TagPred<Seq<u8>>>, buf: Seq<u8>) {
111    }
112}
113
114impl DisjointFrom<Refined<Bytes, TagPred<Seq<u8>>>> for Refined<Bytes, TagPred<Seq<u8>>> {
115    open spec fn disjoint_from(&self, other: &Refined<Bytes, TagPred<Seq<u8>>>) -> bool {
116        self.predicate.0 != other.predicate.0 && self.inner.0 == other.inner.0
117    }
118
119    proof fn parse_disjoint_on(&self, other: &Refined<Bytes, TagPred<Seq<u8>>>, buf: Seq<u8>) {
120    }
121}
122
123// if `U1` and `U2` are disjoint, then `(U1, V1)` and `(U2, V2)` are disjoint
124impl<U1, U2, V1, V2> DisjointFrom<(U2, V2)> for (U1, V1) where
125    U1: DisjointFrom<U2>,
126    U1: SecureSpecCombinator,
127    U2: SecureSpecCombinator,
128    V1: SpecCombinator,
129    V2: SpecCombinator,
130 {
131    open spec fn disjoint_from(&self, other: &(U2, V2)) -> bool {
132        self.0.disjoint_from(&other.0)
133    }
134
135    proof fn parse_disjoint_on(&self, other: &(U2, V2), buf: Seq<u8>) {
136        self.0.parse_disjoint_on(&other.0, buf)
137    }
138}
139
140// if `U1` and `U2` are disjoint, then `preceded(U1, V1)` and `preceded(U2, V2)` are disjoint
141impl<U1, U2, V1, V2> DisjointFrom<Preceded<U2, V2>> for Preceded<U1, V1> where
142    U1: DisjointFrom<U2>,
143    U1: SecureSpecCombinator<SpecResult = ()>,
144    U2: SecureSpecCombinator<SpecResult = ()>,
145    V1: SpecCombinator,
146    V2: SpecCombinator,
147 {
148    open spec fn disjoint_from(&self, other: &Preceded<U2, V2>) -> bool {
149        self.0.disjoint_from(&other.0)
150    }
151
152    proof fn parse_disjoint_on(&self, other: &Preceded<U2, V2>, buf: Seq<u8>) {
153        self.0.parse_disjoint_on(&other.0, buf)
154    }
155}
156
157impl<U1, U2, V1, V2> DisjointFrom<SpecDepend<U2, V2>> for SpecDepend<U1, V1> where
158    U1: DisjointFrom<U2>,
159    U1: SecureSpecCombinator,
160    U2: SecureSpecCombinator,
161    V1: SpecCombinator,
162    V2: SpecCombinator,
163 {
164    open spec fn disjoint_from(&self, other: &SpecDepend<U2, V2>) -> bool {
165        self.fst.disjoint_from(&other.fst)
166    }
167
168    proof fn parse_disjoint_on(&self, other: &SpecDepend<U2, V2>, buf: Seq<u8>) {
169        self.fst.parse_disjoint_on(&other.fst, buf)
170    }
171}
172
173// if `S1` and `S2` are both disjoint from `S3`, and `S2` is disjoint from `S1`,
174// then `OrdChoice<S1, S2>` is disjoint from `S3`,
175//
176// this allows composition of the form `OrdChoice(..., OrdChoice(..., OrcChoice(...)))`
177impl<S1, S2, S3> DisjointFrom<S3> for OrdChoice<S1, S2> where
178    S1: SpecCombinator + DisjointFrom<S3>,
179    S2: SpecCombinator + DisjointFrom<S1> + DisjointFrom<S3>,
180    S3: SpecCombinator,
181 {
182    open spec fn disjoint_from(&self, other: &S3) -> bool {
183        self.0.disjoint_from(other) && self.1.disjoint_from(other)
184    }
185
186    proof fn parse_disjoint_on(&self, other: &S3, buf: Seq<u8>) {
187        self.0.parse_disjoint_on(other, buf);
188        self.1.parse_disjoint_on(other, buf);
189    }
190}
191
192impl<U1, U2, M1, M2> DisjointFrom<Mapped<U2, M2>> for Mapped<U1, M1> where
193    U1: DisjointFrom<U2>,
194    U2: SpecCombinator,
195    M1: SpecIso<Src = U1::SpecResult>,
196    M2: SpecIso<Src = U2::SpecResult>,
197    U1::SpecResult: SpecFrom<M1::Dst>,
198    U2::SpecResult: SpecFrom<M2::Dst>,
199    M1::Dst: SpecFrom<U1::SpecResult>,
200    M2::Dst: SpecFrom<U2::SpecResult>,
201 {
202    open spec fn disjoint_from(&self, other: &Mapped<U2, M2>) -> bool {
203        self.inner.disjoint_from(&other.inner)
204    }
205
206    proof fn parse_disjoint_on(&self, other: &Mapped<U2, M2>, buf: Seq<u8>) {
207        self.inner.parse_disjoint_on(&other.inner, buf)
208    }
209}
210
211// if `self.cond` implies `!other.cond`, then `self` is disjoint from `other`
212impl<Inner1, Inner2> DisjointFrom<Cond<Inner2>> for Cond<Inner1> where
213    Inner1: SpecCombinator,
214    Inner2: SpecCombinator,
215 {
216    open spec fn disjoint_from(&self, other: &Cond<Inner2>) -> bool {
217        self.cond ==> !other.cond
218    }
219
220    proof fn parse_disjoint_on(&self, other: &Cond<Inner2>, buf: Seq<u8>) {
221    }
222}
223
224impl<'a, 'b, T1, T2> DisjointFrom<&'a T1> for &'b T2 where
225    T1: SpecCombinator,
226    T2: SpecCombinator + DisjointFrom<T1>,
227 {
228    open spec fn disjoint_from(&self, other: &&T1) -> bool {
229        (*self).disjoint_from(*other)
230    }
231
232    proof fn parse_disjoint_on(&self, other: &&T1, buf: Seq<u8>) {
233        (*self).parse_disjoint_on(*other, buf)
234    }
235}
236
237// `[Fail]` is disjoint from any other combinator
238impl<T> DisjointFrom<T> for Fail where T: SpecCombinator {
239    open spec fn disjoint_from(&self, c: &T) -> bool {
240        true
241    }
242
243    proof fn parse_disjoint_on(&self, c: &T, buf: Seq<u8>) {
244    }
245}
246
247} // verus!
vest/regular/disjoint.rs

vest/regular/
disjoint.rs
