Scaffold proven forEach loop fragment

[Th0rgal]

End goal

Expand Verity's proven compiler fragment so Stmt.forEach loops have a real, documented proof path through compiler preservation instead of being treated as entirely unsupported.

This PR now proves the generic empty-body literal-bound fragment end to end:

Stmt.forEach varName (.literal n) []

for arbitrary natural literal bounds n.

What is proven

Admitted/proven forEach cases:

• Stmt.forEach varName (.literal 0) body, where body is supported under varName :: scope.
• Stmt.forEach varName (.literal n) [], for any literal natural bound n.

The positive empty-body case is no longer staged as separate literal-1 and literal-2 support. It is admitted by the generic forEachLiteralEmpty n constructor and wired through the actual CompiledStmtStep / Compiler.Proofs.EndToEnd preservation path.

What changed

• Adds source-side execForEachLoop semantics and helper lemmas for loop execution.
• Lowers forEach using an internal cached bound and index counter, assigning the user loop variable at the start of each iteration.
• Extends the IR/Yul interpreter proof surface with reusable for_ execution lemmas.
• Adds a Nat-indexed empty-body loop proof for arbitrary literal bounds.
• Wires the generic empty-body loop proof through GenericInduction and EndToEnd.
• Keeps zero-bound supported-body loops on their existing proof path.
• Updates supported-fragment/state-surface/contract-surface predicates so the newly proved cases are reachable and unsupported cases remain fail-closed.
• Refreshes docs, README, docs-site pages, feature-matrix artifacts, proof-length metadata, and CI persistence-key handling.
• Addresses Bugbot review findings, including removing unused private helper lemmas.

Still intentionally unsupported

This PR does not prove general positive forEach loops with non-empty bodies.

Unsupported/fail-closed cases include:

• Stmt.forEach varName count [] when count is not a literal.
• Stmt.forEach varName (.literal n) body for positive n and non-empty body, unless covered by the separate zero-bound rule.

So forEach remains documented as partial: arbitrary literal-bound empty-body loops are proven, zero-bound supported-body loops are proven, and positive non-empty bodies remain future work.

Validation

Local validation on the pushed branch:

• lake build Compiler.Proofs.IRGeneration.GenericInduction passed.
• lake build Compiler.Proofs.EndToEnd passed.
• lake build PrintAxioms passed.
• npm run check:highlighting passed in docs-site.
• npm run build passed in docs-site.
• Audit scan found no live sorry, admit, or new unsound axiom; remaining hits are prose/comment text or standard Lean axioms reported by PrintAxioms.

Current PR head: 417abe2f2394fb78332b41fe46f6dc4158898624.

Review focus

Please review this as a staged proof PR:

• Is the generic empty-body recurrence aligned with source execForEachLoop and compiled Yul for_ semantics?
• Are the supported predicates narrow enough to avoid overclaiming?
• Are unsupported positive non-empty loop bodies still clearly fail-closed?
• Is the proof architecture ready to extend with a body-parametric recurrence in a later PR?

[vercel]

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

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	May 27, 2026 6:16am

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```

[Th0rgal]

Temporarily closing and reopening to clear a wedged GitHub Actions run for this PR. No code change is being abandoned.

[Th0rgal]

CI update: the proof/code changes are pushed at e865066d5e70c1e86f22103ede9e32e1696a44b0, but GitHub Actions is currently blocked by platform infrastructure rather than a proof failure.

Observed from the API:

• the last Verify proofs run for this branch is still stuck as queued on older head e46dd8ac with no jobs exposed: https://github.com/lfglabs-dev/verity/actions/runs/26446011933
• cancel and force-cancel both return 409 (Cannot cancel a workflow re-run that has not yet queued), while rerun says the workflow is already running
• manual workflow dispatch for verify.yml returns HTTP 500
• fresh PR synchronize/reopen events update Vercel/Cursor, but no GitHub Actions check suite is created for current head e865066d

GitHub status currently reports an active incident with Actions and Pages, with Actions in major outage. I will leave the branch as-is; local proof verification has passed and this is waiting on GitHub Actions to recover or the stuck run to clear.

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit 85493d3. Configure here.}