ERC-4337 EntryPoint Execution Invariant

This is a deliberately small result. It is about the modeled validation and execution slice around handleOps, not the whole ERC-4337 protocol and not every behavior of the production EntryPoint.

The exact claim

For a modeled operation at index i, its execution count is one if validation passed and its callData is nonempty. Otherwise the count is zero.

That execution-count statement is the artifact differential in PR #13. The Lean result in PR #14 is different and narrower: its single-operation SourceIR proves validation order, nonce mutation, calldata-sensitive sender-call observables, caught modeled sender reverts, and observable rollback on validation failure. It does not prove that the compiled artifact implements the SourceIR.

The runnable scenario is reduced from the upstream v0.9 case account should pay for tx. It removes signatures, gas-accounting conclusions, and payment conclusions so the test observes only the scoped invariant.

Both targets receive one two-operation batch. Both modeled validations succeed. Operation 0 has 0xdeadbeef callData and records exactly one execution. Operation 1 has empty callData and records zero executions.

This all-valid scenario does not test batch scheduling. Upstream v0.9 validates every operation through _iterateValidationPhase, emits BeforeExecution, and only then executes the batch. The pinned Verity model instead calls handleOp per element, so it can execute op 0 before validating op 1. Public multi-operation handleOps refinement is therefore blocked and divergent.

Evidence, kept separate

• Model: PR #14 defines a single-operation SourceIR with validation trace, nonce state, sender-call payload/revert bit, and rollback outcome.
• Proof: Lean 4.22 checks six named obligations for that SourceIR. The mapping gate rejects missing scoped rows, AST/span drift, unclassified boundaries, sorry, admit, and new axioms.
• Artifact: PR #13 records the Verity bytecode checksum and generation provenance. An artifact is not itself a proof of source refinement.
• Differential test: PR #13 independently deploys the pinned upstream and Verity artifacts and observes counts 1 and 0 for one reduced two-op scenario. One passing scenario is not universal equivalence.
• Assumptions and boundaries: arbitrary account, paymaster and sender bytecode; EVM call frames; ABI encoding; gas; deposits; postOp; and beneficiary compensation are not refined.

What actually ran

The modes deploy independently. The upstream mode reads creation bytecode from the deployment artifact at pinned account-abstraction commit b36a1ed. The Verity mode verifies and deploys the generated artifact directly. It is not an upstream proxy.

The faithful source pipeline also ran its original differential suite: 4 passed, 0 failed, 0 skipped. The extracted repository scenario intentionally keeps only the one invariant-shaped case.

Artifact provenance

• Differential artifact and scenario: erc4337-verity PR #13
• Source lock, mapping, SourceIR and Lean obligations: erc4337-verity PR #14
• Verity artifact: 2,903 bytes, SHA-256 9c1e575266112461c7340d6e353561a4312928439fa8ab3c6494daec5ff4c843
• Verity compiler pin: 1fffe16c4fc910a7316d1dddc59dab5ab7fb1c8e
• Generation benchmark commit: 5a295c53300cd55f6ad9fe149678888db71bd9db
• Tools: Lean 4.22.0, solc 0.8.28, Foundry 1.6.0-rc1.

PR #13 records hashes for the source, compile driver, adapter generator, faithful runner, generated Yul, linked Yul, upstream deployment artifact, upstream creation bytecode, and final Verity bytecode. PR #14 separately pins the complete 29-source Solidity import closure, solc settings, compact AST, source hashes, AST identities, CFG anchors, observables and theorem names for the six scoped mapping rows.

Reproduce it

git clone https://github.com/lfglabs-dev/erc4337-verity
cd erc4337-verity
git fetch origin pull/14/head:phase1-source-refinement
git checkout phase1-source-refinement
git submodule update --init --recursive
python3 scripts/check_source_mapping.py
python3 scripts/generate_source_lock.py --solc /path/to/solc-0.8.28 --check
(cd verity/entrypoint-v0.9 && lake build)
harness/foundry/run-yoav-invariant.sh upstream
harness/foundry/run-yoav-invariant.sh verity

Prerequisites are Lean 4.22.0, Foundry 1.6.0-rc1, solc 0.8.28, Python 3, and jq. CI checks the source lock, mapping completeness and Lean build, then runs the upstream and Verity differential modes. The repository contains a real git submodule pinned to b36a1ed; CI initializes that gitlink and shallow-fetches the v0.9.0 tag inside it before checking the pin.

What remains adapter-required

This run does not establish complete validation ABI correspondence. The faithful post-link adapter projects the successful-validation result used here. Signed SimpleAccount validation, canonical tuple and hash forwarding, and signature rejection remain open.

Exact custom errors, stake and deposit tuples, full paymaster paths, simulation, aggregation, factories and initCode, events, gas and prefund accounting, penalties, beneficiary payments, batch-wide EVM rollback, and Hardhat/TypeChain fixture recognition remain unproved or adapter-required. PR #14 proves only observable rollback in its single-operation SourceIR.

Accordingly, the other 74 mapped upstream EntryPoint cases—and the unreduced assertions in the source case—are not claimed as Verity passes. This is one runnable scenario for one invariant, not a complete ERC-4337 verification claim. The public handleOps mapping is blocked and divergent because the source uses a validate-all- then-execute-all schedule while the pinned model processes each operation validate-then-execute. Phase 1 proves only single-op subpaths, not that batch schedule or batch-wide EVM rollback.