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 parse(&self, ibuf: &I) -> PResult<Self::PT> {
33        assert(self.exec_inv());
34        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
35
36        let (na, va) = self.0.parse(ibuf)?;
37        let rest = ibuf.skip(na);
38        let (nb, vb) = self.1.parse(&rest)?;
39
40        let _total_len = ibuf.len();
41        proof {
42            assert(na + nb <= _total_len);
43        }
44        let nab = na + nb;
45        let pair = (va, vb);
46        assert(self.spec_parse(ibuf@) == Some((nab as int, pair.deep_view())));
47        Ok((nab, pair))
48    }
49}
50
51impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (TA, TB)> for super::Pair<A, B> where
52    TA: DeepView,
53    TB: DeepView,
54    A: Serializer<Output, TA>,
55    B: Serializer<Output, TB>,
56 {
57    #[verifier::prophetic]
58    open spec fn exec_inv(&self) -> bool {
59        &&& self.0.exec_inv()
60        &&& self.1.exec_inv()
61    }
62
63    fn serialize_into(&self, v: &(TA, TB), obuf: &mut Output) {
64        broadcast use crate::core::exec::output::outbuf_lemmas;
65
66        self.0.serialize_into(&v.0, obuf);
67        self.1.serialize_into(&v.1, obuf);
68    }
69}
70
71impl<A, B, TA, TB> Prepare<(TA, TB)> for super::Pair<A, B> where
72    TA: DeepView,
73    TB: DeepView,
74    A: Prepare<TA>,
75    B: Prepare<TB>,
76 {
77    open spec fn exec_inv(&self) -> bool {
78        &&& self.0.exec_inv()
79        &&& self.1.exec_inv()
80    }
81
82    fn prepare(&self, v: &(TA, TB)) -> Result<usize, PreSerializeError> {
83        let la = self.0.prepare(&v.0)?;
84        let lb = self.1.prepare(&v.1)?;
85        if let Some(total) = la.checked_add(lb) {
86            Ok(total)
87        } else {
88            Err(PreSerializeError::length_too_large())
89        }
90    }
91}
92
93impl<A, B, TA, TB> ByteLen<(TA, TB)> for super::Pair<A, B> where
94    TA: DeepView,
95    TB: DeepView,
96    A: ByteLen<TA>,
97    B: ByteLen<TB>,
98 {
99    open spec fn exec_inv(&self) -> bool {
100        &&& self.0.exec_inv()
101        &&& self.1.exec_inv()
102    }
103
104    fn length(&self, v: &(TA, TB)) -> (len: usize) {
105        let la = self.0.length(&v.0);
106        let lb = self.1.length(&v.1);
107        la + lb
108    }
109}
110
111impl<I, A, B> Parser<I> for super::Bind<A, B> where
112    I: InputBuf,
113    A: Parser<I> + SafeParser,
114    B::O: Parser<I> + SafeParser,
115    B: MapRef<A::PT, Input = A::PVal>,
116 {
117    type PT = (A::PT, <B::O as Parser<I>>::PT);
118
119    open spec fn exec_inv(&self) -> bool {
120        &&& self.0.exec_inv()
121        &&& self.0.safe_inv()
122        &&& forall|pb: B::O| #[trigger] pb.exec_inv() && pb.safe_inv()
123    }
124
125    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
126        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
127
128        let (na, key) = self.0.parse(ibuf)?;
129        let rest = ibuf.skip(na);
130        let next = self.1.map(&key);
131        assert(next.exec_inv() && next.safe_inv());
132        let (nb, val) = next.parse(&rest)?;
133
134        let _total_len = ibuf.len();
135        proof {
136            assert(na + nb <= _total_len);
137        }
138        let nab = na + nb;
139        let pair = (key, val);
140        Ok((nab, pair))
141    }
142}
143
144impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (TA, TB)> for super::Bind<A, B> where
145    TA: DeepView,
146    TB: DeepView,
147    A: Serializer<Output, TA>,
148    B::O: Serializer<Output, TB>,
149    B: MapRef<TA, Input = TA::V>,
150 {
151    #[verifier::prophetic]
152    open spec fn exec_inv(&self) -> bool {
153        &&& self.0.exec_inv()
154        &&& forall|pb: B::O| #[trigger] pb.exec_inv()
155    }
156
157    fn serialize_into(&self, v: &(TA, TB), obuf: &mut Output) {
158        broadcast use crate::core::exec::output::outbuf_lemmas;
159
160        let next = self.1.map(&v.0);
161        self.0.serialize_into(&v.0, obuf);
162        next.serialize_into(&v.1, obuf);
163    }
164}
165
166impl<A, B, STA, STB> ByteLen<(STA, STB)> for super::Bind<A, B> where
167    STA: DeepView,
168    STB: DeepView,
169    A: ByteLen<STA>,
170    B::O: ByteLen<STB>,
171    B: MapRef<STA, Input = STA::V>,
172 {
173    open spec fn exec_inv(&self) -> bool {
174        &&& self.0.exec_inv()
175        &&& forall|pb: B::O| #[trigger] pb.exec_inv()
176    }
177
178    fn length(&self, v: &(STA, STB)) -> (len: usize) {
179        let next = self.1.map(&v.0);
180        let la = self.0.length(&v.0);
181        let lb = next.length(&v.1);
182        la + lb
183    }
184}
185
186impl<A, B, STA, STB> Prepare<(STA, STB)> for super::Bind<A, B> where
187    STA: DeepView,
188    STB: DeepView,
189    A: Prepare<STA>,
190    B::O: Prepare<STB>,
191    B: MapRef<STA, Input = STA::V>,
192 {
193    open spec fn exec_inv(&self) -> bool {
194        &&& self.0.exec_inv()
195        &&& forall|pb: B::O| #[trigger] pb.exec_inv()
196    }
197
198    fn prepare(&self, v: &(STA, STB)) -> Result<usize, PreSerializeError> {
199        let next = self.1.map(&v.0);
200        let la = self.0.prepare(&v.0)?;
201        let lb = next.prepare(&v.1)?;
202        if let Some(total) = la.checked_add(lb) {
203            Ok(total)
204        } else {
205            Err(PreSerializeError::length_too_large())
206        }
207    }
208}
209
210} // verus!
vest_lib/combinators/tuple/exec.rs

vest_lib/combinators/tuple/
exec.rs
