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
62
63
64
65
66
67
68
69
70
71
72
73
74
75

//! Correctness proofs for empty and uninhabitable formats.
use crate::core::{proof::*, spec::*};
use vstd::prelude::*;

verus! {

impl SPRoundTripDps for super::Empty {
    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
        assert(self.spec_serialize_dps(v, obuf) == obuf);
        assert(self.spec_parse(obuf) == Some((0int, ())));
    }
}

impl NonMalleable for super::Empty {
    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
    }
}

impl NoLookAhead for super::Empty {
    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
    }
}

impl Productive for super::Empty {
    open spec fn productive_inv(&self) -> bool {
        false
    }

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

impl Productive for super::Void {
    proof fn lemma_productive(&self, s: Seq<u8>) {
    }
}

impl EquivSerializersGeneral for super::Empty {
    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
        assert(self.spec_serialize_dps(v, obuf) == self.spec_serialize(v) + obuf);
    }
}

impl EquivSerializers for super::Empty {
    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
    }
}

impl SPRoundTripDps for super::Void {
    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
        assert(false);
    }
}

impl NonMalleable for super::Void {
    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
    }
}

impl NoLookAhead for super::Void {
    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
    }
}

impl EquivSerializersGeneral for super::Void {
    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
    }
}

impl EquivSerializers for super::Void {
    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
    }
}

} // verus!