vest_lib/core/
fns.rs

1//! Type aliases and trait implementations allowing plain `spec_fn`s to serve as combinators.
2use crate::core::spec::{
3    Consistency, PredFnSpec, SpecByteLen, SpecParser, SpecSerializer, SpecSerializerDps,
4};
5use vstd::prelude::*;
6
7verus! {
8
9/// A spec-level function that computes the serialized byte length of a value.
10pub type ByteLenFnSpec<T> = spec_fn(T) -> nat;
11
12/// A spec-level parser function.
13pub type ParserFnSpec<T> = spec_fn(Seq<u8>) -> Option<(int, T)>;
14
15/// A spec-level serializer function in the "DPS" style.
16pub type SerializerDPSFnSpec<T> = spec_fn(T, Seq<u8>) -> Seq<u8>;
17
18/// A spec-level serializer function.
19pub type SerializerFnSpec<T> = spec_fn(T) -> Seq<u8>;
20
21impl<T> Consistency for PredFnSpec<T> {
22    type Val = T;
23
24    open spec fn consistent(&self, v: Self::Val) -> bool {
25        (self)(v)
26    }
27}
28
29impl<T> SpecByteLen for ByteLenFnSpec<T> {
30    type T = T;
31
32    open spec fn byte_len(&self, v: Self::T) -> nat {
33        (self)(v)
34    }
35}
36
37impl<T> SpecParser for ParserFnSpec<T> {
38    type PVal = T;
39
40    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
41        (self)(ibuf)
42    }
43}
44
45impl<T> SpecSerializerDps for SerializerDPSFnSpec<T> {
46    type SValue = T;
47
48    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
49        (self)(v, obuf)
50    }
51}
52
53impl<T> SpecSerializer for SerializerFnSpec<T> {
54    type SVal = T;
55
56    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
57        (self)(v)
58    }
59}
60
61} // verus!
vest_lib/core/fns.rs

vest_lib/core/
fns.rs
