trusted chunk crate

[Ramla-I]

This crate includes the TrustedChunk type with verified methods that can be used to prove uniqueness of the type.

The modules are:

• external spec: spec files for external types like Option
• spec: Functions used within the specification and/or code that are used to define what we mean by "unique".
• linked_list: A verified linked list implementation
• static_array: A verified wrapper over an array
• trusted_chunk: Contains the TrustedChunk type with its verified methods: new, split, split_at and merge. It also contains the TrustedChunkAllocator type which stores the bookkeeping data structures used in verifying uniqueness and provides the only public interface to create a new TrustedChunk