vest_lib/asn1/
numericstring.rs

1//! ASN.1 NumericString contents.
2//!
3//! NumericString's character repertoire (space and decimal digits) is a strict
4//! subset of PrintableString's repertoire, so its codec is a refinement of the
5//! existing zero-copy PrintableString codec.
6#[cfg(feature = "alloc")]
7use super::PrintableStringOwned;
8use super::{PrintableString, PrintableStringFmt, PrintableStringSpec};
9use crate::combinators::Refined;
10use crate::core::exec::fns::Pred;
11use crate::core::spec::SpecPred;
12use vstd::prelude::*;
13#[cfg(not(feature = "alloc"))]
14use vstd::string::StrSliceExecFns;
15
16verus! {
17
18pub type NumericString<'a> = PrintableString<'a>;
19
20#[cfg(feature = "alloc")]
21pub type NumericStringOwned = PrintableStringOwned;
22
23pub type NumericStringSpec = PrintableStringSpec;
24
25#[derive(Clone, Copy)]
26pub struct NumericStringChars;
27
28/// NumericString permits space and ASCII decimal digits.
29#[verifier::allow_in_spec]
30pub fn is_numeric_string_char(c: char) -> bool
31    returns
32        c == ' ' || ('0' <= c && c <= '9'),
33{
34    c == ' ' || ('0' <= c && c <= '9')
35}
36
37pub open spec fn is_valid_numeric_string(chars: Seq<char>) -> bool {
38    forall|i: int| 0 <= i < chars.len() ==> is_numeric_string_char(#[trigger] chars[i])
39}
40
41impl SpecPred<PrintableStringSpec> for NumericStringChars {
42    open spec fn apply(&self, value: PrintableStringSpec) -> bool {
43        is_valid_numeric_string(value.inner)
44    }
45}
46
47// vstd currently gates its `Chars` iterator contracts behind `alloc`, even
48// though Rust's character iterator itself does not allocate.
49#[cfg(feature = "alloc")]
50fn check_numeric_chars(inner: &str) -> (valid: bool)
51    ensures
52        valid == is_valid_numeric_string(inner.deep_view()),
53{
54    inner.chars().all(
55        |c: char| -> (valid: bool)
56            ensures
57                valid == is_numeric_string_char(c),
58            { is_numeric_string_char(c) },
59    )
60}
61
62#[cfg(not(feature = "alloc"))]
63fn check_numeric_chars(inner: &str) -> (valid: bool)
64    ensures
65        valid == is_valid_numeric_string(inner.deep_view()),
66{
67    let len = inner.unicode_len();
68    for i in 0..len
69        invariant
70            len == inner.deep_view().len(),
71            forall|k: int| 0 <= k < i ==> is_numeric_string_char(#[trigger] inner.deep_view()[k]),
72    {
73        let c = inner.get_char(i);
74        if !is_numeric_string_char(c) {
75            assert(!is_numeric_string_char(inner.deep_view()[i as int]));
76            return false;
77        }
78    }
79    true
80}
81
82impl<'a> Pred<PrintableString<'a>> for NumericStringChars {
83    fn test(&self, value: &PrintableString<'a>) -> (ok: bool) {
84        check_numeric_chars(value.inner())
85    }
86}
87
88#[cfg(feature = "alloc")]
89impl Pred<PrintableStringOwned> for NumericStringChars {
90    fn test(&self, value: &PrintableStringOwned) -> (ok: bool) {
91        check_numeric_chars(value.inner())
92    }
93}
94
95pub type NumericStringFmt = Refined<PrintableStringFmt, NumericStringChars>;
96
97#[allow(non_upper_case_globals)]
98pub const NumericStringFmt: NumericStringFmt = Refined(PrintableStringFmt, NumericStringChars);
99
100} // verus!
vest_lib/asn1/numericstring.rs

vest_lib/asn1/
numericstring.rs
