Skip to content

v0.4.0 release (#50) - #53

Open
leekt wants to merge 27 commits into
masterfrom
v0.4.0
Open

leekt wants to merge 27 commits into
masterfrom
v0.4.0

Conversation

@leekt

@leekt leekt commented Apr 26, 2026

Copy link
Copy Markdown
Contributor
  • chore: update build config for Solidity 0.8.33

  • refactor: centralize type definitions, errors, events, and constants

  • refactor: centralize constants in libs and update patterns

  • fix: security and correctness improvements

  • docs: add NatSpec documentation to variant contracts

  • test: add mock contracts and update test infrastructure

  • test: add BTT trees and tests for Kernel, Factory, and Staker

  • test: add unit, integration, fuzz, invariant, and halmos tests

  • docs: update README, gas snapshots, and add release v0.4.0

leekt and others added 27 commits April 27, 2026 08:24
* chore: update build config for Solidity 0.8.33

* refactor: centralize type definitions, errors, events, and constants

* refactor: centralize constants in libs and update patterns

* fix: security and correctness improvements

* docs: add NatSpec documentation to variant contracts

* test: add mock contracts and update test infrastructure

* test: add BTT trees and tests for Kernel, Factory, and Staker

* test: add unit, integration, fuzz, invariant, and halmos tests

* docs: update README, gas snapshots, and add release v0.4.0
* fix: bump nonce on validation init to default-deny selectors

* fix: validate validator returndata length and require code

* fix: filter permission stateless match by module type

* fix: require root validation be installed

* test: adapt empty-returndata test to graceful-failure behavior

* chore: update gas snapshots after rebase onto v0.4.0

* test(halmos): prove Lib4337.intersectValidationData aggregator precedence (6 rules)

* test(halmos): prove KernelUUPS.upgradeToAndCall gates on EntryPoint or self

* test(halmos): prove _verifyStatelessSignature filters by moduleType

* test(halmos): prove parseNonce roundtrips validator and permission

* test(halmos): prove Kernel7702 + KernelImmutableECDSA fallback ECDSA iff

* test(halmos): prove Staker.approveFactoryWithSignature replay safety

* test(halmos): prove KernelFactory.deploy determinism and idempotency

* test(halmos): prove _checkAndIncrementNonce cannot overflow uint64

* test(halmos): prove _initializeValidation bumps nonce on every path

* docs(audit): add FV round 1 plan, gap audit, and findings log

* test(halmos): prove _checkNonce and _checkAndIncrementNonce agree below saturation

* docs(audit): record Phase B finding (nonce check/increment agreement)

* chore(certora): scaffold harness for Kernel v4 formal verification

* test(certora): add KernelHarness for read-only storage accessors

* test(certora): prove executeUserOp inner-delegatecall gated by validateUserOp

* docs(audit): record Phase C finding (fast-path privilege escalation)

* fix: block executeUserOp.selector grant to non-root validations

* test(certora): re-verify executeUserOp fix; surface setRoot residual finding

* fix: bump old root nonce on _setRoot rotation

* docs(certora): close Phase C — invariant unprovable under CVL summaries

* test(certora): Phase D — prove permission totality, setRoot LIFO, view/write equivalence

* docs(audit): record Phase D Certora results (3/3 properties verified)

* test(kontrol): scaffold #15 ERC1271 nested EIP-712 claim (partial; timeout)

* test(halmos): prove ERC1271 nested EIP-712 PersonalSign verifier-bypass property

* docs(audit): record Phase E results (#15 PersonalSign proven, TypedDataSign partial)

* docs(audit): FV Round 2 plan — proof-obligation coverage strategy

* test(kontrol): tighten #15 bound to signature.length <= 96 (Round 2 retry)

* docs(audit): manual CFG proof closes #15 nested EIP-712 verifier-bypass property

* test(certora): writer-local decomposition closes Phase C bypass-impossible invariant

* docs(audit): mark Phase C invariant closed via writer-local decomposition

* docs(audit): bootstrap FV_COVERAGE.md — proof-obligation matrix for Round 2 Phase 2

* test(halmos): prove _verifyInstallSignatureRaw signature gate

* test(halmos): prove _executeCall + _executeDelegateCall return shape and revert handling

* test(halmos): prove _installHash determinism and field-sensitivity

* test(halmos): prove onlyOwner on Staker stake/approveFactory functions

* test(certora): prove _checkValidation routing predicate per vType

* test(certora): writer-local invariants for executor/selector/hook storage

* docs(audit): update FV_COVERAGE matrix — Phase 2 closure (~83% obligations proven)

* test(halmos): prove top-level execute and executeFromExecutor access control

* fix: reject zero-address module in _installSelector at install boundary

* test(certora): prove validateUserOp then executeUserOp inner-selector composition

* docs(audit): FV_COVERAGE — all Round 2 remaining gaps closed

* ci: lower optimizer_runs to 10 + skip oversized halmos harnesses from --sizes

* docs(audit): FV_COVERAGE — close stale ModuleManager._verifyInstallSignatureRaw row

* chore: update gas snapshots after optimizer_runs drop

* test(halmos): prove chainAgnosticUserOpHash determinism, chain-agnosticism, field-sensitivity

* docs(audit): FV_COVERAGE — sync _installSelector row with shipped hardening + bump commit count

* ci: enable via_ir to restore optimizer_runs=200 with comfortable EIP-170 margin

* docs: sync FV coverage metadata

* chore: gitignore .claude local state and FV research scratch

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
…ay (M), validity-format ordering (M) (#58)

* fix: gate enable-mode install on root signature success

* test: enable-mode install rejected on failed root signature

* fix: advance factory nonce on direct approval changes

* test: direct factory approval advances nonce

* fix: normalize validity ranges before format classification

* test: validity-format ordering regressions

* fix: RP-01 checkValidation EntryPoint v0.9 parity (#59)

* fix: checkValidation block-mode and exclusive validAfter per EntryPoint v0.9

* test: cover checkValidation EntryPoint v0.9 boundaries

* fix: vendor canonical EntryPoint v0.9 release initcode and address
Remove generic type-4 hooks, hook registration storage, sentinel-based installation state, and embedded hook configuration from validations, executors, and fallback selectors.
Remove stateless ERC-1271 module installation and the validation-mode signature byte. Structured signatures now begin with their validation type while ERC-4337 enable mode remains supported.
Add type-11 hooks scoped to validations, executors, and selectors, with explicit scoped identifiers and lifecycle checks. Route hooked validation execution through executeUserOp and prevent direct validation reentry.
Replace generic-hook coverage with validation-, executor-, and selector-scoped lifecycle and execution tests. Update formal harnesses, invariants, mocks, and gas snapshots for the scoped model.
Replace stateless enable-mode coverage with the validation-type-first structured signature format and Kernel7702 raw-signature cases. Remove obsolete stateless validators and formal tests, and differentially fuzz Lib4337 validity handling against EntryPoint v0.9.
Restore the v0.4.0 entry-point gate on fallback selectors that have no
scoped execution hook installed. Installing a type-11 selector-scoped
execution hook makes a selector publicly callable; without one only the
entry point may route to it.

Update tests to install scoped hooks where public access is asserted,
add a regression test and halmos proofs for the gate, and document the
access control in the README.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant