noir-lang / noir

Noir is a domain specific language for zero knowledge proofs
https://noir-lang.org
Apache License 2.0
875 stars 189 forks source link

Consider making guarantee about order of evaluation of function calls in comptime evaluator #4934

Open TomAFrench opened 5 months ago

TomAFrench commented 5 months ago

See PR review comment here: https://github.com/noir-lang/noir/pull/4926/files#r1581593983

Users are going to have expectations about the relative ordering of these two function calls being resolved and so their return values. We should aim to respect this ordering.

fn main() {
    // Order of comptime evaluation between functions isn't guaranteed
    // so we don't know if (id1 == 0 && id2 == 1) or if (id1 == 1 && id2 == 0).
    // we only know they are not equal
    let id1 = id1();
    let id2 = id2();
    assert(id1 != id2);
}
TomAFrench commented 5 months ago

Thought I posted a comment here but obviously didn't hit send.

The comment above imples that this is a guarantee that we can't make, i.e. these calls are resolved in a non-deterministic or deterministic but unintuitive fashion. I spoke with @jfecher about this and his intention on this was more that we shouldn't make this guarantee.

For examples such as a mutable global handing out unique ids such as in the linked PR, as the program grows in complexity it's likely that the user will miss a call to get_unique_id and a different assignment than the get in reality. It's then a footgun to rely on the exact values returned from specific calls to mutable globals so we should dissuade users from relying on these in general.

jfecher commented 5 months ago

Another point to consider is that guaranteeing an evaluation order across different global items (e.g. across separate modules) also locks the compiler to a particular resolution order. Avoiding specifying an order and encouraging users not to rely on one keeps our ability to change the ordering the compiler resolves / type checks / comptime-interprets items if we later discover a reason to change it.