Add multi-result ECM bind syntax

[Th0rgal]

Summary

• add ecmBind [x, y] module [args] as a macro-surface do element for multi-result ECM modules
• validate bound result names against the module and expose them as Uint256 locals to later statements
• add executable placeholder expansion and smoke coverage using bn256AddModule

Verification

• lake build Contracts.Smoke
• git diff --check
• python3 scripts/generate_print_axioms.py --check
• python3 scripts/check_axioms.py
• lake build Benchmark.Cases.UnlinkXyz.Pool.Compile in verity-benchmark against this local Verity checkout

---

Note

Medium Risk
Extends the Verity macro surface and translation pipeline for ECM calls, which can affect compilation/semantic preservation for contracts using external modules. Changes are localized but touch core elaboration/validation logic and add new smoke coverage.

Overview
Adds a new do-element syntax, ecmBind [x, y, ...] module [args], to bind multiple result words from an ECM module and introduce them as fresh Uint256 locals for subsequent statements.

Updates macro translation to typecheck ecmBind arguments, validate that the bound names exactly match the module’s declared resultVars, and lower the statement to a single CompilationModel.Stmt.ecm while extending the local environment.

Introduces a new smoke contract GenericECMMultiResultSmoke (using bn256AddModule) plus proof/model expectations, wires it into invariant + round-trip fuzz harness spec lists and selector/signature snapshots, and adds an auto-generated Solidity property test stub for the new smoke contract.

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

[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```