vest_lib/combinators/named/
spec.rs

1//! Specification delegation through named formats.
2use crate::core::{proof::*, spec::*};
3use vstd::prelude::*;
4
5verus! {
6
7impl<Inner: SpecParser> SpecParser for super::Named<Inner> {
8    type PVal = Inner::PVal;
9
10    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
11        self.1.spec_parse(ibuf)
12    }
13}
14
15impl<Inner: Consistency> Consistency for super::Named<Inner> {
16    type Val = Inner::Val;
17
18    open spec fn consistent(&self, v: Self::Val) -> bool {
19        self.1.consistent(v)
20    }
21}
22
23impl<Inner: AdmitsUniqueVal> AdmitsUniqueVal for super::Named<Inner> {
24    proof fn lemma_unique_consistent_val(&self, v1: Self::Val, v2: Self::Val) {
25        self.1.lemma_unique_consistent_val(v1, v2);
26    }
27}
28
29impl<Inner: SafeParser> SafeParser for super::Named<Inner> {
30    open spec fn safe_inv(&self) -> bool {
31        self.1.safe_inv()
32    }
33
34    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
35        self.1.lemma_parse_safe(ibuf);
36    }
37}
38
39impl<Inner: SoundParser> SoundParser for super::Named<Inner> {
40    open spec fn sound_inv(&self) -> bool {
41        self.1.sound_inv()
42    }
43
44    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
45        self.1.lemma_parse_sound_consumption(ibuf);
46    }
47
48    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
49        self.1.lemma_parse_sound_value(ibuf);
50    }
51}
52
53impl<Inner: SpecSerializerDps> SpecSerializerDps for super::Named<Inner> {
54    type SValue = Inner::SValue;
55
56    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
57        self.1.spec_serialize_dps(v, obuf)
58    }
59}
60
61impl<Inner: SpecSerializer> SpecSerializer for super::Named<Inner> {
62    type SVal = Inner::SVal;
63
64    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
65        self.1.spec_serialize(v)
66    }
67}
68
69impl<Inner: NonTailFmt> NonTailFmt for super::Named<Inner> {
70    open spec fn serialize_dps_inv(&self) -> bool {
71        self.1.serialize_dps_inv()
72    }
73
74    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
75        self.1.lemma_serialize_dps_prepend(v, obuf);
76    }
77
78    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
79        self.1.lemma_serialize_dps_len(v, obuf);
80    }
81}
82
83impl<Inner: GoodSerializer> GoodSerializer for super::Named<Inner> {
84    open spec fn serialize_inv(&self) -> bool {
85        self.1.serialize_inv()
86    }
87
88    proof fn lemma_serialize_len(&self, v: Self::SVal) {
89        self.1.lemma_serialize_len(v);
90    }
91}
92
93impl<Inner: SpecByteLen> SpecByteLen for super::Named<Inner> {
94    type T = Inner::T;
95
96    open spec fn byte_len(&self, v: Self::T) -> nat {
97        self.1.byte_len(v)
98    }
99}
100
101impl<Inner: MinMaxByteLen> MinMaxByteLen for super::Named<Inner> {
102    open spec fn min(&self) -> nat {
103        self.1.min()
104    }
105
106    open spec fn max(&self) -> nat {
107        self.1.max()
108    }
109
110    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
111        self.1.lemma_min_max_byte_len(v);
112    }
113}
114
115impl<Inner: StaticByteLen> StaticByteLen for super::Named<Inner> {
116    open spec fn static_byte_len() -> nat {
117        Inner::static_byte_len()
118    }
119
120    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
121        self.1.lemma_static_len_matches_byte_len(v);
122    }
123}
124
125impl<Inner: ValueByteLen> ValueByteLen for super::Named<Inner> {
126    open spec fn value_byte_len(v: Self::T) -> nat {
127        Inner::value_byte_len(v)
128    }
129
130    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
131        self.1.lemma_value_len_matches_byte_len(v);
132    }
133}
134
135impl<Inner: BytesCombinator> BytesCombinator for super::Named<Inner> {
136    proof fn lemma_byte_len_is_buf_len(&self, buf: Seq<u8>) {
137        self.1.lemma_byte_len_is_buf_len(buf);
138    }
139}
140
141} // verus!
vest_lib/combinators/named/spec.rs

vest_lib/combinators/named/
spec.rs
