Track forEach counters in body scope to fix nested-loop shadowing

[Th0rgal]

Summary

A forEach lowers to a Yul for-loop with two synthetic init variables,
__forEach_idx and __forEach_count, that stay live across the whole loop body.
The body was compiled with scope varName :: inScopeNames, which omits those two
counters. A forEach nested inside another forEach therefore re-derived the same
__forEach_idx / __forEach_count (pickFreshName saw them as unused), and the
inner let collided with the still-live outer binding. solc rejects this with
"Variable name already taken in this scope", so any contract that nests loops fails
to compile.

What

• Add CompilationModel.forEachBodyScope, which extends the body-compile scope with
  the two synthetic counter names. It is definitionally equal to
  idxName :: countName :: varName :: inScopeNames, so generated Yul for non-nested
  loops is byte-identical; for nested loops the inner counters are now freshened
  (__forEach_idx_..., __forEach_count_...) and the output is valid.
• Re-thread the proof side (FunctionBody, GenericInduction,
  EvmYulLeanBodyClosure) through the same handle so the scope-accounting and
  bridged-body theorems continue to hold over the corrected scope.

Audit docs

No new axioms (AXIOMS.md stays at 0 project-level axioms), no trust-boundary change,
no CI-boundary change. Every invariant recorded in AUDIT.md / TRUST_ASSUMPTIONS.md /
AXIOMS.md is preserved (the proofs are re-threaded, not weakened), so per Non-Negotiable
1 those files need no synchronization. Flagging this explicitly so a maintainer can
object if they read it differently.

Testing

• lake build is green on this branch.
• Downstream evidence: with this commit, solc compiles a contract that nests forEach
  loops (Unlink's UnlinkPool) cleanly, where the unfixed compiler emitted
  shadowing-invalid Yul that solc rejected.

Opened as draft for review.

---

Note

Medium Risk
Touches core statement compilation and many IR-generation proofs; behavior change is localized to nested forEach name freshening, but incorrect scope wiring could affect generated Yul or proof soundness.

Overview
Fixes nested forEach lowering so inner loops no longer reuse the outer loop’s __forEach_idx / __forEach_count names, which solc rejected as duplicate bindings in the same Yul scope.

Adds CompilationModel.forEachBodyScope, which extends the in-scope name list passed into compileStmtList for a loop body with the freshly chosen counter names (plus the loop variable). Stmt.forEach codegen now compiles the body with that scope instead of only varName :: inScopeNames. For a single loop the scope matches the previous inline list, so output stays the same; nested loops get suffixed counter locals and valid Yul.

Proof modules (FunctionBody, GenericInduction, EvmYulLeanBodyClosure) are updated to use the same scope handle in induction and bridged-body theorems so IR-generation proofs still align with the compiler.

^{Reviewed by Cursor Bugbot for commit 825b5a7. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jun 2, 2026 9:33pm