Add minimal generic EVM Frames for climb/loop proofs (least surface)

[Th0rgal]

Summary

This is the smallest useful extraction of the frame preservation patterns developed in the SPHINCS- C13 proofs.

The goal (detailed in the companion SPHINCS- PR) is to allow projects like SPHINCS- to factor their climb engines so that:

• Verity provides the generic "preservation without forcing large terms" combinators.
• The consumer (SPHINCS-) only supplies the concrete step relation + the range/data supplier for its specific climbs (Merkle, WOTS, etc.).

What is added (intentionally minimal)

• Compiler/Proofs/Frames.lean (one small file, ~90 lines)
  • PreservesBindingsExcept + execStmt_letVar / mstore cases (abstract on evalExpr so keccaks/bodies are not forced).
  • PreservesSelectorCalldata (very common for verifier contracts that only read from calldata).
  • All lemmas are foundational, additive, and introduce no new axioms or sorry.

This is deliberately the least surface that still gives value for the RAM-control / term-size problem that arises in long climb/loop proofs inside the Verity interpreter model.

Companion change

See the parallel PR on lfglabs-dev/SPHINCS- which:

• Refactors SphincsMinusVerifiers/ to have a thin instantiation layer ("supply step spec + range supplier").
• Keeps the "additive concrete" modelling (C13Concrete etc.) completely separate and untouched.
• Moves toward the thin top-level claim: "the contract returns success and the observed root iff the byte spec accepts and the root matches pk".

Why this shape (least on Verity side)

• No attempt to upstream the full ClimbKit / ClimbLoopGuarded / ClimbMemFrame* / specific segment bodies — those are heavily tied to SPHINCS- memory layout, ADRS, and contract structure.
• Only the truly reusable "how to preserve a binding or a memory cell across a step without evaluating the step's heavy subterms" pattern.
• Future work can grow this (generic ClimbEngine taking a step + specStep + DataSupplier + frame proofs) once the pattern has more consumers.

Test plan

• lake build Compiler (or the full package) succeeds.
• The new lemmas are available for import as Compiler.Proofs.Frames.
• No impact on existing proofs (additive file).

---

Note

Medium Risk
Changes external-call lowering and macro typing for real DeFi-style void interfaces; mistakes could revert after successful calls or mis-encode ABI, though smoke tests and guard messages cover main paths.

Overview
This PR bundles proof infrastructure with compiler/EDSL fixes for typed ABI interfaces.

Void typed interface calls: Interface syntax now allows methods without a returns clause. The macro resolves void vs returning calls (statement vs let … ←), rejects binding void methods or using returning calls as bare statements, and limits void calls to static single-word parameters for now. Statement-position void calls lower to a new externalCallNoReturn ECM (noReturnModule / noReturn) that ABI-encodes and bubbles failure returndata but skips the 32-byte returndata check and return decode—avoiding spurious reverts after successful void callees (e.g. Aave-style supply/borrow). Returning methods still use externalCallWithReturn.

Validation & loading: Dotted interface externals like IPool.supply are skipped in Yul identifier validation (#1952). Module spec loading uses loadExts := true on import and supportInterpreter := true on compiler executables so specs referencing ECM modules (e.g. withReturnModule) evaluate correctly (#1951).

Proofs: New additive Compiler/Proofs/Frames.lean (~90 lines) with binding-preservation and selector/calldata preservation lemmas for letVar and mstore, abstracting over evalExpr for climb/loop proofs (no new axioms).

Tests: Smoke contracts and #guard_msgs for void/view calls and error cases; generated Foundry property stubs for the new smoke contracts.

^{Reviewed by Cursor Bugbot for commit 69150c5. 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 9, 2026 1:13pm

[Th0rgal]

Reviewed the minimal Frames extraction (PreservesBindingsExcept for letVar/mstore + PreservesSelectorCalldata, abstract over evalExpr, ~90 lines, no new axioms/sorries).

The bundled void-interface EDSL fixes (noReturnModule, resolve for void vs returning typed calls, loadExts/supportInterpreter, dotted external skip in validation, smoke + generated property stubs) had already been evolved and refined on the receiving branch (composite static support for tuple params in typed interfaces per #1982 plan, plus the legacy string safe work).

Added the Frames.lean directly and committed as integration of #1983 (see 668d2d16). Conflicts in shared files (Translate, smoke, ValidationCalls, etc.) resolved by taking the more advanced versions from the 1962 lineage + porting intent.

lake build + make check green post-integration (macro health, boundary/sync checks, etc. pass).

This delivers the reusable frame preservation combinators for downstream climb/loop proofs (SPHINCS- etc.) with least surface on Verity.