verdict_parser/x509/
validity.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6// In X.509:
7// Validity ::= SEQUENCE {
8//     notBefore      Time,
9//     notAfter       Time,
10// }
11asn1! {
12    seq Validity {
13        not_before: Time = Time,
14        not_after: Time = Time,
15    }
16}
17
18}
19
20#[cfg(test)]
21mod test {
22    use super::*;
23
24    verus! {
25        /// Check that all trait bounds and preconditions are satisfied
26        #[test]
27        fn is_combinator() {
28            let _ = ASN1(Validity).parse(&[]);
29        }
30    }
31
32    #[test]
33    fn sanity() {
34        assert!(ASN1(Validity)
35            .parse(&[
36                0x30, 0x1E, 0x17, 0x0D, 0x31, 0x36, 0x30, 0x32, 0x30, 0x34, 0x31, 0x32, 0x33, 0x32,
37                0x32, 0x33, 0x5A, 0x17, 0x0D, 0x33, 0x34, 0x31, 0x32, 0x33, 0x31, 0x31, 0x37, 0x32,
38                0x36, 0x33, 0x39, 0x5A,
39            ])
40            .is_ok());
41    }
42}