vest_lib/combinators/
disjoint.rs

1//! Broadcast lemmas establishing `disjoint_domains`
2//! for common combinator compositions.
3use super::mapped::spec::{BiMap, SpecMap, SpecMapper};
4use super::*;
5use crate::core::proof::*;
6use crate::core::spec::SpecPred;
7use crate::core::spec::*;
8use vstd::prelude::*;
9
10verus! {
11
12/// Disjointness is symmetric, but symmetry is deliberately not broadcast: broadcasting it
13/// creates a quantifier-instantiation cycle with every directional decomposition rule below.
14pub proof fn lemma_disjoint_symmetric<Left: SpecParser, Right: SpecParser>(left: Left, right: Right)
15    requires
16        disjoint_domains(left, right),
17    ensures
18        disjoint_domains(right, left),
19{
20    reveal(disjoint_domains);
21}
22
23/// [`Void`] accepts no input and is therefore disjoint from every parser.
24pub broadcast proof fn lemma_disjoint_void_left<Other: SpecParser>(void: Void, other: Other)
25    ensures
26        #[trigger] disjoint_domains(void, other),
27{
28    reveal(disjoint_domains);
29}
30
31/// Every parser is disjoint from [`Void`].
32pub broadcast proof fn lemma_disjoint_void_right<Other: SpecParser>(other: Other, void: Void)
33    ensures
34        #[trigger] disjoint_domains(other, void),
35{
36    reveal(disjoint_domains);
37}
38
39/// Two [`Const`] parsers with the same inner parser but different values are disjoint.
40pub broadcast proof fn lemma_disjoint_const<Inner: SpecParser>(
41    tag1: Const<Inner, Inner::PVal>,
42    tag2: Const<Inner, Inner::PVal>,
43)
44    requires
45        tag1.0 == tag2.0,
46        tag1.1 != tag2.1,
47    ensures
48        #[trigger] disjoint_domains(tag1, tag2),
49{
50    reveal(disjoint_domains);
51}
52
53/// Two [`PrefixTagged`](crate::combinators::PrefixTagged) parsers with the same tag parser but different values are disjoint.
54pub broadcast proof fn lemma_disjoint_prefix_tagged<
55    Tg: SpecByteLen + SpecParser<PVal = Tg::T>,
56    A: SpecParser,
57    B: SpecParser,
58>(prefix1: PrefixTagged<Tg, Tg::T, A>, prefix2: PrefixTagged<Tg, Tg::T, B>)
59    requires
60        prefix1.0 == prefix2.0,
61        prefix1.1 != prefix2.1,
62    ensures
63        #[trigger] disjoint_domains(prefix1, prefix2),
64{
65    reveal(disjoint_domains);
66}
67
68/// Two [`Refined`] parsers with the same inner parser and mutually exclusive predicates are disjoint.
69pub broadcast proof fn lemma_disjoint_refined<
70    Inner: SpecParser,
71    P1: SpecPred<Inner::PVal>,
72    P2: SpecPred<Inner::PVal>,
73>(r1: Refined<Inner, P1>, r2: Refined<Inner, P2>)
74    requires
75        r1.0 == r2.0,
76        forall|v: Inner::PVal| r1.1.apply(v) ==> !r2.1.apply(v),
77    ensures
78        #[trigger] disjoint_domains(r1, r2),
79{
80    reveal(disjoint_domains);
81}
82
83/// Refining the left parser can only narrow its accepted byte domain.
84pub broadcast proof fn lemma_disjoint_refined_left<
85    Inner: SpecParser,
86    Pred: SpecPred<Inner::PVal>,
87    Other: SpecParser,
88>(refined: Refined<Inner, Pred>, other: Other)
89    requires
90        disjoint_domains(refined.0, other),
91    ensures
92        #[trigger] disjoint_domains(refined, other),
93{
94    reveal(disjoint_domains);
95}
96
97/// Refining the right parser can only narrow its accepted byte domain.
98pub broadcast proof fn lemma_disjoint_refined_right<
99    Other: SpecParser,
100    Inner: SpecParser,
101    Pred: SpecPred<Inner::PVal>,
102>(other: Other, refined: Refined<Inner, Pred>)
103    requires
104        disjoint_domains(other, refined.0),
105    ensures
106        #[trigger] disjoint_domains(other, refined),
107{
108    reveal(disjoint_domains);
109}
110
111/// A [`Const`] parser is disjoint from a [`Refined`] parser with the same inner parser if the refined predicate does not hold on the const value.
112pub broadcast proof fn lemma_disjoint_const_refined<Inner: SpecParser, P: SpecPred<Inner::PVal>>(
113    tag: Const<Inner, Inner::PVal>,
114    r: Refined<Inner, P>,
115)
116    requires
117        tag.0 == r.0,
118        !r.1.apply(tag.1),
119    ensures
120        #[trigger] disjoint_domains(tag, r),
121{
122    reveal(disjoint_domains);
123}
124
125/// Two [`Cond`] parsers with mutually exclusive conditions are disjoint.
126pub broadcast proof fn lemma_disjoint_cond<Inner1: SpecParser, Inner2: SpecParser>(
127    c1: Cond<Inner1>,
128    c2: Cond<Inner2>,
129)
130    requires
131        c1.0 && c2.0 ==> false,
132    ensures
133        #[trigger] disjoint_domains(c1, c2),
134{
135    reveal(disjoint_domains);
136}
137
138/// A tuple parser is disjoint from another parser if its first component is.
139pub broadcast proof fn lemma_disjoint_tuple<U: SpecParser, U1: SpecParser, V1: SpecParser>(
140    t: U,
141    t1: Pair<U1, V1>,
142)
143    requires
144        disjoint_domains(t, t1.0),
145    ensures
146        #[trigger] disjoint_domains(t, t1),
147{
148    reveal(disjoint_domains);
149}
150
151/// A tuple parser is disjoint from another parser if its first component is.
152pub broadcast proof fn lemma_disjoint_tuple_left<U1: SpecParser, V1: SpecParser, U: SpecParser>(
153    tuple: Pair<U1, V1>,
154    other: U,
155)
156    requires
157        disjoint_domains(tuple.0, other),
158    ensures
159        #[trigger] disjoint_domains(tuple, other),
160{
161    reveal(disjoint_domains);
162}
163
164/// A dependent tuple is disjoint from another parser if its head parser is.
165pub broadcast proof fn lemma_disjoint_bind<
166    U: SpecParser,
167    Head: SpecParser,
168    Tail: SpecMap<Input = Head::PVal>,
169>(other: U, bind: Bind<Head, Tail>) where Tail::Output: SpecParser
170    requires
171        disjoint_domains(other, bind.0),
172    ensures
173        #[trigger] disjoint_domains(other, bind),
174{
175    reveal(disjoint_domains);
176}
177
178/// A dependent tuple is disjoint from another parser if its head parser is.
179pub broadcast proof fn lemma_disjoint_bind_left<
180    Head: SpecParser,
181    Tail: SpecMap<Input = Head::PVal>,
182    U: SpecParser,
183>(bind: Bind<Head, Tail>, other: U) where Tail::Output: SpecParser
184    requires
185        disjoint_domains(bind.0, other),
186    ensures
187        #[trigger] disjoint_domains(bind, other),
188{
189    reveal(disjoint_domains);
190}
191
192/// An implicit dependent parser is disjoint from another parser if its head parser is.
193pub broadcast proof fn lemma_disjoint_implicit<
194    U: SpecParser,
195    Head: SpecParser,
196    Tail: DepCombinator<Key = Head::PVal>,
197>(other: U, implicit: Implicit<Head, Tail>) where Tail::Body: SpecParser<PVal = Tail::Val>
198    requires
199        disjoint_domains(other, implicit.0),
200    ensures
201        #[trigger] disjoint_domains(other, implicit),
202{
203    reveal(disjoint_domains);
204}
205
206/// An implicit dependent parser is disjoint from another parser if its head parser is.
207pub broadcast proof fn lemma_disjoint_implicit_left<
208    Head: SpecParser,
209    Tail: DepCombinator<Key = Head::PVal>,
210    U: SpecParser,
211>(implicit: Implicit<Head, Tail>, other: U) where Tail::Body: SpecParser<PVal = Tail::Val>
212    requires
213        disjoint_domains(implicit.0, other),
214    ensures
215        #[trigger] disjoint_domains(implicit, other),
216{
217    reveal(disjoint_domains);
218}
219
220/// An [`AndThen`] parser is disjoint from another parser if its byte-source parser is.
221pub broadcast proof fn lemma_disjoint_and_then<
222    U: SpecParser,
223    Head: SpecParser<PVal = Seq<u8>>,
224    Tail: SpecParser,
225>(other: U, and_then: AndThen<Head, Tail>)
226    requires
227        disjoint_domains(other, and_then.0),
228    ensures
229        #[trigger] disjoint_domains(other, and_then),
230{
231    reveal(disjoint_domains);
232}
233
234/// An [`AndThen`] parser is disjoint from another parser if its byte-source parser is.
235pub broadcast proof fn lemma_disjoint_and_then_left<
236    Head: SpecParser<PVal = Seq<u8>>,
237    Tail: SpecParser,
238    U: SpecParser,
239>(and_then: AndThen<Head, Tail>, other: U)
240    requires
241        disjoint_domains(and_then.0, other),
242    ensures
243        #[trigger] disjoint_domains(and_then, other),
244{
245    reveal(disjoint_domains);
246}
247
248/// Two tuples are disjoint if their first parsers consume equal bytes and their second parsers are disjoint.
249pub broadcast proof fn lemma_disjoint_tuple_2<
250    A: SpecParser,
251    B: SpecParser,
252    C: SpecParser,
253    D: SpecParser,
254>(t1: Pair<A, B>, t2: Pair<C, D>)
255    requires
256        forall|input: Seq<u8>| #[trigger]
257            t1.0.spec_parse(input) matches Some((n1, _)) ==> t2.0.spec_parse(input) matches Some(
258                (n2, _),
259            ) ==> n1 == n2,
260        disjoint_domains(t1.1, t2.1),
261    ensures
262        #[trigger] disjoint_domains(t1, t2),
263{
264    reveal(disjoint_domains);
265}
266
267/// A [`Preceded`] parser is disjoint from another parser if its prefix is.
268pub broadcast proof fn lemma_disjoint_preceded<
269    U: SpecParser,
270    U1: SpecParser,
271    V1: SpecParser,
272    const CHECK: bool,
273>(p: U, p1: Preceded<U1, U1::PVal, V1, CHECK>)
274    requires
275        disjoint_domains(p, p1.a),
276    ensures
277        #[trigger] disjoint_domains(p, p1),
278{
279    reveal(disjoint_domains);
280}
281
282/// A [`Preceded`] parser is disjoint from another parser if its prefix is.
283pub broadcast proof fn lemma_disjoint_preceded_left<
284    U1: SpecParser,
285    V1: SpecParser,
286    U: SpecParser,
287    const CHECK: bool,
288>(preceded: Preceded<U1, U1::PVal, V1, CHECK>, other: U)
289    requires
290        disjoint_domains(preceded.a, other),
291    ensures
292        #[trigger] disjoint_domains(preceded, other),
293{
294    reveal(disjoint_domains);
295}
296
297/// A [`Terminated`] parser is disjoint from another parser if its prefix is.
298pub broadcast proof fn lemma_disjoint_terminated<
299    U: SpecParser,
300    U1: SpecParser,
301    V1: SpecParser,
302    const CHECK: bool,
303>(p: U, p1: Terminated<U1, V1, V1::PVal, CHECK>)
304    requires
305        disjoint_domains(p, p1.a),
306    ensures
307        #[trigger] disjoint_domains(p, p1),
308{
309    reveal(disjoint_domains);
310}
311
312/// A [`Terminated`] parser is disjoint from another parser if its content parser is.
313pub broadcast proof fn lemma_disjoint_terminated_left<
314    U1: SpecParser,
315    V1: SpecParser,
316    U: SpecParser,
317    const CHECK: bool,
318>(terminated: Terminated<U1, V1, V1::PVal, CHECK>, other: U)
319    requires
320        disjoint_domains(terminated.a, other),
321    ensures
322        #[trigger] disjoint_domains(terminated, other),
323{
324    reveal(disjoint_domains);
325}
326
327/// A [`Mapped`] parser is disjoint from another parser if its inner parser is.
328pub broadcast proof fn lemma_disjoint_mapped<
329    P: SpecParser,
330    Inner1: SpecParser,
331    M1: SpecMapper<In = Inner1::PVal>,
332>(p: P, m: Mapped<Inner1, M1>)
333    requires
334        disjoint_domains(p, m.inner),
335    ensures
336        #[trigger] disjoint_domains(p, m),
337{
338    reveal(disjoint_domains);
339}
340
341/// A [`Mapped`] parser is disjoint from another parser if its inner parser is.
342pub broadcast proof fn lemma_disjoint_mapped_left<
343    Inner: SpecParser,
344    M: SpecMapper<In = Inner::PVal>,
345    P: SpecParser,
346>(mapped: Mapped<Inner, M>, other: P)
347    requires
348        disjoint_domains(mapped.inner, other),
349    ensures
350        #[trigger] disjoint_domains(mapped, other),
351{
352    reveal(disjoint_domains);
353}
354
355/// A bidirectionally [`Mapped`] parser is disjoint from another parser if its inner parser is.
356pub broadcast proof fn lemma_disjoint_bimap<
357    P: SpecParser,
358    Inner: SpecParser,
359    M: SpecMap<Input = Inner::PVal>,
360    MRev: SpecMap<Input = M::Output, Output = M::Input>,
361>(other: P, mapped: Mapped<Inner, BiMap<M, MRev>>)
362    requires
363        disjoint_domains(other, mapped.inner),
364    ensures
365        #[trigger] disjoint_domains(other, mapped),
366{
367    reveal(disjoint_domains);
368}
369
370/// A bidirectionally [`Mapped`] parser is disjoint from another parser if its inner parser is.
371pub broadcast proof fn lemma_disjoint_bimap_left<
372    Inner: SpecParser,
373    M: SpecMap<Input = Inner::PVal>,
374    MRev: SpecMap<Input = M::Output, Output = M::Input>,
375    P: SpecParser,
376>(mapped: Mapped<Inner, BiMap<M, MRev>>, other: P)
377    requires
378        disjoint_domains(mapped.inner, other),
379    ensures
380        #[trigger] disjoint_domains(mapped, other),
381{
382    reveal(disjoint_domains);
383}
384
385/// A [`Choice`] parser is disjoint from another parser if both branches are.
386///
387/// ## NOTE
388///
389/// The trigger `disjoint_domains(other, choice)` matches `Choice(..., Choice(..., ...))` but not `Choice(Choice(..., ...), ...)`.
390pub broadcast proof fn lemma_disjoint_choice<S1: SpecParser, S2: SpecParser, S3: SpecParser>(
391    choice: Choice<S1, S2>,
392    other: S3,
393)
394    requires
395        disjoint_domains(other, choice.0),
396        disjoint_domains(other, choice.1),
397    ensures
398        #[trigger] disjoint_domains(other, choice),
399{
400    reveal(disjoint_domains);
401}
402
403/// A [`Choice`] parser is disjoint from another parser if both branches are.
404pub broadcast proof fn lemma_disjoint_choice_left<S1: SpecParser, S2: SpecParser, S3: SpecParser>(
405    choice: Choice<S1, S2>,
406    other: S3,
407)
408    requires
409        disjoint_domains(choice.0, other),
410        disjoint_domains(choice.1, other),
411    ensures
412        #[trigger] disjoint_domains(choice, other),
413{
414    reveal(disjoint_domains);
415}
416
417/// Two balanced [`Choice`] trees are disjoint if every cross-branch pair is disjoint.
418///
419/// Unlike composing the two directional decomposition rules, this rule strictly reduces both
420/// visible choice constructors and therefore does not introduce a trigger cycle.
421pub broadcast proof fn lemma_disjoint_choices<
422    A: SpecParser,
423    B: SpecParser,
424    C: SpecParser,
425    D: SpecParser,
426>(left: Choice<A, B>, right: Choice<C, D>)
427    requires
428        disjoint_domains(left.0, right.0),
429        disjoint_domains(left.0, right.1),
430        disjoint_domains(left.1, right.0),
431        disjoint_domains(left.1, right.1),
432    ensures
433        #[trigger] disjoint_domains(left, right),
434{
435    reveal(disjoint_domains);
436}
437
438/// An [`Alt`] parser is disjoint from another parser if both branches are.
439///
440/// ## NOTE
441///
442/// The trigger `disjoint_domains(other, choice)` matches `Alt(..., Alt(..., ...))` but not `Alt(Alt(..., ...), ...)`.
443pub broadcast proof fn lemma_disjoint_alt<
444    S1: SpecParser,
445    S2: SpecParser<PVal = S1::PVal>,
446    S3: SpecParser<PVal = S1::PVal>,
447>(alt: Alt<S1, S2>, other: S3)
448    requires
449        disjoint_domains(other, alt.0),
450        disjoint_domains(other, alt.1),
451    ensures
452        #[trigger] disjoint_domains(other, alt),
453{
454    reveal(disjoint_domains);
455}
456
457/// An [`Alt`] parser is disjoint from another parser if both branches are.
458pub broadcast proof fn lemma_disjoint_alt_left<
459    S1: SpecParser,
460    S2: SpecParser<PVal = S1::PVal>,
461    S3: SpecParser<PVal = S1::PVal>,
462>(alt: Alt<S1, S2>, other: S3)
463    requires
464        disjoint_domains(alt.0, other),
465        disjoint_domains(alt.1, other),
466    ensures
467        #[trigger] disjoint_domains(alt, other),
468{
469    reveal(disjoint_domains);
470}
471
472/// An [`Optional<A, B>`] parser is disjoint from another parser if both `A` and `B` are.
473pub broadcast proof fn lemma_disjoint_optional<P: SpecParser, A: SpecParser, B: SpecParser>(
474    p: P,
475    optional: Optional<A, B>,
476)
477    requires
478        disjoint_domains(p, optional.0),
479        disjoint_domains(p, optional.1),
480    ensures
481        #[trigger] disjoint_domains(p, optional),
482{
483    reveal(disjoint_domains);
484    broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
485
486}
487
488/// An [`Optional<A, B>`] parser is disjoint from another parser if both `A` and `B` are.
489pub broadcast proof fn lemma_disjoint_optional_left<A: SpecParser, B: SpecParser, P: SpecParser>(
490    optional: Optional<A, B>,
491    p: P,
492)
493    requires
494        disjoint_domains(optional.0, p),
495        disjoint_domains(optional.1, p),
496    ensures
497        #[trigger] disjoint_domains(optional, p),
498{
499    reveal(disjoint_domains);
500    broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
501
502}
503
504/// A [`Repeat<A, B>`] parser is disjoint from another parser if both `A` and `B` are.
505pub broadcast proof fn lemma_disjoint_repeat<P: SpecParser, A: SpecParser, B: SpecParser>(
506    p: P,
507    repeat: Repeat<A, B>,
508)
509    requires
510        disjoint_domains(p, repeat.0),
511        disjoint_domains(p, repeat.1),
512    ensures
513        #[trigger] disjoint_domains(p, repeat),
514{
515    reveal(<super::Star::<_> as SpecParser>::spec_parse);
516    reveal(disjoint_domains);
517    broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
518
519}
520
521/// A [`Repeat<A, B>`] parser is disjoint from another parser if both `A` and `B` are.
522pub broadcast proof fn lemma_disjoint_repeat_left<A: SpecParser, B: SpecParser, P: SpecParser>(
523    repeat: Repeat<A, B>,
524    p: P,
525)
526    requires
527        disjoint_domains(repeat.0, p),
528        disjoint_domains(repeat.1, p),
529    ensures
530        #[trigger] disjoint_domains(repeat, p),
531{
532    reveal(<super::Star::<_> as SpecParser>::spec_parse);
533    reveal(disjoint_domains);
534    broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
535
536}
537
538/// A productive parser is disjoint from [`Eof`].
539pub broadcast proof fn lemma_disjoint_eof<P: Productive>(p: P, eof: Eof)
540    requires
541        p.productive_inv(),
542        p.safe_inv(),
543    ensures
544        #[trigger] disjoint_domains(p, eof),
545{
546    reveal(disjoint_domains);
547    assert forall|input: Seq<u8>|
548        #![auto]
549        p.spec_parse(input) is Some && eof.spec_parse(input) is Some implies false by {
550        p.lemma_productive(input);
551        p.lemma_parse_safe(input);
552        if eof.spec_parse(input) is Some {
553            assert(input.len() == 0);
554            assert(input == Seq::<u8>::empty());
555        }
556    }
557}
558
559/// [`Eof`] is disjoint from a productive parser.
560pub broadcast proof fn lemma_disjoint_eof_left<P: Productive>(eof: Eof, p: P)
561    requires
562        p.productive_inv(),
563        p.safe_inv(),
564    ensures
565        #[trigger] disjoint_domains(eof, p),
566{
567    lemma_disjoint_eof(p, eof);
568    lemma_disjoint_symmetric(p, eof);
569}
570
571/// An [`OptionalEnd<A>`] parser is disjoint from another parser if its inner parser is
572/// - productive and safe, and
573/// - disjoint from the other parser.
574pub broadcast proof fn lemma_disjoint_option_end<P: Productive, A: SpecParser>(
575    p: P,
576    opt: OptionalEnd<A>,
577)
578    requires
579        p.productive_inv(),
580        p.safe_inv(),
581        disjoint_domains(p, opt.0),
582    ensures
583        #[trigger] disjoint_domains(p, opt),
584{
585    reveal(disjoint_domains);
586    broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
587
588    assert forall|input: Seq<u8>|
589        #![auto]
590        p.spec_parse(input) is Some && Eof.spec_parse(input) is Some implies false by {
591        p.lemma_productive(input);
592        p.lemma_parse_safe(input);
593    }
594}
595
596/// A [`RepeatTillEnd<A>`] parser is disjoint from another parser if its inner parser is
597/// - productive and safe, and
598/// - disjoint from the other parser.
599pub broadcast proof fn lemma_disjoint_repeat_till_end<P: Productive, A: SpecParser>(
600    p: P,
601    repeat: RepeatTillEnd<A>,
602)
603    requires
604        p.productive_inv(),
605        p.safe_inv(),
606        disjoint_domains(p, repeat.0),
607    ensures
608        #[trigger] disjoint_domains(p, repeat),
609{
610    reveal(disjoint_domains);
611    reveal(<super::Star::<_> as SpecParser>::spec_parse);
612    broadcast use vstd::seq_lib::lemma_seq_skip_nothing;
613
614    assert forall|input: Seq<u8>|
615        #![auto]
616        p.spec_parse(input) is Some && Eof.spec_parse(input) is Some implies false by {
617        p.lemma_productive(input);
618        p.lemma_parse_safe(input);
619    }
620}
621
622/// Borrowing adaptation does not change a parser's accepted byte domain.
623pub broadcast proof fn lemma_disjoint_ref_left<Inner: SpecParser, Other: SpecParser>(
624    borrowed: Ref<Inner>,
625    other: Other,
626)
627    requires
628        disjoint_domains(borrowed.0, other),
629    ensures
630        #[trigger] disjoint_domains(borrowed, other),
631{
632    reveal(disjoint_domains);
633}
634
635/// Borrowing adaptation does not change a parser's accepted byte domain.
636pub broadcast proof fn lemma_disjoint_ref_right<Other: SpecParser, Inner: SpecParser>(
637    other: Other,
638    borrowed: Ref<Inner>,
639)
640    requires
641        disjoint_domains(other, borrowed.0),
642    ensures
643        #[trigger] disjoint_domains(other, borrowed),
644{
645    reveal(disjoint_domains);
646}
647
648/// Naming adaptation does not change a parser's accepted byte domain.
649pub broadcast proof fn lemma_disjoint_named_left<Inner: SpecParser, Other: SpecParser>(
650    named: Named<Inner>,
651    other: Other,
652)
653    requires
654        disjoint_domains(named.1, other),
655    ensures
656        #[trigger] disjoint_domains(named, other),
657{
658    reveal(disjoint_domains);
659}
660
661/// Naming adaptation does not change a parser's accepted byte domain.
662pub broadcast proof fn lemma_disjoint_named_right<Other: SpecParser, Inner: SpecParser>(
663    other: Other,
664    named: Named<Inner>,
665)
666    requires
667        disjoint_domains(other, named.1),
668    ensures
669        #[trigger] disjoint_domains(other, named),
670{
671    reveal(disjoint_domains);
672}
673
674/// Compatibility helper for two borrowing adapters.
675///
676/// This fact is kept directly callable but is not broadcast; the directional `Ref` rules derive
677/// it without adding another competing trigger path.
678pub proof fn lemma_disjoint_refs<Left: SpecParser, Right: SpecParser>(
679    left: Ref<Left>,
680    right: Ref<Right>,
681)
682    requires
683        disjoint_domains(left.0, right.0),
684    ensures
685        #[trigger] disjoint_domains(left, right),
686{
687    reveal(disjoint_domains);
688}
689
690/// Semantic leaf facts that do not recursively decompose parser syntax.
691pub broadcast group disjoint_leaf_lemmas {
692    lemma_disjoint_void_left,
693    lemma_disjoint_void_right,
694    lemma_disjoint_const,
695    lemma_disjoint_prefix_tagged,
696    lemma_disjoint_refined,
697    lemma_disjoint_const_refined,
698    lemma_disjoint_cond,
699}
700
701/// Domain-preserving or domain-narrowing wrappers on the left of `disjoint_domains`.
702pub broadcast group disjoint_left_wrapper_lemmas {
703    lemma_disjoint_refined_left,
704    lemma_disjoint_mapped_left,
705    lemma_disjoint_bimap_left,
706    lemma_disjoint_ref_left,
707    lemma_disjoint_named_left,
708}
709
710/// Domain-preserving or domain-narrowing wrappers on the right of `disjoint_domains`.
711pub broadcast group disjoint_right_wrapper_lemmas {
712    lemma_disjoint_refined_right,
713    lemma_disjoint_mapped,
714    lemma_disjoint_bimap,
715    lemma_disjoint_ref_right,
716    lemma_disjoint_named_right,
717}
718
719/// Syntax-directed decomposition of a right-hand continuation.
720pub broadcast group disjoint_right_continuation_lemmas {
721    lemma_disjoint_tuple,
722    lemma_disjoint_bind,
723    lemma_disjoint_implicit,
724    lemma_disjoint_and_then,
725    lemma_disjoint_preceded,
726    lemma_disjoint_terminated,
727    lemma_disjoint_choice,
728    lemma_disjoint_alt,
729    lemma_disjoint_optional,
730    lemma_disjoint_repeat,
731}
732
733/// Reverse-orientation decomposition, available explicitly when a format is left-associated.
734pub broadcast group disjoint_left_composite_lemmas {
735    lemma_disjoint_tuple_left,
736    lemma_disjoint_bind_left,
737    lemma_disjoint_implicit_left,
738    lemma_disjoint_and_then_left,
739    lemma_disjoint_preceded_left,
740    lemma_disjoint_terminated_left,
741    lemma_disjoint_choice_left,
742    lemma_disjoint_alt_left,
743    lemma_disjoint_optional_left,
744    lemma_disjoint_repeat_left,
745}
746
747/// Boundary rules with productivity/safety side conditions.
748pub broadcast group disjoint_boundary_lemmas {
749    lemma_disjoint_eof,
750    lemma_disjoint_eof_left,
751    lemma_disjoint_option_end,
752    lemma_disjoint_repeat_till_end,
753}
754
755/// Canonical automation for right-associated formats.
756///
757/// Every recursive rule reduces a constructor visible in the trigger. This includes the
758/// right-oriented `OptionalEnd` and `RepeatTillEnd` rules: although they expose productivity and
759/// safety side conditions, they still strictly peel the triggered continuation. Reverse-oriented
760/// rules remain opt-in so that automation cannot oscillate between equivalent orientations.
761pub broadcast group disjointness_lemmas {
762    lemma_disjoint_void_left,
763    lemma_disjoint_void_right,
764    lemma_disjoint_choice,
765    lemma_disjoint_choices,
766    lemma_disjoint_alt,
767    lemma_disjoint_const,
768    lemma_disjoint_prefix_tagged,
769    lemma_disjoint_refined,
770    lemma_disjoint_refined_left,
771    lemma_disjoint_refined_right,
772    lemma_disjoint_const_refined,
773    lemma_disjoint_cond,
774    lemma_disjoint_tuple,
775    lemma_disjoint_bind,
776    lemma_disjoint_implicit,
777    lemma_disjoint_and_then,
778    lemma_disjoint_preceded,
779    lemma_disjoint_terminated,
780    lemma_disjoint_mapped,
781    lemma_disjoint_mapped_left,
782    lemma_disjoint_bimap,
783    lemma_disjoint_bimap_left,
784    lemma_disjoint_optional,
785    lemma_disjoint_repeat,
786    lemma_disjoint_eof,
787    lemma_disjoint_option_end,
788    lemma_disjoint_repeat_till_end,
789    lemma_disjoint_ref_left,
790    lemma_disjoint_ref_right,
791    lemma_disjoint_named_left,
792    lemma_disjoint_named_right,
793}
794
795#[cfg(verus_only)]
796proof fn test_disjoinness() {
797    use crate::combinators::*;
798    use crate::core::proof::*;
799    broadcast use disjointness_lemmas;
800
801    use vstd::pervasive::arbitrary;
802
803    let fmt = Choice(Const(U8, 0), Choice(Const(U8, 1), Choice(Const(U8, 2), Const(U8, 3))));
804    assert(fmt.unambiguous());
805    let fmt2 = Choice(
806        Refined(U8, |b: u8| b == 0),
807        Choice(
808            Refined(U8, |b: u8| b == 1),
809            Choice(Refined(U8, |b: u8| b == 2), Refined(U8, |b: u8| b == 3)),
810        ),
811    );
812    assert(fmt2.unambiguous());
813    let tag: u8 = arbitrary();
814    let fmt3 = Choice(
815        Cond(tag == 0, U8),
816        Choice(Cond(tag == 1, U8), Choice(Cond(tag == 2, U8), Cond(tag == 3, U8))),
817    );
818    assert(fmt3.unambiguous());
819    let fmt4 = Choice(
820        Const(U8, 0),
821        Choice(Const(U8, 1), Choice(Const(U8, 2), Refined(U8, |b: u8| b != 0 && b != 1 && b != 2))),
822    );
823    assert(fmt4.unambiguous());
824    let fmt5 = Optional(
825        PrefixTagged(U8, 10, Fixed::<1>),
826        Repeat(
827            PrefixTagged(U8, 11, Fixed::<2>),
828            Optional(
829                PrefixTagged(U8, 12, Fixed::<3>),
830                RepeatTillEnd(PrefixTagged(U8, 13, Fixed::<4>)),
831            ),
832        ),
833    );
834    assert(fmt5.unambiguous());
835}
836
837#[cfg(verus_only)]
838proof fn test_directional_disjointness_normalization() {
839    broadcast use disjointness_lemmas;
840
841    let first = Const(U8, 1u8);
842    let second = Const(U8, 2u8);
843    let third = Const(U8, 3u8);
844
845    let tuple = Pair(second, U8);
846    assert(disjoint_domains(first, tuple));
847
848    let dependent = Bind(second, |_tag: u8| U8);
849    assert(disjoint_domains(first, dependent));
850
851    let named = Named("second", Ref(Refined(second, |_value: u8| true)));
852    assert(disjoint_domains(first, named));
853
854    let alternatives = Choice(second, third);
855    assert(disjoint_domains(first, alternatives));
856
857    broadcast use disjoint_left_composite_lemmas;
858
859    assert(disjoint_domains(alternatives, first));
860}
861
862} // verus!
vest_lib/combinators/disjoint.rs

vest_lib/combinators/
disjoint.rs
