vest_lib/asn1/
constraints.rs

1//! Reusable executable and specification predicates for ASN.1 subtype constraints.
2#[cfg(feature = "alloc")]
3use super::{BmpString, Ia5StringOwned, PrintableStringOwned, TeletexStringOwned, Utf8StringOwned};
4use super::{
5    BmpStringSpec, Ia5String, Ia5StringSpec, Integer, PrintableString, PrintableStringSpec,
6    TeletexString, TeletexStringSpec,
7};
8use crate::core::exec::fns::Pred;
9use crate::core::spec::SpecPred;
10#[cfg(feature = "alloc")]
11use alloc::vec::Vec;
12use vstd::prelude::*;
13use vstd::string::StringSliceAdditionalSpecFns;
14
15verus! {
16
17/// An ASN.1 `SIZE` interval.
18///
19/// Disabled bounds ignore their corresponding numeric const parameter. Keeping
20/// both flags explicit mirrors ASN.1's `MIN` and `MAX` endpoints and avoids
21/// approximating an unbounded specification with a machine maximum.
22#[derive(Clone, Copy)]
23pub struct Size<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize>;
24
25/// An inclusive ASN.1 `INTEGER` value interval with independently optional bounds.
26///
27/// Bounds use `i64` because generated Rust values use the compact `Small` variant
28/// in that range. Arbitrary-size `Big` values are also handled exactly: their
29/// canonical representation proves that they lie strictly outside the `i64`
30/// interval, so only their sign is needed at runtime.
31#[derive(Clone, Copy)]
32pub struct IntegerRange<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64>;
33
34pub open spec fn integer_in_range<
35    const HAS_MIN: bool,
36    const MIN: i64,
37    const HAS_MAX: bool,
38    const MAX: i64,
39>(value: int) -> bool {
40    &&& (HAS_MIN ==> MIN as int <= value)
41    &&& (HAS_MAX ==> value <= MAX as int)
42}
43
44fn integer_in_range_exec<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64>(
45    value: i64,
46) -> (ok: bool)
47    ensures
48        ok == integer_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value as int),
49{
50    (!HAS_MIN || MIN <= value) && (!HAS_MAX || value <= MAX)
51}
52
53impl<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> SpecPred<
54    int,
55> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX> {
56    open spec fn apply(&self, value: int) -> bool {
57        integer_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value)
58    }
59}
60
61impl<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> SpecPred<
62    i8,
63> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX> {
64    open spec fn apply(&self, value: i8) -> bool {
65        integer_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value as int)
66    }
67}
68
69impl<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> Pred<
70    i8,
71> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX> {
72    fn test(&self, value: &i8) -> (ok: bool) {
73        integer_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(*value as i64)
74    }
75}
76
77impl<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> SpecPred<
78    i16,
79> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX> {
80    open spec fn apply(&self, value: i16) -> bool {
81        integer_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value as int)
82    }
83}
84
85impl<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> Pred<
86    i16,
87> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX> {
88    fn test(&self, value: &i16) -> (ok: bool) {
89        integer_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(*value as i64)
90    }
91}
92
93impl<'a, const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> Pred<
94    Integer<'a>,
95> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX> {
96    fn test(&self, value: &Integer<'a>) -> (ok: bool) {
97        value.in_i64_range::<HAS_MIN, MIN, HAS_MAX, MAX>()
98    }
99}
100
101pub open spec fn size_in_range<
102    const HAS_MIN: bool,
103    const MIN: usize,
104    const HAS_MAX: bool,
105    const MAX: usize,
106>(len: nat) -> bool {
107    &&& (HAS_MIN ==> MIN as nat <= len)
108    &&& (HAS_MAX ==> len <= MAX as nat)
109}
110
111fn size_in_range_exec<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize>(
112    len: usize,
113) -> (ok: bool)
114    ensures
115        ok == size_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(len as nat),
116{
117    (!HAS_MIN || MIN <= len) && (!HAS_MAX || len <= MAX)
118}
119
120impl<T, const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<
121    Seq<T>,
122> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
123    open spec fn apply(&self, value: Seq<T>) -> bool {
124        size_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value.len())
125    }
126}
127
128impl<
129    'a,
130    T: DeepView,
131    const HAS_MIN: bool,
132    const MIN: usize,
133    const HAS_MAX: bool,
134    const MAX: usize,
135> Pred<&'a [T]> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
136    fn test(&self, value: &&'a [T]) -> (ok: bool) {
137        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.len())
138    }
139}
140
141#[cfg(feature = "alloc")]
142impl<
143    T: DeepView,
144    const HAS_MIN: bool,
145    const MIN: usize,
146    const HAS_MAX: bool,
147    const MAX: usize,
148> Pred<Vec<T>> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
149    fn test(&self, value: &Vec<T>) -> (ok: bool) {
150        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.len())
151    }
152}
153
154impl<'a, const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<
155    &'a str,
156> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
157    fn test(&self, value: &&'a str) -> (ok: bool) {
158        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.unicode_len())
159    }
160}
161
162#[cfg(feature = "alloc")]
163impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<
164    Utf8StringOwned,
165> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
166    fn test(&self, value: &Utf8StringOwned) -> (ok: bool) {
167        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.as_str().unicode_len())
168    }
169}
170
171impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<
172    PrintableStringSpec,
173> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
174    open spec fn apply(&self, value: PrintableStringSpec) -> bool {
175        size_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner.len())
176    }
177}
178
179impl<'a, const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<
180    PrintableString<'a>,
181> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
182    fn test(&self, value: &PrintableString<'a>) -> (ok: bool) {
183        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner().unicode_len())
184    }
185}
186
187#[cfg(feature = "alloc")]
188impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<
189    PrintableStringOwned,
190> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
191    fn test(&self, value: &PrintableStringOwned) -> (ok: bool) {
192        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner().unicode_len())
193    }
194}
195
196impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<
197    Ia5StringSpec,
198> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
199    open spec fn apply(&self, value: Ia5StringSpec) -> bool {
200        size_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner.len())
201    }
202}
203
204impl<'a, const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<
205    Ia5String<'a>,
206> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
207    fn test(&self, value: &Ia5String<'a>) -> (ok: bool) {
208        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner().unicode_len())
209    }
210}
211
212#[cfg(feature = "alloc")]
213impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<
214    Ia5StringOwned,
215> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
216    fn test(&self, value: &Ia5StringOwned) -> (ok: bool) {
217        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner().unicode_len())
218    }
219}
220
221impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<
222    TeletexStringSpec,
223> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
224    open spec fn apply(&self, value: TeletexStringSpec) -> bool {
225        size_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner.len())
226    }
227}
228
229impl<'a, const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<
230    TeletexString<'a>,
231> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
232    fn test(&self, value: &TeletexString<'a>) -> (ok: bool) {
233        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner().unicode_len())
234    }
235}
236
237#[cfg(feature = "alloc")]
238impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<
239    TeletexStringOwned,
240> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
241    fn test(&self, value: &TeletexStringOwned) -> (ok: bool) {
242        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner().unicode_len())
243    }
244}
245
246impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<
247    BmpStringSpec,
248> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
249    open spec fn apply(&self, value: BmpStringSpec) -> bool {
250        size_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner.len())
251    }
252}
253
254#[cfg(feature = "alloc")]
255impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<
256    BmpString,
257> for Size<HAS_MIN, MIN, HAS_MAX, MAX> {
258    fn test(&self, value: &BmpString) -> (ok: bool) {
259        size_in_range_exec::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner().unicode_len())
260    }
261}
262
263/// Logical union of two executable/specification predicates.
264#[derive(Copy)]
265pub struct ConstraintOr<L, R>(pub L, pub R);
266
267impl<L: Clone, R: Clone> Clone for ConstraintOr<L, R> {
268    fn clone(&self) -> (cloned: Self)
269        ensures
270            call_ensures(L::clone, (&self.0,), cloned.0),
271            call_ensures(R::clone, (&self.1,), cloned.1),
272    {
273        ConstraintOr(self.0.clone(), self.1.clone())
274    }
275}
276
277impl<T, L: SpecPred<T>, R: SpecPred<T>> SpecPred<T> for ConstraintOr<L, R> {
278    open spec fn apply(&self, value: T) -> bool {
279        self.0.apply(value) || self.1.apply(value)
280    }
281}
282
283impl<T: DeepView, L: Pred<T>, R: Pred<T>> Pred<T> for ConstraintOr<L, R> {
284    fn test(&self, value: &T) -> (ok: bool) {
285        self.0.test(value) || self.1.test(value)
286    }
287}
288
289/// Logical intersection of two executable/specification predicates.
290#[derive(Copy)]
291pub struct ConstraintAnd<L, R>(pub L, pub R);
292
293impl<L: Clone, R: Clone> Clone for ConstraintAnd<L, R> {
294    fn clone(&self) -> (cloned: Self)
295        ensures
296            call_ensures(L::clone, (&self.0,), cloned.0),
297            call_ensures(R::clone, (&self.1,), cloned.1),
298    {
299        ConstraintAnd(self.0.clone(), self.1.clone())
300    }
301}
302
303impl<T, L: SpecPred<T>, R: SpecPred<T>> SpecPred<T> for ConstraintAnd<L, R> {
304    open spec fn apply(&self, value: T) -> bool {
305        self.0.apply(value) && self.1.apply(value)
306    }
307}
308
309impl<T: DeepView, L: Pred<T>, R: Pred<T>> Pred<T> for ConstraintAnd<L, R> {
310    fn test(&self, value: &T) -> (ok: bool) {
311        self.0.test(value) && self.1.test(value)
312    }
313}
314
315/// Logical complement of an executable/specification predicate.
316#[derive(Copy)]
317pub struct ConstraintNot<P>(pub P);
318
319impl<P: Clone> Clone for ConstraintNot<P> {
320    fn clone(&self) -> (cloned: Self)
321        ensures
322            call_ensures(P::clone, (&self.0,), cloned.0),
323    {
324        ConstraintNot(self.0.clone())
325    }
326}
327
328impl<T, P: SpecPred<T>> SpecPred<T> for ConstraintNot<P> {
329    open spec fn apply(&self, value: T) -> bool {
330        !self.0.apply(value)
331    }
332}
333
334impl<T: DeepView, P: Pred<T>> Pred<T> for ConstraintNot<P> {
335    fn test(&self, value: &T) -> (ok: bool) {
336        !self.0.test(value)
337    }
338}
339
340} // verus!
vest_lib/asn1/constraints.rs

vest_lib/asn1/
constraints.rs
