verdict_parser/x509/
alg_id.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6broadcast use super::oid::axiom_disjoint_oids;
7
8// In X.509:
9// AlgorithmIdentifier  ::=  SEQUENCE  {
10//     algorithm               OBJECT IDENTIFIER,
11//     parameters              ANY DEFINED BY algorithm OPTIONAL
12// }
13pub type AlgorithmIdentifierInner = Mapped<
14    LengthWrapped<
15        Depend<
16            ASN1<ObjectIdentifier>,
17            <AlgorithmParamCont as Continuation>::Output,
18            AlgorithmParamCont,
19        >,
20    >,
21    AlgorithmIdentifierMapper>;
22
23wrap_combinator! {
24    pub struct AlgorithmIdentifier: AlgorithmIdentifierInner =>
25        spec SpecAlgorithmIdentifierValue,
26        exec<'a> AlgorithmIdentifierValue<'a>,
27        owned AlgorithmIdentifierValueOwned,
28    = Mapped {
29            inner: LengthWrapped(Depend {
30                fst: ASN1(ObjectIdentifier),
31                snd: AlgorithmParamCont,
32                spec_snd: Ghost(|i| AlgorithmParamCont::spec_apply(i)),
33            }),
34            mapper: AlgorithmIdentifierMapper,
35        };
36}
37
38asn1_tagged!(AlgorithmIdentifier, tag_of!(SEQUENCE));
39
40mapper! {
41    pub struct AlgorithmIdentifierMapper;
42
43    for <Id, Param>
44    from AlgorithmIdentifierFrom where type AlgorithmIdentifierFrom<Id, Param> = (Id, Param);
45    to AlgorithmIdentifierPoly where pub struct AlgorithmIdentifierPoly<Id, Param> {
46        pub id: Id,
47        pub param: Param,
48    }
49
50    spec SpecAlgorithmIdentifierValue with <SpecObjectIdentifierValue, SpecAlgorithmParamValue>;
51    exec AlgorithmIdentifierValue<'a> with <ObjectIdentifierValue, AlgorithmParamValue<'a>>;
52    owned AlgorithmIdentifierValueOwned with <ObjectIdentifierValueOwned, AlgorithmParamValueOwned>;
53
54    forward(x) {
55        AlgorithmIdentifierPoly {
56            id: x.0,
57            param: x.1,
58        }
59    }
60
61    backward(y) {
62        (y.id, y.param)
63    }
64}
65
66impl<'a> PolyfillEq for AlgorithmIdentifierValue<'a> {
67    fn polyfill_eq(&self, other: &Self) -> bool {
68        self.id.polyfill_eq(&other.id) &&
69        self.param.polyfill_eq(&other.param)
70    }
71}
72
73}
74
75#[cfg(test)]
76mod test {
77    use super::*;
78
79    verus! {
80        /// Check that all trait bounds and preconditions are satisfied
81        #[test]
82        fn is_combinator() {
83            let _ = ASN1(AlgorithmIdentifier).parse(&[]);
84        }
85    }
86
87    #[test]
88    fn sanity() {
89        assert!(ASN1(AlgorithmIdentifier)
90            .parse(&[
91                0x30, 0x0D, 0x06, 0x09, 0x2A, 0x86, 0x48, 0x86, 0xF7, 0x0D, 0x01, 0x01, 0x0C, 0x05,
92                0x00,
93            ])
94            .is_ok());
95    }
96}
verdict_parser/x509/alg_id.rs

verdict_parser/x509/
alg_id.rs
