Describe the function preconditions in comments/docstrings

[hwwhww]

Issue

Pointed out by @franck44 and @protolambda, it would be more readable if we can more it clear of what are the preconditions of each function.

How to solve it

Add more detailed comments about the pre-conditions.

/cc @protolambda feel free to update this issue content. :)

[ericsson49]

It might be helpful to use Nagini to specify pre- and post-conditions (as well as other useful annotations).
It enriches statically-typed Python3 subset (PEP-484, mypy) with constructs to specify pre-conditions (Requires) and post-conditions (Ensures), exceptional post-conditions (Exsures), as well as invariants, function purity (@Pure), assertions, predicates, etc.

It uses Boogie and Z3 as Dafny, though it's underlying logic is different. However, the idea is to use its extensions to annotate the py-spec with pre-/post-conditions and other useful annotations (like @Pure).

One option can be to design a contract library based on the ideas of the Nagini contract library (e.g. one can express Dafny annotations instead of Viper ones).

[hwwhww]

Took a look Viper and Nagini today. Some quick notes:

• The verification system is great!
• Nagini requires input programs to comply to the static, nominal type system defined in PEP 484 as implemented in the Mypy, which means it requires remerkleable complies Mypy rules + Add SSZ utils to mypy checking scope #1707
• I'm worried that Nagini is not actively maintained. Since remerkleable has some complicated typing tricks, we may have some edge cases. (Sometimes, the issue is in mypy)