vest_lib/combinators/marker/
proof.rs

1//! Correctness proofs for empty and uninhabitable formats.
2use crate::core::{proof::*, spec::*};
3use vstd::prelude::*;
4
5verus! {
6
7impl SPRoundTripDps for super::Empty {
8    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
9        assert(self.spec_serialize_dps(v, obuf) == obuf);
10        assert(self.spec_parse(obuf) == Some((0int, ())));
11    }
12}
13
14impl NonMalleable for super::Empty {
15    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
16    }
17}
18
19impl NoLookAhead for super::Empty {
20    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
21    }
22}
23
24impl Productive for super::Empty {
25    open spec fn productive_inv(&self) -> bool {
26        false
27    }
28
29    proof fn lemma_productive(&self, s: Seq<u8>) {
30    }
31}
32
33impl Productive for super::Void {
34    proof fn lemma_productive(&self, s: Seq<u8>) {
35    }
36}
37
38impl EquivSerializersGeneral for super::Empty {
39    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
40        assert(self.spec_serialize_dps(v, obuf) == self.spec_serialize(v) + obuf);
41    }
42}
43
44impl EquivSerializers for super::Empty {
45    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
46    }
47}
48
49impl SPRoundTripDps for super::Void {
50    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
51        assert(false);
52    }
53}
54
55impl NonMalleable for super::Void {
56    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
57    }
58}
59
60impl NoLookAhead for super::Void {
61    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
62    }
63}
64
65impl EquivSerializersGeneral for super::Void {
66    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
67    }
68}
69
70impl EquivSerializers for super::Void {
71    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
72    }
73}
74
75} // verus!
vest_lib/combinators/marker/proof.rs

vest_lib/combinators/marker/
proof.rs
