vest_lib/combinators/cond/
proof.rs

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

vest_lib/combinators/cond/
proof.rs
