Description
Reading the summary for this proposal, I find myself confused. On the one hand, it says
The same instruction at (1) and (2), when given the same inputs, can return two different results.
This sounds like the normal kind of non-determinism we consider on PL theory, like a choice: () -> bool function that returns some arbitrary boolean value each time it is executed.
But then later, it says
Some operators are host-dependent, because the set of possible results may depend on properties of the host environment (such as hardware). Technically, each such operator produces a fixed-size list of sets of allowed values. For each execution of the operator in the same environment, only values from the set at the same position in the list are returned, i.e., each environment globally chooses a fixed projection for each operator.
which sounds very different! Now the choice cannot be made independently each time the code is executed, instead the choice is made once upfront when "the environment" is fixed. It remains unclear what exactly is part of "the environment".
So concretely, if within the same wasm module I run such an instruction twice in a row with the same inputs, is it allowed to return different results? (I don't care whether that's likely or unlikely, I only care about whether this is permitted by a correct implementation.)
And what exactly is part of "the environment" -- in particular, at which point during the lifetime of a wasm module can I assume that "the environment" is fixed and can no longer change (so that I can rely on operations now behaving deterministically)?