verdict_parser/common/
pair.rs

1use super::*;
2/// Use a custom pair type so that we can impl traits on it
3use vstd::prelude::*;
4
5verus! {
6
7#[derive(Debug, View)]
8pub struct Pair<C1, C2>(pub C1, pub C2);
9
10#[derive(Debug, View, PolyfillClone)]
11pub struct PairValue<T1, T2>(pub T1, pub T2);
12
13impl<C1, C2> SpecCombinator for Pair<C1, C2> where
14    C1: SecureSpecCombinator,
15    C2: SecureSpecCombinator,
16{
17    type SpecResult = PairValue<C1::SpecResult, C2::SpecResult>;
18
19    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
20        match (self.0, self.1).spec_parse(s) {
21            Ok((n, v)) => Ok((n, PairValue(v.0, v.1))),
22            Err(()) => Err(()),
23        }
24    }
25
26    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
27        (self.0, self.1).spec_serialize((v.0, v.1))
28    }
29
30    proof fn spec_parse_wf(&self, s: Seq<u8>) {
31        (self.0, self.1).spec_parse_wf(s)
32    }
33}
34
35impl<C1, C2> SecureSpecCombinator for Pair<C1, C2> where
36    C1: SecureSpecCombinator,
37    C2: SecureSpecCombinator,
38{
39    open spec fn is_prefix_secure() -> bool {
40        C1::is_prefix_secure() && C2::is_prefix_secure()
41    }
42
43    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
44        (self.0, self.1).theorem_serialize_parse_roundtrip((v.0, v.1))
45    }
46
47    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
48        (self.0, self.1).theorem_parse_serialize_roundtrip(buf)
49    }
50
51    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
52        (self.0, self.1).lemma_prefix_secure(s1, s2)
53    }
54}
55
56impl<C1, C2> Combinator for Pair<C1, C2> where
57    C1: Combinator,
58    C2: Combinator,
59    C1::V: SecureSpecCombinator<SpecResult = <C1::Owned as View>::V>,
60    C2::V: SecureSpecCombinator<SpecResult = <C2::Owned as View>::V>,
61{
62    type Result<'a> = PairValue<C1::Result<'a>, C2::Result<'a>>;
63    type Owned = PairValue<C1::Owned, C2::Owned>;
64
65    open spec fn spec_length(&self) -> Option<usize> {
66        Some(0)
67    }
68
69    fn length(&self) -> Option<usize> {
70        Some(0)
71    }
72
73    open spec fn parse_requires(&self) -> bool {
74        &&& self.0.parse_requires()
75        &&& self.1.parse_requires()
76        &&& C1::V::is_prefix_secure()
77    }
78
79    #[inline(always)]
80    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
81        let (n, v) = (&self.0, &self.1).parse(s)?;
82        Ok((n, PairValue(v.0, v.1)))
83    }
84
85    open spec fn serialize_requires(&self) -> bool {
86        &&& self.0.serialize_requires()
87        &&& self.1.serialize_requires()
88        &&& C1::V::is_prefix_secure()
89    }
90
91    #[inline(always)]
92    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
93        (&self.0, &self.1).serialize((v.0, v.1), data, pos)
94    }
95}
96
97}
verdict_parser/common/pair.rs

verdict_parser/common/
pair.rs
