verdict_parser/common/
default.rs

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

verdict_parser/common/
default.rs
