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

vest_lib/combinators/preceded/
exec.rs
