1 Commits

Author SHA1 Message Date
Brummel ba981689fc plan: 0064 iter 1 — let-binder type table + value-typed let exemption (#57)
First iteration of spec 0064 (#57 hardening). Tees the (def,binder)->Type
table out of the typecheck pass (the inferred let-binder type computed at
synth's Let arm and discarded today) and threads it into the linearity
walk, then seeds BinderState.is_value for value-typed let-binders from
the table -- closing false-positive class 3 (the class spec 0063
deferred). Two tasks, RED-first: Task 1 adds examples/c3_value_let.ail to
the harden_ownership_false_positives_are_clean list (RED:
use-after-consume on xnew); Task 2 threads the table end-to-end
(synth -> check_fn -> check_in_workspace -> check_workspace ->
check_module_with_visible -> Checker, all callers in one compile-atomic
task) and seeds is_value at Term::Let (GREEN), plus two in-source unit
tests (value-let clean, heap-let still errors).

Fixes 1/2/4 (local fn-param modes, alias-redirect, partition_eithers
rewrite) are later iterations of the same spec, explicitly out of scope
here. plan-recon mapped the threading path; the parse-the-bytes gate
fired on the inlined fixture (RED confirmed).

refs #57
2026-06-01 17:34:28 +02:00