[sebastian-griego]

safe.ts has 23,992 tokens against a 24,000-token limit. This refactor reduces it to 19,196 tokens. It recovers 4,796 tokens without changing the limit or moving code to another file.

The change groups translation state by pass, shares typed kernel-node constructors, and removes repeated telescope and model-search context. scope_hide adds a kernel binder. scope_bind requires an explicit source type or null. Each binder creates one fresh scope object and copies only the arrays that change. Source bindings are written at their level, and missing-entry guards remain in place. Local names do not hide pass-level bindings.

Most of the token reduction comes from comment consolidation. The comments retain the representation rules, source-checking boundary, model choices, and reasons for nonlocal behavior. The source checker, compiler, runtimes, and BendTT kernel are unchanged. The exporter retains its checks, diagnostics, search limits, rollback behavior, and handling of unsupported declarations.

Local validation against main at d0d0c212:

• All 1,756 repository source cases retain the same export and --verdict results. All 1,249 emitted books are byte-identical, including partial exports.
• All 142 additional equality, dependent-type, and proof-reuse cases retain the same source, export, kernel, and verdict results. All 48 kernel negative controls remain rejected.
• Repeated export and check calls match across 15 books. The comparison covers group restarts, rollback, model search, diagnostics, and changes to book metadata.
• All 4,660 focused scope assertions pass. They cover sparse and truncated scopes, changed source levels, frozen inputs, zero quantities, binding identity, missing-entry guards, and positive and negative type controls.
• The repository gate passes 54/54 checks. git diff --check passes.

Fresh serial measurements use the generic, proof, and tree workloads with Bun 1.3.14. Warm translation medians decrease by 9.7 ms for generics and 28.9 ms for proofs. The tree median increases by 0.20 ms, from 3.13 ms to 3.34 ms. Complete-command medians change by -1.27%, +0.09%, and +0.55%, respectively. The timing intervals include zero in all three complete-command comparisons.

Memory results vary between runs. In the first proof sample, peak process RSS increases by 219.9 MiB for cold exports and 291.5 MiB for repeated warm exports. These samples include source checking. A fixed follow-up measures the unmodified CLI with 36 commands per version. Compared with main, its median peak RSS decreases by 28.8 MiB and its mean decreases by 31.4 MiB. Both versions reach about 1.84 GB. Their median command times are equal to within 0.1 ms. Compared with the version before the review corrections, the corrected version uses 68.5 MiB more mean peak RSS. Thus, the corrections lose part of that version's measured memory gain. Warm tree peak RSS also increases by 2.3 MiB.

The higher earlier samples remain part of the results. The cold sample measures peak RSS through translation; the follow-up measures the complete command. They are separate measurements. The records suggest different collection timing, but do not establish its cause or prove zero memory cost. The distributed and GPU gates were not run locally after the review corrections.

[Lorenzobattistela]

Thanks for this. I merged current main (d0d0c21) into the branch as 5150564. That resolves the conflict with #1704 by applying its two Math.max bounds in the nested group_call and group_emit.

On 5150564 the change is behavior-neutral as far as we can measure:

• All 1,756 .bend files under tests/, demos/ and bench/ give byte-identical -o output and identical logs against main.
• Gates: repo 54/54, test 1671/1671, perf 124/124, ping 63/63, and safe identical to main (agree 1091, 0 false rejects).
• safe.ts is at 18,992 ttok, down from 23,992.

Before a merge, these need to change:

1. scope_bind(s, T?, q?) (safe.ts:1301) gives one optional argument three meanings: undefined hides the binder, null binds an untyped source variable, and a term binds a typed one. Today's callers are correct (all?.A ?? null, q && q.T). But a future scope_bind(s, all?.A, q) would silently hide the binder and shift every later source level, with no type error. Please make hiding explicit, for example a separate scope_hide(s, q) or a flag, so undefined can't select it.

2. scope_alias/scope_bind now append ([...s.c, b]) where main writes at the level (c[s.d] = b) (safe.ts:1297). That is only correct while s.c.length === s.d, which nothing enforces. tree()'s convoy reducer (safe.ts:648, 654) also dropped its hole guards on the same assumption. Either write at s.d as before, or keep the guards. As it stands, a scope built as { ...s, d: k } resolves the wrong variable, and a hole crashes --verdict with a TypeError.

3. Folding everything into the safe_pass closure leaves locals that hide pass-level names. o_uses' parameter out hides the emitted out, let_term's put hides put(), root_emit's pick hides pick(), arg_term's tree hides tree(), and group_call's args hides args(). Please rename the locals. It costs almost nothing in ttok.

4. Comments: the model comment (safe.ts:476) says the second pass prefers "a live codomain parameter". The code prefers any non-erased λ hypothesis of matching type, and the example of why that pass exists ({a == sub(add(a,b),b)} vs {add(a,b) == add(b,a)}) is gone. The header also dropped facts stated nowhere else: a field recurs through the name D, a book bend2 rejects never reaches the kernel, and an out-of-scope def's dependents leave with it. safe.ts is the boundary the BendTT proofs rely on, so please fix the model comment and restore those notes. There is room under the cap.

[sebastian-griego]

Thanks for the review and for merging main. I addressed all four points in 317f6fa:

1. scope_hide now adds a kernel binder explicitly. scope_bind requires a source type or null; undefined cannot select the operation.
2. Both source-binding helpers write at c[s.d]. I restored all four missing-entry guards, including the guard in scope_move.
3. I renamed the five listed locals and three more that hid pass-level names.
4. I corrected the model-search explanation and restored the examples and header notes.

Fresh comparisons against main at d0d0c212 retain all 1,756 export and verdict results. All 1,249 emitted books are byte-identical. The additional regression cases also match, including all 48 kernel negative controls. The focused scope checks cover sparse arrays, changed source levels, and invalid helper calls. GitHub's repository check passes. I have not rerun the distributed or GPU gates on this revision.

The file now has 19,196 tokens, a reduction of 4,796. The PR description includes fresh timing and memory measurements, including the approximately 0.2 ms tree translation cost and the variation in memory results.

[Lorenzobattistela]

I will close this for now because in the current state of the things and the rhythm of new PRs / Issues, we discussed and reached the conclusion that we rather not mess with a risky part of the code that is important to soundness (specially a full rewrite). But we are going to keep this on portfolio for simplifications later. Thanks a lot for the contribution.