Cleanup/Refactor

[emarzion]

Ideas and discussions for cleanup/refactor

• couple the well-formedness proof with the state in something like a sigma type so our operations produce wf_states, not just states
• bring back some of the dependent types around stuff like perfect binary trees, vectors, etc.? I don't want to complicate things for the security proofs but perhaps some of these could help.
• renaming stuff (related to #14), regulating style/naming conventions, etc.?

[PalindromeLeung]

• pruning off some of the unused definitions based on the dependency graph
• cleaner binary relation theory over the Poram monad

[emarzion]

Can you document and/or make a script or something to run the dependency graph stuff?

[PalindromeLeung]

• consider moving some of the lemmas in PathORAMFunCorrect.v to its own file
• change the return type of lookup_ret_data to option nat
• refine binary relations over the Poram monad

[emarzion]

• Write a good README