vest_lib/combinators/preceded/
exec.rs

1//! Executable implementation for sequential formats discarding their prefix.
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, AVal, B> Parser<I> for super::Preceded<A, AVal, B, false> where
22    I: InputBuf,
23    A: Parser<I, PT = AVal> + SafeParser<PVal = AVal>,
24    B: Parser<I> + SafeParser,
25    AVal: DeepView<V = AVal>,
26 {
27    type PT = B::PT;
28
29    fn min_byte_len(&self) -> usize {
30        self.a.min_byte_len().saturating_add(self.b.min_byte_len())
31    }
32
33    open spec fn exec_inv(&self) -> bool {
34        Pair(&self.a, &self.b).exec_inv()
35    }
36
37    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
38        let (n, (_, v)) = Pair(&self.a, &self.b).parse(ibuf)?;
39        Ok((n, v))
40    }
41}
42
43// Non-malleable version
44impl<I, A, AVal, B> Parser<I> for super::Preceded<A, AVal, B, true> where
45    I: InputBuf,
46    A: Parser<I, PT = AVal> + SafeParser<PVal = AVal>,
47    B: Parser<I> + SafeParser,
48    AVal: DeepView<V = AVal> + PartialEq + Structural,
49 {
50    type PT = B::PT;
51
52    fn min_byte_len(&self) -> usize {
53        self.a.min_byte_len().saturating_add(self.b.min_byte_len())
54    }
55
56    open spec fn exec_inv(&self) -> bool {
57        &&& Pair(&self.a, &self.b).exec_inv()
58        &&& forall|v: AVal| v.deep_view() == v
59    }
60
61    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
62        let (n, (va, v)) = Pair(&self.a, &self.b).parse(ibuf)?;
63        if va == self.a_val {
64            Ok((n, v))
65        } else {
66            Err(ParseError::non_canonical())
67        }
68    }
69}
70
71impl<Output: OutputBuf, A, AVal, B, T, const CHECK: bool> Serializer<Output, T> for super::Preceded<
72    A,
73    AVal,
74    B,
75    CHECK,
76> where
77    AVal: DeepView<V = AVal>,
78    T: DeepView,
79    A: Serializer<Output, AVal>,
80    B: Serializer<Output, T>,
81 {
82    #[verifier::prophetic]
83    open spec fn exec_inv(&self) -> bool {
84        &&& self.a.exec_inv()
85        &&& self.b.exec_inv()
86        &&& forall|v: AVal| v.deep_view() == v
87    }
88
89    fn serialize_into(&self, v: &T, obuf: &mut Output) {
90        broadcast use crate::core::exec::output::outbuf_lemmas;
91
92        self.a.serialize_into(&self.a_val, obuf);
93        self.b.serialize_into(v, obuf);
94
95    }
96}
97
98impl<A, AVal, B, BVal, const CHECK: bool> ByteLen<BVal> for super::Preceded<
99    A,
100    AVal,
101    B,
102    CHECK,
103> where AVal: DeepView<V = AVal>, BVal: DeepView, A: ByteLen<AVal>, B: ByteLen<BVal> {
104    open spec fn exec_inv(&self) -> bool {
105        &&& self.a.exec_inv()
106        &&& self.b.exec_inv()
107        &&& forall|v: AVal| v.deep_view() == v
108    }
109
110    fn length(&self, v: &BVal) -> (len: usize) {
111        self.a.length(&self.a_val) + self.b.length(v)
112    }
113}
114
115impl<A, AVal, B, BVal, const CHECK: bool> Prepare<BVal> for super::Preceded<
116    A,
117    AVal,
118    B,
119    CHECK,
120> where AVal: DeepView<V = AVal>, BVal: DeepView, A: Prepare<AVal>, B: Prepare<BVal> {
121    open spec fn exec_inv(&self) -> bool {
122        &&& self.a.exec_inv()
123        &&& self.b.exec_inv()
124        &&& forall|v: AVal| v.deep_view() == v
125    }
126
127    fn prepare(&self, v: &BVal) -> (checked: Result<usize, PreSerializeError>) {
128        let la = self.a.prepare(&self.a_val)?;
129        let lb = self.b.prepare(v)?;
130        if let Some(total) = la.checked_add(lb) {
131            Ok(total)
132        } else {
133            Err(PreSerializeError::length_too_large())
134        }
135    }
136}
137
138} // verus!
vest_lib/combinators/preceded/exec.rs

vest_lib/combinators/preceded/
exec.rs
