From 731e514e8a384433fbcaf498b9d6784fe78932ca Mon Sep 17 00:00:00 2001 From: Chris Hunter Date: Tue, 7 Jul 2026 17:19:17 -0400 Subject: [PATCH] test: add Halmos symbolic proofs and invariant suite for AccountConfiguration - test/fv: symbolic (Halmos) proofs, stateful invariant suite, handler, and harness for AccountConfiguration. - Add halmos.toml and requirements-fv.txt (pinned halmos) for local + CI runs. - foundry.toml: add [fuzz]/[invariant] run configuration for the invariant suite. - CI: add a formal-verification job running the symbolic proofs. - .gitignore: ignore the local Halmos virtualenv and cache. --- .github/workflows/test.yml | 30 +++ .gitignore | 4 + foundry.toml | 8 + halmos.toml | 14 + requirements-fv.txt | 4 + test/fv/AccountConfiguration.invariant.t.sol | 148 +++++++++++ test/fv/AccountConfiguration.symbolic.t.sol | 177 +++++++++++++ test/fv/AccountConfigurationHandler.sol | 260 +++++++++++++++++++ test/fv/AccountConfigurationHarness.sol | 100 +++++++ 9 files changed, 745 insertions(+) create mode 100644 halmos.toml create mode 100644 requirements-fv.txt create mode 100644 test/fv/AccountConfiguration.invariant.t.sol create mode 100644 test/fv/AccountConfiguration.symbolic.t.sol create mode 100644 test/fv/AccountConfigurationHandler.sol create mode 100644 test/fv/AccountConfigurationHarness.sol diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 55e6933..1c50fa3 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -41,3 +41,33 @@ jobs: - name: Run Forge tests run: forge test -vvv + + formal-verification: + name: Symbolic verification (Halmos) + runs-on: ubuntu-latest + permissions: + contents: read + steps: + - name: Harden the runner (Audit all outbound calls) + uses: step-security/harden-runner@a90bcbc6539c36a85cdfeb73f7e2f433735f215b # v2.15.0 + with: + egress-policy: audit + + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5.0.1 + with: + persist-credentials: false + submodules: recursive + + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@8789b3e21e6c11b2697f5eb56eddae542f746c10 # v1.7.0 + + - name: Set up Python + uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0 + with: + python-version: "3.12" + + - name: Install Halmos + run: pip install -r requirements-fv.txt + + - name: Run Halmos symbolic proofs + run: halmos --match-contract AccountConfigurationSymbolicTest diff --git a/.gitignore b/.gitignore index 0117584..87a2ab9 100644 --- a/.gitignore +++ b/.gitignore @@ -16,6 +16,10 @@ docs/ # Node node_modules/ +# Formal-verification tooling (Halmos) local virtualenv +.venv-fv/ +halmos-cache/ + # Tool reports (generated output) **/reports/*.json **/reports/*.txt diff --git a/foundry.toml b/foundry.toml index 4869b7f..79054f9 100644 --- a/foundry.toml +++ b/foundry.toml @@ -8,6 +8,14 @@ remappings = [ "solady/=lib/solady/src/", ] +[fuzz] +runs = 256 + +[invariant] +runs = 256 +depth = 500 +fail_on_revert = false + [lint] lint_on_build = false exclude_lints = [ diff --git a/halmos.toml b/halmos.toml new file mode 100644 index 0000000..eeac18c --- /dev/null +++ b/halmos.toml @@ -0,0 +1,14 @@ +# Halmos symbolic-verification configuration for the EIP-8130 reference implementation. +# See https://github.com/a16z/halmos for the full option reference. +# +# Run all symbolic proofs: halmos --match-contract AccountConfigurationSymbolicTest +[global] +# Restrict discovery to the symbolic proof suite (files named *.symbolic.t.sol drive the `check_*` proofs). +match-contract = "SymbolicTest" + +# Loop/array unrolling bound for symbolic execution. The proofs are written to stay within small bounds; raise this +# if a new proof needs to reason about longer dynamic arrays. +loop = 4 + +# Fail fast and print a concrete counterexample model when a proof is violated. +early-exit = false diff --git a/requirements-fv.txt b/requirements-fv.txt new file mode 100644 index 0000000..aeb21a8 --- /dev/null +++ b/requirements-fv.txt @@ -0,0 +1,4 @@ +# Formal-verification tooling for the EIP-8130 reference implementation. +# Install into a virtualenv: python3 -m venv .venv-fv && . .venv-fv/bin/activate && pip install -r requirements-fv.txt +# Then run the symbolic proofs: halmos --match-contract AccountConfigurationSymbolicTest +halmos==0.3.3 diff --git a/test/fv/AccountConfiguration.invariant.t.sol b/test/fv/AccountConfiguration.invariant.t.sol new file mode 100644 index 0000000..4054c4e --- /dev/null +++ b/test/fv/AccountConfiguration.invariant.t.sol @@ -0,0 +1,148 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.30; + +import {Test} from "forge-std/Test.sol"; + +import {AccountConfigurationHarness} from "./AccountConfigurationHarness.sol"; +import {AccountConfigurationHandler} from "./AccountConfigurationHandler.sol"; +import {DefaultAccount} from "../../src/accounts/DefaultAccount.sol"; + +/// @notice Layer 1 of the verification stack: stateful invariant (fuzz) testing. +/// +/// These invariants encode the security-critical guarantees that {AccountConfiguration} currently states only in +/// prose comments. The handler drives the contract through long randomized sequences of validly-signed operations; +/// after every step Foundry re-checks each `invariant_*` below. A single counterexample sequence fails the run. +contract AccountConfigurationInvariantTest is Test { + uint8 constant SCOPE_CONFIG = 0x08; + + AccountConfigurationHarness internal cfg; + AccountConfigurationHandler internal handler; + address internal K1; + + function setUp() public { + cfg = new AccountConfigurationHarness(); + K1 = cfg.K1_AUTHENTICATOR(); + address impl = address(new DefaultAccount(address(cfg))); + handler = new AccountConfigurationHandler(cfg, impl); + + // Only fuzz the state-mutating handler actions (not its view getters). + bytes4[] memory selectors = new bytes4[](7); + selectors[0] = handler.handler_createAccount.selector; + selectors[1] = handler.handler_authorize.selector; + selectors[2] = handler.handler_revoke.selector; + selectors[3] = handler.handler_lock.selector; + selectors[4] = handler.handler_initiateUnlock.selector; + selectors[5] = handler.handler_warp.selector; + selectors[6] = handler.handler_createAccountBadCode.selector; + targetSelector(FuzzSelector({addr: address(handler), selectors: selectors})); + targetContract(address(handler)); + } + + /// @notice INV-1: The inline-k1 self and the non-k1 self are never simultaneously live, and whenever the inline + /// self is live its `_actorConfig` self home is empty (and never holds a stray K1 selector). This is the + /// mutual-exclusion guarantee `_authorizeActor` / `_revokeActor` claim in prose. + function invariant_selfHomesMutuallyExclusive() public view { + uint256 n = handler.accountsLength(); + for (uint256 i; i < n; i++) { + address account = handler.accounts(i); + bool inlineLive = cfg.h_inlineSelfLive(account); + bool nonK1Live = cfg.h_nonK1SelfLive(account); + assertFalse(inlineLive && nonK1Live, "both self homes live"); + + address rawSelfAuth = cfg.h_actorConfigAuthenticator(account, cfg.h_selfActorId(account)); + if (inlineLive) { + assertEq(rawSelfAuth, address(0), "inline self live but _actorConfig self home populated"); + } + // The k1 self never lives in _actorConfig (it is inline-only), so the raw self home is never a K1 selector. + assertTrue(rawSelfAuth != K1, "K1 selector leaked into _actorConfig self home"); + } + } + + /// @notice INV-2: Across both homes, `_policyCommitment` and `_policyManager` are non-zero *iff* the actor's + /// effective `policyType` is non-zero. No stale policy state may leak past a revoke or a downgrade to + /// POLICY_NONE. This is the invariant `getPolicyCommitment` / `getPolicyManager` rely on. + function invariant_policySlotsIffPolicyType() public view { + uint256 n = handler.pairsLength(); + for (uint256 i; i < n; i++) { + (address account, bytes32 actorId) = handler.pairAt(i); + (bool live, uint8 policyType,) = _effective(account, actorId); + + bool hasPolicy = live && policyType != 0; + bool commitmentSet = cfg.h_policyCommitment(account, actorId) != bytes32(0); + bool managerSet = cfg.h_policyManager(account, actorId) != address(0); + + assertEq(commitmentSet, hasPolicy, "commitment set != has policy"); + assertEq(managerSet, hasPolicy, "manager set != has policy"); + } + } + + /// @notice INV-3: Any live policy-bearing actor is scope-restricted and never holds CONFIG (change-actors) scope. + /// Otherwise a gated key could authorize fresh unrestricted actors and escape its own policy — the exact + /// escalation `_authorizeActor` guards against. + function invariant_policyActorCannotChangeActors() public view { + uint256 n = handler.pairsLength(); + for (uint256 i; i < n; i++) { + (address account, bytes32 actorId) = handler.pairAt(i); + (bool live, uint8 policyType, uint8 scope) = _effective(account, actorId); + if (live && policyType != 0) { + assertTrue(scope != 0, "policy actor has scope 0"); + assertEq(scope & SCOPE_CONFIG, 0, "policy actor holds CONFIG scope"); + } + } + } + + /// @notice INV-4: Per-account change sequences are monotonically non-decreasing. Any observed regression would + /// open a signed-change replay window; the handler flips this flag if it ever sees one. + function invariant_sequencesMonotonic() public view { + assertTrue(handler.sequenceMonotonicityHeld(), "sequence regressed"); + } + + /// @notice INV-5: A created account is permanently initialized (localSequence >= 1), which is what blocks + /// re-initialization via createAccount/importAccount. + function invariant_createdAccountsStayInitialized() public view { + uint256 n = handler.accountsLength(); + for (uint256 i; i < n; i++) { + address account = handler.accounts(i); + assertGe(cfg.getChangeSequences(account).local, 1, "created account de-initialized"); + } + } + + /// @notice INV-6: A successfully created account always has deployed code, and a createAccount whose deployment + /// failed leaves no state and no code behind. This is the "no orphaned config" guarantee enforced by the + /// CREATE2 return-value check; the pre-fix contract (swallowed CREATE2 result) would violate it. + function invariant_noOrphanedAccountState() public view { + uint256 n = handler.accountsLength(); + for (uint256 i; i < n; i++) { + address account = handler.accounts(i); + assertGt(account.code.length, 0, "created account has no code"); + } + + uint256 f = handler.failedCreationsLength(); + for (uint256 i; i < f; i++) { + address ghost = handler.failedCreations(i); + assertEq(ghost.code.length, 0, "failed creation left code"); + assertEq(cfg.getChangeSequences(ghost).local, 0, "failed creation left local sequence"); + assertEq(cfg.getChangeSequences(ghost).multichain, 0, "failed creation left multichain sequence"); + } + } + + // ── Helpers ── + + /// @dev Resolve an actor's effective liveness, policyType and scope, mirroring the contract's home routing: + /// a populated `_actorConfig` entry wins; otherwise the inline-k1 self applies to the self-actorId when + /// live; otherwise the actor is not live. + function _effective(address account, bytes32 actorId) + internal + view + returns (bool live, uint8 policyType, uint8 scope) + { + address rawAuth = cfg.h_actorConfigAuthenticator(account, actorId); + if (rawAuth != address(0)) { + return (true, cfg.h_actorConfigPolicyType(account, actorId), cfg.h_actorConfigScope(account, actorId)); + } + if (actorId == cfg.h_selfActorId(account) && cfg.h_inlineSelfLive(account)) { + return (true, cfg.h_inlineSelfPolicyType(account), cfg.h_inlineSelfScope(account)); + } + return (false, 0, 0); + } +} diff --git a/test/fv/AccountConfiguration.symbolic.t.sol b/test/fv/AccountConfiguration.symbolic.t.sol new file mode 100644 index 0000000..2ee7a60 --- /dev/null +++ b/test/fv/AccountConfiguration.symbolic.t.sol @@ -0,0 +1,177 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.30; + +import {Test} from "forge-std/Test.sol"; + +import {AccountConfiguration} from "../../src/AccountConfiguration.sol"; +import {AccountConfigurationHarness} from "./AccountConfigurationHarness.sol"; + +/// @notice Layer 2 of the verification stack: symbolic verification with Halmos. +/// +/// Each `check_*` function is explored by Halmos over the *entire* symbolic input domain (all scopes, expiries, +/// policy bytes, actor ids, ...) rather than sampled fuzz values, so a passing check is a bounded formal proof that +/// no input violates the asserted property. We drive the internal state-machine units directly via the harness's +/// `sym_*` wrappers, which lets Halmos reason about the storage transitions without having to model `ecrecover` +/// (the signature gate on the public change path). +/// +/// Run with: halmos --match-contract AccountConfigurationSymbolicTest +contract AccountConfigurationSymbolicTest is Test { + AccountConfigurationHarness internal cfg; + address internal K1; + address internal constant NON_K1 = address(0xA11CE); + uint8 internal constant SCOPE_CONFIG = 0x08; + + function setUp() public { + cfg = new AccountConfigurationHarness(); + K1 = cfg.K1_AUTHENTICATOR(); + } + + // ── _slicePolicy: exact, total parsing ── + + /// @notice POLICY_NONE with empty data yields the zero policy; any non-empty data reverts. + function check_slicePolicy_none(bytes calldata data) external view { + if (data.length == 0) { + (address m, bytes32 c) = cfg.sym_slicePolicy(0, data); + assert(m == address(0)); + assert(c == bytes32(0)); + } else { + try cfg.sym_slicePolicy(0, data) returns (address, bytes32) { + assert(false); // non-empty data under POLICY_NONE must revert + } catch {} + } + } + + /// @notice A gated policy blob of exactly `manager(20) || commitment(32)` parses back byte-for-byte, for every + /// non-zero manager and commitment. + function check_slicePolicy_parsesExactly(bytes32 mgrSeed, bytes32 commitment) external view { + address manager = address(uint160(uint256(mgrSeed))); + vm.assume(manager != address(0)); + vm.assume(commitment != bytes32(0)); + + bytes memory data = abi.encodePacked(manager, commitment); + (address gotM, bytes32 gotC) = cfg.sym_slicePolicy(1, data); + assert(gotM == manager); + assert(gotC == commitment); + } + + // ── _authorizeActor: storage round-trip + policy invariant (non-self actor) ── + + /// @notice For every scope/expiry, authorizing an ungated non-self k1 actor stores exactly those fields and + /// leaves the policy slots empty (the "commitment iff policyType" invariant, ungated direction). + function check_authorize_ungated_roundTrip(address account, bytes20 rawActor, uint8 scope, uint48 expiry) external { + vm.assume(account != address(0)); + vm.assume(bytes32(rawActor) != bytes32(bytes20(account))); // non-self + + bytes32 actorId = bytes32(rawActor); + AccountConfiguration.ActorConfig memory config = + AccountConfiguration.ActorConfig({authenticator: K1, scope: scope, expiry: expiry, policyType: 0}); + + cfg.sym_authorizeActor(account, actorId, config, ""); + + AccountConfiguration.ActorConfig memory got = cfg.getActorConfig(account, actorId); + assert(got.authenticator == K1); + assert(got.scope == scope); + assert(got.expiry == expiry); + assert(got.policyType == 0); + assert(cfg.getPolicyCommitment(account, actorId) == bytes32(0)); + assert(cfg.getPolicyManager(account, actorId) == address(0)); + } + + /// @notice A gated actor can only be authorized when it is scope-restricted and lacks change-actors scope; + /// when it is authorized, both policy slots become non-zero and the policyType is stored. + function check_authorize_gated_setsPolicyAndGuardsScope( + address account, + bytes20 rawActor, + uint8 scope, + bytes32 commitment + ) external { + vm.assume(account != address(0)); + vm.assume(bytes32(rawActor) != bytes32(bytes20(account))); + vm.assume(commitment != bytes32(0)); + + bytes32 actorId = bytes32(rawActor); + address manager = address(0xBEEF); + AccountConfiguration.ActorConfig memory config = + AccountConfiguration.ActorConfig({authenticator: K1, scope: scope, expiry: 0, policyType: 1}); + bytes memory policyData = abi.encodePacked(manager, commitment); + + bool legalScope = scope != 0 && scope & SCOPE_CONFIG == 0; + + try cfg.sym_authorizeActor(account, actorId, config, policyData) { + // Success implies the scope was legal, and the policy slots are now populated. + assert(legalScope); + assert(cfg.getPolicyCommitment(account, actorId) == commitment); + assert(cfg.getPolicyManager(account, actorId) == manager); + AccountConfiguration.ActorConfig memory got = cfg.getActorConfig(account, actorId); + assert(got.policyType == 1); + } catch { + // A revert implies the scope was illegal for a gated actor. + assert(!legalScope); + } + } + + // ── _revokeActor: total cleanup ── + + /// @notice Revoking a previously-gated non-self actor clears its config and both policy slots. + function check_revoke_clearsEverything(address account, bytes20 rawActor, bytes32 commitment) external { + vm.assume(account != address(0)); + vm.assume(bytes32(rawActor) != bytes32(bytes20(account))); + vm.assume(commitment != bytes32(0)); + + bytes32 actorId = bytes32(rawActor); + AccountConfiguration.ActorConfig memory config = AccountConfiguration.ActorConfig({ + authenticator: K1, + scope: 0x02, // SCOPE_SENDER: legal for a gated actor + expiry: 0, + policyType: 1 + }); + cfg.sym_authorizeActor(account, actorId, config, abi.encodePacked(address(0xBEEF), commitment)); + + cfg.sym_revokeActor(account, actorId); + + assert(!cfg.isActor(account, actorId)); + assert(cfg.getPolicyCommitment(account, actorId) == bytes32(0)); + assert(cfg.getPolicyManager(account, actorId) == address(0)); + } + + // ── Self-home mutual exclusion (the core, hardest invariant) ── + + /// @notice Authorizing the self-actorId as a k1 actor and then as a non-k1 actor (and vice-versa) never leaves + /// both self homes live — proved symbolically over the account address and both self scopes. + function check_selfHomes_neverBothLive(address account, uint8 scopeA, uint8 scopeB) external { + vm.assume(account != address(0)); + bytes32 self = bytes32(bytes20(account)); + + // Authorize the k1 self (inline home). + cfg.sym_authorizeActor( + account, + self, + AccountConfiguration.ActorConfig({authenticator: K1, scope: scopeA, expiry: 0, policyType: 0}), + "" + ); + assert(!(cfg.h_inlineSelfLive(account) && cfg.h_nonK1SelfLive(account))); + + // Now authorize a non-k1 self: inline must switch off, non-k1 home on. + cfg.sym_authorizeActor( + account, + self, + AccountConfiguration.ActorConfig({authenticator: NON_K1, scope: scopeB, expiry: 0, policyType: 0}), + "" + ); + assert(!(cfg.h_inlineSelfLive(account) && cfg.h_nonK1SelfLive(account))); + assert(!cfg.h_inlineSelfLive(account)); + assert(cfg.h_nonK1SelfLive(account)); + + // Switch back to the k1 self: non-k1 home cleared, inline live again. + cfg.sym_authorizeActor( + account, + self, + AccountConfiguration.ActorConfig({authenticator: K1, scope: scopeA, expiry: 0, policyType: 0}), + "" + ); + assert(!(cfg.h_inlineSelfLive(account) && cfg.h_nonK1SelfLive(account))); + assert(cfg.h_inlineSelfLive(account)); + assert(!cfg.h_nonK1SelfLive(account)); + assert(cfg.h_actorConfigAuthenticator(account, self) == address(0)); + } +} diff --git a/test/fv/AccountConfigurationHandler.sol b/test/fv/AccountConfigurationHandler.sol new file mode 100644 index 0000000..6952033 --- /dev/null +++ b/test/fv/AccountConfigurationHandler.sol @@ -0,0 +1,260 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.30; + +import {Test} from "forge-std/Test.sol"; + +import {AccountConfiguration} from "../../src/AccountConfiguration.sol"; +import {AccountConfigurationHarness} from "./AccountConfigurationHarness.sol"; +import {DefaultAccount} from "../../src/accounts/DefaultAccount.sol"; + +/// @notice Stateful-fuzzing handler for the {AccountConfiguration} invariant suite. It drives the contract through +/// validly-signed, in-distribution operations (create, authorize/revoke actors across both self homes, lock, +/// unlock, and time travel) so the fuzzer explores *reachable* states. Every state-mutating call is wrapped in +/// try/catch: invalid fuzzed combinations are expected to revert and are simply skipped, while the successful +/// ones evolve the system. The handler also tracks the (account, actorId) pairs it has touched and the last +/// observed sequence numbers, which the invariant contract reads to phrase its assertions. +contract AccountConfigurationHandler is Test { + AccountConfigurationHarness public immutable cfg; + address public immutable accountImpl; + address public immutable K1; + + bytes32 constant SIGNED_ACTOR_CHANGES_TYPEHASH = keccak256( + "SignedActorChanges(address account,uint256 chainId,uint64 sequence,ActorChange[] actorChanges)" + "ActorChange(uint8 changeType,bytes32 actorId,bytes data)" + ); + bytes32 constant ACTORCHANGE_TYPEHASH = keccak256("ActorChange(uint8 changeType,bytes32 actorId,bytes data)"); + + uint8 constant AUTHORIZE_ACTOR = 0x01; + uint8 constant REVOKE_ACTOR = 0x02; + uint8 constant SCOPE_CONFIG = 0x08; + + /// @dev A non-k1 authenticator selector. `_authorizeActor` only requires `authenticator >= K1_AUTHENTICATOR` and + /// does not call it, so any address > K1 exercises the non-k1 self / non-k1 actor storage home. + address constant NON_K1_AUTHENTICATOR = address(0xA11CE); + + // Owner private keys. Each created account is bootstrapped with exactly one of these as its unrestricted owner + // (a non-self k1 actor), and that owner signs every subsequent change for the account. + uint256[3] internal OWNER_PKS = [uint256(0xA1), uint256(0xB2), uint256(0xC3)]; + // Target keys used as the actorIds we authorize/revoke. + uint256[3] internal TARGET_PKS = [uint256(0xD4), uint256(0xE5), uint256(0xF6)]; + + address[] public accounts; + mapping(address => uint256) public ownerPkOf; + mapping(address => bool) public isCreated; + + // Addresses whose createAccount was expected to fail at the CREATE2 step; they must never carry state or code. + address[] public failedCreations; + + // Touched (account, actorId) pairs, for invariant enumeration. + struct Pair { + address account; + bytes32 actorId; + } + + Pair[] internal _pairs; + mapping(bytes32 => bool) internal _pairSeen; + + // Monotonicity tracking. + mapping(address => uint64) public lastLocalSeq; + mapping(address => uint64) public lastMultiSeq; + bool public sequenceMonotonicityHeld = true; + + uint256 internal _saltNonce; + + constructor(AccountConfigurationHarness _cfg, address _accountImpl) { + cfg = _cfg; + accountImpl = _accountImpl; + K1 = _cfg.K1_AUTHENTICATOR(); + } + + // ── Views for the invariant contract ── + + function accountsLength() external view returns (uint256) { + return accounts.length; + } + + function pairsLength() external view returns (uint256) { + return _pairs.length; + } + + function pairAt(uint256 i) external view returns (address account, bytes32 actorId) { + Pair storage p = _pairs[i]; + return (p.account, p.actorId); + } + + function failedCreationsLength() external view returns (uint256) { + return failedCreations.length; + } + + // ── Handler actions ── + + function handler_createAccount(uint256 ownerSeed) external { + uint256 pk = OWNER_PKS[ownerSeed % OWNER_PKS.length]; + if (accounts.length >= 4) return; // bound state size + + address owner = vm.addr(pk); + bytes32 ownerActorId = bytes32(bytes20(owner)); + + AccountConfiguration.InitialActor[] memory actors = new AccountConfiguration.InitialActor[](1); + actors[0] = AccountConfiguration.InitialActor({actorId: ownerActorId, authenticator: K1}); + + bytes memory bytecode = _erc1167(accountImpl); + bytes32 salt = bytes32(++_saltNonce); + + try cfg.createAccount(salt, bytecode, actors) returns (address account) { + if (!isCreated[account]) { + isCreated[account] = true; + accounts.push(account); + ownerPkOf[account] = pk; + _registerPair(account, ownerActorId); + _registerPair(account, bytes32(bytes20(account))); // self-actorId + _syncSeq(account); + } + } catch {} + } + + /// @dev Attempts a createAccount whose runtime code begins with 0xEF, which EIP-3541 rejects, so the underlying + /// CREATE2 returns address(0). The contract must revert (unwinding state) rather than leave an + /// initialized-but-codeless account. The predicted address is recorded for the orphaned-state invariant. + function handler_createAccountBadCode(uint256 ownerSeed) external { + if (failedCreations.length >= 8) return; // bound state size + uint256 pk = OWNER_PKS[ownerSeed % OWNER_PKS.length]; + address owner = vm.addr(pk); + + AccountConfiguration.InitialActor[] memory actors = new AccountConfiguration.InitialActor[](1); + actors[0] = AccountConfiguration.InitialActor({actorId: bytes32(bytes20(owner)), authenticator: K1}); + + bytes memory bytecode = hex"EF"; // EIP-3541: a leading 0xEF byte makes deployment fail. + bytes32 salt = bytes32(++_saltNonce); + address predicted = cfg.computeAddress(salt, bytecode, actors); + + try cfg.createAccount(salt, bytecode, actors) returns (address created) { + // Not expected to succeed; if a future EVM ever allowed it, treat it like a normal creation. + if (!isCreated[created]) { + isCreated[created] = true; + accounts.push(created); + ownerPkOf[created] = pk; + _syncSeq(created); + } + } catch { + failedCreations.push(predicted); + } + } + + function handler_authorize( + uint256 acctSeed, + uint256 targetSeed, + bool selfTarget, + bool nonK1, + uint8 scope, + uint48 expiry, + uint8 policyType + ) external { + if (accounts.length == 0) return; + address account = accounts[acctSeed % accounts.length]; + + bytes32 actorId = selfTarget + ? bytes32(bytes20(account)) + : bytes32(bytes20(vm.addr(TARGET_PKS[targetSeed % TARGET_PKS.length]))); + address authenticator = nonK1 ? NON_K1_AUTHENTICATOR : K1; + + AccountConfiguration.ActorConfig memory config = AccountConfiguration.ActorConfig({ + authenticator: authenticator, scope: scope, expiry: expiry, policyType: policyType + }); + + bytes memory policyData; + if (policyType != 0) { + // Provide a well-formed policy blob; whether the (scope, policyType) combo is legal is enforced by the + // contract (and rejected combos simply revert into the catch below). + policyData = abi.encodePacked(address(0xBEEF), keccak256(abi.encode("commit", acctSeed, targetSeed))); + } + + _apply(account, actorId, AUTHORIZE_ACTOR, abi.encode(config, policyData)); + _registerPair(account, actorId); + } + + function handler_revoke(uint256 acctSeed, uint256 targetSeed, bool selfTarget) external { + if (accounts.length == 0) return; + address account = accounts[acctSeed % accounts.length]; + bytes32 actorId = selfTarget + ? bytes32(bytes20(account)) + : bytes32(bytes20(vm.addr(TARGET_PKS[targetSeed % TARGET_PKS.length]))); + + _apply(account, actorId, REVOKE_ACTOR, ""); + } + + function handler_lock(uint256 acctSeed, uint16 delay) external { + if (accounts.length == 0) return; + address account = accounts[acctSeed % accounts.length]; + vm.prank(account); + try cfg.lock(delay) {} catch {} + } + + function handler_initiateUnlock(uint256 acctSeed) external { + if (accounts.length == 0) return; + address account = accounts[acctSeed % accounts.length]; + vm.prank(account); + try cfg.initiateUnlock() {} catch {} + } + + function handler_warp(uint32 dt) external { + vm.warp(block.timestamp + (uint256(dt) % 40 days) + 1); + } + + // ── Internal ── + + function _apply(address account, bytes32 actorId, uint8 changeType, bytes memory data) internal { + AccountConfiguration.ActorChange[] memory changes = new AccountConfiguration.ActorChange[](1); + changes[0] = AccountConfiguration.ActorChange({changeType: changeType, actorId: actorId, data: data}); + + uint256 chainId = block.chainid; + uint64 seq = cfg.getChangeSequences(account).local; + bytes32 digest = _digest(account, chainId, seq, changes); + + uint256 ownerPk = ownerPkOf[account]; + (uint8 v, bytes32 r, bytes32 s) = vm.sign(ownerPk, digest); + bytes memory auth = abi.encodePacked(K1, r, s, v); + + try cfg.applySignedActorChanges(account, chainId, changes, auth) { + _syncSeq(account); + } catch {} + } + + function _syncSeq(address account) internal { + AccountConfiguration.ChangeSequences memory s = cfg.getChangeSequences(account); + if (s.local < lastLocalSeq[account] || s.multichain < lastMultiSeq[account]) { + sequenceMonotonicityHeld = false; + } + lastLocalSeq[account] = s.local; + lastMultiSeq[account] = s.multichain; + } + + function _registerPair(address account, bytes32 actorId) internal { + bytes32 key = keccak256(abi.encodePacked(account, actorId)); + if (!_pairSeen[key]) { + _pairSeen[key] = true; + _pairs.push(Pair({account: account, actorId: actorId})); + } + } + + function _digest( + address account, + uint256 chainId, + uint64 sequence, + AccountConfiguration.ActorChange[] memory changes + ) internal pure returns (bytes32) { + bytes32[] memory h = new bytes32[](changes.length); + for (uint256 i; i < changes.length; i++) { + h[i] = keccak256( + abi.encode(ACTORCHANGE_TYPEHASH, changes[i].changeType, changes[i].actorId, keccak256(changes[i].data)) + ); + } + return keccak256( + abi.encode(SIGNED_ACTOR_CHANGES_TYPEHASH, account, chainId, sequence, keccak256(abi.encodePacked(h))) + ); + } + + function _erc1167(address impl) internal pure returns (bytes memory) { + return abi.encodePacked(hex"363d3d373d3d3d363d73", impl, hex"5af43d82803e903d91602b57fd5bf3"); + } +} diff --git a/test/fv/AccountConfigurationHarness.sol b/test/fv/AccountConfigurationHarness.sol new file mode 100644 index 0000000..80f037e --- /dev/null +++ b/test/fv/AccountConfigurationHarness.sol @@ -0,0 +1,100 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.30; + +import {AccountConfiguration} from "../../src/AccountConfiguration.sol"; + +/// @notice Formal-verification / invariant-testing harness for {AccountConfiguration}. +/// @dev Adds *read-only* accessors for `internal` storage that the public interface intentionally hides behind the +/// merged self-home view (see {AccountConfiguration.getActorConfig}). The invariants we want to prove — most +/// importantly the mutual exclusion of the inline-k1 self and the non-k1 self — are about the *raw* storage +/// state, which the merged view cannot distinguish. This contract adds no state and overrides no behavior; the +/// deployed logic under test is byte-for-byte the base contract. +contract AccountConfigurationHarness is AccountConfiguration { + /// @notice Raw `_actorConfig[actorId][account].authenticator`, without the inline-self synthesis that + /// {getActorConfig} applies. `address(0)` means "no explicit `_actorConfig` entry". + function h_actorConfigAuthenticator(address account, bytes32 actorId) external view returns (address) { + return _actorConfig[actorId][account].authenticator; + } + + function h_actorConfigScope(address account, bytes32 actorId) external view returns (uint8) { + return _actorConfig[actorId][account].scope; + } + + function h_actorConfigExpiry(address account, bytes32 actorId) external view returns (uint48) { + return _actorConfig[actorId][account].expiry; + } + + function h_actorConfigPolicyType(address account, bytes32 actorId) external view returns (uint8) { + return _actorConfig[actorId][account].policyType; + } + + /// @notice Raw `AccountState.flags` byte. + function h_flags(address account) external view returns (uint8) { + return _accountState[account].flags; + } + + /// @notice True when the inline-k1 self (the implicit/scoped default EOA in `AccountState`) is live — i.e. the + /// FLAG_REVOKE_DEFAULT_EOA bit is unset. This is the exact predicate `_authenticateK1` gates on. + function h_inlineSelfLive(address account) external view returns (bool) { + return _accountState[account].flags & FLAG_REVOKE_DEFAULT_EOA == 0; + } + + /// @notice True when a *non-k1* self authenticator occupies the `_actorConfig` self home. + function h_nonK1SelfLive(address account) external view returns (bool) { + return _actorConfig[bytes32(bytes20(account))][account].authenticator > K1_AUTHENTICATOR; + } + + function h_inlineSelfScope(address account) external view returns (uint8) { + return _accountState[account].defaultEOAScope; + } + + function h_inlineSelfPolicyType(address account) external view returns (uint8) { + return _accountState[account].defaultEOAPolicyType; + } + + function h_inlineSelfExpiry(address account) external view returns (uint48) { + return _accountState[account].defaultEOAExpiry; + } + + /// @notice Raw policy-slot reads (identical to the public accessors, mirrored here for symmetry in specs). + function h_policyCommitment(address account, bytes32 actorId) external view returns (bytes32) { + return _policyCommitment[actorId][account]; + } + + function h_policyManager(address account, bytes32 actorId) external view returns (address) { + return _policyManager[actorId][account]; + } + + function h_selfActorId(address account) external pure returns (bytes32) { + return bytes32(bytes20(account)); + } + + // ───────────────────────────────────────────────────────────────────────────────────────────────────────────── + // SYMBOLIC-VERIFICATION WRAPPERS + // + // Direct entrypoints to the internal state-machine units, so a symbolic engine (Halmos) can verify them over the + // full input domain *without* modeling `ecrecover` (the signature gate on the public change path). These call the + // exact same internal functions the production paths use; they add no logic of their own. + // ───────────────────────────────────────────────────────────────────────────────────────────────────────────── + + function sym_slicePolicy(uint8 policyType, bytes calldata policyData) + external + pure + returns (address manager, bytes32 commitment) + { + return _slicePolicy(policyType, policyData); + } + + function sym_authorizeActor( + address account, + bytes32 actorId, + AccountConfiguration.ActorConfig calldata config, + bytes calldata policyData + ) external { + _authorizeActor(account, actorId, config, policyData); + } + + function sym_revokeActor(address account, bytes32 actorId) external { + _revokeActor(account, actorId); + } +}