research: [1623] audit forEach soundness gap

[Th0rgal]

Summary

• add docs/research/1623-foreach-soundness-audit.md
• audit the exact semantic split between the EDSL forEach helper, compilation-model/source semantics, and generated Yul
• enumerate every in-repo forEach use and identify the concrete proof surface affected today

Why Option A

I chose Option A because issue #1623 is a P0 soundness bug and the highest-leverage first step is to pin down the exact mismatch before changing semantics. The audit shows that the trusted EDSL helper executes the loop body once regardless of count, while compiled Yul emits a real bounded loop, and the current SourceSemantics layer does not execute .forEach at all.

Issue

Closes #1623

---

Note

Low Risk
Low risk: this PR only adds research documentation and does not change any code paths, proofs, or compiler behavior.

Overview
Adds a new research note docs/research/1623-foreach-soundness-audit.md that documents the current semantic mismatch for forEach across the trusted EDSL helper, the compilation-model source semantics, and the generated Yul.

The doc enumerates current in-repo forEach usages and calls out the specific contract surface (Contracts.Counter.previewLowLevel) where the mismatch can make reasoning/proofs unsound, plus outlines the concrete follow-up fixes needed.

^{Written by Cursor Bugbot for commit 4cb07a3. This will update automatically on new commits. Configure here.}