Create a basic functional model of WiredTiger, which supports just the basic key-value operations PUT, GET, and DELETE, which would be suitable as in lightweight formal verification.

Specifically, the model should support:

• Historical values
• Multiple tables
• Timestamps

The model must also support a mechanism to examine its state, e.g., to iterate over all key-value pairs in order, so that we can compare the state of the model to the state of a WiredTiger database.