[move-prover] experimental modeling of a heterogeneous key-value store

[meng-xu-cs]

WIP, not intended for landing until feature complete Reviewers are tagged for information and discussion only

Motivation

Prover currently supports two collection data types, (including mutable borrow and write-backs):

• vector<T>: which is essentially a mapping of num -> T
• map<K, V>: a homogeneous table where all keys are in type K and values in type V

This PR investigates the feasibility of whether the prover can support a third data type:

• store: a heterogeneous table where keys and values can be in different types

The semantics of the store type are defined in the INTRINSIC_TYPE_KVS intrinsic and its associated functions.

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

CI