verdict_parser/common/
optional.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Essentially doing OrdChoice((C1, C2), C2),
7/// but the result is mapped through
8///   Left((A, B)) <-> (Some(A), B)
9///   Right(B) <-> (None, B)
10///
11/// NOTE: we are not directly using OrdChoice since we don't want
12/// to enforce C2::is_prefix_secure()
13#[derive(Debug, View)]
14pub struct Optional<C1, C2>(pub C1, pub C2);
15
16pub type OptionalValue<T1, T2> = PairValue<OptionDeep<T1>, T2>;
17
18impl<C1, C2> SpecCombinator for Optional<C1, C2> where
19    C1: SecureSpecCombinator,
20    C2: SecureSpecCombinator + DisjointFrom<C1>,
21{
22    type SpecResult = PairValue<OptionDeep<C1::SpecResult>, C2::SpecResult>;
23
24    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()>
25    {
26        if self.1.disjoint_from(&self.0) {
27            if let Ok((n, (v1, v2))) = (self.0, self.1).spec_parse(s) {
28                Ok((n, PairValue(OptionDeep::Some(v1), v2)))
29            } else if let Ok((n, v)) = self.1.spec_parse(s) {
30                Ok((n, PairValue(OptionDeep::None, v)))
31            } else {
32                Err(())
33            }
34        } else {
35            Err(())
36        }
37    }
38
39    proof fn spec_parse_wf(&self, s: Seq<u8>) {
40        (self.0, self.1).spec_parse_wf(s);
41        self.1.spec_parse_wf(s);
42    }
43
44    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()>
45    {
46        if self.1.disjoint_from(&self.0) {
47            match v {
48                PairValue(OptionDeep::Some(v1), v2) => (self.0, self.1).spec_serialize((v1, v2)),
49                PairValue(OptionDeep::None, v2) => self.1.spec_serialize(v2),
50            }
51        } else {
52            Err(())
53        }
54    }
55}
56
57impl<C1, C2> SecureSpecCombinator for Optional<C1, C2> where
58    C1: SecureSpecCombinator,
59    C2: SecureSpecCombinator + DisjointFrom<C1>
60{
61    open spec fn is_prefix_secure() -> bool {
62        C1::is_prefix_secure() && C2::is_prefix_secure()
63    }
64
65    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
66        match v {
67            PairValue(OptionDeep::Some(v1), v2) => {
68                (self.0, self.1).theorem_serialize_parse_roundtrip((v1, v2));
69            },
70            PairValue(OptionDeep::None, v2) => {
71                if let Ok(buf) = self.1.spec_serialize(v2) {
72                    if self.1.disjoint_from(&self.0) {
73                        self.1.parse_disjoint_on(&self.0, buf);
74                    }
75                }
76                self.1.theorem_serialize_parse_roundtrip(v2);
77            },
78        }
79    }
80
81    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
82        (self.0, self.1).theorem_parse_serialize_roundtrip(buf);
83        self.1.theorem_parse_serialize_roundtrip(buf);
84        assert(self.spec_parse(buf) matches Ok((n, v)) ==> self.spec_serialize(v).unwrap() == buf.subrange(0, n as int));
85    }
86
87    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
88        if self.1.disjoint_from(&self.0) {
89            self.1.parse_disjoint_on(&self.0, s1.add(s2));
90            (self.0, self.1).lemma_prefix_secure(s1, s2);
91            self.1.lemma_prefix_secure(s1, s2);
92        }
93    }
94}
95
96impl<C1, C2> Combinator for Optional<C1, C2> where
97    C1: Combinator,
98    C2: Combinator,
99
100    C1::V: SecureSpecCombinator<SpecResult = <C1::Owned as View>::V>,
101    C2::V: SecureSpecCombinator<SpecResult = <C2::Owned as View>::V> + DisjointFrom<C1::V>,
102{
103    type Result<'a> = OptionalValue<C1::Result<'a>, C2::Result<'a>>;
104    type Owned = OptionalValue<C1::Owned, C2::Owned>;
105
106    closed spec fn spec_length(&self) -> Option<usize> {
107        None
108    }
109
110    fn length(&self) -> Option<usize> {
111        None
112    }
113
114    open spec fn parse_requires(&self) -> bool {
115        &&& self.0.parse_requires()
116        &&& self.1.parse_requires()
117        &&& self.1@.disjoint_from(&self.0@)
118        &&& C1::V::is_prefix_secure()
119    }
120
121    #[inline(always)]
122    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
123        let res = if let Ok((n, (v1, v2))) = (&self.0, &self.1).parse(s) {
124            Ok((n, PairValue(OptionDeep::Some(v1), v2)))
125        } else if let Ok((n, v2)) = self.1.parse(s) {
126            Ok((n, PairValue(OptionDeep::None, v2)))
127        } else {
128            Err(ParseError::OrdChoiceNoMatch)
129        };
130
131        // TODO: why do we need this?
132        assert(res matches Ok((n, v)) ==> {
133            &&& self@.spec_parse(s@) is Ok
134            &&& self@.spec_parse(s@) matches Ok((m, w)) ==> n == m && v@ == w && n <= s@.len()
135        });
136
137        res
138    }
139
140    open spec fn serialize_requires(&self) -> bool {
141        &&& self.0.serialize_requires()
142        &&& self.1.serialize_requires()
143        &&& self.1@.disjoint_from(&self.0@)
144        &&& C1::V::is_prefix_secure()
145    }
146
147    #[inline(always)]
148    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
149        let len = match v {
150            PairValue(OptionDeep::Some(v1), v2) => (&self.0, &self.1).serialize((v1, v2), data, pos),
151            PairValue(OptionDeep::None, v2) => self.1.serialize(v2, data, pos),
152        }?;
153
154        assert(data@ =~= seq_splice(old(data)@, pos, self@.spec_serialize(v@).unwrap()));
155
156        Ok(len)
157    }
158}
159
160/// If T2 and T3 are both disjoint from T1, then
161/// something like Optional<T1, Optional<T2, T3>> is doable
162impl<T1, T2, T3> DisjointFrom<T1> for Optional<T2, T3> where
163    T1: SecureSpecCombinator,
164    T2: SecureSpecCombinator,
165    T3: SecureSpecCombinator,
166    T2: DisjointFrom<T1>,
167    T3: DisjointFrom<T1>,
168    T3: DisjointFrom<T2>,
169{
170    open spec fn disjoint_from(&self, other: &T1) -> bool {
171        self.0.disjoint_from(other) &&
172        self.1.disjoint_from(other)
173    }
174
175    proof fn parse_disjoint_on(&self, other: &T1, buf: Seq<u8>) {
176        self.0.parse_disjoint_on(other, buf);
177        self.1.parse_disjoint_on(other, buf);
178    }
179}
180
181}
verdict_parser/common/optional.rs

verdict_parser/common/
optional.rs
