Module cbordet

This module is an implementation of Deterministically Encoded CBOR (RFC 8949 Section 4.2.1) minus floating-point values, fully formally verified for functional correctness and absence of panics related to breach of abstraction, buffer overruns or arithmetic overflow/underflow. This module never allocates into the heap.

Structs

CborDetArray

The read-only type of Deterministic CBOR arrays. Values of this type cannot be manually constructed by the user, they are meant to be obtained only via cbor_det_destruct below. The abstraction is justified by the use of a refinement type, as per the definition of cbor_det_array in pulse/CBOR.Pulse.Det.API.Rust.fst

CborDetArrayIterator

The type of iterators over Deterministic CBOR arrays. It is made abstract since it is meant to be used with an implementation of the Iterator trait only.

CborDetMap

The read-only type of Deterministic CBOR maps. Values of this type cannot be manually constructed by the user, they are meant to be obtained only via cbor_det_destruct below. The abstraction is justified by the use of a refinement type, as per the definition of cbor_det_map in pulse/CBOR.Pulse.Det.API.Rust.fst

CborDetMapIterator

The type of iterators over Deterministic CBOR maps. It is made abstract since it is meant to be used with an implementation of the Iterator trait only.

Enums

CborDetIntKind

The kind of 64-bit integer: unsigned (to represent non-negative values), or negative (to represent negative values in two’s complement.)

CborDetView

A read-only view of a Deterministic CBOR object, as obtained by peeling the first layer of nesting via cbor_det_destruct below.

Functions

cbor_det_destruct

Destructs a Deterministic CBOR object by peeling its first layer of nesting. This function does not recursively descend into array or map payloads, and only reads the header of a tagged payload. As such, it consumes constant stack space. This function respects the UTF-8 well-formedness invariants.

cbor_det_equal

Compares Deterministic CBOR objects for semantic equality. This function consumes stack space linear in the maximum nesting of its two arguments.

cbor_det_get_array_item

Returns the ith element of the CBOR array x. Returns None if i is equal to or larger than the number of array elements, Some(object) otherwise.

cbor_det_get_array_length

Returns the number of elements in a Deterministic CBOR array.

cbor_det_get_map_length

Returns the number of elements in a Deterministic CBOR map.

cbor_det_map_entry_key

Read the key of a map entry.

cbor_det_map_entry_value

Read the value of a map entry.

cbor_det_map_get

Looks up a map x for an entry associated to the key k. If such an entry exists, returns Some(object) where object is the value associated to that key. Otherwise, returns None.

cbor_det_mk_array

Constructs a Deterministic CBOR of “array” type. This function does not copy its input array. It returns None if the input array has more than $2^64 - 1$ elements, Some(object) otherwise.

cbor_det_mk_byte_string

Constructs a Deterministic CBOR object of “byte string” type, with the contents of s as value. This function does not perform any copy of its input s. It returns None if the byte size of s is larger than $2^64 - 1$, Some(object) otherwise.

cbor_det_mk_int64

Constructs a Deterministic CBOR object of “integer” type, with kind ty and value v.

cbor_det_mk_map

Constructs a map from a slice of map entries. This function does not copy its input array. If the input slice has more than $2^64 - 1$ entries, then this function returns None and does not change the input slice. Otherwise, this function tries to sort the input slice in-place with respect to the key order specified in Section 4.2.1 of RFC 8949 (without actually serializing the map entries.) If the sorting detects duplicate keys, then this function returns None. Otherwise, it returns Some(object). Due to the sorting, this function consumes stack space logarithmic in the size of the input slice, and linear in the maximum nesting of map entry keys, and the function may have changed the order of map entries in the input slice.

cbor_det_mk_map_entry

Constructs a map entry from a key xk and a value xv.

cbor_det_mk_simple_value

Constructs a Deterministic CBOR object of “simple value” type, with value v. Returns None if the value v lies in the reserved range (24..31), as specified by Table 4 of RFC 8949 Section 3.3; Some(object) otherwise.

cbor_det_mk_tagged

Constructs a Deterministic CBOR object of Tagged type, with tag tag, and the contents of r as value. This function does not perform any copy of its input r.

cbor_det_mk_text_string

Constructs a Deterministic CBOR object of “text string” type, with the contents of s as value. This function does not perform any copy of its input s. It returns None if the byte size of s is larger than $2^64 - 1$, Some(object) otherwise. This function respects the UTF-8 well-formedness invariants.

cbor_det_parse

Tries to parse a Deterministic CBOR object from the first bytes of input, following RFC 8949 Section 4.2.1, minus floating-point values. Returns None in case of failure, or Some(object, rem) in case of success, where rem is the remainder of the input slice past those first bytes of input that contain the valid binary representation of input. This function does not perform a deep parse of input, it only copies the object type, tag and/or size of the top-most object. As such, it uses constant stack space (including data validation.) “Destructor” functions are to be used on the returned object, to examine each level of nesting one at a time. NOTE: This implementation checks for the basic validity constraints of Section 5.3.1, i.e. the absence of duplicate map keys (which is a consequence of the deterministic encoding.), and the well-formedness of UTF-8 text strings.

cbor_det_serialize

Writes the binary representation of the Deterministic CBOR object x into the first bytes of the output byte slice, following RFC 8949 Section 4.2.1. This function first checks the size of x and returns None if it is larger than the size of output; otherwise it returns Some(size), where size is the byte size of x, the number of bytes written to output. This function uses stack space in the order of the level of nesting of the use of “constructor” functions used to build x; the serialization of those “subobjects” of x obtained from cbor_det_parse uses only constant extra stack space for each such subobject (in the sense that the serialization does not recursively nest into such subobjects.)

cbor_det_size

Computes the byte size of the binary representation of the Deterministic CBOR object x following RFC 8949 Section 4.2.1, but without serializing x. Returns None if that size is strictly larger than bound; Some(size) otherwise. This function uses stack space in the order of the level of nesting of the use of “constructor” functions used to build x; the computation of the sizes of those “subobjects” of x obtained from cbor_det_parse uses only constant extra stack space for each such subobject (in the sense that the computation does not recursively nest into such subobjects.)

Type Aliases

CborDet

An abstract type to represent a Deterministic CBOR object, which can be obtained either using “constructor” functions of this module, or by parsing from serialized data. Declared in pulse/CBOR.Pulse.Det.API.Rust.fsti. Its corresponding pure (“mathematical”) functional specification is the cbor type in spec/CBOR.Spec.Type.fsti.

CborDetMapEntry

The type of key-value map entries.