vest_lib/regular/
disjoint.rs

1use super::fail::Fail;
2use super::modifier::{Cond, Mapped, Refined, SpecIso, SpecPartialIsoFn, SpecPred, TryMap};
3use super::sequence::{Preceded, SpecPair};
4use super::tag::Tag;
5use super::variant::Choice;
6use crate::properties::*;
7use crate::regular::end::End;
8use vstd::prelude::*;
9
10verus! {
11
12/// A helper trait for [`Choice`] combinator.
13pub trait DisjointFrom<Other> where Self: SpecCombinator, Other: SpecCombinator {
14    /// pre-condition that must be held for [`Self`] and [`Other`] to be disjoint
15    spec fn disjoint_from(&self, other: &Other) -> bool;
16
17    /// The combinator [`Self`] is disjoint from the combinator [`Other`] if the bytes `buf` can be
18    /// parsed by [`Self`] but not by [`Other`]
19    proof fn parse_disjoint_on(&self, other: &Other, buf: Seq<u8>)
20        requires
21            self.disjoint_from(
22                other,
23            ),
24    // just one direction is enough for the proofs of `Choice`
25
26        ensures
27            self.spec_parse(buf) is Some ==> other.spec_parse(buf) is None,
28    ;
29}
30
31// two `Tag(T, value)`s are disjoint if their inner `Refined` combinators are disjoint
32impl<Inner, T> DisjointFrom<Tag<Inner, T>> for Tag<Inner, T> where Inner: SpecCombinator<Type = T> {
33    open spec fn disjoint_from(&self, other: &Tag<Inner, T>) -> bool {
34        self.0.disjoint_from(&other.0)
35    }
36
37    proof fn parse_disjoint_on(&self, other: &Tag<Inner, T>, buf: Seq<u8>) {
38    }
39}
40
41// if `U1` and `U2` are disjoint, then `(U1, V1)` and `(U2, V2)` are disjoint
42impl<U1, U2, V1, V2> DisjointFrom<(U2, V2)> for (U1, V1) where
43    U1: DisjointFrom<U2>,
44    U1: SecureSpecCombinator,
45    U2: SecureSpecCombinator,
46    V1: SpecCombinator,
47    V2: SpecCombinator,
48 {
49    open spec fn disjoint_from(&self, other: &(U2, V2)) -> bool {
50        self.0.disjoint_from(&other.0)
51    }
52
53    proof fn parse_disjoint_on(&self, other: &(U2, V2), buf: Seq<u8>) {
54        self.0.parse_disjoint_on(&other.0, buf)
55    }
56}
57
58// if `U1` and `U2` are disjoint, then `preceded(U1, V1)` and `preceded(U2, V2)` are disjoint
59impl<U1, U2, V1, V2> DisjointFrom<Preceded<U2, V2>> for Preceded<U1, V1> where
60    U1: DisjointFrom<U2>,
61    U1: SecureSpecCombinator<Type = ()>,
62    U2: SecureSpecCombinator<Type = ()>,
63    V1: SpecCombinator,
64    V2: SpecCombinator,
65 {
66    open spec fn disjoint_from(&self, other: &Preceded<U2, V2>) -> bool {
67        self.0.disjoint_from(&other.0)
68    }
69
70    proof fn parse_disjoint_on(&self, other: &Preceded<U2, V2>, buf: Seq<u8>) {
71        self.0.parse_disjoint_on(&other.0, buf)
72    }
73}
74
75impl<U1, U2, V1, V2> DisjointFrom<SpecPair<U2, V2>> for SpecPair<U1, V1> where
76    U1: DisjointFrom<U2>,
77    U1: SecureSpecCombinator,
78    U2: SecureSpecCombinator,
79    V1: SpecCombinator,
80    V2: SpecCombinator,
81 {
82    open spec fn disjoint_from(&self, other: &SpecPair<U2, V2>) -> bool {
83        self.fst.disjoint_from(&other.fst)
84    }
85
86    proof fn parse_disjoint_on(&self, other: &SpecPair<U2, V2>, buf: Seq<u8>) {
87        self.fst.parse_disjoint_on(&other.fst, buf)
88    }
89}
90
91// if `S1` and `S2` are both disjoint from `S3`, and `S2` is disjoint from `S1`,
92// then `Choice<S1, S2>` is disjoint from `S3`,
93//
94// this allows composition of the form `Choice(..., Choice(..., OrcChoice(...)))`
95impl<S1, S2, S3> DisjointFrom<S3> for Choice<S1, S2> where
96    S1: SpecCombinator + DisjointFrom<S3>,
97    S2: SpecCombinator + DisjointFrom<S1> + DisjointFrom<S3>,
98    S3: SpecCombinator,
99 {
100    open spec fn disjoint_from(&self, other: &S3) -> bool {
101        self.0.disjoint_from(other) && self.1.disjoint_from(other)
102    }
103
104    proof fn parse_disjoint_on(&self, other: &S3, buf: Seq<u8>) {
105        self.0.parse_disjoint_on(other, buf);
106        self.1.parse_disjoint_on(other, buf);
107    }
108}
109
110impl<U1, U2, M1, M2> DisjointFrom<Mapped<U2, M2>> for Mapped<U1, M1> where
111    U1: DisjointFrom<U2>,
112    U2: SpecCombinator,
113    M1: SpecIso<Src = U1::Type>,
114    M2: SpecIso<Src = U2::Type>,
115    U1::Type: SpecFrom<M1::Dst>,
116    U2::Type: SpecFrom<M2::Dst>,
117    M1::Dst: SpecFrom<U1::Type>,
118    M2::Dst: SpecFrom<U2::Type>,
119 {
120    open spec fn disjoint_from(&self, other: &Mapped<U2, M2>) -> bool {
121        self.inner.disjoint_from(&other.inner)
122    }
123
124    proof fn parse_disjoint_on(&self, other: &Mapped<U2, M2>, buf: Seq<u8>) {
125        self.inner.parse_disjoint_on(&other.inner, buf)
126    }
127}
128
129// if `U` succeeds on `M1` implies `U` fails on `M2`, then `TryMap<U, M1>` is disjoint from
130// `TryMap<U, M2>`
131impl<U, M1, M2> DisjointFrom<TryMap<U, M2>> for TryMap<U, M1> where
132    U: SpecCombinator,
133    M1: SpecPartialIsoFn<Src = U::Type>,
134    M2: SpecPartialIsoFn<Src = U::Type>,
135    U::Type: SpecTryFrom<M1::Dst>,
136    U::Type: SpecTryFrom<M2::Dst>,
137    M1::Dst: SpecTryFrom<U::Type>,
138    M2::Dst: SpecTryFrom<U::Type>,
139 {
140    open spec fn disjoint_from(&self, other: &TryMap<U, M2>) -> bool {
141        self.inner == other.inner && forall|t|
142            {
143                <M1 as SpecPartialIsoFn>::spec_apply(t) is Ok
144                    ==> <M2 as SpecPartialIsoFn>::spec_apply(t) is Err
145            }
146    }
147
148    proof fn parse_disjoint_on(&self, other: &TryMap<U, M2>, buf: Seq<u8>) {
149    }
150}
151
152// if `self.cond` implies `!other.cond`, then `self` is disjoint from `other`
153impl<Inner1, Inner2> DisjointFrom<Cond<Inner2>> for Cond<Inner1> where
154    Inner1: SpecCombinator,
155    Inner2: SpecCombinator,
156 {
157    open spec fn disjoint_from(&self, other: &Cond<Inner2>) -> bool {
158        self.cond ==> !other.cond
159    }
160
161    proof fn parse_disjoint_on(&self, other: &Cond<Inner2>, buf: Seq<u8>) {
162    }
163}
164
165// if the inner combinator is the same, and whenever `self.predicate` succeeds, `other.predicate`
166// fails, then `self` is disjoint from `other`
167impl<Inner, P1, P2> DisjointFrom<Refined<Inner, P2>> for Refined<Inner, P1> where
168    Inner: SpecCombinator,
169    P1: SpecPred<Inner::Type>,
170    P2: SpecPred<Inner::Type>,
171 {
172    open spec fn disjoint_from(&self, other: &Refined<Inner, P2>) -> bool {
173        self.inner == other.inner && forall|i|
174            { self.predicate.spec_apply(&i) ==> !other.predicate.spec_apply(&i) }
175    }
176
177    proof fn parse_disjoint_on(&self, other: &Refined<Inner, P2>, buf: Seq<u8>) {
178    }
179}
180
181impl<'a, 'b, T1, T2> DisjointFrom<&'a T1> for &'b T2 where
182    T1: SpecCombinator,
183    T2: SpecCombinator + DisjointFrom<T1>,
184 {
185    open spec fn disjoint_from(&self, other: &&T1) -> bool {
186        (*self).disjoint_from(*other)
187    }
188
189    proof fn parse_disjoint_on(&self, other: &&T1, buf: Seq<u8>) {
190        (*self).parse_disjoint_on(*other, buf)
191    }
192}
193
194// `[Fail]` is disjoint from any other combinator
195impl<T> DisjointFrom<T> for Fail where T: SpecCombinator {
196    open spec fn disjoint_from(&self, c: &T) -> bool {
197        true
198    }
199
200    proof fn parse_disjoint_on(&self, c: &T, buf: Seq<u8>) {
201    }
202}
203
204impl<T> DisjointFrom<T> for End where T: SecureSpecCombinator {
205    open spec fn disjoint_from(&self, c: &T) -> bool {
206        c.requires() && c.is_productive()
207    }
208
209    proof fn parse_disjoint_on(&self, c: &T, buf: Seq<u8>) {
210        if let Some((n, v)) = self.spec_parse(buf) {
211            assert(n == 0);
212            c.lemma_parse_productive(buf);
213            c.lemma_parse_length(buf);
214        }
215    }
216}
217
218} // verus!
vest_lib/regular/disjoint.rs

vest_lib/regular/
disjoint.rs
