vest_lib 0.0.5

VestLib: A library of formally verified parser and serializer combinators
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77

use crate::properties::*;
use vstd::prelude::*;

verus! {

/// Combinator that always succeeds and consumes nothing
pub struct Success;

impl View for Success {
    type V = Self;

    open spec fn view(&self) -> Self::V {
        *self
    }
}

impl SpecCombinator for Success {
    type Type = ();

    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
        Some((0, ()))
    }

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

impl SecureSpecCombinator for Success {
    open spec fn is_prefix_secure() -> bool {
        true
    }

    open spec fn is_productive(&self) -> bool {
        false
    }

    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
    }

    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
    }

    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
        assert(s.subrange(0, 0) == Seq::<u8>::empty());
    }

    proof fn lemma_parse_length(&self, s: Seq<u8>) {
    }

    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
    }
}

impl<'x, I: VestInput, O: VestOutput<I>> Combinator<'x, I, O> for Success {
    type Type = ();

    type SType = ();

    fn length(&self, _v: Self::SType) -> usize {
        0
    }

    fn parse(&self, _s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
        Ok((0, ()))
    }

    fn serialize(&self, _v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
        usize,
        SerializeError,
    >) {
        assert(seq_splice(data@, pos, Seq::<u8>::empty()) == data@);
        Ok(0)
    }
}

} // verus!