[SpaceManiac]

Follow-up to #251.

• Spec: add push-effect-handler-frame, add-effect-handler, and pop-effect-handler-frame.
• Compiler: properly forward parameters from outer effect handler to with function.
• Compiler: properly handle ABIs defining multiple effects.
• Compiler: call push/add/pop for stack propriety.
• Runtime: bail if an effect goes completely unhandled.
• Runtime: walk explicit effect stack looking for a matching handler.
  • While a handler is being called, truncate the stack above it, to properly route effects raised by the handler.
• Runtime: pass parameters from raise to effect handler, and result from handler to raise.
  • Keep an explicit stack of component::Instance rather than using the debug stack walk which only returns core Instances.

Remaining future work:

• Compiler: implement pattern support in the with clause.
• Compiler: allow access to variables in the parent scope (may require spilling to globals).

[SpaceManiac]

@ecioppettini I'd like to hear from you on two points:

1. I suspect that my changes to starstream-proving-runtime/src/templates.rs to get the tests passing are probably not correct. What's the right way to do this?
2. The unhandled_effect_is_rejected_by_the_circuit test is currently failing because the runtime itself now rejects such executions. How would you prefer to handle this?

[ecioppettini]

@ecioppettini I'd like to hear from you on two points:

1. I suspect that my changes to [starstream-proving-runtime/src/templates.rs](https://github.com/LFDT-Nightstream/Starstream/pull/263/changes#diff-e521ca731def6575bd89e9fcc6851da892b5f12934170437a084eb5c32024892) to get the tests passing are probably not correct. What's the right way to do this?

Well, the proper way is to add the opcode in the quint spec, the template itself should not use a constant method hash and instead source that from the arguments, and then that needs to be added to the circuit too

But I can do that myself after this. Or if you want I can stack a PR, if you think we don't want to merge the intermediate state (but I think it is fine?)

2. The `unhandled_effect_is_rejected_by_the_circuit` test is currently failing because the runtime itself now rejects such executions. How would you prefer to handle this?

Well, tbh we could just remove this unless you think it is useful as a test for the runtime. The circuit technically has coverage for this anyway.

[SpaceManiac]

But I can do that myself after this

Alright, will leave it to you.

we could just remove this

Done.

[ecioppettini]

I think this logic is wrong?

Here we are calling into the handler with call_async, but with the same instance stack. But what if the handler raises another effect? we would be searching from the same point, which could be a child

like, this allows something like:

A -> B -> C (raise E) -> B (handle E) -> B (raise F inside the handler) -> C (handle F) !

where C would be handling an effect for B, which is the parent

instead when B raises, the instance_stack should be narrowed to start searching from B

[SpaceManiac]

Hmm, you might be right. I'll have to think about which way makes more sense...

[ecioppettini]

I don't think the current semantics really make sense under any model? If I'm reading this right

There are systems that have bidirectional effect handlers (https://dl.acm.org/doi/10.1145/3428207), where you could have a handler performing an effect that the child handles. Kind of like an effect handler that needs effects, that are defined on the point where the effect is performed/raised.

But that's a different type system feature generally, because the required effect is on the handler and not on the function that defines the handler.

Plus this doesn't even implement that I think, because if you have A -> B -> C -> D, then C may be the right handler for an effect in B, but this would still look in D.

[SpaceManiac]

Nested try/withs are now handled properly:

abi Effects {
    effect Hello();
    event Log(point: u32);
}

test {
    emit Log(1);
    try {
        try {
            emit Log(2);
            raise Hello();
            emit Log(6);
        } with Hello() {
            emit Log(3);
            raise Hello();
            emit Log(5);
        }
    } with Hello() {
        emit Log(4);
    }
    emit Log(7);
}

 INFO starstream_cli::test: Running test test=""
 INFO starstream_cli::run: abi="effects" event="log" params="(1)"
 INFO starstream_cli::run: abi="effects" event="log" params="(2)"
 INFO starstream_cli::run: abi="effects" event="log" params="(3)"
 INFO starstream_cli::run: abi="effects" event="log" params="(4)"
 INFO starstream_cli::run: abi="effects" event="log" params="(5)"
 INFO starstream_cli::run: abi="effects" event="log" params="(6)"
 INFO starstream_cli::run: abi="effects" event="log" params="(7)"
 INFO starstream_cli::test: test="" output="()"

[SpaceManiac]

Failing test is starstream-proving-runtime::runtime_e2e effect_handler_reentry_satisfies_the_circuit.

[ecioppettini]

I think this may still be wrong, since a try inside an effect handler would get the wrong instance.

like

try {
 foo()
}
with E() {
  try {
   // this push-effect-handler-frame may get foo's instance (or a child of it)
    bar()
  } with F() {
  }
}

I feel like we should just keep track of the current instance. At least that's how I would implement this in the prover (although I wouldn't use wasmtime's instance ids in there, the prover just allocates contiguous ids in instantiation order)

[SpaceManiac]

Ah, you're right. We need to push the handler's instance to the instance stack while we call the handler.

As far as I can tell, wasmtime is generally not interested in exposing the "current instance". wasmtime::Caller doesn't do it and even debug_exit_frames only returns the core Instance, not the component Instance.