vest_lib 0.2.2

Verified parser and serializer combinators in Verus
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

//! Type aliases and trait implementations allowing plain `spec_fn`s to serve as combinators.
use crate::core::spec::{
    Consistency, PredFnSpec, SpecByteLen, SpecParser, SpecSerializer, SpecSerializerDps,
};
use vstd::prelude::*;

verus! {

/// A spec-level function that computes the serialized byte length of a value.
pub type ByteLenFnSpec<T> = spec_fn(T) -> nat;

/// A spec-level parser function.
pub type ParserFnSpec<T> = spec_fn(Seq<u8>) -> Option<(int, T)>;

/// A spec-level serializer function in the "DPS" style.
pub type SerializerDPSFnSpec<T> = spec_fn(T, Seq<u8>) -> Seq<u8>;

/// A spec-level serializer function.
pub type SerializerFnSpec<T> = spec_fn(T) -> Seq<u8>;

impl<T> Consistency for PredFnSpec<T> {
    type Val = T;

    open spec fn consistent(&self, v: Self::Val) -> bool {
        (self)(v)
    }
}

impl<T> SpecByteLen for ByteLenFnSpec<T> {
    type T = T;

    open spec fn byte_len(&self, v: Self::T) -> nat {
        (self)(v)
    }
}

impl<T> SpecParser for ParserFnSpec<T> {
    type PVal = T;

    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
        (self)(ibuf)
    }
}

impl<T> SpecSerializerDps for SerializerDPSFnSpec<T> {
    type SValue = T;

    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
        (self)(v, obuf)
    }
}

impl<T> SpecSerializer for SerializerFnSpec<T> {
    type SVal = T;

    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
        (self)(v)
    }
}

} // verus!