1use crate::properties::*;
2use vstd::prelude::*;
3use vstd::slice::slice_subrange;
4
5verus! {
6
7impl<Fst: SecureSpecCombinator, Snd: SpecCombinator> SpecCombinator for (Fst, Snd) {
8 type SpecResult = (Fst::SpecResult, Snd::SpecResult);
9
10 open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
11 if Fst::is_prefix_secure() {
12 if let Ok((n, v1)) = self.0.spec_parse(s) {
13 if let Ok((m, v2)) = self.1.spec_parse(s.subrange(n as int, s.len() as int)) {
14 if n <= usize::MAX - m {
15 Ok(((n + m) as usize, (v1, v2)))
16 } else {
17 Err(())
18 }
19 } else {
20 Err(())
21 }
22 } else {
23 Err(())
24 }
25 } else {
26 Err(())
27 }
28 }
29
30 proof fn spec_parse_wf(&self, s: Seq<u8>) {
31 if let Ok((n, v1)) = self.0.spec_parse(s) {
32 if let Ok((m, v2)) = self.1.spec_parse(s.subrange(n as int, s.len() as int)) {
33 self.0.spec_parse_wf(s);
34 self.1.spec_parse_wf(s.subrange(n as int, s.len() as int));
35 }
36 }
37 }
38
39 open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
40 if Fst::is_prefix_secure() {
41 if let Ok(buf1) = self.0.spec_serialize(v.0) {
42 if let Ok(buf2) = self.1.spec_serialize(v.1) {
43 if buf1.len() + buf2.len() <= usize::MAX {
44 Ok(buf1.add(buf2))
45 } else {
46 Err(())
47 }
48 } else {
49 Err(())
50 }
51 } else {
52 Err(())
53 }
54 } else {
55 Err(())
56 }
57 }
58}
59
60impl<Fst: SecureSpecCombinator, Snd: SecureSpecCombinator> SecureSpecCombinator for (Fst, Snd) {
61 proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
62 if let Ok((buf)) = self.spec_serialize(v) {
63 let buf0 = self.0.spec_serialize(v.0).unwrap();
64 let buf1 = self.1.spec_serialize(v.1).unwrap();
65 self.0.theorem_serialize_parse_roundtrip(v.0);
66 self.0.lemma_prefix_secure(buf0, buf1);
67 self.1.theorem_serialize_parse_roundtrip(v.1);
68 assert(buf0.add(buf1).subrange(buf0.len() as int, buf.len() as int) == buf1);
69 }
70 }
71
72 proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
73 if let Ok((nm, (v0, v1))) = self.spec_parse(buf) {
74 let (n, v0_) = self.0.spec_parse(buf).unwrap();
75 self.0.spec_parse_wf(buf);
76 let buf0 = buf.subrange(0, n as int);
77 let buf1 = buf.subrange(n as int, buf.len() as int);
78 assert(buf == buf0.add(buf1));
79 self.0.lemma_prefix_secure(buf0, buf1);
80 self.0.theorem_parse_serialize_roundtrip(buf);
81 let (m, v1_) = self.1.spec_parse(buf1).unwrap();
82 self.1.theorem_parse_serialize_roundtrip(buf1);
83 self.1.spec_parse_wf(buf1);
84 let buf2 = self.spec_serialize((v0, v1)).unwrap();
85 assert(buf2 == buf.subrange(0, nm as int));
86 } else {
87 }
88 }
89
90 open spec fn is_prefix_secure() -> bool {
91 Fst::is_prefix_secure() && Snd::is_prefix_secure()
92 }
93
94 proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>) {
95 if Fst::is_prefix_secure() && Snd::is_prefix_secure() {
96 if let Ok((nm, (v0, v1))) = self.spec_parse(buf) {
97 let (n, _) = self.0.spec_parse(buf).unwrap();
98 self.0.spec_parse_wf(buf);
99 let buf0 = buf.subrange(0, n as int);
100 let buf1 = buf.subrange(n as int, buf.len() as int);
101 self.0.lemma_prefix_secure(buf0, buf1);
102 self.0.lemma_prefix_secure(buf0, buf1.add(s2));
103 self.0.lemma_prefix_secure(buf, s2);
104 let (m, v1_) = self.1.spec_parse(buf1).unwrap();
105 assert(buf.add(s2).subrange(0, n as int) == buf0);
106 assert(buf.add(s2).subrange(n as int, buf.add(s2).len() as int) == buf1.add(s2));
107 self.1.lemma_prefix_secure(buf1, s2);
108 } else {
109 }
110 } else {
111 }
112 }
113}
114
115impl<Fst, Snd> Combinator for (Fst, Snd) where
116 Fst: Combinator,
117 Snd: Combinator,
118 Fst::V: SecureSpecCombinator<SpecResult = <Fst::Owned as View>::V>,
119 Snd::V: SecureSpecCombinator<SpecResult = <Snd::Owned as View>::V>,
120 {
121 type Result<'a> = (Fst::Result<'a>, Snd::Result<'a>);
122
123 type Owned = (Fst::Owned, Snd::Owned);
124
125 open spec fn spec_length(&self) -> Option<usize> {
126 if let Some(n) = self.0.spec_length() {
127 if let Some(m) = self.1.spec_length() {
128 if n <= usize::MAX - m {
129 Some((n + m) as usize)
130 } else {
131 None
132 }
133 } else {
134 None
135 }
136 } else {
137 None
138 }
139 }
140
141 fn length(&self) -> Option<usize> {
142 if let Some(n) = self.0.length() {
143 if let Some(m) = self.1.length() {
144 if n <= usize::MAX - m {
145 Some(n + m)
146 } else {
147 None
148 }
149 } else {
150 None
151 }
152 } else {
153 None
154 }
155 }
156
157 open spec fn parse_requires(&self) -> bool {
158 self.0.parse_requires() && self.1.parse_requires() && Fst::V::is_prefix_secure()
159 }
160
161 fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
162 let (n, v1) = self.0.parse(s)?;
163 let s_ = slice_subrange(s, n, s.len());
164 let (m, v2) = self.1.parse(s_)?;
165 if n <= usize::MAX - m {
166 Ok(((n + m), (v1, v2)))
167 } else {
168 Err(ParseError::SizeOverflow)
169 }
170 }
171
172 open spec fn serialize_requires(&self) -> bool {
173 self.0.serialize_requires() && self.1.serialize_requires() && Fst::V::is_prefix_secure()
174 }
175
176 fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<
177 usize,
178 SerializeError,
179 >) {
180 let n = self.0.serialize(v.0, data, pos)?;
181 if n <= usize::MAX - pos && n + pos <= data.len() {
182 let m = self.1.serialize(v.1, data, pos + n)?;
183 if m <= usize::MAX - n {
184 assert(data@.subrange(pos as int, pos + n + m as int) == self@.spec_serialize(
185 v@,
186 ).unwrap());
187 assert(data@ == seq_splice(old(data)@, pos, self@.spec_serialize(v@).unwrap()));
188 Ok(n + m)
189 } else {
190 Err(SerializeError::SizeOverflow)
191 }
192 } else {
193 Err(SerializeError::InsufficientBuffer)
194 }
195 }
196}
197
198}