From 39380d361d530a95a4f1c718c0e201f8312d3ac4 Mon Sep 17 00:00:00 2001
From: Brummel <mould@mycelium.de>
Date: Mon, 18 May 2026 00:08:51 +0200
Subject: [PATCH] =?UTF-8?q?test:=20RED=20=E2=80=94=20lambda=20capturing=20?=
 =?UTF-8?q?a=20loop=20binder=20must=20fail=20ail=20check=20(loop-recur.tid?=
 =?UTF-8?q?y)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Milestone-close audit (architect, edd2558) surfaced a [high]
correctness defect: a (lam ...) body that references a loop binder
passes `ail check` (exit 0) then panics unreachable!() at codegen
(crates/ailang-codegen/src/lambda.rs:102) on type-correct input —
a DESIGN.md "Robustness against hallucinations" violation.

Root cause (debugger-confirmed): the Term::Lam escape guard at
crates/ailang-check/src/lib.rs:3608 inspects only mut_scope_stack;
loop binders live in `locals` (Term::Loop arm ~:3911, iter-2
design), so the mut.4-tidy MutVarCapturedByLambda-class rejection
has no loop-binder counterpart — the capture is accepted at check
and crashes codegen.

This RED commit pins the FIXED contract: the program must fail
`ail check` with code `loop-binder-captured-by-lambda` (symmetric
to mut-var-captured-by-lambda), NOT panic codegen. RED today
(left: [] vs right: ["loop-binder-captured-by-lambda"]); 6 prior
loop_recur_typecheck_pin tests still green. GREEN follows.
---
 .../tests/loop_recur_typecheck_pin.rs         | 17 ++++++++
 ...st_loop_binder_captured_by_lambda.ail.json | 42 +++++++++++++++++++
 2 files changed, 59 insertions(+)
 create mode 100644 examples/test_loop_binder_captured_by_lambda.ail.json

diff --git a/crates/ailang-check/tests/loop_recur_typecheck_pin.rs b/crates/ailang-check/tests/loop_recur_typecheck_pin.rs
index 060806e..bed062c 100644
--- a/crates/ailang-check/tests/loop_recur_typecheck_pin.rs
+++ b/crates/ailang-check/tests/loop_recur_typecheck_pin.rs
@@ -66,3 +66,20 @@ fn infinite_loop_typechecks_clean_no_termination_claim() {
     let codes = check_fixture("loop_forever.ail");
     assert!(codes.is_empty(), "infinite loop must typecheck (no totality claim), got {codes:?}");
 }
+
+/// Property: a `Term::Lam` whose body captures a `Term::Loop` binder
+/// must be rejected at `ail check` with a dedicated diagnostic,
+/// symmetric to `mut-var-captured-by-lambda`. Loop binders are
+/// alloca-resident and cannot escape their loop frame (iter-3 reuses
+/// the `mut_var_allocas` registry, `std::mem::take`-emptied at the
+/// lambda boundary), exactly the mut-var escape rule. Today the
+/// escape guard inspects only `mut_scope_stack`; loop binders live
+/// in `locals`, so check passes (exit 0) and codegen panics
+/// `unreachable!()` at `crates/ailang-codegen/src/lambda.rs:102`.
+/// This test pins the FIXED contract — RED until the guard also
+/// rejects loop-binder captures.
+#[test]
+fn lambda_capturing_loop_binder_emits_loop_binder_captured_by_lambda() {
+    let codes = check_fixture("test_loop_binder_captured_by_lambda.ail.json");
+    assert_eq!(codes, vec!["loop-binder-captured-by-lambda".to_string()]);
+}
diff --git a/examples/test_loop_binder_captured_by_lambda.ail.json b/examples/test_loop_binder_captured_by_lambda.ail.json
new file mode 100644
index 0000000..1b8e296
--- /dev/null
+++ b/examples/test_loop_binder_captured_by_lambda.ail.json
@@ -0,0 +1,42 @@
+{
+  "schema": "ailang/v0",
+  "name": "test_loop_binder_captured_by_lambda",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Int" },
+        "effects": []
+      },
+      "params": [],
+      "doc": "loop-recur follow-on: a lambda inside a loop body that references the enclosing loop binder `acc` is rejected with loop-binder-captured-by-lambda. Loop binders are alloca-resident and lexically scoped (iter-3 reuses the mut_var_allocas registry, emptied at the lambda frame boundary); lifting them into a heap-closure env is the same deferred work as the mut-var case. Symmetric to mut-var-captured-by-lambda.",
+      "body": {
+        "t": "loop",
+        "binders": [
+          {
+            "name": "acc",
+            "type": { "k": "con", "name": "Int" },
+            "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+          }
+        ],
+        "body": {
+          "t": "let",
+          "name": "f",
+          "value": {
+            "t": "lam",
+            "params": [],
+            "paramTypes": [],
+            "retType": { "k": "con", "name": "Int" },
+            "effects": [],
+            "body": { "t": "var", "name": "acc" }
+          },
+          "body": { "t": "app", "fn": { "t": "var", "name": "f" }, "args": [] }
+        }
+      }
+    }
+  ]
+}