feat(EVM,Trace,Core): land ERC-4337 frame primitives upstream

[Th0rgal]

Summary

Promotes a set of reusable EVM-frame and counting-trace primitives from the ERC-4337 EntryPoint benchmark (lfglabs-dev/verity-benchmark#32) into Verity proper. Each component closes a trust gap or removes boilerplate for every benchmark that uses external calls, transient reentrancy guards, solc memory layouts, or trace-counting properties — not just ERC-4337.

Modules landed (7 items)

#	Module	What it does
1	Verity/EVM/Frame.lean	CallerFrame + CalleeResult + applyCallToCaller; 4 single-call + 3 iterated-call preservation theorems. Discharges the EVM frame condition (CALL cannot mutate caller storage/transient/memory outside output buffer) as a theorem instead of an axiom.
2	Verity/Core.lean	nonReentrantTransient (EIP-1153) alongside the existing storage-slot nonReentrant. @[simp] nonReentrantTransient_locked_reverts + _revert_preserves_state.
4	Verity/EVM/MemoryModel.lean	MemState + myMload/myMstore + callWithReturnBuffer + Disjoint + call_preserves_disjoint_region + iterated form + memory_frame_under_arbitrary_callee.
5	Verity/EVM/Layout.lean	SolcLayout schema + canonicalSolcLayout + ScratchOutputBuffer + call_buffer_disjoint_from_heap and its MemoryModel.Disjoint form. Discharges the disjointness premise from standard solc-allocator invariants.
6	Verity/Trace.lean	Generic countMatching + emitLoop + origin lemma + emitter-contains lemma + count_le_one_under_pairwise_distinct. Parametric over event type and matching key.
8	Contracts/Common.lean	Rewrites let _ := rhs inside the contract DSL to a fresh-name binding so users can discard external-call results naturally.
7	deferred	verity_contract doc-comment support — requires parser surgery on a hot path; ship separately with cross-benchmark testing. Documented in docs/ROADMAP.md.

Removed since first push

Verity/Compiler/FromSolidity.lean has been removed pending a proper in-process translator design. A CLI-shelling wrapper is not sufficient trust reduction to justify the public API surface; the scaffold form was producing confusion about what was actually proven vs. shelled out. The follow-up in docs/ROADMAP.md no longer references it.

Documentation updates

• AXIOMS.md: External Call Module section now points to the new caller-frame preservation theorems and clarifies that EVM frame preservation is no longer an assumption.
• TRUST_ASSUMPTIONS.md: Add raise-slot helper and example #7 External Call Modules entry calls out the same shift.
• docs/ROADMAP.md: new section ✅ ERC-4337 Frame Primitives Landed with follow-ups (EvmYul ↔ frame correspondence, solc_disjoint tactic, verity_contract doc-comment support).

Build

lake build green on every new module and downstream consumer (Contracts.Common, Verity.Core).

Why this matters

The ERC-4337 EntryPoint benchmark exercises every part of Verity's external-call surface and was the first benchmark that needed proper EVM frame conditions to defeat the Certora-era 'arbitrary callee bytecode' challenge. The frame proofs were already in verity-benchmark; landing them upstream makes them available to every benchmark and replaces a trust assumption with a proven theorem.

Trust-gap reduction

Before this PR (per AXIOMS.md "External Call Module Assumptions"):

• Verity assumed that the contract-DSL call primitive was storage-pure.

After this PR:

• Verity.EVM.Frame proves the EVM-side equivalent (CALL preserves caller state) as a theorem over the abstract CallerFrame / CalleeResult interface, universally quantified over callee bytecode.
• Closing the abstract-model ↔ EvmYul correspondence is the explicit next item in docs/ROADMAP.md.

Follow-ups (tracked in docs/ROADMAP.md)

1. EvmYul ↔ frame correspondence (~2-4 weeks). Closes the abstract-model gap. Not yet scheduled.
2. solc_disjoint tactic (~1 week). Removes the boilerplate around call_buffer_disjoint_from_heap.
3. verity_contract doc-comment support (~1 day, deferred). Parser surgery; ship as its own PR.

🤖 Generated with Claude Code

[vercel]

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

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jun 7, 2026 1:06pm

[Th0rgal]

@BugBot review

[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 f3732ac. Configure here.}