cborrs

Module cbordet

Source
Expand description

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.