Conversation
* 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
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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