Changes to support loam

[wwared]

To support the v0 initial loam<->lair integration, we'll need:

• An Op::Require for raw require!(...) calls
• An Op::Provide for raw provide!(...) calls
• A Ctrl::Exit for terminating a function (semantically equivalent to return () but without providing anything)
• An Op::Exec for executing a function that uses Ctrl::Exit

We might also be able to refactor existing opcodes in term of the new ones, if that makes sense to do (e.g. implement the current Return as a Provide+Exit)

[arthurpaulino]

On a first glance, I disagree with the refactoring because I think it leads to weird semantics

[wwared]

As a side note, the "Exit" opcode is most likely not needed, because you can do this:

fn something(x): [0] {
    range_u8!(x); // or anything making use of `x`
    return ()
}

And it works, returning 0 elements and setting the output_size of the Func to 0.

[arthurpaulino]

@wwared won't that approach need a pairing require without values? I think it will because the relation includes more values than just what the function returns. So if we don't do the require manually we will get "cumulative sum not zero" errors.

Thus I think it's better to leave these control variants separate, such that Ctrl::Exit doesn't provide anything at all.

The other side of the coin is having a Op::Exec, which is similar to Op::Call but doesn't require anything at all.

(yes, we could do return () and let _: [0] = call(...), but that adds unnecessary overhead)

[wwared]

@arthurpaulino That's a good point, return () would make a provide for the given function call. I think that might be fine (doing the let _x: [0] = call(...) thing you mentioned), but it depends on what semantics the Loam program needs. That is, if the Loam programs require the memoization "called-exactly-once" behavior, doing that with an Exit that doesn't provide anything might be more difficult to guarantee.

It's unclear to me how we would call a Func that has a Ctrl::Exit at the end if it does not perform a provide indicating that the function has been called with a set of arguments. That is, let's say we have a function with the hypothetical operators:

fn something(x, y, z) {
    let a = add(x, y);
    provide!(a, z);
    if y {
        require!(x, z);
    }
    exit
}

How do you invoke something(1, 2, 3)? We can't use the call(...) syntax since that does a require(...) corresponding to it. We would need something like raw_call(...) or whatever that does not do a corresponding require(...). These low-level primitives could easily lead to weirdness like the function something(1, 2, 3) being possibly called more than once. Essentially, we would need to modify the Entrypoint chip to perform all the calls that it needs to perform, and the only way to ensure those functions were correctly called is via lookups.

I'm not sure, maybe this was poorly explained and confusing. I think that we might actually need this Exit behavior to provide something in return to ensure that the function calls are being performed correctly (in which case return () would be semantically equivalent). Or possibly the correct semantics is to rely solely on the raw provide/require calls within functions and let the prover non-deterministically call all the functions from the Entrypoint chip just passing the right arguments around to the functions. It's unclear to me at this point whether that could lead to soundness issues.

[arthurpaulino]

Sorry, I added a comment about that by editing my post. See what I said about Op::Exec above. Then we would be able to say exec(foo, arg1, arg2, ...)

[wwared]

Yes that's probably fine, we'll need to ensure that if you exec(foo, ...) that foo has no return values, since this is technically a non-deterministic, unconstrained prover hint, and the real constraint here requiring the prover to execute foo with the correct arguments are the provide!/require!s performed by foo. It should be an error to exec or use exit in a function that has no raw provide!/require! (since it doesn't make sense for you to exec a function without "side-effects")