Merge branch 'main' into fix/558-refinement-honest-reject

Author: hyperpolymath

lib/interp.ml

@@ -280,11 +280,33 @@ let rec eval (env : env) (expr : expr) : value result =
                result of the entire `handle` expression.  This is correct for
                the common single-shot, tail-resume pattern.  Full multi-shot
                continuations require either OCaml 5 effects or a CPS transform. *)
+            (* #555: the shallow continuation is sound only for single-shot
+               tail-resume.  Multi-shot resume (calling `resume` more than
+               once) cannot be expressed without reified continuations and
+               previously produced a silently-wrong value — each call merely
+               returned its argument, so e.g. `resume(1) + resume(2)` yielded
+               `3` instead of running the continuation twice.  Count
+               invocations and fail loudly on the second call so a multi-shot
+               handler can never silently miscompute.  (Non-tail single-shot
+               resume — `let x = op(); x + 100` resuming to `5` rather than
+               `105` — remains a documented shallow-resume incompleteness: the
+               body has already unwound the bind chain, so the discarded
+               continuation is undetectable here without a CPS transform.) *)
+            let resume_count = ref 0 in
             let resume_fn = VBuiltin ("__resume__", fun resume_args ->
-              match resume_args with
-              | [v] -> Ok v
-              | []  -> Ok VUnit
-              | vs  -> Ok (VTuple vs)
+              incr resume_count;
+              if !resume_count > 1 then
+                Error (RuntimeError
+                  ("multi-shot resume is not supported by the tree-walking \
+                    interpreter: `resume` was called more than once in the \
+                    handler for effect `" ^ op_name ^ "` (Refs #555). Only \
+                    single-shot tail-resume is implemented; multi-shot \
+                    handlers require reified delimited continuations."))
+              else
+                match resume_args with
+                | [v] -> Ok v
+                | []  -> Ok VUnit
+                | vs  -> Ok (VTuple vs)
             ) in
             (* Bind effect argument values to handler patterns.
                Convention: all declared params first, then the continuation as

test/e2e/fixtures/handle_resume_multishot.affine

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// Issue #555 regression fixture (NEGATIVE). The arm calls `resume` twice. The
+// tree-walking interpreter has no reified continuation, so each call
+// previously just returned its argument and `a + b` silently evaluated to 3
+// instead of running the continuation twice. The second `resume` must now fail
+// loudly rather than silently miscompute.
+effect Choose { fn pick() -> Int; }
+
+fn main() -> Int {
+  handle pick() {
+    pick() => {
+      let a = resume(1);
+      let b = resume(2);
+      a + b
+    }
+  }
+}

test/e2e/fixtures/handle_resume_nontail.affine

@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// Issue #555 regression fixture (KNOWN INCOMPLETENESS). Non-tail single-shot
+// resume: `compute` performs `ask()` and then computes `x + 100`, so the
+// correct result is 105. The shallow tree-walking interpreter unwinds the body
+// at the perform and cannot replay the discarded continuation, so it returns
+// the resumed value 5 instead. This case is undetectable at runtime without a
+// CPS transform; the test pins the current shallow value (5) so a future
+// delimited-continuation implementation flips it to 105 deliberately.
+effect Ask { fn ask() -> Int; }
+
+fn compute() -> Int / Ask {
+  let x = ask();
+  x + 100
+}
+
+fn main() -> Int {
+  handle compute() {
+    ask() => resume(5)
+  }
+}

test/e2e/fixtures/handle_resume_tail.affine

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// Issue #555 regression fixture (POSITIVE). Single-shot tail-resume: the
+// handled computation `ask()` is itself the perform, so resuming with 5 makes
+// the whole `handle` evaluate to 5. This is the one resume shape the
+// tree-walking interpreter implements correctly; the multi-shot guard must not
+// disturb it. (First interpreter test to actually exercise `resume`.)
+effect Ask { fn ask() -> Int; }
+
+fn main() -> Int {
+  handle ask() {
+    ask() => resume(5)
+  }
+}

test/test_e2e.ml

@@ -2332,6 +2332,71 @@ let async_fence_tests = [
   Alcotest.test_case "wasm: async row without async call compiles"        `Quick test_async_no_boundary_still_compiles;
 ]
 
+(* ============================================================================
+   Issue #555: interpreter resume soundness (multi-shot loud-fail)
+   ============================================================================
+
+   The tree-walking interpreter models `resume` with an identity continuation,
+   correct only for single-shot tail-resume. Multi-shot resume (>1 call)
+   previously produced a silently-wrong value (each call merely returned its
+   argument); it must now fail loudly. Non-tail single-shot resume stays a
+   documented shallow-resume incompleteness (undetectable without a CPS
+   transform), pinned here as an executable fact. Unlike the existing
+   handler-fence tests, these actually APPLY `main` so the handler runs. *)
+
+let interp_main path =
+  let open Result in
+  let ( let* ) = bind in
+  let* (prog, _resolve_ctx) = run_frontend path in
+  let* env =
+    match Interp.eval_program prog with
+    | Ok env -> Ok env
+    | Error e -> Error (Value.show_eval_error e)
+  in
+  let* main_fn =
+    match Value.lookup_env "main" env with
+    | Ok f -> Ok f
+    | Error _ -> Error "no `main` binding"
+  in
+  match Interp.apply_function main_fn [] with
+  | Ok v -> Ok v
+  | Error e -> Error (Value.show_eval_error e)
+
+let test_resume_single_shot_tail () =
+  match interp_main (fixture "handle_resume_tail.affine") with
+  | Ok (Value.VInt 5) -> ()
+  | Ok v -> Alcotest.failf "single-shot tail-resume: expected VInt 5, got %s" (Value.show_value v)
+  | Error msg -> Alcotest.failf "single-shot tail-resume should evaluate, got error: %s" msg
+
+let test_resume_multishot_loud_fail () =
+  match interp_main (fixture "handle_resume_multishot.affine") with
+  | Ok v ->
+      Alcotest.failf
+        "expected a loud multi-shot resume error (Refs #555); got Ok %s — \
+         silent multi-shot miscompute has regressed" (Value.show_value v)
+  | Error msg ->
+      Alcotest.(check bool) "error names the multi-shot resume limit" true
+        (contains_str "multi-shot resume" msg)
+
+let test_resume_nontail_known_shallow () =
+  (* KNOWN shallow-resume incompleteness: the correct result is 105; the
+     shallow interpreter returns the resumed value 5. Flip to VInt 105 when
+     delimited continuations land (Refs #555). *)
+  match interp_main (fixture "handle_resume_nontail.affine") with
+  | Ok (Value.VInt 5) -> ()
+  | Ok (Value.VInt 105) ->
+      Alcotest.fail
+        "non-tail resume now returns 105 — delimited continuations appear to \
+         have landed; update this pin and the #555 CAPABILITY-MATRIX note"
+  | Ok v -> Alcotest.failf "non-tail resume: expected VInt 5 (known shallow), got %s" (Value.show_value v)
+  | Error msg -> Alcotest.failf "non-tail resume should evaluate (shallow), got error: %s" msg
+
+let resume_soundness_tests = [
+  Alcotest.test_case "interp: single-shot tail-resume evaluates to 5"   `Quick test_resume_single_shot_tail;
+  Alcotest.test_case "interp: multi-shot resume → loud failure"         `Quick test_resume_multishot_loud_fail;
+  Alcotest.test_case "interp: non-tail resume → 5 (KNOWN shallow #555)" `Quick test_resume_nontail_known_shallow;
+]
+
 (* ============================================================================
    Section: Stage 7 — typed-wasm Ownership Verifier (Tw_verify)
    ============================================================================
@@ -5479,6 +5544,7 @@ let tests =
     ("E2E Try/Catch/Finally", try_catch_tests);
     ("E2E Handler Fence (#555)", handler_fence_tests);
     ("E2E Async Fence (#556)", async_fence_tests);
+    ("E2E Resume Soundness (#555)", resume_soundness_tests);
     ("E2E Ownership Verify", tw_verify_tests);
     ("E2E Cmd Linearity", cmd_linear_tests);
     ("E2E Boundary Verify", tw_interface_tests);