Review Dexter code and come up with list of functions to verify, english specs

[ehildenb]

In subdirectory tests/proofs/dexter, let's add a document README.md which describes:

• Each function we intend to do functional verification for.
• High level English spec of that function including:
  • Type signature
  • Assumptions about inputs
  • State updates
  • Return value