cborrs/
cbordet.rs

1/* FIXME: This module to be rewritten with `pub use crate::cbordetver`,
2 * once Karamel can extract Rust code with documentation (coming from
3 * FStar attributes), abstract types, references instead of one-sized
4 * slices, proper casing of type names, and native Rust
5 * `std::Option`. */
6//! This module is an implementation of Deterministically Encoded CBOR
7//! (RFC 8949 Section 4.2.1) minus floating-point values, fully
8//! formally verified for functional correctness and absence of panics
9//! related to breach of abstraction, buffer overruns or arithmetic
10//! overflow/underflow. This module never allocates into the heap.
11
12/* FIXME: `cbordet` to be defined as abstract in cbordetveraux
13 * already. I cannot abstract it here since `cbor_det_mk_tagged`,
14 * `cbor_det_mk_array` and `cbor_det_mk_map` use references and arrays
15 * of `cbordet` elements as input arguments.
16 */
17/// An abstract type to represent a Deterministic CBOR object, which
18/// can be obtained either using "constructor" functions of this
19/// module, or by parsing from serialized data. Declared in
20/// `pulse/CBOR.Pulse.Det.API.Rust.fsti`. Its corresponding pure
21/// ("mathematical") functional specification is the `cbor` type in
22/// `spec/CBOR.Spec.Type.fsti`.
23pub type CborDet <'a> = crate::cbordetver::cbordet <'a>;
24
25/// Tries to parse a Deterministic CBOR object from the first bytes of
26/// `input`, following RFC 8949 Section 4.2.1, minus floating-point
27/// values. Returns `None` in case of failure, or `Some(object, rem)`
28/// in case of success, where `rem` is the remainder of the input
29/// slice past those first bytes of `input` that contain the valid
30/// binary representation of
31/// `input`. This function does not perform a deep parse of `input`,
32/// it only copies the object type, tag and/or size of the top-most
33/// object. As such, it uses constant stack space (including data
34/// validation.) "Destructor" functions are to be used on the returned
35/// object, to examine each level of nesting one at a time. NOTE: This
36/// implementation checks for the basic validity constraints of
37/// Section 5.3.1, i.e. the absence of duplicate map keys (which is a
38/// consequence of the deterministic encoding.), and the
39/// well-formedness of UTF-8 text strings.
40pub fn cbor_det_parse <'a>(input: &'a [u8]) ->
41    Option<(CborDet<'a>, &'a [u8])>
42{
43    match crate::cbordetver::cbor_det_parse(input) {
44	crate::cbordetver::option__·CBOR_Pulse_Raw_Type_cbor_raw···Pulse_Lib_Slice_slice·uint8_t·::None => {
45	    return None;
46	}
47	crate::cbordetver::option__·CBOR_Pulse_Raw_Type_cbor_raw···Pulse_Lib_Slice_slice·uint8_t·::Some {v} => {
48	    let (object, rem) = v;
49	    return Some((object, rem));
50	}
51    }
52}
53
54/// Computes the byte size of the binary representation of the
55/// Deterministic CBOR object `x` following RFC 8949 Section 4.2.1,
56/// but without serializing `x`. Returns `None` if that size is
57/// strictly larger than `bound`; `Some(size)` otherwise. This function
58/// uses stack space in the order of the level of nesting of the use
59/// of "constructor" functions used to build `x`; the computation of
60/// the sizes of those "subobjects" of `x` obtained from
61/// `cbor_det_parse` uses only constant extra stack space for each
62/// such subobject (in the sense that the computation does not
63/// recursively nest into such subobjects.)
64pub fn cbor_det_size <'a>(x: CborDet <'a>, bound: usize) -> Option<usize>
65{
66    match crate::cbordetver::cbor_det_size(x, bound) {
67	crate::cbordetver::option__size_t::None => {
68	    return None;
69	}
70	crate::cbordetver::option__size_t::Some {v} => {
71	    return Some(v);
72	}
73    }
74}
75
76/// Writes the binary representation of the Deterministic CBOR object
77/// `x` into the first bytes of the `output` byte slice, following RFC
78/// 8949 Section 4.2.1. This function first checks the size of `x` and
79/// returns `None` if it is larger than the size of `output`;
80/// otherwise it returns `Some(size)`, where `size` is the byte size
81/// of `x`, the number of bytes written to `output`. This function
82/// uses stack space in the order of the level of nesting of the use
83/// of "constructor" functions used to build `x`; the serialization of
84/// those "subobjects" of `x` obtained from `cbor_det_parse` uses only
85/// constant extra stack space for each such subobject (in the sense
86/// that the serialization does not recursively nest into such
87/// subobjects.)
88pub fn cbor_det_serialize <'a>(x: CborDet <'a>, output: &'a mut [u8]) ->
89    Option<usize>
90{
91    match crate::cbordetver::cbor_det_serialize(x, output) {
92	crate::cbordetver::option__size_t::None => {
93	    return None;
94	}
95	crate::cbordetver::option__size_t::Some {v} => {
96	    return Some(v);
97	}
98    }
99}
100
101/// Constructs a Deterministic CBOR object of "simple value" type,
102/// with value `v`. Returns `None` if the value `v` lies in the
103/// reserved range (`24..31`), as specified by Table 4 of RFC 8949
104/// Section 3.3; `Some(object)` otherwise.
105pub fn cbor_det_mk_simple_value <'a>(v: u8) -> Option<CborDet<'a>>
106{
107    match crate::cbordetver::cbor_det_mk_simple_value(v) {
108	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::None => {
109	    return None;
110	}
111	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::Some {v} => {
112	    return Some(v);
113	}
114    }
115}
116
117/// The kind of 64-bit integer: unsigned (to represent non-negative
118/// values), or negative (to represent negative values in two's
119/// complement.)
120#[derive(PartialEq, Clone, Copy)]
121pub enum CborDetIntKind
122{
123    UInt64,
124    NegInt64
125}
126
127/// Constructs a Deterministic CBOR object of "integer" type, with
128/// kind `ty` and value `v`.
129pub fn cbor_det_mk_int64 <'a>(ty: CborDetIntKind, v: u64) ->
130    CborDet <'a>
131{
132    let ty· : crate::cbordetver::cbor_det_int_kind =
133	match ty {
134	    CborDetIntKind::UInt64 => {
135		crate::cbordetver::cbor_det_int_kind::UInt64
136	    }
137	    CborDetIntKind::NegInt64 => {
138		crate::cbordetver::cbor_det_int_kind::NegInt64
139	    }
140	};
141    crate::cbordetver::cbor_det_mk_int64(ty·, v)
142}
143
144/// Constructs a Deterministic CBOR object of "text string" type, with
145/// the contents of `s` as value. This function does not perform any
146/// copy of its input `s`. It returns `None` if the byte size of `s`
147/// is larger than $2^64 - 1$, `Some(object)` otherwise. This function
148/// respects the UTF-8 well-formedness invariants.
149pub fn cbor_det_mk_text_string <'a>(s: &'a str) ->
150    Option<CborDet<'a>>
151{
152    let ty· : crate::cbordetver::cbor_det_string_kind =
153	crate::cbordetver::cbor_det_string_kind::TextString;
154    match crate::cbordetver::cbor_det_mk_string(ty·, s.as_bytes()) {
155	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::None => {
156	    None
157	}
158	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::Some { v } => {
159	    Some(v)
160	}
161    }
162}
163
164/// Constructs a Deterministic CBOR object of "byte string" type, with
165/// the contents of `s` as value. This function does not perform any
166/// copy of its input `s`. It returns `None` if the byte size of `s`
167/// is larger than $2^64 - 1$, `Some(object)` otherwise.
168pub fn cbor_det_mk_byte_string <'a>(s: &'a [u8]) ->
169    Option<CborDet<'a>>
170{
171    let ty· : crate::cbordetver::cbor_det_string_kind =
172	crate::cbordetver::cbor_det_string_kind::ByteString;
173    match crate::cbordetver::cbor_det_mk_string(ty·, s) {
174	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::None => {
175	    None
176	}
177	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::Some { v } => {
178	    Some(v)
179	}
180    }
181}
182
183/* FIXME: this function to be extracted with references instead of
184 * slices. The verified FStar/Pulse code is already using references,
185 * but Karamel extracts them as slices. Because of that, I need to
186 * manually write this piece of glue code to convert a reference into
187 * a slice, which Karamel cannot extract (and FStar/Pulse cannot
188 * currently model.)
189 */
190/// Constructs a Deterministic CBOR object of Tagged type, with tag
191/// `tag`, and the contents of `r` as value. This function does not
192/// perform any copy of its input `r`.
193pub fn cbor_det_mk_tagged <'a>(tag: u64, r: &'a CborDet <'a>) ->
194    CborDet <'a>
195{
196    return crate::cbordetver::cbor_det_mk_tagged(tag, std::slice::from_ref(r));
197}
198
199/// Constructs a Deterministic CBOR of "array" type. This function
200/// does not copy its input array. It returns `None` if the input
201/// array has more than $2^64 - 1$ elements, `Some(object)` otherwise.
202pub fn cbor_det_mk_array <'a>(a: &'a [CborDet <'a>]) ->
203    Option<CborDet<'a>>
204{
205    match crate::cbordetver::cbor_det_mk_array(a) {
206	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::None => {
207	    None
208	}
209	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::Some {v} => {
210	    Some(v)
211	}
212    }
213}
214
215/* FIXME: this type to be defined as abstract in cbordetveraux
216 * already. I cannot abstract it here since `cbor_det_mk_map` uses
217 * arrays of map entry elements as input arguments.
218 */
219/// The type of key-value map entries.
220pub type CborDetMapEntry <'a> = crate::cbordetveraux::cbor_map_entry <'a>;
221
222/// Constructs a map entry from a key `xk` and a value `xv`.
223pub fn cbor_det_mk_map_entry <'a>(
224    xk: CborDet <'a>,
225    xv: CborDet <'a>
226) ->
227    CborDetMapEntry <'a>
228{
229    return crate::cbordetver::cbor_det_mk_map_entry(xk, xv);
230}
231
232/// Constructs a map from a slice of map entries. This function does
233/// not copy its input array. If the input slice has more than $2^64 -
234/// 1$ entries, then this function returns `None` and does not change
235/// the input slice. Otherwise, this function tries to sort the input
236/// slice in-place with respect to the key order specified in Section
237/// 4.2.1 of RFC 8949 (without actually serializing the map entries.)
238/// If the sorting detects duplicate keys, then this function returns
239/// `None`. Otherwise, it returns `Some(object)`. Due to the sorting,
240/// this function consumes stack space logarithmic in the size of the
241/// input slice, and linear in the maximum nesting of map entry keys,
242/// and the function may have changed the order of map entries in the
243/// input slice.
244pub fn cbor_det_mk_map <'a>(a: &'a mut [CborDetMapEntry <'a>]) ->
245    Option<CborDet<'a>>
246{
247    match crate::cbordetver::cbor_det_mk_map(a) {
248	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::None => {
249	    None
250	}
251	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::Some {v} => {
252	    Some(v)
253	}
254    }
255}
256
257/// Compares Deterministic CBOR objects for semantic equality. This
258/// function consumes stack space linear in the maximum nesting of its
259/// two arguments.
260pub fn cbor_det_equal <'a>(
261    x1: CborDet <'a>,
262    x2: CborDet <'a>
263) ->
264    bool
265{
266    crate::cbordetver::cbor_det_equal(x1, x2)
267}
268
269/// The read-only type of Deterministic CBOR arrays. Values of this
270/// type cannot be manually constructed by the user, they are meant to
271/// be obtained only via `cbor_det_destruct` below. The abstraction is
272/// justified by the use of a refinement type, as per the definition
273/// of `cbor_det_array` in `pulse/CBOR.Pulse.Det.API.Rust.fst`
274#[derive(PartialEq, Clone, Copy)]
275pub struct CborDetArray <'a> { array: crate::cbordetver::cbor_det_array <'a> }
276
277/// The read-only type of Deterministic CBOR maps. Values of this
278/// type cannot be manually constructed by the user, they are meant to
279/// be obtained only via `cbor_det_destruct` below. The abstraction is
280/// justified by the use of a refinement type, as per the definition
281/// of `cbor_det_map` in `pulse/CBOR.Pulse.Det.API.Rust.fst`
282#[derive(PartialEq, Clone, Copy)]
283pub struct CborDetMap <'a> { map: crate::cbordetver::cbor_det_map <'a> }
284
285/// A read-only view of a Deterministic CBOR object, as obtained by
286/// peeling the first layer of nesting via `cbor_det_destruct` below.
287#[derive(PartialEq, Clone, Copy)]
288pub enum CborDetView <'a>
289{
290    Int64 { kind: CborDetIntKind, value: u64 },
291    ByteString { payload: &'a [u8] },
292    TextString { payload: &'a str },
293    Array { _0: CborDetArray <'a> },
294    Map { _0: CborDetMap <'a> },
295    Tagged { tag: u64, payload: CborDet <'a> },
296    SimpleValue { _0: u8 }
297}
298
299/// Destructs a Deterministic CBOR object by peeling its first layer
300/// of nesting. This function does not recursively descend into array
301/// or map payloads, and only reads the header of a tagged payload. As
302/// such, it consumes constant stack space. This function respects the
303/// UTF-8 well-formedness invariants.
304pub fn cbor_det_destruct <'a>(c: CborDet <'a>) -> CborDetView <'a>
305{
306    match crate::cbordetver::cbor_det_destruct(c) {
307	crate::cbordetver::cbor_det_view::Int64 { kind, value } => {
308	    let kind· : CborDetIntKind =
309		match kind {
310		    crate::cbordetver::cbor_det_int_kind::UInt64 => {
311			CborDetIntKind::UInt64
312		    }
313		    crate::cbordetver::cbor_det_int_kind::NegInt64 => {
314			CborDetIntKind::NegInt64
315		    }
316		};
317	    CborDetView::Int64 {kind: kind·, value}
318	}
319	crate::cbordetver::cbor_det_view::String { kind, payload } => {
320	    match kind {
321		crate::cbordetver::cbor_det_string_kind::ByteString => {
322		    CborDetView::ByteString {payload}
323		}
324		crate::cbordetver::cbor_det_string_kind::TextString => {
325		    CborDetView::TextString {payload: std::str::from_utf8(payload).unwrap()}
326		}
327	    }
328	}
329	crate::cbordetver::cbor_det_view::Array { _0 } => {
330	    CborDetView::Array { _0: CborDetArray {array: _0 } }
331	}
332	crate::cbordetver::cbor_det_view::Map { _0 } => {
333	    CborDetView::Map { _0: CborDetMap {map: _0 } }
334	}
335	crate::cbordetver::cbor_det_view::Tagged { tag, payload } => {
336	    CborDetView::Tagged {tag, payload}
337	}
338	crate::cbordetver::cbor_det_view::SimpleValue { _0 } => {
339	    CborDetView::SimpleValue {_0}
340	}
341    }
342}
343
344/// Returns the number of elements in a Deterministic CBOR array.
345pub fn cbor_det_get_array_length <'a>(x: CborDetArray <'a>) -> u64
346{
347    crate::cbordetver::cbor_det_get_array_length(x.array)
348}
349
350/// The type of iterators over Deterministic CBOR arrays. It is made
351/// abstract since it is meant to be used with an implementation of
352/// the `Iterator` trait only.
353pub struct CborDetArrayIterator <'a> { iter: crate::cbordetveraux::cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_raw <'a> }
354
355impl <'a> Iterator for CborDetArrayIterator <'a> {
356    type Item = CborDet <'a>;
357    fn next(&mut self) -> Option<Self::Item> {
358	if crate::cbordetver::cbor_det_array_iterator_is_empty(self.iter) {
359	    None
360	} else {
361	    Some (crate::cbordetver::cbor_det_array_iterator_next(std::slice::from_mut(& mut self.iter)))
362	}
363    }
364}
365
366impl <'a> IntoIterator for CborDetArray <'a> {
367    type Item = CborDet <'a>;
368    type IntoIter = CborDetArrayIterator <'a>;
369    fn into_iter(self) -> Self::IntoIter {
370	CborDetArrayIterator { iter: crate::cbordetver::cbor_det_array_iterator_start(self.array) }
371    }
372}
373
374/// Returns the `i`th element of the CBOR array `x`. Returns `None` if
375/// `i` is equal to or larger than the number of array elements,
376/// `Some(object)` otherwise.
377pub fn cbor_det_get_array_item <'a>(x: CborDetArray <'a>, i: u64) ->
378    Option<CborDet<'a>>
379{
380    match crate::cbordetver::cbor_det_get_array_item(x.array, i) {
381	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::None => {
382	    None
383	}
384	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::Some {v} => {
385	    Some(v)
386	}
387    }
388}
389
390/// Returns the number of elements in a Deterministic CBOR map.
391pub fn cbor_det_get_map_length <'a>(x: CborDetMap <'a>) -> u64
392{
393    crate::cbordetver::cbor_det_map_length(x.map)
394}
395
396/// The type of iterators over Deterministic CBOR maps. It is made
397/// abstract since it is meant to be used with an implementation of
398/// the `Iterator` trait only.
399pub struct CborDetMapIterator <'a> { iter: crate::cbordetveraux::cbor_raw_iterator__CBOR_Pulse_Raw_Type_cbor_map_entry <'a> }
400
401impl <'a> Iterator for CborDetMapIterator <'a> {
402    type Item = CborDetMapEntry <'a>;
403    fn next(&mut self) -> Option<Self::Item> {
404	if crate::cbordetver::cbor_det_map_iterator_is_empty(self.iter) {
405	    None
406	} else {
407	    Some (crate::cbordetver::cbor_det_map_iterator_next(std::slice::from_mut(& mut self.iter)))
408	}
409    }
410}
411
412impl <'a> IntoIterator for CborDetMap <'a> {
413    type Item = CborDetMapEntry <'a>;
414    type IntoIter = CborDetMapIterator <'a>;
415    fn into_iter(self) -> Self::IntoIter {
416	CborDetMapIterator { iter: crate::cbordetver::cbor_det_map_iterator_start(self.map) }
417    }
418}
419
420/// Read the key of a map entry.
421pub fn cbor_det_map_entry_key <'a>(x2: CborDetMapEntry <'a>) ->
422    CborDet
423    <'a>
424{ crate::cbordetver::cbor_det_map_entry_key(x2) }
425
426/// Read the value of a map entry.
427pub fn cbor_det_map_entry_value <'a>(x2: CborDetMapEntry <'a>) ->
428    CborDet
429    <'a>
430{ crate::cbordetver::cbor_det_map_entry_value(x2) }
431
432/// Looks up a map `x` for an entry associated to the key `k`. If such
433/// an entry exists, returns `Some(object)` where `object` is the
434/// value associated to that key. Otherwise, returns `None`.
435pub fn cbor_det_map_get <'a>(
436    x: CborDetMap <'a>,
437    k: CborDet <'a>
438) ->
439    Option<CborDet<'a>>
440{
441    match crate::cbordetver::cbor_det_map_get(x.map, k) {
442	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::None => {
443	    None
444	}
445	crate::cbordetver::option__CBOR_Pulse_Raw_Type_cbor_raw::Some {v} => {
446	    Some(v)
447	}
448    }
449}
cborrs/cbordet.rs

cborrs/
cbordet.rs
