Trait Combinator Copy item path

self@.requires(),

self.ex_requires(),

self@.wf(v@),

self@.spec_serialize(v@).len() <= usize::MAX,

len == self@.spec_serialize(v@).len(),

The length of the output buffer. This can be used to optimize serialization by pre-allocating the buffer.

self@.requires(),

self.ex_requires(),

s@.len() <= usize::MAX,

res matches Ok((n, v)) ==> self@.spec_parse(s@) == Some((n as int, v@)),

self@.spec_parse(s@) matches Some((n, v)) ==> res matches Ok((m, u)) && m == n && v == u@,

res is Err ==> self@.spec_parse(s@) is None,

self@.spec_parse(s@) is None ==> res is Err,

The parsing function. To enable “zero-copy” parsing, implementations of parse should not consume/deepcopy the input buffer I, but rather return a slice of the input buffer for Self::Type whenever possible. See crate::buf_traits::VestInput and crate::buf_traits::VestPublicInput for more details.

§Pre-conditions

• SpecCombinator::requires
• Combinator::ex_requires

§Post-conditions

Essentially, the implementation of parse is functionally correct with respect to the specification spec_parse on both success and failure cases.

self@.requires(),

self.ex_requires(),

self@.wf(v@),

pos <= old(buf)@.len() <= usize::MAX,

res matches Ok(
    n,
) ==> {
    &&& buf@.len() == old(buf)@.len()
    &&& pos <= usize::MAX - n && pos + n <= buf@.len()
    &&& n == self@.spec_serialize(v@).len()
    &&& buf@ == seq_splice(old(buf)@, pos, self@.spec_serialize(v@))

},

The serialization function. The intended use of serialize is to serialize a value v into the buffer buf at the position pos “in-place” (i.e., without allocating a new buffer or extending the buffer).

§Pre-conditions

• SpecCombinator::requires
• Combinator::ex_requires
• SpecCombinator::wf
• pos is less than or equal to the length of the buffer, whose length is less than or equal to usize::MAX.

§Post-conditions

serialize ensures that it is functionally correct with respect to the specification spec_serialize when it returns Ok. This is because serialize being a partial function can fail (e.g., insufficient buffer space), while spec_serialize is a total function (with infinite buffer size) and will never fail.

{ true }

Additional pre-conditions for parsing and serialization

e.g., crate::regular::sequence::Pair combinator requires that the crate::regular::sequence::Continuation is well-formed w.r.t. the spec_fn closure.