vest_lib/combinators/marker/
spec.rs

1//! Specifications for empty and uninhabitable formats.
2use crate::core::{proof::*, spec::*};
3use crate::Never;
4use vstd::prelude::*;
5
6verus! {
7
8pub const ZERO_BYTE_LEN: usize = 0;
9
10impl SpecParser for super::Empty {
11    type PVal = ();
12
13    open spec fn spec_parse(&self, _ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
14        Some((0, ()))
15    }
16}
17
18impl Consistency for super::Empty {
19    type Val = ();
20
21    open spec fn consistent(&self, _v: Self::Val) -> bool {
22        true
23    }
24}
25
26impl AdmitsUniqueVal for super::Empty {
27    proof fn lemma_unique_consistent_val(&self, v1: Self::Val, v2: Self::Val) {
28    }
29}
30
31impl SafeParser for super::Empty {
32    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
33    }
34}
35
36impl SoundParser for super::Empty {
37    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
38    }
39
40    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
41    }
42}
43
44impl SpecSerializerDps for super::Empty {
45    type SValue = ();
46
47    open spec fn spec_serialize_dps(&self, _v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
48        obuf
49    }
50}
51
52impl SpecSerializer for super::Empty {
53    type SVal = ();
54
55    open spec fn spec_serialize(&self, _v: Self::SVal) -> Seq<u8> {
56        Seq::empty()
57    }
58}
59
60impl NonTailFmt for super::Empty {
61    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
62        assert(self.spec_serialize_dps(v, obuf) == Seq::<u8>::empty() + obuf);
63    }
64
65    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
66        assert(self.spec_serialize_dps(v, obuf).len() - obuf.len() == 0);
67    }
68}
69
70impl GoodSerializer for super::Empty {
71    proof fn lemma_serialize_len(&self, v: Self::SVal) {
72        assert(self.spec_serialize(v).len() == 0);
73    }
74}
75
76impl SpecByteLen for super::Empty {
77    type T = ();
78
79    open spec fn byte_len(&self, _v: Self::T) -> nat {
80        ZERO_BYTE_LEN as nat
81    }
82}
83
84impl MinMaxByteLen for super::Empty {
85    open spec fn min(&self) -> nat {
86        ZERO_BYTE_LEN as nat
87    }
88
89    open spec fn max(&self) -> nat {
90        ZERO_BYTE_LEN as nat
91    }
92
93    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
94    }
95}
96
97impl StaticByteLen for super::Empty {
98    open spec fn static_byte_len() -> nat {
99        ZERO_BYTE_LEN as nat
100    }
101
102    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
103    }
104}
105
106impl ValueByteLen for super::Empty {
107    open spec fn value_byte_len(_v: Self::T) -> nat {
108        ZERO_BYTE_LEN as nat
109    }
110
111    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
112    }
113}
114
115impl SpecParser for super::Void {
116    type PVal = Never;
117
118    open spec fn spec_parse(&self, _ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
119        None
120    }
121}
122
123impl Consistency for super::Void {
124    type Val = Never;
125
126    open spec fn consistent(&self, _v: Self::Val) -> bool {
127        false
128    }
129}
130
131impl AdmitsUniqueVal for super::Void {
132    proof fn lemma_unique_consistent_val(&self, v1: Self::Val, v2: Self::Val) {
133    }
134}
135
136impl SafeParser for super::Void {
137    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
138    }
139}
140
141impl SoundParser for super::Void {
142    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
143    }
144
145    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
146    }
147}
148
149impl SpecSerializerDps for super::Void {
150    type SValue = Never;
151
152    // It doesn't matter what we put here since there are no consistent values for Void.
153    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
154        obuf
155    }
156}
157
158impl SpecSerializer for super::Void {
159    type SVal = Never;
160
161    // It doesn't matter what we put here since there are no consistent values for Void.
162    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
163        Seq::empty()
164    }
165}
166
167impl NonTailFmt for super::Void {
168    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
169        let new_buf = Seq::<u8>::empty();
170        assert(obuf == new_buf + obuf);
171    }
172
173    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
174    }
175}
176
177impl GoodSerializer for super::Void {
178    proof fn lemma_serialize_len(&self, v: Self::SVal) {
179    }
180}
181
182impl SpecByteLen for super::Void {
183    type T = Never;
184
185    open spec fn byte_len(&self, v: Self::T) -> nat {
186        ZERO_BYTE_LEN as nat
187    }
188}
189
190impl MinMaxByteLen for super::Void {
191    open spec fn min(&self) -> nat {
192        ZERO_BYTE_LEN as nat
193    }
194
195    open spec fn max(&self) -> nat {
196        ZERO_BYTE_LEN as nat
197    }
198
199    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
200    }
201}
202
203impl StaticByteLen for super::Void {
204    open spec fn static_byte_len() -> nat {
205        ZERO_BYTE_LEN as nat
206    }
207
208    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
209    }
210}
211
212impl ValueByteLen for super::Void {
213    open spec fn value_byte_len(_v: Self::T) -> nat {
214        ZERO_BYTE_LEN as nat
215    }
216
217    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
218    }
219}
220
221} // verus!
vest_lib/combinators/marker/spec.rs

vest_lib/combinators/marker/
spec.rs
