verdict_parser/x509/
extension.rs

1use super::*;
2use crate::asn1::Boolean;
3use vstd::prelude::*;
4
5verus! {
6
7broadcast use super::oid::axiom_disjoint_oids;
8
9/// Extension  ::=  SEQUENCE  {
10///     extnID      OBJECT IDENTIFIER,
11///     critical    BOOLEAN DEFAULT FALSE,
12///     extnValue   OCTET STRING
13/// }
14pub type ExtensionInner = Mapped<
15    LengthWrapped<
16        Depend<
17            ASN1<ObjectIdentifier>,
18            <ExtensionCont as Continuation>::Output,
19            ExtensionCont,
20        >,
21    >,
22    ExtensionMapper>;
23
24pub type ExtensionsInner = SequenceOf<ASN1<Extension>>;
25
26wrap_combinator! {
27    pub struct Extension: ExtensionInner =>
28        spec SpecExtensionValue,
29        exec<'a> ExtensionValue<'a>,
30        owned ExtensionValueOwned,
31    = Mapped {
32            inner: LengthWrapped(Depend {
33                fst: ASN1(ObjectIdentifier),
34                snd: ExtensionCont,
35                spec_snd: Ghost(|i| ExtensionCont::spec_apply(i)),
36            }),
37            mapper: ExtensionMapper,
38        };
39}
40
41asn1_tagged!(Extension, tag_of!(SEQUENCE));
42
43asn1! {
44    seq of Extensions(ASN1(Extension)): ASN1<Extension>;
45}
46
47mapper! {
48    pub struct ExtensionMapper;
49
50    for <Id, Param>
51    from ExtensionFrom where type ExtensionFrom<Id, Param> = (Id, PairValue<OptionDeep<bool>, Param>);
52    to ExtensionPoly where pub struct ExtensionPoly<Id, Param> {
53        pub id: Id,
54        pub critical: OptionDeep<bool>,
55        pub param: Param,
56    }
57
58    spec SpecExtensionValue with <SpecObjectIdentifierValue, SpecExtensionParamValue>;
59    exec ExtensionValue<'a> with <ObjectIdentifierValue, ExtensionParamValue<'a>>;
60    owned ExtensionValueOwned with <ObjectIdentifierValueOwned, ExtensionParamValueOwned>;
61
62    forward(x) {
63        ExtensionPoly {
64            id: x.0,
65            critical: x.1.0,
66            param: x.1.1,
67        }
68    }
69
70    backward(y) {
71        (y.id, PairValue(y.critical, y.param))
72    }
73}
74
75/// Parse an optional boolean field ("critical") (default to bool)
76/// before the actual extension parameter
77#[derive(Debug, View)]
78pub struct ExtensionCont;
79
80impl ExtensionCont {
81    pub open spec fn spec_apply(i: SpecObjectIdentifierValue) -> <ExtensionCont as Continuation>::Output {
82        Optional(spec_new_wrapped(ASN1(Boolean)), ExtensionParamCont::spec_apply(i))
83    }
84}
85
86impl Continuation for ExtensionCont {
87    type Input<'a> = ObjectIdentifierValue;
88    type Output = Optional<Wrapped<ASN1<Boolean>>, <ExtensionParamCont as Continuation>::Output>;
89
90    fn apply<'a>(&self, i: Self::Input<'a>) -> (o: Self::Output) {
91        Optional(new_wrapped(ASN1(Boolean)), ExtensionParamCont.apply(i))
92    }
93
94    open spec fn requires<'a>(&self, i: Self::Input<'a>) -> bool {
95        true
96    }
97
98    open spec fn ensures<'a>(&self, i: Self::Input<'a>, o: Self::Output) -> bool {
99        o@ == Self::spec_apply(i@)
100    }
101}
102
103}
104
105#[cfg(test)]
106mod test {
107    use super::*;
108
109    verus! {
110        /// Check that all trait bounds and preconditions are satisfied
111        #[test]
112        fn is_combinator() {
113            let _ = ASN1(Extension).parse(&[]);
114            let _ = ASN1(Extensions).parse(&[]);
115        }
116    }
117
118    #[test]
119    fn sanity() {
120        assert!(ASN1(Extension)
121            .parse(&[
122                0x30, 0x1D, 0x06, 0x03, 0x55, 0x1D, 0x0E, 0x04, 0x16, 0x04, 0x14, 0xE4, 0xAF, 0x2B,
123                0x26, 0x71, 0x1A, 0x2B, 0x48, 0x27, 0x85, 0x2F, 0x52, 0x66, 0x2C, 0xEF, 0xF0, 0x89,
124                0x13, 0x71, 0x3E,
125            ])
126            .is_ok());
127
128        assert!(ASN1(Extensions)
129            .parse(&[
130                0x30, 0x40, 0x30, 0x0E, 0x06, 0x03, 0x55, 0x1D, 0x0F, 0x01, 0x01, 0xFF, 0x04, 0x04,
131                0x03, 0x02, 0x01, 0x86, 0x30, 0x0F, 0x06, 0x03, 0x55, 0x1D, 0x13, 0x01, 0x01, 0xFF,
132                0x04, 0x05, 0x30, 0x03, 0x01, 0x01, 0xFF, 0x30, 0x1D, 0x06, 0x03, 0x55, 0x1D, 0x0E,
133                0x04, 0x16, 0x04, 0x14, 0xE4, 0xAF, 0x2B, 0x26, 0x71, 0x1A, 0x2B, 0x48, 0x27, 0x85,
134                0x2F, 0x52, 0x66, 0x2C, 0xEF, 0xF0, 0x89, 0x13, 0x71, 0x3E,
135            ])
136            .is_ok());
137    }
138}
verdict_parser/x509/extension.rs

verdict_parser/x509/
extension.rs
