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

//! Correctness proofs for boolean-gated formats.
use crate::core::{proof::*, spec::*};
use vstd::prelude::*;

verus! {

impl<Inner: SPRoundTripDps> SPRoundTripDps for super::Cond<Inner> {
    open spec fn unambiguous(&self) -> bool {
        self.1.unambiguous()
    }

    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
        self.1.theorem_serialize_dps_parse_roundtrip(v, obuf);
    }
}

impl<Inner: NonMalleable> NonMalleable for super::Cond<Inner> {
    open spec fn nonmal_inv(&self) -> bool {
        self.1.nonmal_inv()
    }

    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
        self.1.lemma_parse_non_malleable(buf1, buf2);
    }
}

impl<Inner: NoLookAhead> NoLookAhead for super::Cond<Inner> {
    open spec fn no_lookahead_inv(&self) -> bool {
        self.1.no_lookahead_inv()
    }

    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
        if let Some((n, v)) = self.spec_parse(i1) {
            if 0 <= n <= i2.len() {
                if i2[0..n] == i1[0..n] {
                    self.1.lemma_no_lookahead(i1, i2);
                }
            }
        }
    }
}

impl<Inner: Productive> Productive for super::Cond<Inner> {
    open spec fn productive_inv(&self) -> bool {
        self.1.productive_inv()
    }

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

impl<Inner: EquivSerializersGeneral> EquivSerializersGeneral for super::Cond<Inner> {
    open spec fn equiv_general_inv(&self) -> bool {
        self.1.equiv_general_inv()
    }

    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
        self.1.lemma_serialize_equiv(v, obuf);
    }
}

impl<Inner: EquivSerializers> EquivSerializers for super::Cond<Inner> {
    open spec fn equiv_inv(&self) -> bool {
        self.1.equiv_inv()
    }

    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
        self.1.lemma_serialize_equiv_on_empty(v);
    }
}

} // verus!