vest_lib/regular/
modifier.rs

1#![allow(rustdoc::broken_intra_doc_links)]
2use crate::properties::*;
3use vstd::prelude::*;
4
5use super::bytes::Variable;
6
7verus! {
8
9/// Spec version of [`Iso`].
10pub trait SpecIso {
11    /// The source type of the isomorphism.
12    type Src: SpecFrom<Self::Dst>;
13
14    /// The destination type of the isomorphism.
15    type Dst: SpecFrom<Self::Src>;
16}
17
18/// The bijective functions of [`SpecIso`]
19pub trait SpecIsoFn: SpecIso {
20    /// Applies the isomorphism to the source type.
21    spec fn spec_apply(s: Self::Src) -> Self::Dst;
22
23    /// Applies the reverse isomorphism to the destination type.
24    spec fn spec_rev_apply(s: Self::Dst) -> Self::Src;
25}
26
27// Blanket implementation for all types that implement `SpecIso`
28impl<T: SpecIso> SpecIsoFn for T {
29    open spec fn spec_apply(s: Self::Src) -> Self::Dst {
30        <Self::Dst as SpecFrom<Self::Src>>::spec_from(s)
31    }
32
33    open spec fn spec_rev_apply(s: Self::Dst) -> Self::Src {
34        <Self::Src as SpecFrom<Self::Dst>>::spec_from(s)
35    }
36}
37
38/// The proof of [`SpecIsoFn`]
39pub trait SpecIsoProof: SpecIsoFn {
40    /// One direction of the isomorphism.
41    proof fn spec_iso(s: Self::Src)
42        ensures
43            Self::spec_rev_apply(Self::spec_apply(s)) == s,
44    ;
45
46    /// The other direction of the isomorphism.
47    proof fn spec_iso_rev(s: Self::Dst)
48        ensures
49            Self::spec_apply(Self::spec_rev_apply(s)) == s,
50    ;
51}
52
53/// All isomorphisms to be used in [`Mapped`] combinator must implement this trait.
54pub trait Iso<'x>: View where
55    Self::V: SpecIso<Src = <Self::Src as View>::V, Dst = <Self::Dst as View>::V>,
56    <Self::Src as View>::V: SpecFrom<<Self::Dst as View>::V>,
57    <Self::Dst as View>::V: SpecFrom<<Self::Src as View>::V>,
58    Self::Dst: 'x,
59 {
60    /// The source type of the isomorphism.
61    type Src: View;
62
63    /// The reference of the [`Src`] type.
64    type RefSrc: View<V = <Self::Src as View>::V> + From<&'x Self::Dst>;
65
66    /// The destination type of the isomorphism.
67    type Dst: View + From<Self::Src>;
68}
69
70/// The bijective functions of [`Iso`]
71/// [`Self::apply`] and [`Self::rev_apply`] must be inverses of each other.
72/// See [`SpecIsoFn::spec_iso`] and [`SpecIsoFn::spec_iso_rev`] for more details.
73pub trait IsoFn<'x>: Iso<'x> where
74    Self::V: SpecIso<Src = <Self::Src as View>::V, Dst = <Self::Dst as View>::V>,
75    <Self::Src as View>::V: SpecFrom<<Self::Dst as View>::V>,
76    <Self::Dst as View>::V: SpecFrom<<Self::Src as View>::V>,
77    Self::Dst: 'x,
78 {
79    /// Applies the isomorphism to the source type.
80    fn apply(s: Self::Src) -> (res: Self::Dst)
81        ensures
82            res@ == Self::V::spec_apply(s@),
83    ;
84
85    /// Applies the reverse isomorphism to the destination type.
86    fn rev_apply(s: &'x Self::Dst) -> (res: Self::RefSrc)
87        ensures
88            res@ == Self::V::spec_rev_apply(s@),
89    ;
90}
91
92// Blanket implementation for all types that implement `Iso`
93impl<'x, T: Iso<'x>> IsoFn<'x> for T where
94    T::V: SpecIso<Src = <T::Src as View>::V, Dst = <T::Dst as View>::V>,
95    <T::Src as View>::V: SpecFrom<<T::Dst as View>::V>,
96    <T::Dst as View>::V: SpecFrom<<T::Src as View>::V>,
97    Self::Dst: 'x,
98 {
99    fn apply(s: Self::Src) -> (res: Self::Dst) {
100        Self::Dst::ex_from(s)
101    }
102
103    fn rev_apply(s: &'x Self::Dst) -> (res: Self::RefSrc) {
104        Self::RefSrc::ex_from(s)
105    }
106}
107
108/// Combinator that maps the result of an `inner` combinator with an isomorphism that implements
109/// [`Iso`].
110pub struct Mapped<Inner, M> {
111    /// The inner combinator.
112    pub inner: Inner,
113    /// The isomorphism.
114    pub mapper: M,
115}
116
117impl<Inner: View, M: View> View for Mapped<Inner, M> {
118    type V = Mapped<Inner::V, M::V>;
119
120    open spec fn view(&self) -> Self::V {
121        Mapped { inner: self.inner@, mapper: self.mapper@ }
122    }
123}
124
125impl<Inner, M> SpecCombinator for Mapped<Inner, M> where
126    Inner: SpecCombinator,
127    M: SpecIso<Src = Inner::Type>,
128    Inner::Type: SpecFrom<M::Dst>,
129    M::Dst: SpecFrom<Inner::Type>,
130 {
131    type Type = M::Dst;
132
133    open spec fn requires(&self) -> bool {
134        self.inner.requires()
135    }
136
137    open spec fn wf(&self, v: Self::Type) -> bool {
138        self.inner.wf(M::spec_rev_apply(v))
139    }
140
141    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
142        match self.inner.spec_parse(s) {
143            Some((n, v)) => Some((n, M::spec_apply(v))),
144            None => None,
145        }
146    }
147
148    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
149        self.inner.spec_serialize(M::spec_rev_apply(v))
150    }
151}
152
153impl<Inner, M> SecureSpecCombinator for Mapped<Inner, M> where
154    Inner: SecureSpecCombinator,
155    M: SpecIsoProof<Src = Inner::Type>,
156    Inner::Type: SpecFrom<M::Dst>,
157    M::Dst: SpecFrom<Inner::Type>,
158 {
159    open spec fn is_prefix_secure() -> bool {
160        Inner::is_prefix_secure()
161    }
162
163    open spec fn is_productive(&self) -> bool {
164        self.inner.is_productive()
165    }
166
167    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
168        let buf = self.inner.spec_serialize(M::spec_rev_apply(v));
169        M::spec_iso_rev(v);
170        self.inner.theorem_serialize_parse_roundtrip(M::spec_rev_apply(v))
171    }
172
173    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
174        self.inner.lemma_parse_length(buf);
175        self.inner.theorem_parse_serialize_roundtrip(buf);
176        if let Some((n, v)) = self.inner.spec_parse(buf) {
177            M::spec_iso(v)
178        }
179    }
180
181    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
182        self.inner.lemma_prefix_secure(s1, s2);
183        if let Some((n, v)) = self.inner.spec_parse(s1) {
184            self.inner.lemma_parse_length(s1);
185            M::spec_iso(v)
186        }
187    }
188
189    proof fn lemma_parse_length(&self, s: Seq<u8>) {
190        self.inner.lemma_parse_length(s);
191        if let Some((n, v)) = self.inner.spec_parse(s) {
192            M::spec_iso(v);
193        }
194    }
195
196    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
197        self.inner.lemma_parse_productive(s);
198        if let Some((n, v)) = self.inner.spec_parse(s) {
199            M::spec_iso(v);
200        }
201    }
202}
203
204impl<'x, I, O, Inner, M> Combinator<'x, I, O> for Mapped<Inner, M> where
205    I: VestInput,
206    O: VestOutput<I>,
207    Inner: Combinator<'x, I, O>,
208    Inner::V: SecureSpecCombinator<Type = <Inner::Type as View>::V>,
209    M: Iso<'x, Src = Inner::Type, RefSrc = Inner::SType>,
210    M::Dst: From<Inner::Type> + View,
211    Inner::SType: From<&'x M::Dst> + View,
212    M::V: SpecIsoProof<Src = <Inner::Type as View>::V, Dst = <M::Dst as View>::V>,
213    <Inner::Type as View>::V: SpecFrom<<M::Dst as View>::V>,
214    <M::Dst as View>::V: SpecFrom<<Inner::Type as View>::V>,
215 {
216    type Type = M::Dst;
217
218    type SType = &'x M::Dst;
219
220    fn length(&self, v: Self::SType) -> usize {
221        self.inner.length(M::rev_apply(v))
222    }
223
224    open spec fn ex_requires(&self) -> bool {
225        self.inner.ex_requires()
226    }
227
228    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
229        match self.inner.parse(s) {
230            Err(e) => Err(e),
231            Ok((n, v)) => {
232                proof {
233                    M::V::spec_iso(v@);
234                }
235                Ok((n, M::apply(v)))
236            },
237        }
238    }
239
240    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
241        usize,
242        SerializeError,
243    >) {
244        self.inner.serialize(M::rev_apply(v), data, pos)
245    }
246}
247
248/// Spec version of [`PartialIso`].
249pub trait SpecPartialIso {
250    /// The source type
251    type Src: SpecTryFrom<Self::Dst>;
252
253    /// The destination type
254    type Dst: SpecTryFrom<Self::Src>;
255}
256
257/// The fallible functions of [`SpecPartialIso`]
258pub trait SpecPartialIsoFn: SpecPartialIso {
259    /// Applies the fallible conversion to the source type.
260    spec fn spec_apply(s: Self::Src) -> Result<
261        Self::Dst,
262        <Self::Dst as SpecTryFrom<Self::Src>>::Error,
263    >;
264
265    /// Applies the reverse fallible conversion to the destination type.
266    spec fn spec_rev_apply(s: Self::Dst) -> Result<
267        Self::Src,
268        <Self::Src as SpecTryFrom<Self::Dst>>::Error,
269    >;
270}
271
272// Blanket implementation for all types that implement `SpecPartialIso`
273impl<T: SpecPartialIso> SpecPartialIsoFn for T {
274    open spec fn spec_apply(s: Self::Src) -> Result<
275        Self::Dst,
276        <Self::Dst as SpecTryFrom<Self::Src>>::Error,
277    > {
278        Self::Dst::spec_try_from(s)
279    }
280
281    open spec fn spec_rev_apply(s: Self::Dst) -> Result<
282        Self::Src,
283        <Self::Src as SpecTryFrom<Self::Dst>>::Error,
284    > {
285        Self::Src::spec_try_from(s)
286    }
287}
288
289/// The proof of [`SpecPartialIsoFn`]
290pub trait SpecPartialIsoProof: SpecPartialIsoFn {
291    /// One direction of the isomorphism when the conversion is successful.
292    proof fn spec_iso(s: Self::Src)
293        ensures
294            Self::spec_apply(s) matches Ok(d) ==> Self::spec_rev_apply(d) == Ok::<
295                _,
296                <Self::Src as SpecTryFrom<Self::Dst>>::Error,
297            >(s),
298    ;
299
300    /// The other direction of the isomorphism when the conversion is successful.
301    proof fn spec_iso_rev(d: Self::Dst)
302        ensures
303            Self::spec_rev_apply(d) matches Ok(s) ==> Self::spec_apply(s) == Ok::<
304                _,
305                <Self::Dst as SpecTryFrom<Self::Src>>::Error,
306            >(d),
307    ;
308}
309
310/// Fallible version of [`Iso`].
311pub trait PartialIso<'x>: View where
312    Self::V: SpecPartialIso<Src = <Self::Src as View>::V, Dst = <Self::Dst as View>::V>,
313    <Self::Src as View>::V: SpecTryFrom<<Self::Dst as View>::V>,
314    <Self::Dst as View>::V: SpecTryFrom<<Self::Src as View>::V>,
315    Self::Dst: 'x,
316 {
317    /// The source type
318    type Src: View;
319
320    /// The reference of the [`Src`] type.
321    type RefSrc: View<V = <Self::Src as View>::V> + TryFrom<&'x Self::Dst>;
322
323    /// The destination type
324    type Dst: View + TryFrom<Self::Src>;
325}
326
327/// The fallible functions of [`PartialIso`]
328pub trait PartialIsoFn<'x>: PartialIso<'x> where
329    Self::V: SpecPartialIso<Src = <Self::Src as View>::V, Dst = <Self::Dst as View>::V>,
330    <Self::Src as View>::V: SpecTryFrom<<Self::Dst as View>::V>,
331    <Self::Dst as View>::V: SpecTryFrom<<Self::Src as View>::V>,
332    Self::Dst: 'x,
333 {
334    /// Applies the fallible conversion to the source type.
335    fn apply(s: Self::Src) -> (res: Result<Self::Dst, <Self::Dst as TryFrom<Self::Src>>::Error>)
336        ensures
337            res matches Ok(v) ==> {
338                &&& Self::V::spec_apply(s@) is Ok
339                &&& Self::V::spec_apply(s@) matches Ok(v_) && v@ == v_
340            },
341            res matches Err(e) ==> Self::V::spec_apply(s@) is Err,
342    ;
343
344    /// Applies the reverse fallible conversion to the destination type.
345    fn rev_apply(s: &'x Self::Dst) -> (res: Result<
346        Self::RefSrc,
347        <Self::RefSrc as TryFrom<&'x Self::Dst>>::Error,
348    >)
349        ensures
350            res matches Ok(v) ==> {
351                &&& Self::V::spec_rev_apply(s@) is Ok
352                &&& Self::V::spec_rev_apply(s@) matches Ok(v_) && v@ == v_
353            },
354            res matches Err(e) ==> Self::V::spec_rev_apply(s@) is Err,
355    ;
356}
357
358// Blanket implementation for all types that implement `PartialIso`
359impl<'x, T: PartialIso<'x>> PartialIsoFn<'x> for T where
360    T::V: SpecPartialIso<Src = <T::Src as View>::V, Dst = <T::Dst as View>::V>,
361    <T::Src as View>::V: SpecTryFrom<<T::Dst as View>::V>,
362    <T::Dst as View>::V: SpecTryFrom<<T::Src as View>::V>,
363    Self::Dst: 'x,
364 {
365    fn apply(s: Self::Src) -> (res: Result<Self::Dst, <Self::Dst as TryFrom<Self::Src>>::Error>) {
366        Self::Dst::ex_try_from(s)
367    }
368
369    fn rev_apply(s: &'x Self::Dst) -> (res: Result<
370        Self::RefSrc,
371        <Self::RefSrc as TryFrom<&'x Self::Dst>>::Error,
372    >) {
373        Self::RefSrc::ex_try_from(s)
374    }
375}
376
377/// Combinator that maps the result of an `inner` combinator with a fallible conversion
378/// that implements [`TryFromInto`].
379pub struct TryMap<Inner, M> {
380    /// The inner combinator.
381    pub inner: Inner,
382    /// The fallible conversion.
383    pub mapper: M,
384}
385
386impl<Inner: View, M: View> View for TryMap<Inner, M> {
387    type V = TryMap<Inner::V, M::V>;
388
389    open spec fn view(&self) -> Self::V {
390        TryMap { inner: self.inner@, mapper: self.mapper@ }
391    }
392}
393
394impl<Inner, M> SpecCombinator for TryMap<Inner, M> where
395    Inner: SpecCombinator,
396    M: SpecPartialIso<Src = Inner::Type>,
397    Inner::Type: SpecTryFrom<M::Dst>,
398    M::Dst: SpecTryFrom<Inner::Type>,
399 {
400    type Type = M::Dst;
401
402    open spec fn requires(&self) -> bool {
403        self.inner.requires()
404    }
405
406    open spec fn wf(&self, v: Self::Type) -> bool {
407        match M::spec_rev_apply(v) {
408            Ok(v) => self.inner.wf(v),
409            Err(_) => false,
410        }
411    }
412
413    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
414        match self.inner.spec_parse(s) {
415            Some((n, v)) => match M::spec_apply(v) {
416                Ok(v) => Some((n, v)),
417                Err(_) => None,
418            },
419            None => None,
420        }
421    }
422
423    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
424        match M::spec_rev_apply(v) {
425            Ok(v) => self.inner.spec_serialize(v),
426            Err(_) => Seq::empty(),  // won't happen when `self.wf(v)`
427        }
428    }
429}
430
431impl<Inner, M> SecureSpecCombinator for TryMap<Inner, M> where
432    Inner: SecureSpecCombinator,
433    M: SpecPartialIsoProof<Src = Inner::Type>,
434    Inner::Type: SpecTryFrom<M::Dst>,
435    M::Dst: SpecTryFrom<Inner::Type>,
436 {
437    open spec fn is_prefix_secure() -> bool {
438        Inner::is_prefix_secure()
439    }
440
441    open spec fn is_productive(&self) -> bool {
442        self.inner.is_productive()
443    }
444
445    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
446        if let Ok(v_) = M::spec_rev_apply(v) {
447            M::spec_iso_rev(v);
448            self.inner.theorem_serialize_parse_roundtrip(v_);
449        }
450    }
451
452    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
453        self.inner.lemma_parse_length(buf);
454        self.inner.theorem_parse_serialize_roundtrip(buf);
455        if let Some((n, v)) = self.inner.spec_parse(buf) {
456            M::spec_iso(v)
457        }
458    }
459
460    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
461        self.inner.lemma_prefix_secure(s1, s2);
462        if let Some((n, v)) = self.inner.spec_parse(s1) {
463            self.inner.lemma_parse_length(s1);
464            M::spec_iso(v)
465        }
466    }
467
468    proof fn lemma_parse_length(&self, s: Seq<u8>) {
469        self.inner.lemma_parse_length(s);
470        if let Some((n, v)) = self.inner.spec_parse(s) {
471            M::spec_iso(v);
472        }
473    }
474
475    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
476        self.inner.lemma_parse_productive(s);
477        if let Some((n, v)) = self.inner.spec_parse(s) {
478            M::spec_iso(v);
479        }
480    }
481}
482
483impl<'x, I, O, Inner, M> Combinator<'x, I, O> for TryMap<Inner, M> where
484    I: VestInput,
485    O: VestOutput<I>,
486    Inner: Combinator<'x, I, O>,
487    Inner::V: SecureSpecCombinator<Type = <Inner::Type as View>::V>,
488    M: PartialIso<'x, Src = Inner::Type, RefSrc = Inner::SType>,
489    M::Dst: TryFrom<Inner::Type> + View,
490    Inner::SType: TryFrom<&'x M::Dst> + View,
491    M::V: SpecPartialIsoProof<Src = <Inner::Type as View>::V, Dst = <M::Dst as View>::V>,
492    <Inner::Type as View>::V: SpecTryFrom<<M::Dst as View>::V>,
493    <M::Dst as View>::V: SpecTryFrom<<Inner::Type as View>::V>,
494    <Inner::SType as TryFrom<&'x M::Dst>>::Error: core::fmt::Debug,
495 {
496    type Type = M::Dst;
497
498    type SType = &'x M::Dst;
499
500    fn length(&self, v: Self::SType) -> usize {
501        self.inner.length(M::rev_apply(v).unwrap())
502    }
503
504    open spec fn ex_requires(&self) -> bool {
505        self.inner.ex_requires()
506    }
507
508    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
509        match self.inner.parse(s) {
510            Err(e) => Err(e),
511            Ok((n, v)) => match M::apply(v) {
512                Ok(v) => Ok((n, v)),
513                Err(_) => Err(ParseError::TryMapFailed),
514            },
515        }
516    }
517
518    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
519        usize,
520        SerializeError,
521    >) {
522        // we know `v` is well-formed, so we can unwrap it
523        self.inner.serialize(M::rev_apply(v).unwrap(), data, pos)
524    }
525}
526
527/// The spec version of [`Pred`].
528pub trait SpecPred<Input> {
529    // /// The input type of the predicate.
530    // type Input;
531    /// Applies the predicate to the input.
532    spec fn spec_apply(&self, i: &Input) -> bool;
533}
534
535/// All predicates to be used in [`Refined`] combinator must implement this trait.
536pub trait Pred<Input: View + ?Sized>: View where Self::V: SpecPred<<Input as View>::V> {
537    // /// The input type of the predicate.
538    // type Input: View + ?Sized;
539    /// Applies the predicate to the input.
540    fn apply(&self, i: &Input) -> (res: bool)
541        ensures
542            res == self@.spec_apply(&i@),
543    ;
544}
545
546/// Combinator that refines the result of an `inner` combinator with a predicate that implements
547/// [`Pred`].
548pub struct Refined<Inner, P> {
549    /// The inner combinator.
550    pub inner: Inner,
551    /// The predicate.
552    pub predicate: P,
553}
554
555impl<Inner: View, P: View> View for Refined<Inner, P> where  {
556    type V = Refined<Inner::V, P::V>;
557
558    open spec fn view(&self) -> Self::V {
559        Refined { inner: self.inner@, predicate: self.predicate@ }
560    }
561}
562
563impl<Inner, P> SpecCombinator for Refined<Inner, P> where
564    Inner: SpecCombinator,
565    P: SpecPred<Inner::Type>,
566 {
567    type Type = Inner::Type;
568
569    open spec fn requires(&self) -> bool {
570        self.inner.requires()
571    }
572
573    open spec fn wf(&self, v: Self::Type) -> bool {
574        self.inner.wf(v) && self.predicate.spec_apply(&v)
575    }
576
577    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
578        match self.inner.spec_parse(s) {
579            Some((n, v)) if self.predicate.spec_apply(&v) => Some((n, v)),
580            _ => None,
581        }
582    }
583
584    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
585        self.inner.spec_serialize(v)
586    }
587}
588
589impl<Inner, P> SecureSpecCombinator for Refined<Inner, P> where
590    Inner: SecureSpecCombinator,
591    P: SpecPred<Inner::Type>,
592 {
593    open spec fn is_prefix_secure() -> bool {
594        Inner::is_prefix_secure()
595    }
596
597    open spec fn is_productive(&self) -> bool {
598        self.inner.is_productive()
599    }
600
601    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
602        self.inner.theorem_serialize_parse_roundtrip(v);
603    }
604
605    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
606        self.inner.theorem_parse_serialize_roundtrip(buf);
607    }
608
609    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
610        self.inner.lemma_prefix_secure(s1, s2);
611        assert(Self::is_prefix_secure() ==> self.spec_parse(s1) is Some ==> self.spec_parse(
612            s1.add(s2),
613        ) == self.spec_parse(s1));
614    }
615
616    proof fn lemma_parse_length(&self, s: Seq<u8>) {
617        self.inner.lemma_parse_length(s);
618    }
619
620    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
621        self.inner.lemma_parse_productive(s);
622    }
623}
624
625impl<'x, I, O, Inner, P> Combinator<'x, I, O> for Refined<Inner, P> where
626    I: VestInput,
627    O: VestOutput<I>,
628    Inner: Combinator<'x, I, O, SType = &'x <Inner as Combinator<'x, I, O>>::Type>,
629    Inner::V: SecureSpecCombinator<Type = <Inner::Type as View>::V>,
630    P: Pred<Inner::Type>,
631    P::V: SpecPred<<Inner::Type as View>::V>,
632    Inner::Type: 'x,
633 {
634    type Type = Inner::Type;
635
636    type SType = Inner::SType;
637
638    fn length(&self, v: Self::SType) -> usize {
639        self.inner.length(v)
640    }
641
642    open spec fn ex_requires(&self) -> bool {
643        self.inner.ex_requires()
644    }
645
646    fn parse(&self, s: I) -> Result<(usize, Self::Type), ParseError> {
647        match self.inner.parse(s) {
648            Ok((n, v)) => if self.predicate.apply(&v) {
649                Ok((n, v))
650            } else {
651                Err(ParseError::RefinedPredicateFailed)
652            },
653            Err(e) => Err(e),
654        }
655    }
656
657    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> Result<usize, SerializeError> {
658        // we know `v` is well-formed, so we can skip the predicate check
659        self.inner.serialize(v, data, pos)
660    }
661}
662
663/// Combinator that checks if `cond` is true and then delegates to the `inner` combinator.
664pub struct Cond<Inner> {
665    /// The condition to check before parsing or serializing.
666    pub cond: bool,
667    /// The combinator to delegate to if `cond` is true.
668    pub inner: Inner,
669}
670
671impl<Inner: View> View for Cond<Inner> {
672    type V = Cond<Inner::V>;
673
674    open spec fn view(&self) -> Self::V {
675        Cond { cond: self.cond, inner: self.inner@ }
676    }
677}
678
679impl<Inner: SpecCombinator> SpecCombinator for Cond<Inner> {
680    type Type = Inner::Type;
681
682    open spec fn requires(&self) -> bool {
683        self.inner.requires()
684    }
685
686    open spec fn wf(&self, v: Self::Type) -> bool {
687        &&& self.inner.wf(v)
688        // call `serializer` only if `cond` is true
689        &&& self.cond
690    }
691
692    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
693        if self.cond {
694            self.inner.spec_parse(s)
695        } else {
696            None
697        }
698    }
699
700    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
701        self.inner.spec_serialize(v)
702    }
703}
704
705impl<Inner: SecureSpecCombinator> SecureSpecCombinator for Cond<Inner> {
706    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
707        self.inner.theorem_serialize_parse_roundtrip(v);
708    }
709
710    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
711        if self.cond {
712            self.inner.theorem_parse_serialize_roundtrip(buf);
713        }
714    }
715
716    open spec fn is_prefix_secure() -> bool {
717        Inner::is_prefix_secure()
718    }
719
720    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
721        if self.cond {
722            self.inner.lemma_prefix_secure(s1, s2);
723        }
724    }
725
726    proof fn lemma_parse_length(&self, s: Seq<u8>) {
727        if self.cond {
728            self.inner.lemma_parse_length(s);
729        }
730    }
731
732    open spec fn is_productive(&self) -> bool {
733        self.inner.is_productive()
734    }
735
736    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
737        self.inner.lemma_parse_productive(s);
738    }
739}
740
741impl<'x, I: VestInput, O: VestOutput<I>, Inner: Combinator<'x, I, O>> Combinator<'x, I, O> for Cond<
742    Inner,
743> where Inner::V: SecureSpecCombinator<Type = <Inner::Type as View>::V> {
744    type Type = Inner::Type;
745
746    type SType = Inner::SType;
747
748    fn length(&self, v: Self::SType) -> usize {
749        self.inner.length(v)
750    }
751
752    open spec fn ex_requires(&self) -> bool {
753        self.inner.ex_requires()
754    }
755
756    fn parse(&self, s: I) -> Result<(usize, Self::Type), ParseError> {
757        if self.cond {
758            self.inner.parse(s)
759        } else {
760            Err(ParseError::CondFailed)
761        }
762    }
763
764    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> Result<usize, SerializeError> {
765        // we know `self.cond` must be true when `serialize` is called
766        // so we can skip the check
767        self.inner.serialize(v, data, pos)
768    }
769}
770
771/// Combinator that monadically chains two combinators.
772pub struct AndThen<Prev, Next>(pub Prev, pub Next);
773
774impl<Prev: View, Next: View> View for AndThen<Prev, Next> {
775    type V = AndThen<Prev::V, Next::V>;
776
777    open spec fn view(&self) -> Self::V {
778        AndThen(self.0@, self.1@)
779    }
780}
781
782impl<Next: SpecCombinator> SpecCombinator for AndThen<Variable, Next> {
783    type Type = Next::Type;
784
785    open spec fn requires(&self) -> bool {
786        self.0.requires() && self.1.requires()
787    }
788
789    open spec fn wf(&self, v: Self::Type) -> bool {
790        self.1.wf(v) && self.0.wf(self.1.spec_serialize(v))
791    }
792
793    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
794        if let Some((n, v1)) = self.0.spec_parse(s) {
795            if let Some((m, v2)) = self.1.spec_parse(v1) {
796                // !! for security, can only proceed if the `Next` parser consumed the entire
797                // !! output from the `Prev` parser
798                if m == n {
799                    Some((n, v2))
800                } else {
801                    None
802                }
803            } else {
804                None
805            }
806        } else {
807            None
808        }
809    }
810
811    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
812        let buf1 = self.1.spec_serialize(v);
813        self.0.spec_serialize(buf1)
814    }
815}
816
817impl<Next: SecureSpecCombinator> SecureSpecCombinator for AndThen<Variable, Next> {
818    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
819        let buf1 = self.1.spec_serialize(v);
820        self.1.theorem_serialize_parse_roundtrip(v);
821        self.0.theorem_serialize_parse_roundtrip(buf1);
822    }
823
824    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
825        if let Some((n, v1)) = self.0.spec_parse(buf) {
826            if let Some((m, v2)) = self.1.spec_parse(v1) {
827                self.0.theorem_parse_serialize_roundtrip(buf);
828                self.1.theorem_parse_serialize_roundtrip(v1);
829                if m == n {
830                    let buf2 = self.1.spec_serialize(v2);
831                    let buf1 = self.0.spec_serialize(buf2);
832                    assert(buf1 == buf.subrange(0, n as int));
833                }
834            }
835        }
836    }
837
838    open spec fn is_prefix_secure() -> bool {
839        Variable::is_prefix_secure()
840    }
841
842    proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>) {
843        self.0.lemma_prefix_secure(buf, s2);
844    }
845
846    proof fn lemma_parse_length(&self, s: Seq<u8>) {
847        if let Some((n, v1)) = self.0.spec_parse(s) {
848            self.0.lemma_parse_length(s);
849            self.1.lemma_parse_length(v1);
850        }
851    }
852
853    open spec fn is_productive(&self) -> bool {
854        self.0.is_productive()
855    }
856
857    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
858    }
859}
860
861impl<'x, I, O, Next: Combinator<'x, I, O>> Combinator<'x, I, O> for AndThen<Variable, Next> where
862    I: VestInput,
863    O: VestOutput<I>,
864    Next::V: SecureSpecCombinator<Type = <Next::Type as View>::V>,
865 {
866    type Type = Next::Type;
867
868    type SType = Next::SType;
869
870    fn length(&self, _v: Self::SType) -> usize {
871        self.0.0
872    }
873
874    open spec fn ex_requires(&self) -> bool {
875        self.1.ex_requires()
876    }
877
878    fn parse(&self, s: I) -> Result<(usize, Self::Type), ParseError> {
879        let (n, v1) = <_ as Combinator<I, O>>::parse(&self.0, s)?;
880        let (m, v2) = self.1.parse(v1)?;
881        if m == n {
882            Ok((n, v2))
883        } else {
884            Err(ParseError::AndThenUnusedBytes)
885        }
886    }
887
888    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> Result<usize, SerializeError> {
889        // we can skip the call to `self.0.serialize` because we know that it
890        // will be an "no-op"
891        let n = self.1.serialize(v, data, pos)?;
892        Ok(n)
893    }
894}
895
896} // verus!
vest_lib/regular/modifier.rs

vest_lib/regular/
modifier.rs
