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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

//! Correctness proofs for byte-aligned bitfield formats.
use crate::combinators::{mapped::spec::*, Mapped, Pair, Refined};
use crate::core::{proof::*, spec::*};
use vstd::prelude::*;

use super::spec::*;

verus! {

impl<Repr, Tuple, Nominal> SPRoundTripDps for super::Bits<Repr, Tuple, Nominal> where
    Repr: SPRoundTripDps,
 {
    open spec fn unambiguous(&self) -> bool {
        // let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        // fmt.unambiguous()
        // &&& forall|ibuf| #[trigger]
        //     fmt.spec_parse(ibuf) matches Some((_, v)) ==> (self.consistent)(v)
        &&& self.repr.unambiguous()
        &&& forall|unpacked: Tuple|
            (#[trigger] (self.consistent)((self.ctor)(unpacked)) && (self.refinement)(unpacked))
                ==> (self.unpack)((self.pack)(unpacked)) == unpacked
        &&& forall|t: Nominal| #[trigger] (self.consistent)(t) ==> (self.ctor)((self.dtor)(t)) == t
    }

    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
        let packed = (self.pack)((self.dtor)(v));
        self.repr.theorem_serialize_dps_parse_roundtrip(packed, obuf);
    }
}

impl<Repr, Tuple, Nominal> NonMalleable for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen + SoundParser + NonMalleable<PVal = Repr::T>,
 {
    open spec fn nonmal_inv(&self) -> bool {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.nonmal_inv()
    }

    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        assert(self.nonmal_inv() == fmt.nonmal_inv());
        fmt.lemma_parse_non_malleable(buf1, buf2);
    }
}

impl<Repr, Tuple, Nominal> NoLookAhead for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen + NoLookAhead<PVal = Repr::T>,
 {
    open spec fn no_lookahead_inv(&self) -> bool {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.no_lookahead_inv()
    }

    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        assert(self.no_lookahead_inv() == fmt.no_lookahead_inv());
        fmt.lemma_no_lookahead(i1, i2);
    }
}

impl<Repr, Tuple, Nominal> Productive for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen + Productive<PVal = Repr::T>,
 {
    open spec fn productive_inv(&self) -> bool {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.productive_inv()
    }

    proof fn lemma_productive(&self, s: Seq<u8>) {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        assert(self.productive_inv() == fmt.productive_inv());
        fmt.lemma_productive(s);
    }
}

impl<Repr, Tuple, Nominal> EquivSerializersGeneral for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen + EquivSerializersGeneral<SVal = Repr::T>,
 {
    open spec fn equiv_general_inv(&self) -> bool {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.equiv_general_inv()
    }

    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        assert(self.equiv_general_inv() == fmt.equiv_general_inv());
        fmt.lemma_serialize_equiv(v, obuf);
    }
}

impl<Repr, Tuple, Nominal> EquivSerializers for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen + EquivSerializers<SVal = Repr::T>,
 {
    open spec fn equiv_inv(&self) -> bool {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.equiv_inv()
    }

    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.lemma_serialize_equiv_on_empty(v);
    }
}

} // verus!