C data types (structs, unions, arrays) for Steel

[john-ml]

This PR adds:

• Steel.C.Connection: PCM morphisms and PCM connections, which are a generic way of relating a PCM for a part of a structure to a PCM for the whole structure.
• Steel.C.Ref: definitions for fundamental operations (read, write, split, gather) on references that additionally support an operation for "focusing" on a part of a whole via a PCM connection.
• Steel.C.Reference: a model of non-nullable C pointers for Steel, built atop Steel.C.Ref.
• Steel.C.Struct, Steel.C.StructLiteral: a model of C structs for Steel, culminating in the definition of combinator addr_of_struct_field for taking a pointer to a field of a struct along with its inverse unaddr_of_struct_field
• Steel.C.Union, Steel.C.UnionLiteral: a model of C unions for Steel, culminating in the definition of combinator addr_of_union_field for taking a pointer to a field of a union along with its inverse unaddr_of_union_field
• Steel.C.Array: a model of C arrays for Steel. The interface is minimal but supports common array operations, and @tahina-pro is currently working on the model.

Along the way, it adds the following to ulib:

• FStar.FSet: a library for finite sets.

It also defines the following helper modules:

• Steel.C.PCM: an alternative formulation of PCMs where the composability predicate is expressed as a function returning GTot bool, allowing for values of type (pcm a) to remain in universe zero, along with adapter functions between these PCMs and the ones in FStar.PCM.
• Steel.C.Opt, Steel.C.Frac, Steel.C.Uninit: PCMs for representing exclusive ownership, fractional permissions, and possibly-uninitialized data respectively.
• Steel.C.Universe: combinators for raising and lowering the universe of PCMs.
• Steel.C.Typenat, Steel.C.Typestring: an encoding of strings and natural numbers as F* types, allowing such values to be used in types without fear of erasure (for an explanation of why we need this, see Steel.C.Typestring.fsti).
• Steel.C.Fields: an encoding of struct and union definitions as lists of (field name, typedef) pairs.
• Steel.C.StdInt: a model of bounded integers, used to describe the size of arrays.
• Steel.C.Ptr: a model of nullable C pointers for Steel.

Finally, it implements extraction for code using Steel.C.References to idiomatic C. examples/steel/arraystructs contains three examples:

• PointStruct.fst defines a struct named point containing two u32s and extracts functions that swap a point's x and y coordinates.
• ScalarUnion.fst demonstrates extraction of code that manipulates a union of two scalar values.
• HaclExample.fst demonstrates extraction of code that manipulates a struct resembling the kinds of data structures used in the HaclStar project.

[tahina-pro]

Hi everyone. Steel moved to its own repository, FStarLang/steel, where SteelC is now in the main branch: the SteelC data types are now in https://github.com/FStarLang/steel/tree/main/lib/steel/c , with the proofs in https://github.com/FStarLang/steel/tree/main/src/proofs/steelc .
For reference, I saved the latest state of this PR into https://github.com/tahina-pro/FStar/tree/_john_ml_steel_c
Thank you again @john-ml for your work! It is now in the main branch of FStarLang/steel as described above.