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::*;
13use vstd::string::StrSliceExecFns;
14
15verus! {
16
17pub type NumericString<'a> = PrintableString<'a>;
18
19#[cfg(feature = "alloc")]
20pub type NumericStringOwned = PrintableStringOwned;
21
22pub type NumericStringSpec = PrintableStringSpec;
23
24#[derive(Clone, Copy)]
25pub struct NumericStringChars;
26
27pub open spec fn is_numeric_string_char(c: char) -> bool {
28    c as u32 == 0x20 || (0x30 <= c as u32 && c as u32 <= 0x39)
29}
30
31pub open spec fn is_valid_numeric_string(chars: Seq<char>) -> bool {
32    forall|i: int| 0 <= i < chars.len() ==> is_numeric_string_char(#[trigger] chars[i])
33}
34
35impl SpecPred<PrintableStringSpec> for NumericStringChars {
36    open spec fn apply(&self, value: PrintableStringSpec) -> bool {
37        is_valid_numeric_string(value.inner)
38    }
39}
40
41impl<'a> Pred<PrintableString<'a>> for NumericStringChars {
42    fn test(&self, value: &PrintableString<'a>) -> (ok: bool) {
43        let inner = value.inner();
44        let len = inner.unicode_len();
45        for i in 0..len
46            invariant
47                len == inner.deep_view().len(),
48                inner.deep_view() == value.deep_view().inner,
49                forall|k: int|
50                    0 <= k < i ==> is_numeric_string_char(#[trigger] inner.deep_view()[k]),
51        {
52            let c = inner.get_char(i);
53            let code = c as u32;
54            if !(code == 0x20 || (0x30 <= code && code <= 0x39)) {
55                assert(!is_numeric_string_char(inner.deep_view()[i as int]));
56                return false;
57            }
58        }
59        true
60    }
61}
62
63#[cfg(feature = "alloc")]
64impl Pred<PrintableStringOwned> for NumericStringChars {
65    fn test(&self, value: &PrintableStringOwned) -> (ok: bool) {
66        let inner = value.inner();
67        let len = inner.unicode_len();
68        for i in 0..len
69            invariant
70                len == inner.deep_view().len(),
71                inner.deep_view() == value.deep_view().inner,
72                forall|k: int|
73                    0 <= k < i ==> is_numeric_string_char(#[trigger] inner.deep_view()[k]),
74        {
75            let c = inner.get_char(i);
76            let code = c as u32;
77            if !(code == 0x20 || (0x30 <= code && code <= 0x39)) {
78                assert(!is_numeric_string_char(inner.deep_view()[i as int]));
79                return false;
80            }
81        }
82        true
83    }
84}
85
86pub type NumericStringFmt = Refined<PrintableStringFmt, NumericStringChars>;
87
88#[allow(non_upper_case_globals)]
89pub const NumericStringFmt: NumericStringFmt = Refined(PrintableStringFmt, NumericStringChars);
90
91} // verus!
vest_lib/asn1/numericstring.rs

vest_lib/asn1/
numericstring.rs
