vest_lib/combinators/terminated/
exec.rs

1//! Executable implementation for sequential formats discarding their suffix.
2use crate::core::exec::output::*;
3use crate::{
4    combinators::Pair,
5    core::{
6        exec::{
7            input::InputBuf,
8            parser::{PResult, Parser},
9            serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
10            ParseError,
11        },
12        spec::{SafeParser, SpecByteLen, SpecParser, SpecSerializer},
13    },
14};
15use vstd::prelude::*;
16use OutputBuf;
17
18verus! {
19
20// Malleable version
21impl<I, A, B, BVal> Parser<I> for super::Terminated<A, B, BVal, false> where
22    I: InputBuf,
23    A: Parser<I> + SafeParser,
24    B: Parser<I, PT = BVal> + SafeParser<PVal = BVal>,
25    BVal: DeepView<V = BVal>,
26 {
27    type PT = A::PT;
28
29    open spec fn exec_inv(&self) -> bool {
30        Pair(&self.a, &self.b).exec_inv()
31    }
32
33    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
34        let (n, (v, _)) = Pair(&self.a, &self.b).parse(ibuf)?;
35        Ok((n, v))
36    }
37}
38
39// Non-malleable version
40impl<I, A, B, BVal> Parser<I> for super::Terminated<A, B, BVal, true> where
41    I: InputBuf,
42    A: Parser<I> + SafeParser,
43    B: Parser<I, PT = BVal> + SafeParser<PVal = BVal>,
44    BVal: DeepView<V = BVal> + PartialEq + Structural,
45 {
46    type PT = A::PT;
47
48    open spec fn exec_inv(&self) -> bool {
49        &&& Pair(&self.a, &self.b).exec_inv()
50        &&& forall|v: BVal| v.deep_view() == v
51    }
52
53    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
54        let (n, (v, vb)) = Pair(&self.a, &self.b).parse(ibuf)?;
55        if vb == self.b_val {
56            Ok((n, v))
57        } else {
58            Err(ParseError::non_canonical())
59        }
60    }
61}
62
63impl<Output: OutputBuf, A, B, BVal, T, const CHECK: bool> Serializer<
64    Output,
65    T,
66> for super::Terminated<A, B, BVal, CHECK> where
67    T: DeepView,
68    BVal: DeepView<V = BVal>,
69    A: Serializer<Output, T>,
70    B: Serializer<Output, BVal>,
71 {
72    #[verifier::prophetic]
73    open spec fn exec_inv(&self) -> bool {
74        &&& self.a.exec_inv()
75        &&& self.b.exec_inv()
76        &&& forall|v: BVal| v.deep_view() == v
77    }
78
79    fn serialize_into(&self, v: &T, obuf: &mut Output) {
80        broadcast use crate::core::exec::output::outbuf_lemmas;
81
82        self.a.serialize_into(v, obuf);
83        self.b.serialize_into(&self.b_val, obuf);
84    }
85}
86
87impl<A, B, BVal, T, const CHECK: bool> ByteLen<T> for super::Terminated<A, B, BVal, CHECK> where
88    T: DeepView,
89    BVal: DeepView<V = BVal>,
90    A: ByteLen<T>,
91    B: ByteLen<BVal>,
92 {
93    open spec fn exec_inv(&self) -> bool {
94        &&& self.a.exec_inv()
95        &&& self.b.exec_inv()
96        &&& forall|v: BVal| v.deep_view() == v
97    }
98
99    fn length(&self, v: &T) -> (len: usize) {
100        self.a.length(v) + self.b.length(&self.b_val)
101    }
102}
103
104impl<A, B, BVal, T, const CHECK: bool> Prepare<T> for super::Terminated<A, B, BVal, CHECK> where
105    T: DeepView,
106    BVal: DeepView<V = BVal>,
107    A: Prepare<T>,
108    B: Prepare<BVal>,
109 {
110    open spec fn exec_inv(&self) -> bool {
111        &&& self.a.exec_inv()
112        &&& self.b.exec_inv()
113        &&& forall|v: BVal| v.deep_view() == v
114    }
115
116    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
117        let la = self.a.prepare(v)?;
118        let lb = self.b.prepare(&self.b_val)?;
119        if let Some(total) = la.checked_add(lb) {
120            Ok(total)
121        } else {
122            Err(PreSerializeError::length_too_large())
123        }
124    }
125}
126
127} // verus!
vest_lib/combinators/terminated/exec.rs

vest_lib/combinators/terminated/
exec.rs
