vest_lib/combinators/named/
proof.rs

1//! Proof delegation through named formats.
2use crate::core::{proof::*, spec::*};
3use vstd::prelude::*;
4
5verus! {
6
7impl<Inner: SPRoundTripDps> SPRoundTripDps for super::Named<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::Named<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::Named<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        self.1.lemma_no_lookahead(i1, i2);
34    }
35}
36
37impl<Inner: Productive> Productive for super::Named<Inner> {
38    open spec fn productive_inv(&self) -> bool {
39        self.1.productive_inv()
40    }
41
42    proof fn lemma_productive(&self, s: Seq<u8>) {
43        self.1.lemma_productive(s);
44    }
45}
46
47impl<Inner: EquivSerializersGeneral> EquivSerializersGeneral for super::Named<Inner> {
48    open spec fn equiv_general_inv(&self) -> bool {
49        self.1.equiv_general_inv()
50    }
51
52    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
53        self.1.lemma_serialize_equiv(v, obuf);
54    }
55}
56
57impl<Inner: EquivSerializers> EquivSerializers for super::Named<Inner> {
58    open spec fn equiv_inv(&self) -> bool {
59        self.1.equiv_inv()
60    }
61
62    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
63        self.1.lemma_serialize_equiv_on_empty(v);
64    }
65}
66
67} // verus!
vest_lib/combinators/named/proof.rs

vest_lib/combinators/named/
proof.rs
