vest_lib 0.2.2

Verified parser and serializer combinators in Verus
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136

//! Predicate refinement and constant-value formats.
//!
//! [`Refined`] keeps only values satisfying a predicate. [`Const`] fixes that value and is commonly used for static tags or discriminants.
/// Executable trait implementations for this combinator.
pub mod exec;
/// Correctness proofs for this combinator.
pub mod proof;
/// Specification trait implementations for this combinator.
pub mod spec;

use vstd::prelude::*;

use super::{Preceded, Terminated};

verus! {

/// Value refinement combinator: filters values through a predicate.
///
/// ## Consistency
///
/// `inner.consistent(v) && predicate.apply(v)`.
#[derive(Copy)]
pub struct Refined<Inner, Predicate>(pub Inner, pub Predicate);

impl<Inner: Clone, Predicate: Clone> Clone for Refined<Inner, Predicate> {
    fn clone(&self) -> (cloned: Self)
        ensures
            call_ensures(Inner::clone, (&self.0,), cloned.0),
            call_ensures(Predicate::clone, (&self.1,), cloned.1),
    {
        Refined(self.0.clone(), self.1.clone())
    }
}

/// Constant-value combinator: matches a specific constant value.
///
/// Parsing semantics: parses with `inner` and succeeds only if the result equals the expected value.
/// The matched constant value itself is returned.
///
/// Implements [`AdmitsUniqueVal`](crate::core::spec::AdmitsUniqueVal).
#[derive(Copy)]
pub struct Const<Inner, Value>(pub Inner, pub Value);

impl<Inner: Clone, Value: Clone> Clone for Const<Inner, Value> {
    fn clone(&self) -> (cloned: Self)
        ensures
            call_ensures(Inner::clone, (&self.0,), cloned.0),
            call_ensures(Value::clone, (&self.1,), cloned.1),
    {
        Const(self.0.clone(), self.1.clone())
    }
}

// #[allow(type_alias_bounds)]
// pub type PrefixTagged<TagFmt: SpecByteLen, Of, Tag = <TagFmt as SpecByteLen>::T> = Preceded<
//     Const<TagFmt, Tag>,
//     Tag,
//     Of,
//     false,
// >;
// #[allow(type_alias_bounds)]
// pub type SuffixTagged<Of, TagFmt: SpecByteLen, Tag = <TagFmt as SpecByteLen>::T> = Terminated<
//     Of,
//     Const<TagFmt, Tag>,
//     Tag,
//     false,
// >;
// #[allow(non_snake_case)]
// #[verifier::allow_in_spec]
// pub fn PrefixTagged<TagFmt, Of, Tag>(tag_fmt: TagFmt, tag: Tag, body: Of) -> PrefixTagged<
//     TagFmt,
//     Of,
//     Tag,
// > where TagFmt: SpecByteLen, Tag: Copy
//     returns
//         (Preceded::<Const<TagFmt, Tag>, Tag, Of, false> {
//             a: Const(tag_fmt, tag),
//             a_val: tag,
//             b: body,
//         }),
// {
//     let a = Const(tag_fmt, tag);
//     let b = body;
//     let a_val = tag;
//     Preceded { a, a_val, b }
// }
// #[allow(non_snake_case)]
// #[verifier::allow_in_spec]
// pub fn SuffixTagged<Of, TagFmt, Tag>(body: Of, tag_fmt: TagFmt, tag: Tag) -> SuffixTagged<
//     Of,
//     TagFmt,
//     Tag,
// > where TagFmt: SpecByteLen, Tag: Copy
//     returns
//         (Terminated::<Of, Const<TagFmt, Tag>, Tag, false> {
//             a: body,
//             b: Const(tag_fmt, tag),
//             b_val: tag,
//         }),
// {
//     let a = body;
//     let b = Const(tag_fmt, tag);
//     let b_val = tag;
//     Terminated { a, b, b_val }
// }
/// Sugar for `Preceded { a: Const(inner, tag), a_val: tag, b: body }`.
#[derive(Copy)]
pub struct PrefixTagged<Tg, Tag, Of>(pub Tg, pub Tag, pub Of);

impl<Tg: Clone, Tag: Clone, Of: Clone> Clone for PrefixTagged<Tg, Tag, Of> {
    fn clone(&self) -> (cloned: Self)
        ensures
            call_ensures(Tg::clone, (&self.0,), cloned.0),
            call_ensures(Tag::clone, (&self.1,), cloned.1),
            call_ensures(Of::clone, (&self.2,), cloned.2),
    {
        PrefixTagged(self.0.clone(), self.1.clone(), self.2.clone())
    }
}

/// Sugar for `Terminated { a: body, b: Const(inner, tag), b_val: tag }`.
#[derive(Copy)]
pub struct SuffixTagged<Of, Tg, Tag>(pub Of, pub Tg, pub Tag);

impl<Of: Clone, Tg: Clone, Tag: Clone> Clone for SuffixTagged<Of, Tg, Tag> {
    fn clone(&self) -> (cloned: Self)
        ensures
            call_ensures(Of::clone, (&self.0,), cloned.0),
            call_ensures(Tg::clone, (&self.1,), cloned.1),
            call_ensures(Tag::clone, (&self.2,), cloned.2),
    {
        SuffixTagged(self.0.clone(), self.1.clone(), self.2.clone())
    }
}

} // verus!