Add ERC-4337 EntryPoint invariant benchmark case

[Th0rgal]

Summary

• Adds the ERC-4337 EntryPoint core invariant as a new benchmark case, proving the property that Certora spent over a year attempting to verify with SMT solvers
• Models the two-loop handleOps structure (validation phase + execution phase) as pure Lean functions with universally quantified validation results
• All 8 theorems fully proven with zero sorry — builds clean with lake build

What is proven

The core ERC-4337 security property from the EIP spec:

"The EntryPoint only calls the sender with userOp.callData if and only if validateUserOp on that specific sender has passed."

This decomposes into:

Theorem	Property	Difficulty
execution_implies_validation	Safety: execution → validation	medium
validation_implies_execution	Liveness: validation → execution	medium
execution_iff_validation	Combined biconditional (the full invariant)	hard
all_validated_on_success	All-or-nothing validation loop	easy
all_executed_on_success	All executions attempted on success	easy
no_execution_on_revert	No execution on validation failure	easy
single_op_execution_on_validation	Verity contract: batchExecuted set	easy
single_op_fee_collected	Verity contract: fees incremented	easy

Why this matters

Certora's SMT-based approach cannot universally quantify over arbitrary Turing-complete programs (the account/paymaster contracts). Lean's interactive theorem proving handles this naturally — the proofs hold for ALL possible validation outcomes via standard universal quantification over List Bool.

Files

• Benchmark/Cases/ERC4337/EntryPointInvariant/Contract.lean — Abstract model of handleOps two-loop structure
• Benchmark/Cases/ERC4337/EntryPointInvariant/Specs.lean — Invariant specifications
• Benchmark/Cases/ERC4337/EntryPointInvariant/Proofs.lean — Complete proofs (no sorry)
• Benchmark/Cases/ERC4337/EntryPointInvariant/Compile.lean — Build gate
• cases/erc4337/entry_point_invariant/ — YAML metadata (case + 8 tasks)

Test plan

• lake build passes with no errors
• Zero sorry in all proof files
• All existing benchmark cases still build

🤖 Generated with Claude Code

---

Note

Medium Risk
Adds a new benchmark case with substantial new Lean/Verity model+proof code and updates the benchmark registry/report, so breakage risk is mostly around build/integration and task generation rather than runtime behavior.

Overview
Adds a new ERC-4337 EntryPointInvariant benchmark case, including a pure-Lean control-flow model of handleOps (validation phase + execution phase), corresponding Verity contract model (EntryPointModel), and completed reference proofs/specs for the execution-attempt iff validation-passed invariant.

Wires the new case into the benchmark entrypoints (Benchmark.lean, Benchmark/Cases.lean) and updates REPORT.md to include the new family/case and its associated proof tasks.

Includes minor API renaming in the Zama ERC-7984 model (mint parameter to → recipient) and updates the related specs/proofs and generated task stubs accordingly.

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

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 81bd0dfabd

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[cursor]

Cursor Bugbot has reviewed your changes and found 2 potential issues.

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

^{Reviewed by Cursor Bugbot for commit 81bd0df. Configure here.}

[Th0rgal]

Migrated this benchmark PR to the faithful Verity model from lfglabs-dev/verity#1746.

Changes pushed in 7891277:

• pins verity to 57d47acd44f273df9848bc2df612d2daa8aedf18
• adds a native ERC-4337 handleOpsNative model using executable forEach, oracle-backed externalCall, and oracle-backed call/tryCatch
• updates the Zama mint binder from to to recipient for compatibility with the new Verity syntax

Local verification: lake build passes.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 789127790c

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: a8bf0bcd7f

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Keep case verity_version in sync with pin bump

Updating the global Verity dependency pin here to de937... without updating existing cases/*/*/case.yaml manifests leaves most cases still declaring 4ebe..., and scripts/run_case.sh records provenance from each case manifest’s verity_version rather than from Lake. In practice, non-ERC4337 runs after this commit build against one Verity commit but publish a different verity_commit in results metadata, which breaks reproducibility/auditability; either update all case manifests in the same commit or source the recorded commit from lakefile.lean.

Useful? React with 👍 / 👎.