So far EverCBOR only supported the deterministic encoding of CBOR (IETF RFC 8979 Section 4.2.1.)

This PR introduces CBORNondet, a verified CBOR parsing and serialization library supporting definite-length non-deterministic encoding of CBOR. As a major contribution, CBORNondet checks for map key duplicates in the basic data model, using an amount of stack proportional to the nesting of maps in map entry keys. The user can specify such a bound when calling the CBORNondet parser.

This PR introduces a safe C API for CBORNondet, with as few preconditions as possible: liveness of pointers (but not necessarily the fact that they are not null), consistency of array lengths, and data invariant on values of CBOR object type, but nothing more. In particular, CBORNondet accessor functions no longer require a specific major type on the CBOR object being accessed: for instance, cbor_nondet_map_iterator_start will gracefully fail if applied to a non-map CBOR object.

TODO:

• C snapshot in src/cbor/pulse/nondet/c
• Rust snapshot
• Merge ArrayPtr: support for null pointer, converting from ref FStarLang/pulse#500, which is critical for the safe C API
• Reuse the safe C API in CBORDet: Reuse the safe C API for CBORDet #250
• Support for retrieving several map entries into an array with one pass on a map (cf. unverified implementation in https://github.com/tahina-pro/CCF/blob/0fc73c6ddac9ebd3f0a74a3f31e3eda6c91d3e82/src/node/uvm_endorsements.cpp#L20-L49 )
• Allow computing the size of an object before serializing it. Contrary to the deterministic encoding, one can no longer rely on an accurate size function on CBOR objects, but a maximum size function, and a separation logic predicate for the actual size.
• Connect with EverCDDL: Connect EverCDDL and CBORNondet #251. so far the EverCDDL parsing side is agnostic to the CBOR implementation, so instantiating it to CBORNondet should be fine; but the EverCDDL serialization side is currently tied to the deterministic encoding and must be generalized. Such generalization is expected to remove the few admits remaining in Upgrade to F* Universes #244

More hypothetical:

• Allow use of CBORDet objects in CBORNondet. This might be necessary for COSE, but we are not sure yet. Note that we do not intend to implement full determinization of CBORNondet objects, because this is not reasonably implementable in constant stack space (thus, we do not intend to support using CBORNondet objects in CBORDet.)
• Add support for floating-point values. This is contingent on ongoing IETF CBOR working group discussions about equivalence of NaNs for the purpose of map key comparisons, which are not fully standardized yet.
• Add support for extended data models, such as big integers including the domain of regular integers. CBOR.Spec.Raw.Valid.fsti and CBOR.Spec.Raw.Nondet.fst are generic in the data model, but their implementations CBOR.Pulse.Raw.Nondet.Compare.fst and CBOR.Spec.Raw.fst only support the basic data model.