vest/regular/
tag.rs

1use super::refined::{Pred, Refined, SpecPred};
2use super::uints::FromToBytes;
3use crate::properties::*;
4use vstd::prelude::*;
5
6verus! {
7
8/// tag predicate that matches the input with a given value
9pub struct TagPred<T>(pub T);
10
11impl<T: View> View for TagPred<T> {
12    type V = TagPred<T::V>;
13
14    open spec fn view(&self) -> Self::V {
15        TagPred(self.0@)
16    }
17}
18
19impl<T> SpecPred for TagPred<T> {
20    type Input = T;
21
22    open spec fn spec_apply(&self, i: &Self::Input) -> bool {
23        *i == self.0
24    }
25}
26
27impl<T: FromToBytes> Pred for TagPred<T> {
28    type Input<'a> = T;
29
30    type InputOwned = T;
31
32    fn apply(&self, i: &Self::Input<'_>) -> bool {
33        self.0.eq(i)
34    }
35}
36
37impl<const N: usize> Pred for TagPred<[u8; N]> {
38    type Input<'b> = &'b [u8];
39
40    type InputOwned = Vec<u8>;
41
42    fn apply(&self, i: &Self::Input<'_>) -> bool {
43        compare_slice(self.0.as_slice(), *i)
44    }
45}
46
47impl<'a> Pred for TagPred<&'a [u8]> {
48    type Input<'b> = &'b [u8];
49
50    type InputOwned = Vec<u8>;
51
52    fn apply(&self, i: &Self::Input<'_>) -> bool {
53        compare_slice(self.0, *i)
54    }
55}
56
57/// Generic tag combinator that matches the input with a given value and discards it
58/// e.g. `Tag(Int::<u8>, 0)` matches the byte `0`; `Tag(Bytes::<3>, &[1, 2, 3])` matches the
59/// bytes `[1, 2, 3]`
60pub struct Tag<Inner, T>(pub Refined<Inner, TagPred<T>>);
61
62impl<Inner, T> Tag<Inner, T> {
63    /// Creates a new `Tag` combinator.
64    pub fn new(inner: Inner, tag: T) -> (o: Self)
65        ensures
66            o == Tag(Refined { inner, predicate: TagPred(tag) }),
67    {
68        Tag(Refined { inner, predicate: TagPred(tag) })
69    }
70
71    /// Creates a new `Tag` combinator.
72    pub open spec fn spec_new(inner: Inner, tag: T) -> Self {
73        Tag(Refined { inner, predicate: TagPred(tag) })
74    }
75}
76
77impl<Inner: View, T: View> View for Tag<Inner, T> {
78    type V = Tag<Inner::V, T::V>;
79
80    open spec fn view(&self) -> Self::V {
81        Tag(self.0@)
82    }
83}
84
85impl<Inner: SpecCombinator<SpecResult = T>, T> SpecCombinator for Tag<Inner, T> {
86    type SpecResult = ();
87
88    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
89        if let Ok((n, _)) = self.0.spec_parse(s) {
90            Ok((n, ()))
91        } else {
92            Err(())
93        }
94    }
95
96    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
97        self.0.spec_serialize(self.0.predicate.0)
98    }
99
100    proof fn spec_parse_wf(&self, s: Seq<u8>) {
101        self.0.spec_parse_wf(s);
102    }
103}
104
105impl<Inner: SecureSpecCombinator<SpecResult = T>, T> SecureSpecCombinator for Tag<Inner, T> {
106    open spec fn is_prefix_secure() -> bool {
107        Inner::is_prefix_secure()
108    }
109
110    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
111        self.0.theorem_serialize_parse_roundtrip(self.0.predicate.0);
112    }
113
114    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
115        self.0.theorem_parse_serialize_roundtrip(buf);
116    }
117
118    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
119        self.0.lemma_prefix_secure(s1, s2);
120        assert(Self::is_prefix_secure() ==> self.spec_parse(s1).is_ok() ==> self.spec_parse(
121            s1.add(s2),
122        ) == self.spec_parse(s1));
123    }
124}
125
126impl<Inner, T> Combinator for Tag<Inner, T> where
127    Inner: for <'a>Combinator<Result<'a> = T, Owned = T>,
128    Inner::V: SecureSpecCombinator<SpecResult = T::V>, T: FromToBytes
129 {
130    type Result<'a> = ();
131
132    type Owned = ();
133
134    open spec fn spec_length(&self) -> Option<usize> {
135        self.0.spec_length()
136    }
137
138    fn length(&self) -> Option<usize> {
139        self.0.length()
140    }
141
142    open spec fn parse_requires(&self) -> bool {
143        self.0.parse_requires()
144    }
145
146    fn parse<'a>(&self, s: &'a [u8]) -> Result<(usize, Self::Result<'a>), ParseError> {
147        let (n, _) = self.0.parse(s)?;
148        Ok((n, ()))
149    }
150
151    open spec fn serialize_requires(&self) -> bool {
152        self.0.serialize_requires()
153    }
154
155    fn serialize(&self, _v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> Result<
156        usize,
157        SerializeError,
158    > {
159        self.0.serialize(self.0.predicate.0, data, pos)
160    }
161}
162
163impl<Inner, const N: usize> Combinator for Tag<Inner, [u8; N]> where
164    Inner: for <'b>Combinator<Result<'b> = &'b [u8], Owned = Vec<u8>>,
165    Inner::V: SecureSpecCombinator<SpecResult = Seq<u8>>
166 {
167    type Result<'b> = ();
168
169    type Owned = ();
170
171    open spec fn spec_length(&self) -> Option<usize> {
172        self.0.spec_length()
173    }
174
175    fn length(&self) -> Option<usize> {
176        self.0.length()
177    }
178
179    open spec fn parse_requires(&self) -> bool {
180        self.0.parse_requires()
181    }
182
183    fn parse<'b>(&self, s: &'b [u8]) -> Result<(usize, Self::Result<'b>), ParseError> {
184        let (n, _) = self.0.parse(s)?;
185        Ok((n, ()))
186    }
187
188    open spec fn serialize_requires(&self) -> bool {
189        self.0.serialize_requires()
190    }
191
192    fn serialize(&self, _v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> Result<
193        usize,
194        SerializeError,
195    > {
196        self.0.serialize(self.0.predicate.0.as_slice(), data, pos)
197    }
198}
199
200impl<Inner, 'a> Combinator for Tag<Inner, &'a [u8]> where
201    Inner: for <'b>Combinator<Result<'b> = &'b [u8], Owned = Vec<u8>>,
202    Inner::V: SecureSpecCombinator<SpecResult = Seq<u8>>
203 {
204    type Result<'b> = ();
205
206    type Owned = ();
207
208    open spec fn spec_length(&self) -> Option<usize> {
209        self.0.spec_length()
210    }
211
212    fn length(&self) -> Option<usize> {
213        self.0.length()
214    }
215
216    open spec fn parse_requires(&self) -> bool {
217        self.0.parse_requires()
218    }
219
220    fn parse<'b>(&self, s: &'b [u8]) -> Result<(usize, Self::Result<'b>), ParseError> {
221        let (n, _) = self.0.parse(s)?;
222        Ok((n, ()))
223    }
224
225    open spec fn serialize_requires(&self) -> bool {
226        self.0.serialize_requires()
227    }
228
229    fn serialize(&self, _v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> Result<
230        usize,
231        SerializeError,
232    > {
233        self.0.serialize(self.0.predicate.0, data, pos)
234    }
235}
236
237#[cfg(test)]
238#[allow(unused)]
239mod test {
240    use crate::regular::choice::OrdChoice;
241    use super::*;
242    use super::super::uints::{U8};
243    use super::super::bytes::Bytes;
244    use super::super::bytes_n::BytesN;
245
246    proof fn test(s: Seq<u8>)
247        requires
248            s.len() <= usize::MAX,
249    {
250        let tag = Tag::spec_new(BytesN::<3>, seq![0u8, 0, 0]);
251        if let Ok((n, v)) = tag.spec_parse(s) {
252            if let Ok(buf) = tag.spec_serialize(v) {
253                tag.theorem_parse_serialize_roundtrip(s);
254                assert(buf == s.subrange(0, n as int));
255            }
256        }
257    }
258
259    fn test1(s: &[u8])
260        requires
261            s@.len() <= usize::MAX,
262    {
263        let bytes = [0u8, 0, 0];
264        let tag = Tag::new(BytesN::<3>, bytes.as_slice());
265        proof {
266            let spec_tag = Tag::spec_new(BytesN::<3>, bytes@);
267            assert(tag@ == spec_tag);
268        }
269        if let Ok((n, v)) = tag.parse(s) {
270            let mut buf = Vec::new();
271            buf.push(0);
272            if let Ok(m) = tag.serialize(v, &mut buf, 0) {
273                proof {
274                    tag@.theorem_parse_serialize_roundtrip(s@);
275                }
276                assert(buf@ == s@.subrange(0, n as int));
277            }
278        }
279    }
280
281    proof fn test3(s: Seq<u8>)
282        requires
283            s.len() <= usize::MAX,
284    {
285        let tag1 = Tag::spec_new(U8, 0x42);
286        let tag2 = Tag::spec_new(U8, 0x43);
287        let ord = OrdChoice(tag1, tag2);
288        if let Ok((n, v)) = ord.spec_parse(s) {
289            if let Ok(buf) = ord.spec_serialize(v) {
290                ord.theorem_parse_serialize_roundtrip(s);
291                assert(buf == s.subrange(0, n as int));
292            }
293        }
294        let tag3 = Tag::spec_new(BytesN::<3>, seq![1u8, 0, 0]);
295        let tag4 = Tag::spec_new(BytesN::<3>, seq![2u8, 0, 0]);
296        let ord2 = OrdChoice(tag3, tag4);
297        if let Ok((n, v)) = ord2.spec_parse(s) {
298            if let Ok(buf) = ord2.spec_serialize(v) {
299                ord2.theorem_parse_serialize_roundtrip(s);
300                assert(buf == s.subrange(0, n as int));
301            }
302        }
303    }
304
305    fn test4(s: &[u8])
306        requires
307            s@.len() <= usize::MAX,
308    {
309        let tag1 = Tag::new(U8, 0x42);
310        let tag2 = Tag::new(U8, 0x43);
311        let ord = OrdChoice(tag1, tag2);
312        if let Ok((n, v)) = ord.parse(s) {
313            let mut buf = Vec::new();
314            buf.push(0);
315            if let Ok(m) = ord.serialize(v, &mut buf, 0) {
316                proof {
317                    ord@.theorem_parse_serialize_roundtrip(s@);
318                }
319                assert(buf@ == s@.subrange(0, n as int));
320            }
321        }
322        let b1 = [0u8, 0, 0];
323        let b2 = [1u8, 0, 0];
324        let tag3 = Tag::new(Bytes(3), b1.as_slice());
325        let tag4 = Tag::new(Bytes(3), b2.as_slice());
326        let ord2 = OrdChoice(tag3, tag4);
327        if let Ok((n, v)) = ord2.parse(s) {
328            let mut buf = Vec::new();
329            buf.push(0);
330            buf.push(0);
331            buf.push(0);
332            if let Ok(m) = ord2.serialize(v, &mut buf, 0) {
333                proof {
334                    ord2@.theorem_parse_serialize_roundtrip(s@);
335                }
336                assert(buf@ == s@.subrange(0, n as int));
337            }
338        }
339    }
340
341}
342
343// old code
344// /// generic tag combinator that matches the input with a given value and discards it
345// /// e.g. `Tag(Int::<u8>, 0)` matches the byte `0`; `Tag(Bytes::<3>, &[1, 2, 3])` matches the bytes `[1, 2, 3]`
346// pub struct Tag<Inner, T>(pub Inner, pub T);
347//
348// impl<Inner, T> View for Tag<Inner, T> where Inner: View, T: View {
349//     type V = Tag<Inner::V, T::V>;
350//
351//     open spec fn view(&self) -> Self::V {
352//         Tag(self.0@, self.1@)
353//     }
354// }
355//
356// impl<Inner, T> SpecCombinator for Tag<Inner, T> where Inner: SpecCombinator<SpecResult = T> {
357//     type SpecResult = ();
358//
359//     open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
360//         match self.0.spec_parse(s) {
361//             Ok((n, v)) if v == self.1 => Ok((n, ())),
362//             _ => Err(()),
363//         }
364//     }
365//
366//     open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
367//         self.0.spec_serialize(self.1)
368//     }
369//
370//     proof fn spec_parse_wf(&self, s: Seq<u8>) {
371//         self.0.spec_parse_wf(s);
372//     }
373// }
374//
375// impl<Inner, T> SecureSpecCombinator for Tag<Inner, T> where
376//     Inner: SecureSpecCombinator<SpecResult = T>,
377//  {
378//     open spec fn spec_is_prefix_secure() -> bool {
379//         Inner::spec_is_prefix_secure()
380//     }
381//
382//     proof fn theorem_serialize_parse_roundtrip(&self, v: ()) {
383//         self.0.theorem_serialize_parse_roundtrip(self.1);
384//     }
385//
386//     proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
387//         self.0.theorem_parse_serialize_roundtrip(buf);
388//     }
389//
390//     proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
391//         self.0.lemma_prefix_secure(s1, s2);
392//     }
393// }
394//
395// // the line `for <'a, 'b>Inner::Result<'a>: Compare<Inner::Result<'b>> + From<T>`
396// // says that `Inner::Result<'a>` must impl `From<T> for all lifetimes `'a`
397// // at the type level, this means even a static `Inner::Result<'static>` can be converted from
398// // `T`, which in turn mandates that `T: 'static` (if both `T` and `Inner::Result<'a>` are
399// // types without actual lifetimes, e.g. `u8`, then it's fine)
400// //
401// // it would be nice if Rust supports "existential" lifetimes like:
402// // `exist <'a>Inner::Result<'a>: From<T>`
403// impl<Inner, T> Combinator for Tag<Inner, T> where
404//     Inner: Combinator,
405//     Inner::V: SecureSpecCombinator<SpecResult = T::V>,
406//     T: View<V = <Inner::Owned as View>::V> + Copy,
407//     for <'a, 'b>Inner::Result<'a>: Compare<Inner::Result<'b>> + From<T>,
408//  {
409//     type Result<'a> = ();
410//
411//     type Owned = ();
412//
413//     open spec fn spec_length(&self) -> Option<usize> {
414//         self.0.spec_length()
415//     }
416//
417//     fn length(&self) -> Option<usize> {
418//         self.0.length()
419//     }
420//
421//     fn exec_is_prefix_secure() -> bool {
422//         Inner::exec_is_prefix_secure()
423//     }
424//
425//     open spec fn parse_requires(&self) -> bool {
426//         self.0.parse_requires()
427//     }
428//
429//     fn parse(&self, s: &[u8]) -> (res: Result<(usize, ()), ()>) {
430//         match self.0.parse(s) {
431//             Ok((n, v)) if v.compare(&self.1.ex_into()) => Ok((n, ())),
432//             _ => Err(()),
433//         }
434//     }
435//
436//     open spec fn serialize_requires(&self) -> bool {
437//         self.0.serialize_requires()
438//     }
439//
440//     fn serialize(&self, v: (), data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, ()>) {
441//         self.0.serialize(self.1.ex_into(), data, pos)
442//     }
443// }
444//
445// pub type U8Tag = Tag<Int<u8>, u8>;
446//
447// pub type U16Tag = Tag<Int<u16>, u16>;
448//
449// pub type U32Tag = Tag<Int<u32>, u32>;
450//
451// pub type U64Tag = Tag<Int<u64>, u64>;
452//
453// pub type SpecStaticBytesTag<const N: usize> = Tag<BytesN<N>, Seq<u8>>;
454//
455// pub type StaticBytesTag<const N: usize> = Tag<BytesN<N>, &'static [u8; N]>;
456//
457// /// combinator for matching a dynamic byte slice
458// ///
459// /// **Note**: due to the current limitations of Rust borrow checker
460// /// the generic `Tag` combinator cannot be used with dynamic byte slices (`Tag<Bytes, &'a [u8]>`)
461// pub struct DynamicBytesTag<'a>(pub Bytes, pub &'a [u8]);
462//
463// pub struct SpecDynamicBytesTag(pub Bytes, pub Seq<u8>);
464//
465// impl<'a> View for DynamicBytesTag<'a> {
466//     type V = SpecDynamicBytesTag;
467//
468//     open spec fn view(&self) -> Self::V {
469//         SpecDynamicBytesTag(self.0@, self.1@)
470//     }
471// }
472//
473// impl SpecCombinator for SpecDynamicBytesTag {
474//     type SpecResult = ();
475//
476//     open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
477//         match self.0.spec_parse(s) {
478//             Ok((n, v)) if n == self.1.len() && v == self.1 => Ok((n, ())),
479//             _ => Err(()),
480//         }
481//     }
482//
483//     open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
484//         self.0.spec_serialize(self.1)
485//     }
486//
487//     proof fn spec_parse_wf(&self, s: Seq<u8>) {
488//     }
489// }
490//
491// impl SecureSpecCombinator for SpecDynamicBytesTag {
492//     open spec fn spec_is_prefix_secure() -> bool {
493//         Bytes::spec_is_prefix_secure()
494//     }
495//
496//     proof fn theorem_serialize_parse_roundtrip(&self, v: ()) {
497//         self.0.theorem_serialize_parse_roundtrip(self.1);
498//     }
499//
500//     proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
501//         self.0.theorem_parse_serialize_roundtrip(buf);
502//     }
503//
504//     proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
505//         self.0.lemma_prefix_secure(s1, s2);
506//     }
507// }
508//
509// impl<'a> Combinator for DynamicBytesTag<'a> {
510//     type Result<'b> = ();
511//
512//     type Owned = ();
513//
514//     open spec fn spec_length(&self) -> Option<usize> {
515//         Some(self.0.0)
516//     }
517//
518//     fn length(&self) -> Option<usize> {
519//         Some(self.0.0)
520//     }
521//
522//     fn exec_is_prefix_secure() -> bool {
523//         Bytes::exec_is_prefix_secure()
524//     }
525//
526//     fn parse(&self, s: &[u8]) -> (res: Result<(usize, Self::Result<'_>), ()>) {
527//         match self.0.parse(s) {
528//             Ok((n, v)) if compare_slice(v, self.1) => Ok((n, ())),
529//             _ => Err(()),
530//         }
531//     }
532//
533//     fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<
534//         usize,
535//         (),
536//     >) {
537//         self.0.serialize(self.1, data, pos)
538//     }
539// }
540//
541// #[cfg(test)]
542// mod test {
543//     use super::*;
544//
545//     const MAGIC: u8 = 0x42;
546//
547//     spec const SPEC_BYTES_123: Seq<u8> = seq![1, 2, 3];
548//
549//     exec static BYTES_123: [u8; 3]
550//         ensures
551//             BYTES_123@ == SPEC_BYTES_123,
552//     {
553//         let a: [u8; 3] = [1, 2, 3];
554//         assert(a@ == SPEC_BYTES_123);
555//         a
556//     }
557//
558//     spec fn spec_tag(input: Seq<u8>) -> (U8Tag, SpecStaticBytesTag<3>) {
559//         let t1: U8Tag = Tag(U8, MAGIC);
560//         let t2: SpecStaticBytesTag<3> = Tag(BytesN::<3>, SPEC_BYTES_123);
561//         (t1, t2)
562//     }
563//
564//     fn tag(input: &[u8]) -> (res: (U8Tag, StaticBytesTag<3>))
565//         ensures
566//             res@ == spec_tag(input@),
567//     {
568//         let tem_magic: u8 = 0x42;
569//         let t1: U8Tag = Tag(U8, tem_magic);  // ok
570//         let t1: U8Tag = Tag(U8, MAGIC);  // ok
571//         let t2: StaticBytesTag<3> = Tag(BytesN::<3>, &BYTES_123);
572//         (t1, t2)
573//     }
574//
575//     fn tag2<'a>(input: &'a [u8]) {
576//         // let tmp_bytes_123: [u8; 3] = [1, 2, 3];
577//         // let t1 = Tag(BytesN::<3>, &tmp_bytes_123); // err: TMP_BYTES_123 does not live long enough
578//         // it's required that `tmp_bytes_123` is borrowed for `'static`
579//         // let t1 = Tag(Bytes(3), &TMP_BYTES_123); // same err
580//         let t1 = Tag(Bytes(3), &BYTES_123);  // ok
581//         let _ = t1.parse(input);
582//     }
583//
584//     fn tag3<'a, 'b>(input: &'a [u8], tmp_bytes_123: &'b [u8; 3]) where 'b: 'a {
585//         // let t1 = Tag(BytesN::<3>, tmp_bytes_123); // err: TMP_BYTES_123 does not live long enough
586//         // let t1 = Tag(Bytes(3), tmp_bytes_123); // same err
587//         let t1 = Tag(Bytes(3), &BYTES_123);  // ok
588//         let _ = t1.parse(input);
589//     }
590//
591// }
592} // verus!
vest/regular/tag.rs

vest/regular/
tag.rs
