vest_lib/asn1/
boolean.rs

1//! ASN.1 BOOLEAN contents under DER and BER rules.
2use crate::core::exec::input::{InputBuf, InputSlice};
3use crate::core::exec::output::*;
4use crate::core::exec::{
5    parser::{PResult, Parser},
6    serializer::{ByteLen, ComplianceErrorKind, PreSerializeError, Prepare, Serializer},
7    ParseError,
8};
9use crate::{
10    combinators::{mapped::spec::FnSpecMapper, Mapped, Refined, U8},
11    core::{proof::*, spec::*},
12};
13use OutputBuf;
14
15use vstd::prelude::*;
16
17verus! {
18
19pub const BOOL_BYTE_LEN: usize = 1;
20
21pub const FALSE_BYTE: u8 = 0x00;
22
23pub const CANONICAL_TRUE_BYTE: u8 = 0xFF;
24
25pub struct BoolMapper<const DER: bool>;
26
27#[verifier::allow_in_spec]
28pub fn non_zero(b: u8) -> bool
29    returns
30        b != FALSE_BYTE,
31{
32    b != FALSE_BYTE
33}
34
35#[verifier::allow_in_spec]
36pub fn der_bool_byte(b: u8) -> bool
37    returns
38        b == CANONICAL_TRUE_BYTE || b == FALSE_BYTE,
39{
40    b == CANONICAL_TRUE_BYTE || b == FALSE_BYTE
41}
42
43pub open spec fn true_byte<const DER: bool>() -> u8 {
44    // if DER {
45    //     CANONICAL_TRUE_BYTE
46    // } else {
47    //     choose|x: u8| non_zero(x)
48    // }
49    // BER accepts any non-zero TRUE octet, but the serializer deliberately
50    // normalizes both BER and DER output to DER's canonical 0xff spelling.
51    CANONICAL_TRUE_BYTE
52}
53
54pub type BoolFmt<const DER: bool> = Mapped<Refined<U8, PredFnSpec<u8>>, FnSpecMapper<u8, bool>>;
55
56pub open spec fn bool_fmt<const DER: bool>() -> BoolFmt<DER> {
57    Mapped {
58        inner: Refined(U8, |b: u8| DER ==> der_bool_byte(b)),
59        mapper: (
60            |b: u8| non_zero(b),
61            |b: bool|
62                if b {
63                    true_byte::<DER>()
64                } else {
65                    FALSE_BYTE
66                },
67        ),
68    }
69}
70
71mod derived_specs {
72    use super::*;
73    use super::super::BoolFmt;
74
75    impl<const DER: bool> SpecParser for BoolFmt<DER> {
76        type PVal = bool;
77
78        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
79            bool_fmt::<DER>().spec_parse(ibuf)
80        }
81    }
82
83    impl<const DER: bool> Consistency for BoolFmt<DER> {
84        type Val = bool;
85
86        open spec fn consistent(&self, v: Self::Val) -> bool {
87            bool_fmt::<DER>().consistent(v)
88        }
89    }
90
91    impl<const DER: bool> SpecSerializerDps for BoolFmt<DER> {
92        type SValue = bool;
93
94        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
95            bool_fmt::<DER>().spec_serialize_dps(v, obuf)
96        }
97    }
98
99    impl<const DER: bool> SpecSerializer for BoolFmt<DER> {
100        type SVal = bool;
101
102        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
103            bool_fmt::<DER>().spec_serialize(v)
104        }
105    }
106
107    impl<const DER: bool> SpecByteLen for BoolFmt<DER> {
108        type T = bool;
109
110        open spec fn byte_len(&self, v: Self::T) -> nat {
111            BOOL_BYTE_LEN as nat
112        }
113    }
114
115    impl<const DER: bool> MinMaxByteLen for BoolFmt<DER> {
116        open spec fn min(&self) -> nat {
117            BOOL_BYTE_LEN as nat
118        }
119
120        open spec fn max(&self) -> nat {
121            BOOL_BYTE_LEN as nat
122        }
123
124        proof fn lemma_min_max_byte_len(&self, v: Self::T) {
125        }
126    }
127
128    impl<const DER: bool> StaticByteLen for BoolFmt<DER> {
129        open spec fn static_byte_len() -> nat {
130            BOOL_BYTE_LEN as nat
131        }
132
133        proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
134            bool_fmt::<DER>().lemma_static_len_matches_byte_len(v);
135        }
136    }
137
138    impl<const DER: bool> ValueByteLen for BoolFmt<DER> {
139        open spec fn value_byte_len(_v: Self::T) -> nat {
140            BOOL_BYTE_LEN as nat
141        }
142
143        proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
144            bool_fmt::<DER>().lemma_static_len_matches_byte_len(v);
145        }
146    }
147
148}
149
150mod derived_proofs {
151    use super::*;
152    use super::super::BoolFmt;
153
154    impl<const DER: bool> SafeParser for BoolFmt<DER> {
155        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
156            bool_fmt::<DER>().lemma_parse_safe(ibuf);
157        }
158    }
159
160    impl<const DER: bool> Productive for BoolFmt<DER> {
161        proof fn lemma_productive(&self, s: Seq<u8>) {
162            bool_fmt::<DER>().lemma_productive(s);
163        }
164    }
165
166    impl<const DER: bool> SoundParser for BoolFmt<DER> {
167        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
168        }
169
170        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
171        }
172    }
173
174    impl<const DER: bool> NonTailFmt for BoolFmt<DER> {
175        proof fn lemma_serialize_dps_prepend(&self, v: bool, obuf: Seq<u8>) {
176            bool_fmt::<DER>().lemma_serialize_dps_prepend(v, obuf);
177        }
178
179        proof fn lemma_serialize_dps_len(&self, v: bool, obuf: Seq<u8>) {
180            bool_fmt::<DER>().lemma_serialize_dps_len(v, obuf);
181        }
182    }
183
184    impl<const DER: bool> GoodSerializer for BoolFmt<DER> {
185        proof fn lemma_serialize_len(&self, v: Self::SVal) {
186            bool_fmt::<DER>().lemma_serialize_len(v);
187        }
188    }
189
190    impl<const DER: bool> SPRoundTripDps for BoolFmt<DER> {
191        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
192            assert(non_zero(CANONICAL_TRUE_BYTE));
193            bool_fmt::<DER>().theorem_serialize_dps_parse_roundtrip(v, obuf);
194        }
195    }
196
197    impl<const DER: bool> NoLookAhead for BoolFmt<DER> {
198        proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
199            bool_fmt::<DER>().lemma_no_lookahead(i1, i2);
200        }
201    }
202
203    impl NonMalleable for BoolFmt<true> {
204        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
205            bool_fmt::<true>().lemma_parse_non_malleable(buf1, buf2);
206        }
207    }
208
209    impl<const DER: bool> EquivSerializersGeneral for BoolFmt<DER> {
210        proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
211            bool_fmt::<DER>().lemma_serialize_equiv(v, obuf);
212        }
213    }
214
215    impl<const DER: bool> EquivSerializers for BoolFmt<DER> {
216        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
217            bool_fmt::<DER>().lemma_serialize_equiv_on_empty(v);
218        }
219    }
220
221}
222
223impl<const DER: bool> Parser<&[u8]> for super::BoolFmt<DER> {
224    type PT = bool;
225
226    fn parse(&self, ibuf: &&[u8]) -> PResult<bool> {
227        let (n, b) = U8.parse(ibuf)?;
228        if DER && !der_bool_byte(b) {
229            Err(ParseError::non_canonical())
230        } else {
231            Ok((n, non_zero(b)))
232        }
233    }
234}
235
236impl<Output: OutputBuf, const DER: bool> Serializer<Output, bool> for super::BoolFmt<DER> {
237    fn serialize_into(&self, v: &bool, obuf: &mut Output) {
238        let b = if *v {
239            CANONICAL_TRUE_BYTE
240        } else {
241            FALSE_BYTE
242        };
243        U8.serialize_into(&b, obuf);
244    }
245}
246
247impl<const DER: bool> Prepare<bool> for super::BoolFmt<DER> {
248    fn prepare(&self, _v: &bool) -> Result<usize, PreSerializeError> {
249        Ok(BOOL_BYTE_LEN)
250    }
251}
252
253impl<const DER: bool> ByteLen<bool> for super::BoolFmt<DER> {
254    fn length(&self, _v: &bool) -> usize {
255        BOOL_BYTE_LEN
256    }
257}
258
259} // verus!
vest_lib/asn1/boolean.rs

vest_lib/asn1/
boolean.rs
