TODO.md

TODO LIST

Prove actual version of deposit smart contract

1. functional version using the simple functions with index commutation lemma.

2. imperative version of algorithm a. use 2 arrays and write a method? b. use one array to update in-place.

Move to using index k instead of path in algorhtms and prove correctness [DONE]

Re-factoring

[DONE]

1. merkle definition [DONE]
2. merkle for a list [DONE]

Finalise

1. proof that deposit() computes according to spec and preserves Valid()
2. branch -> left, zero_h -> right and use branch for reverse(left) and zero_h for reverse(right) to simplify the indices in the algorithm
3. README and documentation: update!!!

Misc

Check the instances cannot be safely inlined.

Refactor

1. shorten names
2. add functional version of algorithm