issue tracker for the trie verification

[LukeXuan]

The current proof for the trie-over-btree has some major holes unfilled. I feel obliged to list them here so whoever takes over them can have a better understanding of the status.

What's done?

An end-to-end correctness (modulo a few minor holes) about put, get, and simple usage of cursors was proved.

What's still a problem?

• [ ] a better invariant about the bordernode is necessary: current invariant does not rule out usage of prefix links of a bordernode while its prefix isn't entirely zeros.
• [ ] One of the links in bordernode can either point to a trie or an arbitrary user-appointed value. The types in C and related funspecs/proofs need changes to support the behavior.
• [ ] Current model about the cursor and key might not strong enough to prove the desired properties of maps (the definition in model/BTreesModule.v and the adapted version in verif/trie/functional/cursored_kv.v). I have no clear idea about which part should be improved, though.
• [ ] The current definitions of get_key and get_value in verif/trie/functional/cursored_kv.v make refinement relationship with C code difficult to prove: get_value can be implemented cheaply in constant time by access the leaf node while get_key requires traverse of the entire cursor. It should be better if these are defined by properties with get rather than functions calling get.
• [ ] The proofs about bordernode are broken (I shall fix it).