vest_lib/regular/
sequence.rs

1use crate::properties::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Alias for Verus's spec function type.
7pub type GhostFn<I, O> = spec_fn(I) -> O;
8
9/// Alias for a spec dependent pair combinator.
10pub type SpecPair<Fst, Snd> = Pair<Fst, Snd, GhostFn<<Fst as SpecCombinator>::Type, Snd>>;
11
12impl<Fst, Snd> SpecCombinator for SpecPair<Fst, Snd> where
13    Fst: SecureSpecCombinator,
14    Snd: SpecCombinator,
15 {
16    type Type = (Fst::Type, Snd::Type);
17
18    open spec fn requires(&self) -> bool {
19        &&& Fst::is_prefix_secure()
20        &&& self.fst.requires()
21        &&& forall|i: Fst::Type| #[trigger] (self.snd)(i).requires()
22    }
23
24    open spec fn wf(&self, v: Self::Type) -> bool {
25        &&& self.fst.wf(v.0)
26        &&& (self.snd)(v.0).wf(v.1)
27    }
28
29    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
30        if let Some((n, v1)) = self.fst.spec_parse(s) {
31            let snd = (self.snd)(v1);
32            if let Some((m, v2)) = snd.spec_parse(s.skip(n as int)) {
33                Some((n + m, (v1, v2)))
34            } else {
35                None
36            }
37        } else {
38            None
39        }
40    }
41
42    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
43        let snd = (self.snd)(v.0);
44        let buf1 = self.fst.spec_serialize(v.0);
45        let buf2 = snd.spec_serialize(v.1);
46        buf1 + buf2
47    }
48}
49
50impl<Fst, Snd> SecureSpecCombinator for SpecPair<Fst, Snd> where
51    Fst: SecureSpecCombinator,
52    Snd: SecureSpecCombinator,
53 {
54    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
55        let buf = self.spec_serialize(v);
56        let buf0 = self.fst.spec_serialize(v.0);
57        let buf1 = (self.snd)(v.0).spec_serialize(v.1);
58        self.fst.theorem_serialize_parse_roundtrip(v.0);
59        self.fst.lemma_prefix_secure(buf0, buf1);
60        (self.snd)(v.0).theorem_serialize_parse_roundtrip(v.1);
61        assert((buf0 + buf1).subrange(buf0.len() as int, buf.len() as int) == buf1);
62    }
63
64    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
65        if let Some((nm, (v0, v1))) = self.spec_parse(buf) {
66            let (n, v0_) = self.fst.spec_parse(buf).unwrap();
67            self.fst.lemma_parse_length(buf);
68            let buf0 = buf.take(n);
69            let buf1 = buf.skip(n);
70            assert(buf == buf0 + buf1);
71            self.fst.theorem_parse_serialize_roundtrip(buf);
72            let (m, v1_) = (self.snd)(v0).spec_parse(buf1).unwrap();
73            (self.snd)(v0).theorem_parse_serialize_roundtrip(buf1);
74            (self.snd)(v0).lemma_parse_length(buf1);
75            let buf2 = self.spec_serialize((v0, v1));
76            assert(buf2 == buf.take(nm as int));
77        } else {
78        }
79    }
80
81    open spec fn is_prefix_secure() -> bool {
82        Fst::is_prefix_secure() && Snd::is_prefix_secure()
83    }
84
85    proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>) {
86        if Fst::is_prefix_secure() && Snd::is_prefix_secure() {
87            if let Some((nm, (v0, v1))) = self.spec_parse(buf) {
88                let (n, _) = self.fst.spec_parse(buf).unwrap();
89                self.fst.lemma_parse_length(buf);
90                let buf0 = buf.subrange(0, n as int);
91                let buf1 = buf.subrange(n as int, buf.len() as int);
92                self.fst.lemma_prefix_secure(buf0, buf1);
93                self.fst.lemma_prefix_secure(buf0, buf1.add(s2));
94                self.fst.lemma_prefix_secure(buf, s2);
95                let snd = (self.snd)(v0);
96                let (m, v1_) = snd.spec_parse(buf1).unwrap();
97                assert(buf.add(s2).subrange(0, n as int) == buf0);
98                assert(buf.add(s2).subrange(n as int, buf.add(s2).len() as int) == buf1.add(s2));
99                snd.lemma_prefix_secure(buf1, s2);
100            } else {
101            }
102        } else {
103        }
104    }
105
106    proof fn lemma_parse_length(&self, s: Seq<u8>) {
107        if let Some((n, v1)) = self.fst.spec_parse(s) {
108            let snd = (self.snd)(v1);
109            if let Some((m, v2)) = snd.spec_parse(s.subrange(n as int, s.len() as int)) {
110                self.fst.lemma_parse_length(s);
111                snd.lemma_parse_length(s.subrange(n as int, s.len() as int));
112            }
113        }
114    }
115
116    open spec fn is_productive(&self) -> bool {
117        ||| self.fst.is_productive()
118        ||| forall|v1| #[trigger] ((self.snd)(v1)).is_productive()
119    }
120
121    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
122        if let Some((n, v1)) = self.fst.spec_parse(s) {
123            let snd = (self.snd)(v1);
124            if let Some((m, v2)) = snd.spec_parse(s.skip(n as int)) {
125                self.fst.lemma_parse_productive(s);
126                snd.lemma_parse_productive(s.skip(n as int));
127                self.fst.lemma_parse_length(s);
128                snd.lemma_parse_length(s.skip(n as int));
129            }
130        }
131    }
132}
133
134/// Use this Continuation trait instead of Fn(Input) -> Output
135/// to avoid unsupported Verus features
136pub trait Continuation<Input> {
137    /// Output type of the continuation
138    type Output;
139
140    /// The actual continuation function
141    fn apply(&self, i: Input) -> (o: Self::Output)
142        requires
143            self.requires(i),
144        ensures
145            self.ensures(i, o),
146    ;
147
148    /// The precondition of the continuation
149    spec fn requires(&self, i: Input) -> bool;
150
151    /// The postcondition of the continuation
152    spec fn ensures(&self, i: Input, o: Self::Output) -> bool;
153}
154
155/// Combinator that sequentially applies two combinators, where the second combinator depends on
156/// the first one.
157pub struct Pair<Fst, Snd, Cont> {
158    /// combinators that contain dependencies
159    pub fst: Fst,
160    // _snd: core::marker::PhantomData<Snd>,
161    /// phantom data representing the second combinator
162    /// (it really should be private, but this is a workaround for Verus's
163    /// conservative treatment of opaque types, which doesn't allow field access
164    /// of opaque types in open spec functions)
165    pub _snd: core::marker::PhantomData<Snd>,
166    /// closure that captures dependencies and maps them to the dependent combinators
167    pub snd: Cont,
168}
169
170impl<Fst, Snd, Cont> Pair<Fst, Snd, Cont> where
171    Fst: View,
172    Snd: View,
173    Cont: View<V = GhostFn<<Fst::V as SpecCombinator>::Type, Snd::V>>,
174    Fst::V: SecureSpecCombinator,
175    Snd::V: SpecCombinator,
176 {
177    /// Creates a new `Pair` combinator.
178    pub fn new(fst: Fst, snd: Cont) -> (o: Self)
179        ensures
180            o.fst == fst,
181            o.snd == snd,
182            o@ == Pair::spec_new(fst@, snd@),
183    {
184        Pair { fst, _snd: core::marker::PhantomData, snd }
185    }
186}
187
188impl<Fst, Snd> Pair<Fst, Snd, GhostFn<Fst::Type, Snd>> where
189    Fst: SecureSpecCombinator,
190    Snd: SpecCombinator,
191 {
192    /// Creates a new `Pair` combinator.
193    pub open spec fn spec_new(fst: Fst, snd: GhostFn<Fst::Type, Snd>) -> Self {
194        Pair { fst, _snd: core::marker::PhantomData, snd }
195    }
196}
197
198impl<Fst, Snd, Cont> View for Pair<Fst, Snd, Cont> where
199    Fst: View,
200    Snd: View,
201    Cont: View<V = GhostFn<<Fst::V as SpecCombinator>::Type, Snd::V>>,
202    Fst::V: SecureSpecCombinator,
203    Snd::V: SpecCombinator,
204 {
205    type V = Pair<Fst::V, Snd::V, GhostFn<<Fst::V as SpecCombinator>::Type, Snd::V>>;
206
207    open spec fn view(&self) -> Self::V {
208        Pair::spec_new(self.fst@, self.snd@)
209    }
210}
211
212/// A type that can be either a `PType` or an `SType`, whose `View` is the same as `PType`.
213/// This is used for the continuation in `Pair`.
214#[allow(missing_docs)]
215pub enum POrSType<PType, SType> {
216    /// Represents the (reference of) parsed type
217    P(PType),
218    /// Represents the type to be serialized
219    S(SType),
220}
221
222impl<PType: View, SType: View<V = <PType as View>::V>> View for POrSType<PType, SType> {
223    type V = PType::V;
224
225    open spec fn view(&self) -> Self::V {
226        match self {
227            POrSType::P(p) => p@,
228            POrSType::S(s) => s@,
229        }
230    }
231}
232
233impl<'x, I, O, Fst, Snd, Cont> Combinator<'x, I, O> for Pair<Fst, Snd, Cont> where
234    I: VestInput,
235    O: VestOutput<I>,
236    Fst: Combinator<'x, I, O>,
237    Snd: Combinator<'x, I, O>,
238    Fst::V: SecureSpecCombinator<Type = <Fst::Type as View>::V>,
239    Snd::V: SecureSpecCombinator<Type = <Snd::Type as View>::V>,
240    Fst::SType: Copy,
241    Cont: for <'a>Continuation<POrSType<&'a Fst::Type, Fst::SType>, Output = Snd>,
242    Cont: View<V = GhostFn<<Fst::Type as View>::V, Snd::V>>,
243    <Fst as Combinator<'x, I, O>>::Type: 'x,
244 {
245    type Type = (Fst::Type, Snd::Type);
246
247    type SType = (Fst::SType, Snd::SType);
248
249    fn length(&self, v: Self::SType) -> usize {
250        let snd = self.snd.apply(POrSType::S(v.0));
251        self.fst.length(v.0) + snd.length(v.1)
252    }
253
254    open spec fn ex_requires(&self) -> bool {
255        let spec_snd_dep = self.snd@;
256        &&& self.fst.ex_requires()
257        &&& forall|i| #[trigger] self.snd.requires(i)
258        &&& forall|i, snd| #[trigger]
259            self.snd.ensures(i, snd) ==> snd.ex_requires() && snd@ == spec_snd_dep(i@)
260    }
261
262    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
263        let (n, v1) = self.fst.parse(s.clone())?;
264        proof {
265            self@.fst.lemma_parse_length(s@);
266        }
267        let s_ = s.subrange(n, s.len());
268        let snd = self.snd.apply(POrSType::P(&v1));
269        let (m, v2) = snd.parse(s_)?;
270        proof {
271            snd@.lemma_parse_length(s@.skip(n as int));
272        }
273        Ok((n + m, (v1, v2)))
274    }
275
276    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
277        usize,
278        SerializeError,
279    >) {
280        let snd = self.snd.apply(POrSType::S(v.0));
281        let n = self.fst.serialize(v.0, data, pos)?;
282        let m = snd.serialize(v.1, data, pos + n)?;
283        assert(data@ == seq_splice(old(data)@, pos, self@.spec_serialize(v@)));
284        Ok(n + m)
285    }
286}
287
288impl<Fst: SecureSpecCombinator, Snd: SpecCombinator> SpecCombinator for (Fst, Snd) {
289    type Type = (Fst::Type, Snd::Type);
290
291    open spec fn requires(&self) -> bool {
292        Pair::spec_new(self.0, |r: Fst::Type| self.1).requires()
293    }
294
295    open spec fn wf(&self, v: Self::Type) -> bool {
296        Pair::spec_new(self.0, |r: Fst::Type| self.1).wf(v)
297    }
298
299    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
300        Pair::spec_new(self.0, |r: Fst::Type| self.1).spec_parse(s)
301    }
302
303    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
304        Pair::spec_new(self.0, |r: Fst::Type| self.1).spec_serialize(v)
305    }
306}
307
308impl<Fst: SecureSpecCombinator, Snd: SecureSpecCombinator> SecureSpecCombinator for (Fst, Snd) {
309    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
310        Pair::spec_new(self.0, |r: Fst::Type| self.1).theorem_serialize_parse_roundtrip(v)
311    }
312
313    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
314        Pair::spec_new(self.0, |r: Fst::Type| self.1).theorem_parse_serialize_roundtrip(buf)
315    }
316
317    open spec fn is_prefix_secure() -> bool {
318        Fst::is_prefix_secure() && Snd::is_prefix_secure()
319    }
320
321    proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>) {
322        Pair::spec_new(self.0, |r: Fst::Type| self.1).lemma_prefix_secure(buf, s2)
323    }
324
325    proof fn lemma_parse_length(&self, s: Seq<u8>) {
326        Pair::spec_new(self.0, |r: Fst::Type| self.1).lemma_parse_length(s)
327    }
328
329    open spec fn is_productive(&self) -> bool {
330        Pair::spec_new(self.0, |r: Fst::Type| self.1).is_productive()
331    }
332
333    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
334        Pair::spec_new(self.0, |r: Fst::Type| self.1).lemma_parse_productive(s)
335    }
336}
337
338impl<'x, Fst, Snd, I, O> Combinator<'x, I, O> for (Fst, Snd) where
339    I: VestInput,
340    O: VestOutput<I>,
341    Fst: Combinator<'x, I, O>,
342    Snd: Combinator<'x, I, O>,
343    Fst::V: SecureSpecCombinator<Type = <Fst::Type as View>::V>,
344    Snd::V: SecureSpecCombinator<Type = <Snd::Type as View>::V>,
345 {
346    type Type = (Fst::Type, Snd::Type);
347
348    type SType = (Fst::SType, Snd::SType);
349
350    fn length(&self, v: Self::SType) -> usize {
351        self.0.length(v.0) + self.1.length(v.1)
352    }
353
354    open spec fn ex_requires(&self) -> bool {
355        self.0.ex_requires() && self.1.ex_requires()
356    }
357
358    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
359        let (n, v1) = self.0.parse(s.clone())?;
360        proof {
361            self@.0.lemma_parse_length(s@);
362        }
363        let s_ = s.subrange(n, s.len());
364        let (m, v2) = self.1.parse(s_)?;
365        proof {
366            self.1@.lemma_parse_length(s@.skip(n as int));
367        }
368        Ok((n + m, (v1, v2)))
369    }
370
371    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
372        usize,
373        SerializeError,
374    >) {
375        let n = self.0.serialize(v.0, data, pos)?;
376        let m = self.1.serialize(v.1, data, pos + n)?;
377        assert(data@ == seq_splice(old(data)@, pos, self@.spec_serialize(v@)));
378        Ok(n + m)
379    }
380}
381
382/// Combinator that sequentially applies two combinators and returns the result of the second one.
383pub struct Preceded<Fst, Snd>(pub Fst, pub Snd);
384
385impl<Fst: View, Snd: View> View for Preceded<Fst, Snd> {
386    type V = Preceded<Fst::V, Snd::V>;
387
388    open spec fn view(&self) -> Self::V {
389        Preceded(self.0@, self.1@)
390    }
391}
392
393impl<Fst: SecureSpecCombinator<Type = ()>, Snd: SpecCombinator> SpecCombinator for Preceded<
394    Fst,
395    Snd,
396> {
397    type Type = Snd::Type;
398
399    open spec fn requires(&self) -> bool {
400        (self.0, self.1).requires()
401    }
402
403    open spec fn wf(&self, v: Self::Type) -> bool {
404        (self.0, self.1).wf(((), v))
405    }
406
407    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
408        if let Some((n, ((), v))) = (self.0, self.1).spec_parse(s) {
409            Some((n, v))
410        } else {
411            None
412        }
413    }
414
415    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
416        (self.0, self.1).spec_serialize(((), v))
417    }
418}
419
420impl<
421    Fst: SecureSpecCombinator<Type = ()>,
422    Snd: SecureSpecCombinator,
423> SecureSpecCombinator for Preceded<Fst, Snd> {
424    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
425        (self.0, self.1).theorem_serialize_parse_roundtrip(((), v));
426    }
427
428    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
429        if let Some((n, ((), v))) = (self.0, self.1).spec_parse(buf) {
430            (self.0, self.1).theorem_parse_serialize_roundtrip(buf);
431        }
432    }
433
434    open spec fn is_prefix_secure() -> bool {
435        Fst::is_prefix_secure() && Snd::is_prefix_secure()
436    }
437
438    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
439        if Fst::is_prefix_secure() && Snd::is_prefix_secure() {
440            (self.0, self.1).lemma_prefix_secure(s1, s2);
441        }
442    }
443
444    proof fn lemma_parse_length(&self, s: Seq<u8>) {
445        if let Some((n, ((), v))) = (self.0, self.1).spec_parse(s) {
446            (self.0, self.1).lemma_parse_length(s);
447        }
448    }
449
450    open spec fn is_productive(&self) -> bool {
451        (self.0, self.1).is_productive()
452    }
453
454    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
455        if let Some((n, ((), v))) = (self.0, self.1).spec_parse(s) {
456            (self.0, self.1).lemma_parse_productive(s);
457        }
458    }
459}
460
461impl<'x, I, O, Fst, Snd> Combinator<'x, I, O> for Preceded<Fst, Snd> where
462    I: VestInput,
463    O: VestOutput<I>,
464    Fst: Combinator<'x, I, O, Type = (), SType = ()>,
465    Snd: Combinator<'x, I, O>,
466    Fst::V: SecureSpecCombinator<Type = ()>,
467    Snd::V: SecureSpecCombinator<Type = <Snd::Type as View>::V>,
468 {
469    type Type = Snd::Type;
470
471    type SType = Snd::SType;
472
473    fn length(&self, v: Self::SType) -> usize {
474        (&self.0, &self.1).length(((), v))
475    }
476
477    open spec fn ex_requires(&self) -> bool {
478        (&self.0, &self.1).ex_requires()
479    }
480
481    fn parse(&self, s: I) -> Result<(usize, Self::Type), ParseError> {
482        let (n, ((), v)) = (&self.0, &self.1).parse(s.clone())?;
483        Ok((n, v))
484    }
485
486    fn serialize<'b>(&self, v: Self::SType, data: &'b mut O, pos: usize) -> Result<
487        usize,
488        SerializeError,
489    > {
490        (&self.0, &self.1).serialize(((), v), data, pos)
491    }
492}
493
494/// Combinator that sequentially applies two combinators and returns the result of the first one.
495pub struct Terminated<Fst, Snd>(pub Fst, pub Snd);
496
497impl<Fst: View, Snd: View> View for Terminated<Fst, Snd> {
498    type V = Terminated<Fst::V, Snd::V>;
499
500    open spec fn view(&self) -> Self::V {
501        Terminated(self.0@, self.1@)
502    }
503}
504
505impl<Fst: SecureSpecCombinator, Snd: SpecCombinator<Type = ()>> SpecCombinator for Terminated<
506    Fst,
507    Snd,
508> {
509    type Type = Fst::Type;
510
511    open spec fn requires(&self) -> bool {
512        (self.0, self.1).requires()
513    }
514
515    open spec fn wf(&self, v: Self::Type) -> bool {
516        (self.0, self.1).wf((v, ()))
517    }
518
519    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
520        if let Some((n, (v, ()))) = (self.0, self.1).spec_parse(s) {
521            Some((n, v))
522        } else {
523            None
524        }
525    }
526
527    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
528        (self.0, self.1).spec_serialize((v, ()))
529    }
530}
531
532impl<
533    Fst: SecureSpecCombinator,
534    Snd: SecureSpecCombinator<Type = ()>,
535> SecureSpecCombinator for Terminated<Fst, Snd> {
536    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
537        (self.0, self.1).theorem_serialize_parse_roundtrip((v, ()));
538    }
539
540    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
541        if let Some((n, (v, ()))) = (self.0, self.1).spec_parse(buf) {
542            (self.0, self.1).theorem_parse_serialize_roundtrip(buf);
543        }
544    }
545
546    open spec fn is_prefix_secure() -> bool {
547        Fst::is_prefix_secure() && Snd::is_prefix_secure()
548    }
549
550    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
551        if Fst::is_prefix_secure() && Snd::is_prefix_secure() {
552            (self.0, self.1).lemma_prefix_secure(s1, s2);
553        }
554    }
555
556    proof fn lemma_parse_length(&self, s: Seq<u8>) {
557        if let Some((n, (v, ()))) = (self.0, self.1).spec_parse(s) {
558            (self.0, self.1).lemma_parse_length(s);
559        }
560    }
561
562    open spec fn is_productive(&self) -> bool {
563        (self.0, self.1).is_productive()
564    }
565
566    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
567        if let Some((n, (v, ()))) = (self.0, self.1).spec_parse(s) {
568            (self.0, self.1).lemma_parse_productive(s);
569        }
570    }
571}
572
573impl<'x, I, O, Fst, Snd> Combinator<'x, I, O> for Terminated<Fst, Snd> where
574    I: VestInput,
575    O: VestOutput<I>,
576    Fst: Combinator<'x, I, O>,
577    Snd: Combinator<'x, I, O, Type = (), SType = ()>,
578    Fst::V: SecureSpecCombinator<Type = <Fst::Type as View>::V>,
579    Snd::V: SecureSpecCombinator<Type = ()>,
580 {
581    type Type = Fst::Type;
582
583    type SType = Fst::SType;
584
585    fn length(&self, v: Self::SType) -> usize {
586        (&self.0, &self.1).length((v, ()))
587    }
588
589    open spec fn ex_requires(&self) -> bool {
590        (&self.0, &self.1).ex_requires()
591    }
592
593    fn parse(&self, s: I) -> Result<(usize, Self::Type), ParseError> {
594        let (n, (v, ())) = (&self.0, &self.1).parse(s.clone())?;
595        Ok((n, v))
596    }
597
598    fn serialize<'b>(&self, v: Self::SType, data: &'b mut O, pos: usize) -> Result<
599        usize,
600        SerializeError,
601    > {
602        (&self.0, &self.1).serialize((v, ()), data, pos)
603    }
604}
605
606} // verus!
vest_lib/regular/sequence.rs

vest_lib/regular/
sequence.rs
