verdict_parser/asn1/
boolean.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Combainator for BOOLEAN in ASN.1
7/// TRUE = 0x01 0x01 0xff
8/// FALSE = 0x01 0x01 0x00
9#[derive(Debug, View)]
10pub struct Boolean;
11
12asn1_tagged!(Boolean, tag_of!(BOOLEAN));
13
14impl SpecCombinator for Boolean {
15    type SpecResult = bool;
16
17    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
18        if s.len() < 2 {
19            Err(())
20        } else if s[0] == 0x01 && s[1] == 0xff {
21            Ok((2, true))
22        } else if s[0] == 0x01 && s[1] == 0x00 {
23            Ok((2, false))
24        } else {
25            Err(())
26        }
27    }
28
29    proof fn spec_parse_wf(&self, s: Seq<u8>) {}
30
31    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
32        if v {
33            Ok(seq![ 0x01, 0xff ])
34        } else {
35            Ok(seq![ 0x01, 0x00 ])
36        }
37    }
38}
39
40impl SecureSpecCombinator for Boolean {
41    open spec fn is_prefix_secure() -> bool {
42        true
43    }
44
45    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {}
46
47    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
48        if let Ok((n, v)) = self.spec_parse(buf) {
49            assert(self.spec_serialize(v).unwrap() =~= buf.subrange(0, 2));
50        }
51    }
52
53    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {}
54}
55
56impl Combinator for Boolean {
57    type Result<'a> = bool;
58    type Owned = bool;
59
60    closed spec fn spec_length(&self) -> Option<usize> {
61        Some(2)
62    }
63
64    fn length(&self) -> Option<usize> {
65        Some(2)
66    }
67
68    #[inline(always)]
69    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
70        if s.len() < 2 {
71            Err(ParseError::UnexpectedEndOfInput)
72        } else if s[0] == 0x01 && s[1] == 0xff {
73            Ok((2, true))
74        } else if s[0] == 0x01 && s[1] == 0x00 {
75            Ok((2, false))
76        } else {
77            Err(ParseError::Other("Invalid boolean value".to_string()))
78        }
79    }
80
81    #[inline(always)]
82    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
83        if pos > usize::MAX - 2 || pos + 2 > data.len() {
84            return Err(SerializeError::InsufficientBuffer);
85        }
86
87        if v {
88            data.set(pos, 0x01);
89            data.set(pos + 1, 0xff);
90        } else {
91            data.set(pos, 0x01);
92            data.set(pos + 1, 0x00);
93        }
94
95        assert(data@ =~= seq_splice(old(data)@, pos, self@.spec_serialize(v@).unwrap()));
96
97        Ok(2)
98    }
99}
100
101}
verdict_parser/asn1/boolean.rs

verdict_parser/asn1/
boolean.rs
