verdict_parser/asn1/
printable_string.rs

1use super::*;
2/// TODO: maybe refactor this using Refined
3use std::fmt::{self, Debug, Formatter};
4use vstd::prelude::*;
5
6verus! {
7
8/// Combinator for PrintableString in ASN.1
9/// Essentially a wrapper around Octet
10/// that checks that each byte is <= 127
11#[derive(Debug, View)]
12pub struct PrintableString;
13
14asn1_tagged!(PrintableString, tag_of!(PRINTABLE_STRING));
15
16pub type SpecPrintableStringValue = Seq<char>;
17pub type PrintableStringValue<'a> = &'a str;
18pub type PrintableStringValueOwned = String;
19
20impl SpecCombinator for PrintableString {
21    type SpecResult = SpecPrintableStringValue;
22
23    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
24        Refined {
25            inner: UTF8String,
26            predicate: PrintableStringPred,
27        }.spec_parse(s)
28    }
29
30    proof fn spec_parse_wf(&self, s: Seq<u8>) {
31        Refined {
32            inner: UTF8String,
33            predicate: PrintableStringPred,
34        }.spec_parse_wf(s)
35    }
36
37    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
38        Refined {
39            inner: UTF8String,
40            predicate: PrintableStringPred,
41        }.spec_serialize(v)
42    }
43}
44
45impl SecureSpecCombinator for PrintableString {
46    open spec fn is_prefix_secure() -> bool {
47        true
48    }
49
50    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
51        Refined {
52            inner: UTF8String,
53            predicate: PrintableStringPred,
54        }.theorem_serialize_parse_roundtrip(v);
55    }
56
57    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
58        Refined {
59            inner: UTF8String,
60            predicate: PrintableStringPred,
61        }.theorem_parse_serialize_roundtrip(buf);
62    }
63
64    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
65        Refined {
66            inner: UTF8String,
67            predicate: PrintableStringPred,
68        }.lemma_prefix_secure(s1, s2);
69    }
70}
71
72impl Combinator for PrintableString {
73    type Result<'a> = PrintableStringValue<'a>;
74    type Owned = PrintableStringValueOwned;
75
76    closed spec fn spec_length(&self) -> Option<usize> {
77        None
78    }
79
80    fn length(&self) -> Option<usize> {
81        None
82    }
83
84    #[inline(always)]
85    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
86        Refined {
87            inner: UTF8String,
88            predicate: PrintableStringPred,
89        }.parse(s)
90    }
91
92    #[inline(always)]
93    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
94        Refined {
95            inner: UTF8String,
96            predicate: PrintableStringPred,
97        }.serialize(v, data, pos)
98    }
99}
100
101/// A condition that the minimal encoding is used
102#[derive(View)]
103pub struct PrintableStringPred;
104
105impl PrintableStringPred {
106    closed spec fn wf_char(c: char) -> bool {
107        // https://en.wikipedia.org/wiki/PrintableString
108        ||| ('A' <= c && c <= 'Z')
109        ||| ('a' <= c && c <= 'z')
110        ||| ('0' <= c && c <= '9')
111        ||| c == ' '
112        ||| ('\'' <= c && c <= ')')
113        ||| ('+' <= c && c <= '/')
114        ||| c == ':'
115        ||| c == '='
116        ||| c == '?'
117    }
118
119    #[inline(always)]
120    fn exec_wf_char(c: char) -> (res: bool)
121        ensures res == Self::wf_char(c)
122    {
123        ('A' <= c && c <= 'Z') ||
124        ('a' <= c && c <= 'z') ||
125        ('0' <= c && c <= '9') ||
126        c == ' ' ||
127        ('\'' <= c && c <= ')') ||
128        ('+' <= c && c <= '/') ||
129        c == ':' ||
130        c == '=' ||
131        c == '?'
132    }
133}
134
135impl SpecPred for PrintableStringPred {
136    type Input = Seq<char>;
137
138    closed spec fn spec_apply(&self, s: &Self::Input) -> bool {
139        forall |i| 0 <= i < s.len() ==> #[trigger] Self::wf_char(s[i])
140    }
141}
142
143impl Pred for PrintableStringPred {
144    type Input<'a> = &'a str;
145    type InputOwned = String;
146
147    fn apply(&self, s: &Self::Input<'_>) -> (res: bool)
148    {
149        let len = s.unicode_len();
150        for i in 0..len
151            invariant
152                len == s@.len(),
153                forall |j| 0 <= j < i ==> #[trigger] Self::wf_char(s@[j]),
154        {
155            if !Self::exec_wf_char(s.get_char(i)) {
156                return false;
157            }
158        }
159        return true;
160    }
161}
162
163}
verdict_parser/asn1/printable_string.rs

verdict_parser/asn1/
printable_string.rs
