vest_lib/combinators/tuple/
exec.rs

1//! Executable sequential composition.
2use crate::combinators::mapped::spec::SpecMap;
3use crate::core::exec::fns::MapRef;
4use crate::core::exec::output::*;
5use crate::core::{
6    exec::{
7        input::InputBuf,
8        parser::{PResult, Parser},
9        serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
10    },
11    spec::{SafeParser, SpecByteLen, SpecParser, SpecSerializer},
12};
13use vstd::prelude::*;
14use OutputBuf;
15
16verus! {
17
18impl<I, A, B> Parser<I> for super::Pair<A, B> where
19    I: InputBuf,
20    A: Parser<I> + SafeParser,
21    B: Parser<I> + SafeParser,
22 {
23    type PT = (A::PT, B::PT);
24
25    open spec fn exec_inv(&self) -> bool {
26        &&& self.0.exec_inv()
27        &&& self.0.safe_inv()
28        &&& self.1.exec_inv()
29        &&& self.1.safe_inv()
30    }
31
32    fn min_byte_len(&self) -> usize {
33        // This is only a hint, so a saturating sum is fine.
34        self.0.min_byte_len().saturating_add(self.1.min_byte_len())
35    }
36
37    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
38        assert(self.exec_inv());
39        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
40
41        let (na, va) = self.0.parse(ibuf)?;
42        let rest = ibuf.skip(na);
43        let (nb, vb) = self.1.parse(&rest)?;
44
45        let _total_len = ibuf.len();
46        proof {
47            assert(na + nb <= _total_len);
48        }
49        let nab = na + nb;
50        let pair = (va, vb);
51        assert(self.spec_parse(ibuf@) == Some((nab as int, pair.deep_view())));
52        Ok((nab, pair))
53    }
54}
55
56impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (TA, TB)> for super::Pair<A, B> where
57    TA: DeepView,
58    TB: DeepView,
59    A: Serializer<Output, TA>,
60    B: Serializer<Output, TB>,
61 {
62    #[verifier::prophetic]
63    open spec fn exec_inv(&self) -> bool {
64        &&& self.0.exec_inv()
65        &&& self.1.exec_inv()
66    }
67
68    fn serialize_into(&self, v: &(TA, TB), obuf: &mut Output) {
69        broadcast use crate::core::exec::output::outbuf_lemmas;
70
71        self.0.serialize_into(&v.0, obuf);
72        self.1.serialize_into(&v.1, obuf);
73    }
74}
75
76impl<A, B, TA, TB> Prepare<(TA, TB)> for super::Pair<A, B> where
77    TA: DeepView,
78    TB: DeepView,
79    A: Prepare<TA>,
80    B: Prepare<TB>,
81 {
82    open spec fn exec_inv(&self) -> bool {
83        &&& self.0.exec_inv()
84        &&& self.1.exec_inv()
85    }
86
87    fn prepare(&self, v: &(TA, TB)) -> Result<usize, PreSerializeError> {
88        let la = self.0.prepare(&v.0)?;
89        let lb = self.1.prepare(&v.1)?;
90        if let Some(total) = la.checked_add(lb) {
91            Ok(total)
92        } else {
93            Err(PreSerializeError::length_too_large())
94        }
95    }
96}
97
98impl<A, B, TA, TB> ByteLen<(TA, TB)> for super::Pair<A, B> where
99    TA: DeepView,
100    TB: DeepView,
101    A: ByteLen<TA>,
102    B: ByteLen<TB>,
103 {
104    open spec fn exec_inv(&self) -> bool {
105        &&& self.0.exec_inv()
106        &&& self.1.exec_inv()
107    }
108
109    fn length(&self, v: &(TA, TB)) -> (len: usize) {
110        let la = self.0.length(&v.0);
111        let lb = self.1.length(&v.1);
112        la + lb
113    }
114}
115
116impl<I, A, B> Parser<I> for super::Bind<A, B> where
117    I: InputBuf,
118    A: Parser<I> + SafeParser,
119    B::O: Parser<I> + SafeParser,
120    B: MapRef<A::PT, Input = A::PVal>,
121 {
122    type PT = (A::PT, <B::O as Parser<I>>::PT);
123
124    fn min_byte_len(&self) -> usize {
125        // `B` is built from `A`'s value, so only `A` is known statically.
126        self.0.min_byte_len()
127    }
128
129    open spec fn exec_inv(&self) -> bool {
130        &&& self.0.exec_inv()
131        &&& self.0.safe_inv()
132        &&& forall|pb: B::O| #[trigger] pb.exec_inv() && pb.safe_inv()
133    }
134
135    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
136        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
137
138        let (na, key) = self.0.parse(ibuf)?;
139        let rest = ibuf.skip(na);
140        let next = self.1.map(&key);
141        assert(next.exec_inv() && next.safe_inv());
142        let (nb, val) = next.parse(&rest)?;
143
144        let _total_len = ibuf.len();
145        proof {
146            assert(na + nb <= _total_len);
147        }
148        let nab = na + nb;
149        let pair = (key, val);
150        Ok((nab, pair))
151    }
152}
153
154impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (TA, TB)> for super::Bind<A, B> where
155    TA: DeepView,
156    TB: DeepView,
157    A: Serializer<Output, TA>,
158    B::O: Serializer<Output, TB>,
159    B: MapRef<TA, Input = TA::V>,
160 {
161    #[verifier::prophetic]
162    open spec fn exec_inv(&self) -> bool {
163        &&& self.0.exec_inv()
164        &&& forall|pb: B::O| #[trigger] pb.exec_inv()
165    }
166
167    fn serialize_into(&self, v: &(TA, TB), obuf: &mut Output) {
168        broadcast use crate::core::exec::output::outbuf_lemmas;
169
170        let next = self.1.map(&v.0);
171        self.0.serialize_into(&v.0, obuf);
172        next.serialize_into(&v.1, obuf);
173    }
174}
175
176impl<A, B, STA, STB> ByteLen<(STA, STB)> for super::Bind<A, B> where
177    STA: DeepView,
178    STB: DeepView,
179    A: ByteLen<STA>,
180    B::O: ByteLen<STB>,
181    B: MapRef<STA, Input = STA::V>,
182 {
183    open spec fn exec_inv(&self) -> bool {
184        &&& self.0.exec_inv()
185        &&& forall|pb: B::O| #[trigger] pb.exec_inv()
186    }
187
188    fn length(&self, v: &(STA, STB)) -> (len: usize) {
189        let next = self.1.map(&v.0);
190        let la = self.0.length(&v.0);
191        let lb = next.length(&v.1);
192        la + lb
193    }
194}
195
196impl<A, B, STA, STB> Prepare<(STA, STB)> for super::Bind<A, B> where
197    STA: DeepView,
198    STB: DeepView,
199    A: Prepare<STA>,
200    B::O: Prepare<STB>,
201    B: MapRef<STA, Input = STA::V>,
202 {
203    open spec fn exec_inv(&self) -> bool {
204        &&& self.0.exec_inv()
205        &&& forall|pb: B::O| #[trigger] pb.exec_inv()
206    }
207
208    fn prepare(&self, v: &(STA, STB)) -> Result<usize, PreSerializeError> {
209        let next = self.1.map(&v.0);
210        let la = self.0.prepare(&v.0)?;
211        let lb = next.prepare(&v.1)?;
212        if let Some(total) = la.checked_add(lb) {
213            Ok(total)
214        } else {
215            Err(PreSerializeError::length_too_large())
216        }
217    }
218}
219
220} // verus!
vest_lib/combinators/tuple/exec.rs

vest_lib/combinators/tuple/
exec.rs
