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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192

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

verus! {

pub open spec fn bits<Repr: SpecByteLen, Tuple, Nominal>(
    repr: Repr,
    unpack: spec_fn(Repr::T) -> Tuple,
    pack: spec_fn(Tuple) -> Repr::T,
    refinement: PredFnSpec<Tuple>,
    ctor: spec_fn(Tuple) -> Nominal,
    dtor: spec_fn(Nominal) -> Tuple,
) -> Mapped<
    Refined<Mapped<Repr, BiMapper<Repr::T, Tuple>>, PredFnSpec<Tuple>>,
    BiMapper<Tuple, Nominal>,
> {
    Mapped {
        inner: Refined(Mapped { inner: repr, mapper: BiMap(unpack, pack) }, refinement),
        mapper: BiMap(ctor, dtor),
    }
}

impl<Repr, Tuple, Nominal> SpecParser for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen + SpecParser<PVal = Repr::T>,
 {
    type PVal = Nominal;

    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.spec_parse(ibuf)
    }
}

impl<Repr, Tuple, Nominal> SpecSerializerDps for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen + SpecSerializerDps<SValue = Repr::T>,
 {
    type SValue = Nominal;

    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.spec_serialize_dps(v, obuf)
    }
}

impl<Repr, Tuple, Nominal> SpecSerializer for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen + SpecSerializer<SVal = Repr::T>,
 {
    type SVal = Nominal;

    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.spec_serialize(v)
    }
}

impl<Repr, Tuple, Nominal> Consistency for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen + Consistency<Val = Repr::T>,
 {
    type Val = Nominal;

    open spec fn consistent(&self, v: Self::Val) -> bool {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        &&& fmt.consistent(v)
        &&& (self.consistent)(v)
    }
}

impl<Repr, Tuple, Nominal> SpecByteLen for super::Bits<Repr, Tuple, Nominal> where
    Repr: SpecByteLen,
 {
    type T = Nominal;

    open spec fn byte_len(&self, v: Self::T) -> nat {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.byte_len(v)
    }
}

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

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

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

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

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

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

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

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

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

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

impl<Repr, Tuple, Nominal> MinMaxByteLen for super::Bits<Repr, Tuple, Nominal> where
    Repr: MinMaxByteLen,
 {
    open spec fn min(&self) -> nat {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.min()
    }

    open spec fn max(&self) -> nat {
        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
        fmt.max()
    }

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

impl<Repr, Tuple, Nominal> StaticByteLen for super::Bits<Repr, Tuple, Nominal> where
    Repr: StaticByteLen,
 {
    open spec fn static_byte_len() -> nat {
        Repr::static_byte_len()
    }

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

} // verus!