vest_lib/cbor/
value.rs

1//! Generic CBOR values and their specification views.
2use alloc::{boxed::Box, string::String, vec::Vec};
3use vstd::assert_seqs_equal;
4use vstd::prelude::*;
5
6verus! {
7
8/// A CBOR floating-point payload.
9///
10/// Width and raw IEEE 754 bits are retained.
11/// A future deterministic floating-point layer can define and verify
12/// shortest-width equivalence without changing the wire-facing value type.
13#[derive(Debug, Clone, Copy, PartialEq, Eq, Structural)]
14pub enum CborFloat {
15    F16(u16),
16    F32(u32),
17    F64(u64),
18}
19
20impl DeepView for CborFloat {
21    type V = Self;
22
23    open spec fn deep_view(&self) -> Self::V {
24        *self
25    }
26}
27
28/// Runtime representation of a CBOR byte string.
29#[verifier::allow(autoderive_clone_without_spec)]
30#[derive(Debug, Clone, PartialEq, Eq)]
31pub enum CborBytes<'i> {
32    /// A definite-length string borrowed directly from the input.
33    Definite(&'i [u8]),
34    /// Flattened contents of an indefinite-length, fragmented string.
35    Indefinite(Vec<u8>),
36}
37
38impl<'i> DeepView for CborBytes<'i> {
39    type V = Seq<u8>;
40
41    open spec fn deep_view(&self) -> Self::V {
42        match self {
43            Self::Definite(bytes) => bytes.deep_view(),
44            Self::Indefinite(bytes) => bytes.deep_view(),
45        }
46    }
47}
48
49/// Runtime representation of a CBOR text string.
50#[verifier::allow(autoderive_clone_without_spec)]
51#[derive(Debug, Clone, PartialEq, Eq)]
52pub enum CborText<'i> {
53    /// A definite-length UTF-8 string borrowed directly from the input.
54    Definite(&'i str),
55    /// Flattened contents of an indefinite-length, fragmented string.
56    Indefinite(String),
57}
58
59impl<'i> DeepView for CborText<'i> {
60    type V = Seq<char>;
61
62    open spec fn deep_view(&self) -> Self::V {
63        match self {
64            Self::Definite(text) => text.deep_view(),
65            Self::Indefinite(text) => text.deep_view(),
66        }
67    }
68}
69
70/// Runtime representation of a CBOR array.
71pub type CborArray<'i> = Vec<CborValue<'i>>;
72
73/// Runtime representation of a CBOR map.
74///
75/// Entries retain wire order and duplicate entries are preserved. This codec
76/// recognizes well-formed CBOR; applications that require RFC 8949 basic
77/// validity must additionally reject duplicate keys (section 5.3.1).
78pub type CborMap<'i> = Vec<(CborValue<'i>, CborValue<'i>)>;
79
80/// Generic CBOR value.
81#[derive(Debug, PartialEq, Eq)]
82pub enum CborValue<'i> {
83    /// An integer in the RFC 8949 range `-2^64 ..= 2^64 - 1`.
84    Integer(i128),
85    Bytes(CborBytes<'i>),
86    Text(CborText<'i>),
87    Array(CborArray<'i>),
88    Map(CborMap<'i>),
89    Tag(u64, Box<CborValue<'i>>),
90    Float(CborFloat),
91    Bool(bool),
92    Null,
93    Undefined,
94    /// An unassigned/registered simple value other than 20 through 23.
95    Simple(u8),
96}
97
98/// Logical value used by CBOR specifications.
99///
100/// Definite/indefinite framing is erased, matching the RFC generic data model.
101/// Floating-point width is retained.
102pub enum CborValueSpec {
103    Integer(i128),
104    Bytes(Seq<u8>),
105    Text(Seq<char>),
106    Array(Seq<CborValueSpec>),
107    Map(Seq<(CborValueSpec, CborValueSpec)>),
108    Tag(u64, Box<CborValueSpec>),
109    Float(CborFloat),
110    Bool(bool),
111    Null,
112    Undefined,
113    Simple(u8),
114}
115
116pub open spec fn cbor_value_view(value: &CborValue) -> CborValueSpec
117    decreases *value,
118{
119    match value {
120        CborValue::Integer(value) => CborValueSpec::Integer(*value),
121        CborValue::Bytes(value) => CborValueSpec::Bytes(value.deep_view()),
122        CborValue::Text(value) => CborValueSpec::Text(value.deep_view()),
123        CborValue::Array(values) => {
124            let seq = values@;
125            CborValueSpec::Array(
126                Seq::new(
127                    seq.len(),
128                    |i: int|
129                        {
130                            if 0 <= i < seq.len() {
131                                cbor_value_view(&seq[i])
132                            } else {
133                                arbitrary()
134                            }
135                        },
136                ),
137            )
138        },
139        CborValue::Map(values) => {
140            let seq = values@;
141            CborValueSpec::Map(
142                Seq::new(
143                    seq.len(),
144                    |i: int|
145                        {
146                            if 0 <= i < seq.len() {
147                                (cbor_value_view(&seq[i].0), cbor_value_view(&seq[i].1))
148                            } else {
149                                arbitrary()
150                            }
151                        },
152                ),
153            )
154        },
155        CborValue::Tag(tag, value) => {
156            CborValueSpec::Tag(*tag, Box::new(cbor_value_view(&**value)))
157        },
158        CborValue::Float(value) => CborValueSpec::Float(*value),
159        CborValue::Bool(value) => CborValueSpec::Bool(*value),
160        CborValue::Null => CborValueSpec::Null,
161        CborValue::Undefined => CborValueSpec::Undefined,
162        CborValue::Simple(value) => CborValueSpec::Simple(*value),
163    }
164}
165
166impl<'i> DeepView for CborValue<'i> {
167    type V = CborValueSpec;
168
169    open spec fn deep_view(&self) -> Self::V {
170        cbor_value_view(self)
171    }
172}
173
174/// Connects the explicit structurally-recursive collection view above to the
175/// standard `Vec<T>::deep_view` used by executable repeat combinators.
176pub proof fn lemma_collection_value_view(value: &CborValue)
177    ensures
178        match value {
179            CborValue::Array(values) => {
180                cbor_value_view(value) == CborValueSpec::Array(values.deep_view())
181            },
182            CborValue::Map(entries) => {
183                cbor_value_view(value) == CborValueSpec::Map(entries.deep_view())
184            },
185            _ => true,
186        },
187    decreases *value,
188{
189    match value {
190        CborValue::Array(values) => {
191            let viewed = cbor_value_view(value);
192            let actual = match viewed {
193                CborValueSpec::Array(s) => s,
194                _ => arbitrary(),
195            };
196            assert_seqs_equal!(actual, values.deep_view(), i => {});
197            assert(viewed == CborValueSpec::Array(actual));
198        },
199        CborValue::Map(entries) => {
200            let viewed = cbor_value_view(value);
201            let actual = match viewed {
202                CborValueSpec::Map(s) => s,
203                _ => arbitrary(),
204            };
205            assert_seqs_equal!(actual, entries.deep_view(), i => {});
206            assert(viewed == CborValueSpec::Map(actual));
207        },
208        _ => {},
209    }
210}
211
212} // verus!
vest_lib/cbor/value.rs

vest_lib/cbor/
value.rs
