verdict_parser/asn1/
null.rs

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

verdict_parser/asn1/
null.rs
