verdict_parser/asn1/
ia5_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 IA5String in ASN.1
9/// Essentially a wrapper around Octet
10/// that checks that each byte is <= 127
11#[derive(Debug, View)]
12pub struct IA5String;
13
14asn1_tagged!(IA5String, tag_of!(IA5_STRING));
15
16pub type SpecIA5StringValue = Seq<char>;
17pub type IA5StringValue<'a> = &'a str;
18pub type IA5StringValueOwned = String;
19
20impl SpecCombinator for IA5String {
21    type SpecResult = SpecIA5StringValue;
22
23    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
24        Refined {
25            inner: UTF8String,
26            predicate: IA5StringPred,
27        }.spec_parse(s)
28    }
29
30    proof fn spec_parse_wf(&self, s: Seq<u8>) {
31        Refined {
32            inner: UTF8String,
33            predicate: IA5StringPred,
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: IA5StringPred,
41        }.spec_serialize(v)
42    }
43}
44
45impl SecureSpecCombinator for IA5String {
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: IA5StringPred,
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: IA5StringPred,
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: IA5StringPred,
68        }.lemma_prefix_secure(s1, s2);
69    }
70}
71
72impl Combinator for IA5String {
73    type Result<'a> = IA5StringValue<'a>;
74    type Owned = IA5StringValueOwned;
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: IA5StringPred,
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: IA5StringPred,
97        }.serialize(v, data, pos)
98    }
99}
100
101/// A condition that the minimal encoding is used
102#[derive(View)]
103pub struct IA5StringPred;
104
105impl IA5StringPred {
106    closed spec fn wf_char(c: char) -> bool {
107        c <= '\x7f'
108    }
109
110    #[inline(always)]
111    fn exec_wf_char(c: char) -> (res: bool)
112        ensures res == Self::wf_char(c)
113    {
114        c <= '\x7f'
115    }
116}
117
118impl SpecPred for IA5StringPred {
119    type Input = Seq<char>;
120
121    closed spec fn spec_apply(&self, s: &Self::Input) -> bool {
122        forall |i| 0 <= i < s.len() ==> #[trigger] Self::wf_char(s[i])
123    }
124}
125
126impl Pred for IA5StringPred {
127    type Input<'a> = &'a str;
128    type InputOwned = String;
129
130    fn apply(&self, s: &Self::Input<'_>) -> (res: bool)
131    {
132        let len = s.unicode_len();
133        for i in 0..len
134            invariant
135                len == s@.len(),
136                forall |j| 0 <= j < i ==> #[trigger] Self::wf_char(s@[j]),
137        {
138            if !Self::exec_wf_char(s.get_char(i)) {
139                return false;
140            }
141        }
142        return true;
143    }
144}
145
146}
147
148#[cfg(test)]
149mod tests {
150    use super::*;
151    use der::Encode;
152
153    fn serialize_ia5_string(v: &str) -> Result<Vec<u8>, SerializeError> {
154        let mut data = vec![0; v.len() + 10];
155        data[0] = 0x16; // Prepend the tag byte
156        let len = IA5String.serialize(v, &mut data, 1)?;
157        data.truncate(len + 1);
158        Ok(data)
159    }
160
161    #[test]
162    fn diff_with_der() {
163        let diff = |s: &str| {
164            let res1 = serialize_ia5_string(s).map_err(|_| ());
165            let res2 = der::asn1::Ia5StringRef::new(s)
166                .unwrap()
167                .to_der()
168                .map_err(|_| ());
169            assert_eq!(res1, res2);
170        };
171
172        diff("");
173        diff("\x7f");
174        diff("asdsad");
175        diff("aaaaaa");
176        diff("aaaaa".repeat(100).as_str());
177    }
178}
verdict_parser/asn1/ia5_string.rs

verdict_parser/asn1/
ia5_string.rs
