Document and Clarify Determinism of Ergo

[jeromesimeon]

Description

For some applications (notably blockchains with a consensus algorithm) it is important to ensure that the contract logic is deterministic.

While Ergo is designed to be deterministic, it would be useful to document the approach and possible source of concerns and address them.

Some initial thoughts

• Ergo is functional, cannot use data which is not in its input, every operation within the language is deterministic
• The official semantics in Coq is deterministic, and the source of truth for what programs mean
• Deterministic is defined with (an implicit or explicit) equality in mind: for all inputs input1 and input2 and ergo invocation of a clause f, input 1 = input 2 -> invoke f (input1) = invoke f (input2)
• Determinism isn't just a factor of the source language semantics, since we are compiling we also want to guarantee that the compiled code (for all supported target runtimes) preserves that semantics (modulo the above equality)
• We rely on some runtime libraries in some cases (the main of those for the JavaScript backend is momentjs)
• We rely on a specific version of a specific execution environment (e.g., what happens when node.js fixes a bug? and users may depend on different versions?)

Some possible aspects that may need review wrt to determinism

• Implementations of IEEE arithmetics are free to return -NaN or +NaN as they wish. Remark: those should be considered equal!
• ....need some investigation...

[jeromesimeon]

To review: https://github.com/WebAssembly/design/blob/master/Nondeterminism.md