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        assert(self.nonmal_inv() == fmt.nonmal_inv());
42        fmt.lemma_parse_non_malleable(buf1, buf2);
43    }
44}
45
46impl<Repr, Tuple, Nominal> NoLookAhead for super::Bits<Repr, Tuple, Nominal> where
47    Repr: SpecByteLen + NoLookAhead<PVal = Repr::T>,
48 {
49    open spec fn no_lookahead_inv(&self) -> bool {
50        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
51        fmt.no_lookahead_inv()
52    }
53
54    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
55        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
56        assert(self.no_lookahead_inv() == fmt.no_lookahead_inv());
57        fmt.lemma_no_lookahead(i1, i2);
58    }
59}
60
61impl<Repr, Tuple, Nominal> Productive for super::Bits<Repr, Tuple, Nominal> where
62    Repr: SpecByteLen + Productive<PVal = Repr::T>,
63 {
64    open spec fn productive_inv(&self) -> bool {
65        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
66        fmt.productive_inv()
67    }
68
69    proof fn lemma_productive(&self, s: Seq<u8>) {
70        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
71        assert(self.productive_inv() == fmt.productive_inv());
72        fmt.lemma_productive(s);
73    }
74}
75
76impl<Repr, Tuple, Nominal> EquivSerializersGeneral for super::Bits<Repr, Tuple, Nominal> where
77    Repr: SpecByteLen + EquivSerializersGeneral<SVal = Repr::T>,
78 {
79    open spec fn equiv_general_inv(&self) -> bool {
80        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
81        fmt.equiv_general_inv()
82    }
83
84    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
85        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
86        assert(self.equiv_general_inv() == fmt.equiv_general_inv());
87        fmt.lemma_serialize_equiv(v, obuf);
88    }
89}
90
91impl<Repr, Tuple, Nominal> EquivSerializers for super::Bits<Repr, Tuple, Nominal> where
92    Repr: SpecByteLen + EquivSerializers<SVal = Repr::T>,
93 {
94    open spec fn equiv_inv(&self) -> bool {
95        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
96        fmt.equiv_inv()
97    }
98
99    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
100        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
101        fmt.lemma_serialize_equiv_on_empty(v);
102    }
103}
104
105} // verus!
vest_lib/combinators/bits/proof.rs

vest_lib/combinators/bits/
proof.rs
