vest_lib/combinators/bits/
proof.rs

1//! Correctness proofs for byte-aligned bitfield formats.
2use crate::combinators::{mapped::spec::*, Mapped, Pair, Refined};
3use crate::core::{proof::*, spec::*};
4use vstd::prelude::*;
5
6use super::spec::*;
7
8verus! {
9
10impl<Repr, Tuple, Nominal> SPRoundTripDps for super::Bits<Repr, Tuple, Nominal> where
11    Repr: SPRoundTripDps,
12 {
13    open spec fn unambiguous(&self) -> bool {
14        // let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
15        // fmt.unambiguous()
16        // &&& forall|ibuf| #[trigger]
17        //     fmt.spec_parse(ibuf) matches Some((_, v)) ==> (self.consistent)(v)
18        &&& self.repr.unambiguous()
19        &&& forall|unpacked: Tuple|
20            (#[trigger] (self.consistent)((self.ctor)(unpacked)) && (self.refinement)(unpacked))
21                ==> (self.unpack)((self.pack)(unpacked)) == unpacked
22        &&& forall|t: Nominal| #[trigger] (self.consistent)(t) ==> (self.ctor)((self.dtor)(t)) == t
23    }
24
25    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
26        let packed = (self.pack)((self.dtor)(v));
27        self.repr.theorem_serialize_dps_parse_roundtrip(packed, obuf);
28    }
29}
30
31impl<Repr, Tuple, Nominal> NonMalleable for super::Bits<Repr, Tuple, Nominal> where
32    Repr: SpecByteLen + SoundParser + NonMalleable<PVal = Repr::T>,
33 {
34    open spec fn nonmal_inv(&self) -> bool {
35        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
36        fmt.nonmal_inv()
37    }
38
39    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
40        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
41        fmt.lemma_parse_non_malleable(buf1, buf2);
42    }
43}
44
45impl<Repr, Tuple, Nominal> NoLookAhead for super::Bits<Repr, Tuple, Nominal> where
46    Repr: SpecByteLen + NoLookAhead<PVal = Repr::T>,
47 {
48    open spec fn no_lookahead_inv(&self) -> bool {
49        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
50        fmt.no_lookahead_inv()
51    }
52
53    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
54        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
55        assert(self.no_lookahead_inv() == fmt.no_lookahead_inv());
56        fmt.lemma_no_lookahead(i1, i2);
57    }
58}
59
60impl<Repr, Tuple, Nominal> Productive for super::Bits<Repr, Tuple, Nominal> where
61    Repr: SpecByteLen + Productive<PVal = Repr::T>,
62 {
63    open spec fn productive_inv(&self) -> bool {
64        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
65        fmt.productive_inv()
66    }
67
68    proof fn lemma_productive(&self, s: Seq<u8>) {
69        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
70        fmt.lemma_productive(s);
71    }
72}
73
74impl<Repr, Tuple, Nominal> EquivSerializersGeneral for super::Bits<Repr, Tuple, Nominal> where
75    Repr: SpecByteLen + EquivSerializersGeneral<SVal = Repr::T>,
76 {
77    open spec fn equiv_general_inv(&self) -> bool {
78        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
79        fmt.equiv_general_inv()
80    }
81
82    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
83        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
84        fmt.lemma_serialize_equiv(v, obuf);
85    }
86}
87
88impl<Repr, Tuple, Nominal> EquivSerializers for super::Bits<Repr, Tuple, Nominal> where
89    Repr: SpecByteLen + EquivSerializers<SVal = Repr::T>,
90 {
91    open spec fn equiv_inv(&self) -> bool {
92        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
93        fmt.equiv_inv()
94    }
95
96    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
97        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
98        fmt.lemma_serialize_equiv_on_empty(v);
99    }
100}
101
102} // verus!
vest_lib/combinators/bits/proof.rs

vest_lib/combinators/bits/
proof.rs
