diff --git a/components/research/EntryPointGuarantee.jsx b/components/research/EntryPointGuarantee.jsx new file mode 100644 index 0000000..d271f4a --- /dev/null +++ b/components/research/EntryPointGuarantee.jsx @@ -0,0 +1,86 @@ +import { useState, useEffect, useRef } from 'react' + +const FORMAL_INVARIANTS = [ + 'attemptExecute(i) → validated(i)', + 'validated(i) → attemptExecute(i)', + 'handleOps reverts → no attemptExecute(i)' +] + +export default function EntryPointGuarantee() { + const [showEnglish, setShowEnglish] = useState(true) + const timerRef = useRef(null) + + useEffect(() => { + timerRef.current = setTimeout(() => setShowEnglish(false), 5000) + return () => clearTimeout(timerRef.current) + }, []) + + const handleToggle = () => { + if (timerRef.current) { + clearTimeout(timerRef.current) + timerRef.current = null + } + setShowEnglish((prev) => !prev) + } + + return ( +
+ + +
+
+ {FORMAL_INVARIANTS.map((formal, i) => ( + + {formal} + + ))} +
+
+

+ In the modeled handleOps control flow, EntryPoint reaches a user + operation's execution path if and only if that same operation + successfully passed validation. +

+
+
+
+ ) +} diff --git a/data/research.js b/data/research.js index 07d639e..c3429e5 100644 --- a/data/research.js +++ b/data/research.js @@ -1,4 +1,14 @@ export const research = [ + { + slug: 'erc4337-entrypoint-execution', + title: 'ERC-4337 EntryPoint Execution Invariant', + subtitle: + 'Formally verified validation-before-execution control-flow slice for EntryPoint.', + description: + 'How we proved that the modeled EntryPoint handleOps execution path is reached exactly when validation succeeds, using Verity and Lean 4.', + date: '2026-04-24', + tag: 'Case study' + }, { slug: 'midas-feed-growth-safety', title: 'Midas Growth-Aware Feed Safety Guarantees', diff --git a/pages/research/erc4337-entrypoint-execution.jsx b/pages/research/erc4337-entrypoint-execution.jsx new file mode 100644 index 0000000..267302b --- /dev/null +++ b/pages/research/erc4337-entrypoint-execution.jsx @@ -0,0 +1,348 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import EntryPointGuarantee from '../../components/research/EntryPointGuarantee' +import Disclosure from '../../components/research/Disclosure' +import CodeBlock from '../../components/research/CodeBlock' +import ExternalLink from '../../components/research/ExternalLink' +import Hypothesis from '../../components/research/Hypothesis' +import { getSortedResearch } from '../../lib/getSortedResearch' + +const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark +cd verity-benchmark +git checkout feat/erc4337-entrypoint-invariant +lake build Benchmark.Cases.ERC4337.EntryPointInvariant.Compile` + +const ENTRYPOINT_SOL = + 'https://github.com/eth-infinitism/account-abstraction/blob/v0.9.0/contracts/core/EntryPoint.sol' + +const BENCHMARK_BRANCH = + 'https://github.com/lfglabs-dev/verity-benchmark/blob/feat/erc4337-entrypoint-invariant' + +const VERITY_PR = 'https://github.com/lfglabs-dev/verity/pull/1746' + +export default function ERC4337EntryPointExecutionPage() { + const otherResearch = getSortedResearch().filter( + (r) => r.slug !== 'erc4337-entrypoint-execution' + ) + + return ( + <> + + + ERC-4337 EntryPoint Execution Invariant | Research | LFG Labs + + + + +
+ + +
+

+ ERC-4337 EntryPoint Execution Invariant +

+
+ +
+ +

+ ERC-4337 adds account abstraction without changing Ethereum + consensus. Users submit{' '} + UserOperations, + bundlers collect them, and a singleton{' '} + EntryPoint{' '} + contract validates and executes the bundle onchain. +

+

+ EntryPoint is the trusted router in that flow. For every + operation, it may deploy the account, call account validation, + call paymaster validation, account for gas, execute the account + call, run post-operation accounting, and compensate the bundler. + The security-critical question is simple to say and hard to + prove in full: can an operation reach execution unless that same + operation passed validation? +

+
+ +
+

+ Why this matters +

+

+ ERC-4337 accounts and paymasters are arbitrary contracts. The + full theorem engineers want would quantify over all of that EVM + behavior. This benchmark proves a narrower, useful slice: the + two-loop EntryPoint control flow that gates the operation + execution path on successful validation. +

+ +

+ The proof tracks validation outcomes and execution-path + attempts for each operation index in a call to{' '} + handleOps. +

+
    +
  • + Safety: EntryPoint never attempts the + execution path for operation{' '} + i unless + validation for that same operation succeeded in the model. +
    • +
  • + Liveness: when the modeled validation phase + succeeds, every in-bounds operation reaches the execution + path. +
    • +
  • + Revert behavior: if validation fails and + handleOps{' '} + reverts, no execution-path attempt is recorded. +
    • +
+

+ The model records reaching _executeUserOp, + not successful account execution. It intentionally elides the + callData.length > 0{' '} + branch, gas accounting, and arbitrary account/paymaster + internals. +

+ +
+ +
+

+ How this was proven +

+

+ The Verity model follows the selected Solidity{' '} + EntryPoint.sol{' '} + control-flow slice. It keeps the validation pass over the bundle + and the transition to the per-operation execution wrapper, while + abstracting data payloads and most accounting details. +

+
    +
  • + Validation phase: models validation as a + universally quantified boolean outcome per operation. +
    • +
  • + Native Verity shape: includes a contract model + using bounded loops, oracle-backed calls, and low-level + try/catch support from Verity PR 1746. +
    • +
  • + Execution phase: records whether the modeled + execution path is reached for each operation index. +
    • +
  • + Failure path: preserves the all-or-nothing + validation loop behavior: a validation failure reverts the + modeled batch before execution attempts. +
    • +
+

+ The proof is written in Lean 4 over the Verity model. The main + theorem decomposes the English statement into safety, liveness, + all-validated-on-success, all-executed-on-success, and + no-execution-on-revert lemmas, then combines the first two into + the biconditional. +

+

+ The benchmark case lives in{' '} + + Contract.lean + + , with specifications in{' '} + + Specs.lean + {' '} + and proofs in{' '} + + Proofs.lean + + . The required Verity features for this native-loop and low-level + call model are introduced in{' '} + Verity PR 1746. +

+ + {VERIFY_COMMAND} +

+ If the build succeeds, Lean has checked every proof term.{' '} + + Benchmark pull request + +

+ +
+ +
+

+ Proof status +

+

+ The case proves the selected EntryPoint control-flow invariant + and supporting properties.{' '} + + Proofs.lean + {' '} + is sorry-free. +

+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
PropertyMeaningStatus
execution_implies_validationno execution-path attempt without validationproven
validation_implies_executionvalidated operations reach the execution pathproven
all_validated_on_successa successful modeled batch has all validations trueproven
all_executed_on_successa successful modeled batch attempts every execution pathproven
no_execution_on_revertvalidation failure records no execution attemptsproven
+
+
+ +
+

+ Assumptions +

+

+ The proof does not establish full arbitrary account/paymaster EVM + correctness. The remaining assumptions are explicit: the selected + Solidity control-flow slice, Verity's semantics for the modeled + constructs, and the abstraction from concrete calls and calldata + to per-index validation and execution-path outcomes. +

+
    + + The case is pinned to EntryPoint v0.9.0 and models the + `handleOps` validation loop plus execution loop, not every + helper branch in the contract. + + + The native Verity model uses oracle-backed calls for the + validation and execution-attempt stubs, while the pure proof + quantifies over all validation result lists. + + + The English guarantee is expressed as a theorem about indexed + validation outcomes and execution-path attempts. It does not + claim account-call success or calldata equivalence. + +
+

+ + View specs in Lean + + + View proofs in Lean + +

+
+ +
+

+ Learn more +

+

+ + ERC-4337 + + {', the account abstraction standard that defines UserOperations and EntryPoint.'} +

+

+ + EntryPoint audits + + {', including OpenZeppelin, Spearbit, and Cantina reviews of the reference implementation.'} +

+

+ + What is a formal proof? + {' '} + A short explanation for non-specialists. +

+
+ + {otherResearch.length > 0 && ( +
+

+ More research +

+
+ {otherResearch.map((r) => ( + + ))} +
+
+ )} +
+ + + ) +}