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.
Brummel
39380d361d