diff --git a/.gas-snapshot b/.gas-snapshot
deleted file mode 100644
index 7f64b9ca..00000000
--- a/.gas-snapshot
+++ /dev/null
@@ -1,271 +0,0 @@
-KernelECDSATest:test_default_validator_disable() (gas: 0)
-KernelECDSATest:test_default_validator_disable() (gas: 180648)
-KernelECDSATest:test_default_validator_enable() (gas: 0)
-KernelECDSATest:test_default_validator_enable() (gas: 188140)
-KernelECDSATest:test_disable_mode() (gas: 183150)
-KernelECDSATest:test_disable_mode() (gas: 192689)
-KernelECDSATest:test_eip712() (gas: 15684)
-KernelECDSATest:test_eip712() (gas: 15684)
-KernelECDSATest:test_enable_then_mode_1() (gas: 279597)
-KernelECDSATest:test_enable_then_mode_1() (gas: 287402)
-KernelECDSATest:test_external_call_batch_execute_fail() (gas: 23625)
-KernelECDSATest:test_external_call_batch_execute_fail() (gas: 29531)
-KernelECDSATest:test_external_call_batch_execute_success() (gas: 20626)
-KernelECDSATest:test_external_call_batch_execute_success() (gas: 26533)
-KernelECDSATest:test_external_call_default() (gas: 23511)
-KernelECDSATest:test_external_call_default() (gas: 29338)
-KernelECDSATest:test_external_call_execute_delegatecall_fail() (gas: 22499)
-KernelECDSATest:test_external_call_execute_delegatecall_fail() (gas: 28381)
-KernelECDSATest:test_external_call_execute_delegatecall_option_fail() (gas: 20434)
-KernelECDSATest:test_external_call_execute_delegatecall_option_fail() (gas: 26329)
-KernelECDSATest:test_external_call_execute_delegatecall_success() (gas: 19738)
-KernelECDSATest:test_external_call_execute_delegatecall_success() (gas: 25621)
-KernelECDSATest:test_external_call_execute_fail() (gas: 21968)
-KernelECDSATest:test_external_call_execute_fail() (gas: 27862)
-KernelECDSATest:test_external_call_execute_success() (gas: 20070)
-KernelECDSATest:test_external_call_execute_success() (gas: 25987)
-KernelECDSATest:test_external_call_execution() (gas: 498410)
-KernelECDSATest:test_external_call_execution() (gas: 511032)
-KernelECDSATest:test_fail_validate_not_activate() (gas: 0)
-KernelECDSATest:test_fail_validate_not_activate() (gas: 303494)
-KernelECDSATest:test_fail_validate_wrongsignature() (gas: 25013)
-KernelECDSATest:test_fail_validate_wrongsignature() (gas: 34351)
-KernelECDSATest:test_get_nonce() (gas: 25179)
-KernelECDSATest:test_get_nonce() (gas: 25201)
-KernelECDSATest:test_get_nonce(uint192) (runs: 1024, μ: 19842, ~: 19842)
-KernelECDSATest:test_get_nonce(uint192) (runs: 1024, μ: 19842, ~: 19842)
-KernelECDSATest:test_ignore() (gas: 868)
-KernelECDSATest:test_initialize() (gas: 126488)
-KernelECDSATest:test_initialize() (gas: 154121)
-KernelECDSATest:test_initialize_twice() (gas: 18555)
-KernelECDSATest:test_initialize_twice() (gas: 18599)
-KernelECDSATest:test_mode_2() (gas: 243897)
-KernelECDSATest:test_mode_2() (gas: 251079)
-KernelECDSATest:test_revert_when_mode_disabled() (gas: 200119)
-KernelECDSATest:test_revert_when_mode_disabled() (gas: 209710)
-KernelECDSATest:test_set_default_validator() (gas: 417747)
-KernelECDSATest:test_set_default_validator() (gas: 423674)
-KernelECDSATest:test_set_execution() (gas: 458742)
-KernelECDSATest:test_set_execution() (gas: 468648)
-KernelECDSATest:test_should_emit_event_on_receive() (gas: 23220)
-KernelECDSATest:test_should_emit_event_on_receive() (gas: 23220)
-KernelECDSATest:test_should_receive_erc1155() (gas: 700299)
-KernelECDSATest:test_should_receive_erc1155() (gas: 700325)
-KernelECDSATest:test_should_receive_erc1155_batch() (gas: 727496)
-KernelECDSATest:test_should_receive_erc1155_batch() (gas: 727496)
-KernelECDSATest:test_should_receive_erc721() (gas: 593075)
-KernelECDSATest:test_should_receive_erc721() (gas: 593097)
-KernelECDSATest:test_should_return_address_if_deployed() (gas: 21970)
-KernelECDSATest:test_should_return_address_if_deployed() (gas: 21976)
-KernelECDSATest:test_sudo() (gas: 170590)
-KernelECDSATest:test_sudo() (gas: 179783)
-KernelECDSATest:test_sudo_wrongSig() (gas: 103121)
-KernelECDSATest:test_sudo_wrongSig() (gas: 116321)
-KernelECDSATest:test_transfer_ownership() (gas: 185003)
-KernelECDSATest:test_upgrade() (gas: 21292)
-KernelECDSATest:test_upgrade() (gas: 21292)
-KernelECDSATest:test_validateUserOp_fail_invalid_mode() (gas: 26934)
-KernelECDSATest:test_validateUserOp_fail_invalid_mode() (gas: 26986)
-KernelECDSATest:test_validateUserOp_fail_not_entryPoint() (gas: 23364)
-KernelECDSATest:test_validateUserOp_fail_not_entryPoint() (gas: 23416)
-KernelECDSATest:test_validate_signature() (gas: 155870)
-KernelECDSATest:test_validate_signature() (gas: 195172)
-KernelECDSATypedTest:test_default_validator_disable() (gas: 185046)
-KernelECDSATypedTest:test_default_validator_enable() (gas: 192011)
-KernelECDSATypedTest:test_disable_mode() (gas: 187373)
-KernelECDSATypedTest:test_eip712() (gas: 15684)
-KernelECDSATypedTest:test_enable_then_mode_1() (gas: 291627)
-KernelECDSATypedTest:test_external_call_batch_execute_fail() (gas: 29575)
-KernelECDSATypedTest:test_external_call_batch_execute_success() (gas: 26577)
-KernelECDSATypedTest:test_external_call_default() (gas: 29382)
-KernelECDSATypedTest:test_external_call_execute_delegatecall_fail() (gas: 28425)
-KernelECDSATypedTest:test_external_call_execute_delegatecall_option_fail() (gas: 26373)
-KernelECDSATypedTest:test_external_call_execute_delegatecall_success() (gas: 25665)
-KernelECDSATypedTest:test_external_call_execute_fail() (gas: 27906)
-KernelECDSATypedTest:test_external_call_execute_success() (gas: 26031)
-KernelECDSATypedTest:test_external_call_execution() (gas: 515344)
-KernelECDSATypedTest:test_fail_validate_not_activate() (gas: 303494)
-KernelECDSATypedTest:test_fail_validate_wrongsignature() (gas: 36477)
-KernelECDSATypedTest:test_get_nonce() (gas: 25179)
-KernelECDSATypedTest:test_get_nonce(uint192) (runs: 1024, μ: 19842, ~: 19842)
-KernelECDSATypedTest:test_ignore() (gas: 868)
-KernelECDSATypedTest:test_initialize() (gas: 153627)
-KernelECDSATypedTest:test_initialize_twice() (gas: 18555)
-KernelECDSATypedTest:test_mode_2() (gas: 253336)
-KernelECDSATypedTest:test_revert_when_mode_disabled() (gas: 204271)
-KernelECDSATypedTest:test_set_default_validator() (gas: 427897)
-KernelECDSATypedTest:test_set_execution() (gas: 472872)
-KernelECDSATypedTest:test_should_emit_event_on_receive() (gas: 23220)
-KernelECDSATypedTest:test_should_receive_erc1155() (gas: 700299)
-KernelECDSATypedTest:test_should_receive_erc1155_batch() (gas: 727496)
-KernelECDSATypedTest:test_should_receive_erc721() (gas: 593097)
-KernelECDSATypedTest:test_should_return_address_if_deployed() (gas: 21976)
-KernelECDSATypedTest:test_sudo() (gas: 184006)
-KernelECDSATypedTest:test_sudo_wrongSig() (gas: 116744)
-KernelECDSATypedTest:test_upgrade() (gas: 21292)
-KernelECDSATypedTest:test_validateUserOp_fail_invalid_mode() (gas: 26934)
-KernelECDSATypedTest:test_validateUserOp_fail_not_entryPoint() (gas: 23364)
-KernelECDSATypedTest:test_validate_signature() (gas: 191595)
-KernelHelperTest:testIntersect(uint48,uint48,uint48,uint48) (runs: 1024, μ: 986, ~: 991)
-KernelWeightedECDSATest:test_default_validator_disable() (gas: 305435)
-KernelWeightedECDSATest:test_default_validator_enable() (gas: 861)
-KernelWeightedECDSATest:test_disable_mode() (gas: 310650)
-KernelWeightedECDSATest:test_eip712() (gas: 15953)
-KernelWeightedECDSATest:test_enable_then_mode_1() (gas: 415042)
-KernelWeightedECDSATest:test_external_call_batch_execute_fail() (gas: 27875)
-KernelWeightedECDSATest:test_external_call_batch_execute_success() (gas: 0)
-KernelWeightedECDSATest:test_external_call_default() (gas: 0)
-KernelWeightedECDSATest:test_external_call_execute_delegatecall_fail() (gas: 66397)
-KernelWeightedECDSATest:test_external_call_execute_delegatecall_option_fail() (gas: 66179)
-KernelWeightedECDSATest:test_external_call_execute_delegatecall_success() (gas: 0)
-KernelWeightedECDSATest:test_external_call_execute_fail() (gas: 65677)
-KernelWeightedECDSATest:test_external_call_execute_success() (gas: 0)
-KernelWeightedECDSATest:test_external_call_execution() (gas: 639603)
-KernelWeightedECDSATest:test_fail_validate_not_activate() (gas: 304469)
-KernelWeightedECDSATest:test_fail_validate_wrongsignature() (gas: 48654)
-KernelWeightedECDSATest:test_get_nonce() (gas: 25643)
-KernelWeightedECDSATest:test_get_nonce(uint192) (runs: 1024, μ: 20178, ~: 20178)
-KernelWeightedECDSATest:test_ignore() (gas: 949)
-KernelWeightedECDSATest:test_initialize() (gas: 250808)
-KernelWeightedECDSATest:test_initialize_twice() (gas: 33199)
-KernelWeightedECDSATest:test_mode_2() (gas: 266572)
-KernelWeightedECDSATest:test_revert_when_mode_disabled() (gas: 329650)
-KernelWeightedECDSATest:test_set_default_validator() (gas: 550884)
-KernelWeightedECDSATest:test_set_execution() (gas: 596300)
-KernelWeightedECDSATest:test_should_emit_event_on_receive() (gas: 23500)
-KernelWeightedECDSATest:test_should_receive_erc1155() (gas: 700509)
-KernelWeightedECDSATest:test_should_receive_erc1155_batch() (gas: 727747)
-KernelWeightedECDSATest:test_should_receive_erc721() (gas: 593329)
-KernelWeightedECDSATest:test_should_return_address_if_deployed() (gas: 37658)
-KernelWeightedECDSATest:test_sudo() (gas: 306510)
-KernelWeightedECDSATest:test_sudo_wrongSig() (gas: 158085)
-KernelWeightedECDSATest:test_upgrade() (gas: 21643)
-KernelWeightedECDSATest:test_validateUserOp_fail_invalid_mode() (gas: 27390)
-KernelWeightedECDSATest:test_validateUserOp_fail_not_entryPoint() (gas: 23678)
-KernelWeightedECDSATest:test_validate_signature() (gas: 311992)
-KillSwitchValidatorTest:test_default_validator_disable() (gas: 180769)
-KillSwitchValidatorTest:test_default_validator_enable() (gas: 188261)
-KillSwitchValidatorTest:test_disable_mode() (gas: 183271)
-KillSwitchValidatorTest:test_eip712() (gas: 15820)
-KillSwitchValidatorTest:test_enable_then_mode_1() (gas: 349996)
-KillSwitchValidatorTest:test_external_call_batch_execute_fail() (gas: 29619)
-KillSwitchValidatorTest:test_external_call_batch_execute_success() (gas: 26555)
-KillSwitchValidatorTest:test_external_call_default() (gas: 29426)
-KillSwitchValidatorTest:test_external_call_execute_delegatecall_fail() (gas: 28469)
-KillSwitchValidatorTest:test_external_call_execute_delegatecall_option_fail() (gas: 26439)
-KillSwitchValidatorTest:test_external_call_execute_delegatecall_success() (gas: 25709)
-KillSwitchValidatorTest:test_external_call_execute_fail() (gas: 27906)
-KillSwitchValidatorTest:test_external_call_execute_success() (gas: 26075)
-KillSwitchValidatorTest:test_external_call_execution() (gas: 511153)
-KillSwitchValidatorTest:test_fail_validate_not_activate() (gas: 303604)
-KillSwitchValidatorTest:test_fail_validate_wrongsignature() (gas: 34494)
-KillSwitchValidatorTest:test_force_unblock() (gas: 394842)
-KillSwitchValidatorTest:test_get_nonce() (gas: 25201)
-KillSwitchValidatorTest:test_get_nonce(uint192) (runs: 1024, μ: 19930, ~: 19930)
-KillSwitchValidatorTest:test_ignore() (gas: 956)
-KillSwitchValidatorTest:test_initialize() (gas: 154209)
-KillSwitchValidatorTest:test_initialize_twice() (gas: 18643)
-KillSwitchValidatorTest:test_mode_2() (gas: 313713)
-KillSwitchValidatorTest:test_revert_when_mode_disabled() (gas: 200273)
-KillSwitchValidatorTest:test_set_default_validator() (gas: 423773)
-KillSwitchValidatorTest:test_set_execution() (gas: 468769)
-KillSwitchValidatorTest:test_should_emit_event_on_receive() (gas: 23330)
-KillSwitchValidatorTest:test_should_fail_with_not_implemented_isValidSignature() (gas: 9236)
-KillSwitchValidatorTest:test_should_fail_with_not_implemented_isValidSignature(bytes32,bytes) (runs: 1024, μ: 9601, ~: 9556)
-KillSwitchValidatorTest:test_should_fail_with_not_implemented_validCaller() (gas: 10157)
-KillSwitchValidatorTest:test_should_fail_with_not_implemented_validCaller(address,bytes) (runs: 1024, μ: 9749, ~: 9703)
-KillSwitchValidatorTest:test_should_receive_erc1155() (gas: 700387)
-KillSwitchValidatorTest:test_should_receive_erc1155_batch() (gas: 727584)
-KillSwitchValidatorTest:test_should_receive_erc721() (gas: 593185)
-KillSwitchValidatorTest:test_should_return_address_if_deployed() (gas: 22086)
-KillSwitchValidatorTest:test_sudo() (gas: 179882)
-KillSwitchValidatorTest:test_sudo_wrongSig() (gas: 116442)
-KillSwitchValidatorTest:test_upgrade() (gas: 21314)
-KillSwitchValidatorTest:test_validateUserOp_fail_invalid_mode() (gas: 27022)
-KillSwitchValidatorTest:test_validateUserOp_fail_not_entryPoint() (gas: 23391)
-KillSwitchValidatorTest:test_validate_signature() (gas: 195249)
-SessionKeyValidatorTest:test_default_validator_disable() (gas: 180670)
-SessionKeyValidatorTest:test_default_validator_enable() (gas: 188140)
-SessionKeyValidatorTest:test_disable_mode() (gas: 183150)
-SessionKeyValidatorTest:test_eip712() (gas: 15684)
-SessionKeyValidatorTest:test_enable_then_mode_1() (gas: 287446)
-SessionKeyValidatorTest:test_external_call_batch_execute_fail() (gas: 29553)
-SessionKeyValidatorTest:test_external_call_batch_execute_success() (gas: 26533)
-SessionKeyValidatorTest:test_external_call_default() (gas: 29360)
-SessionKeyValidatorTest:test_external_call_execute_delegatecall_fail() (gas: 28381)
-SessionKeyValidatorTest:test_external_call_execute_delegatecall_option_fail() (gas: 26373)
-SessionKeyValidatorTest:test_external_call_execute_delegatecall_success() (gas: 25621)
-SessionKeyValidatorTest:test_external_call_execute_fail() (gas: 27862)
-SessionKeyValidatorTest:test_external_call_execute_success() (gas: 26031)
-SessionKeyValidatorTest:test_external_call_execution() (gas: 511076)
-SessionKeyValidatorTest:test_fail_validate_not_activate() (gas: 303538)
-SessionKeyValidatorTest:test_fail_validate_wrongsignature() (gas: 34395)
-SessionKeyValidatorTest:test_get_nonce() (gas: 25179)
-SessionKeyValidatorTest:test_get_nonce(uint192) (runs: 1024, μ: 19842, ~: 19842)
-SessionKeyValidatorTest:test_ignore() (gas: 912)
-SessionKeyValidatorTest:test_initialize() (gas: 154121)
-SessionKeyValidatorTest:test_initialize_twice() (gas: 18555)
-SessionKeyValidatorTest:test_mode_2() (gas: 251156)
-SessionKeyValidatorTest:test_revert_when_mode_disabled() (gas: 200037)
-SessionKeyValidatorTest:test_scenario_batch((uint8,uint8,uint8,uint8,uint48,uint48,uint48,uint48,bool,bool,bool,bool,bool),(uint8)) (runs: 1024, μ: 55953243, ~: 51234062)
-SessionKeyValidatorTest:test_scenario_non_batch((uint8,uint8,uint8,uint8,uint48,uint48,uint48,uint48,bool,bool,bool,bool,bool)) (runs: 1024, μ: 50850417, ~: 50878988)
-SessionKeyValidatorTest:test_set_default_validator() (gas: 423674)
-SessionKeyValidatorTest:test_set_execution() (gas: 468648)
-SessionKeyValidatorTest:test_should_emit_event_on_receive() (gas: 23264)
-SessionKeyValidatorTest:test_should_receive_erc1155() (gas: 700299)
-SessionKeyValidatorTest:test_should_receive_erc1155_batch() (gas: 727496)
-SessionKeyValidatorTest:test_should_receive_erc721() (gas: 593141)
-SessionKeyValidatorTest:test_should_return_address_if_deployed() (gas: 22020)
-SessionKeyValidatorTest:test_sudo() (gas: 179783)
-SessionKeyValidatorTest:test_sudo_wrongSig() (gas: 116365)
-SessionKeyValidatorTest:test_upgrade() (gas: 21292)
-SessionKeyValidatorTest:test_validateUserOp_fail_invalid_mode() (gas: 26958)
-SessionKeyValidatorTest:test_validateUserOp_fail_not_entryPoint() (gas: 23364)
-SessionKeyValidatorTest:test_validate_signature() (gas: 195172)
-TestCallee:test_ignore() (gas: 249)
-TestCounter:test_ignore() (gas: 164)
-TestERC1155:test_ignore() (gas: 313)
-TestERC20:test_ignore() (gas: 389)
-TestERC721:test_ignore() (gas: 399)
-TestExecutor:test_ignore() (gas: 130)
-TestPaymaster:test_ignore() (gas: 174)
-TestValidator:test_ignore() (gas: 351)
-WebAuthnFclValidatorTest:test_default_validator_disable() (gas: 599624)
-WebAuthnFclValidatorTest:test_default_validator_enable() (gas: 610462)
-WebAuthnFclValidatorTest:test_disable_mode() (gas: 606941)
-WebAuthnFclValidatorTest:test_dontRevertForDummySig() (gas: 32708)
-WebAuthnFclValidatorTest:test_eip712() (gas: 15953)
-WebAuthnFclValidatorTest:test_enable_then_mode_1() (gas: 725427)
-WebAuthnFclValidatorTest:test_external_call_batch_execute_fail() (gas: 25082)
-WebAuthnFclValidatorTest:test_external_call_batch_execute_success() (gas: 0)
-WebAuthnFclValidatorTest:test_external_call_default() (gas: 0)
-WebAuthnFclValidatorTest:test_external_call_execute_delegatecall_fail() (gas: 0)
-WebAuthnFclValidatorTest:test_external_call_execute_delegatecall_option_fail() (gas: 21982)
-WebAuthnFclValidatorTest:test_external_call_execute_delegatecall_success() (gas: 0)
-WebAuthnFclValidatorTest:test_external_call_execute_fail() (gas: 21228)
-WebAuthnFclValidatorTest:test_external_call_execute_success() (gas: 0)
-WebAuthnFclValidatorTest:test_external_call_execution() (gas: 0)
-WebAuthnFclValidatorTest:test_fail_validate_InvalidWebAuthnData() (gas: 55738)
-WebAuthnFclValidatorTest:test_fail_validate_not_activate() (gas: 304424)
-WebAuthnFclValidatorTest:test_fail_validate_wrongsignature() (gas: 450136)
-WebAuthnFclValidatorTest:test_get_nonce() (gas: 25621)
-WebAuthnFclValidatorTest:test_get_nonce(uint192) (runs: 1024, μ: 20156, ~: 20156)
-WebAuthnFclValidatorTest:test_initialize() (gas: 178514)
-WebAuthnFclValidatorTest:test_initialize_twice() (gas: 20827)
-WebAuthnFclValidatorTest:test_mode_2() (gas: 698102)
-WebAuthnFclValidatorTest:test_revert_when_mode_disabled() (gas: 623939)
-WebAuthnFclValidatorTest:test_set_default_validator() (gas: 844997)
-WebAuthnFclValidatorTest:test_set_execution() (gas: 897931)
-WebAuthnFclValidatorTest:test_should_emit_event_on_receive() (gas: 23456)
-WebAuthnFclValidatorTest:test_should_receive_erc1155() (gas: 700487)
-WebAuthnFclValidatorTest:test_should_receive_erc1155_batch() (gas: 727747)
-WebAuthnFclValidatorTest:test_should_receive_erc721() (gas: 593263)
-WebAuthnFclValidatorTest:test_should_return_address_if_deployed() (gas: 24521)
-WebAuthnFclValidatorTest:test_sudo() (gas: 602311)
-WebAuthnFclValidatorTest:test_sudo_wrongSig() (gas: 531738)
-WebAuthnFclValidatorTest:test_upgrade() (gas: 21643)
-WebAuthnFclValidatorTest:test_validateUserOp_fail_invalid_mode() (gas: 27368)
-WebAuthnFclValidatorTest:test_validateUserOp_fail_not_entryPoint() (gas: 23656)
-WebAuthnFclValidatorTest:test_validate_signature() (gas: 466394)
-WebAuthnFclValidatorTest:test_webAuthnSignatureGeneration(bytes32,uint256) (runs: 1024, μ: 925827, ~: 849019)
-WebAuthnFclValidatorTest:test_webAuthnSignatureGeneration_solo() (gas: 837725)
\ No newline at end of file
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index cad849ac..e5d65ee1 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -1,77 +1,43 @@
-name: ci
+name: CI
on:
- pull_request:
- branches: [dev,fix/ci]
- paths:
- - '**.sol'
- - '**.yml'
push:
- branches: [dev,fix/ci]
- paths:
- - '**.sol'
- - '**.yml'
-jobs:
- tests:
- name: Forge Testing
- runs-on: ubuntu-latest
- env:
- FOUNDRY_DISABLE_NIGHTLY_WARNING: true
+ pull_request:
+ workflow_dispatch:
+env:
+ FOUNDRY_PROFILE: ci
+
+jobs:
+ check:
strategy:
- matrix:
- profile: [post-prague,post-prague-via-ir,via-ir,min-solc,min-solc-via-ir]
+ fail-fast: true
+ name: Foundry project
+ runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
+ with:
+ submodules: recursive
- name: Install Foundry
uses: foundry-rs/foundry-toolchain@v1
- with:
- version: nightly
- - name: Install Dependencies
- run: forge install
-
- - name: show list
- run: ls
+ - name: Show Forge version
+ run: |
+ forge --version
- - name : pwd
- run: pwd
+ - name: Run Forge fmt
+ run: |
+ forge fmt --check
+ id: fmt
- - name: Run Tests with ${{ matrix.profile }}
- run: >
- ( [ "${{ matrix.profile }}" = "post-prague" ] &&
- forge test --use 0.8.28 --evm-version "prague"
- ) ||
- ( [ "${{ matrix.profile }}" = "post-prague-via-ir" ] &&
- forge test --use 0.8.28 --evm-version "prague" --via-ir
- ) ||
- ( [ "${{ matrix.profile }}" = "via-ir" ] &&
- forge test --via-ir
- ) ||
- ( [ "${{ matrix.profile }}" = "min-solc" ] &&
- forge fmt --check &&
- forge test --use 0.8.28
- ) ||
- ( [ "${{ matrix.profile }}" = "min-solc-via-ir" ] &&
- forge test --use 0.8.28 --via-ir
- )
-
- codespell:
- runs-on: ${{ matrix.os }}
- strategy:
- matrix:
- os:
- - ubuntu-latest
+ - name: Run Forge build
+ run: |
+ forge build --sizes --skip MockKernel
+ id: build
- steps:
- - name: Checkout
- uses: actions/checkout@v4
-
- - name: Run codespell
- uses: codespell-project/actions-codespell@v2.0
- with:
- check_filenames: true
- ignore_words_list: usera
- skip: ./.git,package-lock.json,ackee-blockchain-solady-report.pdf,EIP712Mock.sol,yarn.lock
+ - name: Run Forge tests
+ run: |
+ forge test -vvv
+ id: test
diff --git a/.gitignore b/.gitignore
index f9ff335c..b0f98b94 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,3 +29,17 @@ log/
.envrc
**/.DS_Store
+
+# Certora
+.certora_internal/
+.certora_recent_jobs.json
+.last_confs/
+
+# Kontrol
+.kontrol/
+
+# Claude Code local state
+.claude/
+
+# FV research scratch
+audit/formal-verification-research.html
diff --git a/.gitmodules b/.gitmodules
index 457e25c3..e69de29b 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,9 +0,0 @@
-[submodule "lib/solady"]
- path = lib/solady
- url = https://github.com/vectorized/solady
-[submodule "lib/forge-std"]
- path = lib/forge-std
- url = https://github.com/foundry-rs/forge-std
-[submodule "lib/ExcessivelySafeCall"]
- path = lib/ExcessivelySafeCall
- url = https://github.com/nomad-xyz/ExcessivelySafeCall
diff --git a/.npmignore b/.npmignore
deleted file mode 100644
index 46ebce72..00000000
--- a/.npmignore
+++ /dev/null
@@ -1,32 +0,0 @@
-# Compiler files
-cache/
-out/
-
-# Ignores development broadcast logs
-!/broadcast
-/broadcast/*/31337/
-/broadcast/**/dry-run/
-
-# Docs
-docs/
-
-# Dotenv file
-.env
-
-# coverage files
-coverage/
-node_modules
-.env
-coverage
-coverage.json
-typechain
-typechain-types
-
-# Hardhat files
-cache
-artifacts
-artifacts-selected
-
-cache_hardhat
-
-lcov.info
diff --git a/CHANGELOG_AUDIT.md b/CHANGELOG_AUDIT.md
new file mode 100644
index 00000000..fc320fc1
--- /dev/null
+++ b/CHANGELOG_AUDIT.md
@@ -0,0 +1,173 @@
+# Kernel v4 Audit Changelog
+
+**Commit Range:** `ff20f6c` to `3e72921` (HEAD)
+**Date Range:** October 14, 2025 - November 6, 2025
+**Files Changed:** 21 files in `src/` (+625, -500 lines)
+
+---
+
+## Added Features
+
+### EntryPoint v0.9 Support
+Added support for ERC-4337 EntryPoint version 0.9.
+- Updated account-abstraction dependency from v0.8.0 to v0.9.0 (branch: release-v09)
+- Updated EntryPoint deployment bytecode constant in test utilities
+- Modified test suite to include `vm.startPrank(beneficiary, beneficiary)` calls before `ep.handleOps()` for v0.9 compatibility
+- Updated remappings to support both v0.8.0 and v0.9.0 dependencies
+- Gas snapshot updates reflecting v0.9 optimizations (reduced gas costs across all test scenarios)
+- **Breaking Change:** UserOperation hash calculation has been changed in EntryPoint v0.9
+- **Files:** `foundry.toml`, `remappings.txt`, `soldeer.lock`, `test/utils/EntryPointLib.sol`, `test/KernelUserOpTest.sol`, `test/KernelValidatorTest.sol`
+- **EntryPoint Address:** `0x43370900c8de573dB349BEd8DD53b4Ebd3Cce709`
+- **Commits:** 977ca07, aa91ef1, 110c7af, 3e72921
+- **Note:** The module type ID was updated from 8 to 10 for `MODULE_TYPE_STATELESS_VALIDATOR_WITH_SENDER` as part of this upgrade
+- you can find the release docs in [here](https://docs.google.com/document/d/1RKkKZsP1eYkOoBEkzJ1vWRK_bcWXaewoGPzawMjsleM/edit?usp=drivesdk), please do note that this document is not in public yet
+
+### Staker Contract (`src/Staker.sol`) - NEW
+Factory staking management contract for ERC-4337 EntryPoint compliance.
+- Factory approval whitelist (owner-controlled or EIP-712 signature-based)
+- EntryPoint stake/unstake/withdraw functions
+- `deployWithFactory()` - Deploy accounts through approved factories
+- `approveFactory()` - Owner approves/disapproves factory
+- `approveFactoryWithSignature()` - EIP-712 signature-based approval (chain-agnostic)
+- **Commits:** e4431db, 52265ac
+- **PR:** #20
+
+### Enable Mode Signature Support
+Added support for installing modules via signature in UserOp flow (enable mode).
+- Allows users to install validators/modules atomically with their first UserOp
+- Uses `EnableModeSignature` struct containing: nonce, packages to install, enable signature, and userOp signature
+- EIP-712 signature verification with nonce replay protection
+- Nonce is checked and incremented to prevent replay attacks
+- **Files:** `src/Kernel.sol` (validateUserOp), `src/core/ModuleManager.sol`
+- **Commits:** 7a578c2
+- **PR:** #25
+
+### Root Validator Replacement
+New `setRoot()` overload allows replacing root validator with automatic cleanup of previous root.
+- **Function:** `setRoot(Install[] calldata pkg, bool removeCurrent, bytes calldata uninstallData)`
+- Supports uninstalling validators and permissions (including policies and signers)
+- Calls `onUninstall()` on removed modules
+- **Commits:** a691aad, f646dec, ffe4d58
+- **PR:** #7
+
+### Validator/Permission Management Functions
+New internal functions for module lifecycle management:
+- `_uninstallValidator()` - Uninstall validator with ValidationInfo cleanup
+- `_uninstallPolicyWithVid()` - Remove policy from specific permission
+- `_uninstallSignerWithVid()` - Remove signer from specific permission
+- **Files:** `src/core/ModuleManager.sol`, `src/core/ValidationManager.sol`
+- **Commits:** a691aad
+
+### ValidationId Utility Functions
+Helper functions for ValidationId type extraction and creation in `lib/Utils.sol`:
+- `parseNonce()` - Extract validation mode, type, and ID from nonce (moved from ValidationManager)
+- `getType()` - Extract validation type from ValidationId
+- `getValidator()` - Extract validator address from ValidationId
+- `validatorToIdentifier()` - Create ValidationId from validator address
+- `permissionToIdentifier()` - Create ValidationId from PermissionId
+- `isPermissionType()` - Check if validation type is permission variant
+- `calldataKeccak()` - Efficient calldata hashing for EIP-712
+- **Commits:** 5ee7a26, b6e1ee4, f67e36c, 6e3a5f5
+- **PR:** #19
+
+### ERC-1271 Raw Hash Signing
+Support for raw hash signing in EIP-7702 accounts (without EIP-712 wrapping).
+- **Hook:** `_erc1271RawAllowed()` - Override to enable raw signing
+- Enabled by default in `Kernel7702` contract
+- **Files:** `src/Kernel7702.sol`, `src/lib/ERC1271.sol`
+- **Commits:** 40b0ff6, 83d6e32, 776fe04, 8999222
+- **PR:** #24
+
+---
+
+## Changed Features
+
+### ValidationId Encoding (BREAKING CHANGE)
+ValidationId changed from 20 bytes to 21 bytes to embed validation type in first byte.
+- **Before:** `bytes20` (address only)
+- **After:** `bytes21` (1 byte type + 20 bytes address/permissionId)
+- **Encoding:** Byte 0 = ValidationType (ROOT=0, VALIDATOR=1, PERMISSION=2), Bytes 1-21 = address/permissionId
+- **Impact:** Type checking no longer requires storage reads, eliminates `vType` field from ValidationInfo struct
+- **Migration:** Use `validatorToIdentifier()` and `permissionToIdentifier()` utility functions
+- **Storage Optimization:** Removed `vType` field from ValidationInfo struct
+- **Commits:** 5ee7a26, b6e1ee4, f67e36c, 6e3a5f5
+- **PR:** #19
+
+### Initialization Pattern Refactor
+- `Kernel.initialize()` is now `virtual` and `payable` - implementation moved to derived contracts
+- `KernelUUPS.initialize()` has `initializer` modifier and properly initializes in constructor
+- `KernelUUPS` constructor calls `_disableInitializers()` to prevent implementation initialization
+- `Kernel7702.initialize()` is NO-OP (stateless accounts don't need initialization)
+- `KernelImmutableECDSA._initialize()` removed `initializer` modifier (protection at UUPS level)
+- **Files:** `src/Kernel.sol`, `src/KernelUUPS.sol`, `src/Kernel7702.sol`, `src/KernelImmutableECDSA.sol`
+- **Commits:** 75e788b, 69e12fb, 041bb87, a8cec2c
+- **PR:** #17
+
+### Factory Deployment Protection
+Factory now checks if account is already deployed before calling initialize.
+- Prevents re-initialization of already deployed accounts
+- **Files:** `src/KernelFactory.sol`
+- **Functions:** `deployImmutableECDSA()`, `deployImmutableECDSAWithExtraCall()`
+- **Commits:** 75e788b
+- **PR:** #17
+
+### Factory Salt Calculation Optimization
+Optimized to use `EfficientHashLib` instead of `keccak256(abi.encode())`.
+- **File:** `src/KernelFactory.sol`
+- **Function:** `_calculateSalt()` - NEW internal function using EfficientHashLib
+- **Commits:** e4431db
+
+### Executor Authorization Check
+Added installation verification in `executeFromExecutor()` flow via `executorHook` modifier.
+- **Change:** Added `require(address(hook) != address(0), Unauthorized())` in `executorHook` modifier
+- Prevents uninstalled executors from executing transactions
+- **File:** `src/core/ModuleManager.sol`
+- **Commits:** 7f55374, eff6542, dcec72e
+- **PR:** #18
+
+### Module Type Validation
+`supportsModule()` now returns false for moduleTypeId == 0 (invalid/undefined type).
+- **File:** `src/Kernel.sol`
+- **Commits:** 73a61ed
+- **PR:** #13
+
+### Enable Mode Nonce Replay Protection
+Added nonce check and increment in `validateUserOp()` enable mode flow.
+- **Change:** Added `_checkAndIncrementNonce(sig.nonce)` after signature verification
+- Prevents signature replay attacks
+- **File:** `src/Kernel.sol`
+- **Commits:** 7a578c2
+- **PR:** #25
+
+### Hook Validation Logic Enhancement
+Optimized hook validation check in UserOp flow.
+- **Change:** Reordered conditional logic for gas optimization (root or hookless paths first)
+- **File:** `src/Kernel.sol`
+- **Commits:** fa6a1bd, cdf738b
+- **PR:** #22
+
+### Signature Verification Optimization
+Use `ECDSA.tryRecoverCalldata()` instead of `ECDSA.tryRecover()` when signature is in calldata.
+- **Files:** `src/KernelImmutableECDSA.sol`, `src/Kernel7702.sol`
+- **Impact:** Gas savings for signature verification
+
+### Access Control Modifier Optimization
+Changed `_onlyEntryPointOrSelf()` and `_authorizeUpgrade()` to `view` functions.
+- Prevents accidental state changes in authorization checks
+- **Files:** `src/Kernel.sol`, `src/KernelUUPS.sol`
+
+---
+
+## Removed Features
+
+### KernelHelper.sol - DELETED
+EIP-712 digest generation moved inline to `ModuleManager.sol`.
+- Reduces external dependencies
+- Functions moved: `installDigest()`, `_installHash()`, `_hashTypedData()`, `_hashTypedDataSansChainId()`
+- Now implemented as internal functions in ModuleManager
+
+### Removed Functions
+- `ExecutorManager.installAndExecute()` - Removed unused and potentially dangerous function
+- `KernelImmutableECDSA._statelessInitializeCheck()` - Removed unused hook
+- `KernelImmutableECDSA` EthSign prefix handling - Simplified to use only standard ECDSA recovery
+- **Commits:** 35f65fe
diff --git a/CLAUDE.md b/CLAUDE.md
deleted file mode 100644
index ee808600..00000000
--- a/CLAUDE.md
+++ /dev/null
@@ -1,33 +0,0 @@
-# Development Guidelines
-
-## Build Commands
-- `forge build` - Compile all contracts
-- `forge test` - Run all tests
-- `forge test --match-test testFunctionName` - Run a single test
-- `forge test --match-path test/Kernel.t.sol` - Run tests in a specific file
-- `forge test -vv` - Run tests with verbose output
-- `FOUNDRY_PROFILE=optimized forge test` - Run tests with optimized profile
-
-## Code Style
-
-### Formatting
-- Indentation: 4 spaces
-- Opening braces: same line as declaration
-- Use named imports: `import {Contract} from "./path.sol";`
-- Line separators: `// --- Section Name ---`
-
-### Naming Conventions
-- Contracts: PascalCase (e.g. `Kernel`)
-- Interfaces: Prefixed with "I" (e.g. `IValidator`)
-- Functions: camelCase (e.g. `validateUserOp`)
-- Private/internal: underscore prefix (e.g. `_executeUserOp`)
-- Constants: ALL_CAPS_WITH_UNDERSCORES
-
-### Error Handling
-- Use custom errors instead of require (e.g. `error InvalidValidator();`)
-- Use if-revert pattern: `if (condition) { revert ErrorName(); }`
-
-### Types and Structure
-- Use immutable variables when possible for gas optimization
-- Follow ERC-4337 and ERC-7579 standards
-- Use explicit storage slots with assembly for upgradeability
\ No newline at end of file
diff --git a/LICENSE.txt b/LICENSE.txt
deleted file mode 100644
index e9410207..00000000
--- a/LICENSE.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-Copyright 2023 ZeroDev, Inc.
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
index fb9f57f5..24c6eba2 100644
--- a/README.md
+++ b/README.md
@@ -1,149 +1,420 @@
-# Kernel
+# Kernel v4
-Kernel is a smart contract account that is:
+ERC-4337 / ERC-7702 modular smart account with pluggable validation, execution, and hook modules. Implements [ERC-7579](https://eips.ethereum.org/EIPS/eip-7579) for standardized module interfaces.
-- Compatible with [ERC-4337](https://eips.ethereum.org/EIPS/eip-4337).
-- Modular (supports [ERC-7579 plugins](https://eips.ethereum.org/EIPS/eip-7579)).
-- [Highly gas-efficient](https://github.com/zerodevapp/aa-benchmark).
+## Key Features
-Kernel is also a winner of [the inaugural Ethereum AA grant](https://erc4337.mirror.xyz/hRn_41cef8oKn44ZncN9pXvY3VID6LZOtpLlktXYtmA). At the time of writing, [Kernel is the most widely used modular smart account.](https://www.bundlebear.com).
+### Modular Architecture (ERC-7579)
-## SDKs
+Six pluggable module types that can be installed and uninstalled at runtime:
-Kernel is supported by all major AA SDKs, including:
+| Type | Role |
+|------|------|
+| **Validator** | Validates UserOps and signatures — owns a nonce key namespace |
+| **Executor** | Calls `executeFromExecutor` to perform actions on behalf of the account |
+| **Fallback** | Extends the account with new function selectors (call or delegatecall) |
+| **Hook** | Pre/post execution checks on validators, executors, and fallback selectors |
+| **Policy** | Part of a permission — enforces rules (e.g. spending limits, target allowlists) |
+| **Signer** | Part of a permission — provides the signature verification (e.g. passkey, multisig) |
-- [ZeroDev](https://docs.zerodev.app/)
-- [Viem](https://viem.sh/account-abstraction/accounts/smart/toEcdsaKernelSmartAccount)
-- [Permissionless.js](https://docs.pimlico.io/permissionless/how-to/accounts/use-kernel-account)
+### Permission System
-## Plugins
+Beyond simple validator modules, Kernel v4 supports **permissions** — a composition of one signer and one or more policies. This enables granular session keys: a dapp gets a signer that can only call specific selectors, under specific policies (spending caps, time windows, target restrictions), without touching the root validator.
-- Read more about [Kernel's permissions system](https://docs.zerodev.app/sdk/permissions/intro) and learn to build your own plugins.
-- For officially maintained plugins, some live in [this repo](https://github.com/zerodevapp/kernel-7579-plugins/tree/master), and the rest live in [`/src`](/src).
+### Three Account Variants
-## Build
+- **`KernelUUPS`** — UUPS upgradeable proxy. Standard deployment via `KernelFactory.deploy()`. Supports full module lifecycle and proxy upgrades via UserOp.
+- **`KernelImmutableECDSA`** — ERC-1967 clone with an ECDSA fallback signer in immutable args. The fallback signer is fixed at deploy time, but users can `setRoot` to a different validator and the proxy is still UUPS-upgradeable. Deployed via `KernelFactory.deployECDSA()`.
+- **`Kernel7702`** — EIP-7702 variant for EOA delegation. The EOA itself is the fallback signer (`ECDSA.recover == address(this)`). No initialization needed. Supports raw ERC-1271 signatures.
-Make sure [Foundry](https://github.com/foundry-rs/foundry) is installed. Then:
+### Enable Mode
+Install modules atomically with the first UserOp — no separate setup transaction. The UserOp nonce encodes an enable-mode flag; the signature carries both the install payload (with root validator approval) and the UserOp signature. Supports chain-specific and replayable (chain-agnostic) variants.
+
+### Nonce-Encoded Validation
+
+The 32-byte ERC-4337 nonce encodes which validator to use, giving each validator/permission its own nonce namespace. See [Data Encoding > UserOp Nonce](#userop-nonce) for the full layout.
+
+### Hook System
+
+Hooks provide pre/post execution checks. They bind to validators, executors, and fallback selectors independently:
+
+- **Validator hook** — Runs around `executeUserOp` when a non-root validator with a hook is used
+- **Executor hook** — Runs around `executeFromExecutor` for any installed executor
+- **Fallback hook** — Runs around fallback selector dispatch
+
+Two sentinel values: `address(0)` = not installed, `address(1)` = installed with no hook.
+
+### Signature Verification (ERC-1271 / ERC-7739)
+
+Three signature modes for `isValidSignature`:
+1. **Raw** — Direct hash signing (only on `Kernel7702` where the EOA is the signer)
+2. **Chain-specific nested EIP-712** — Wraps the hash in a `TypedDataSign` struct bound to chain ID
+3. **Replayable nested EIP-712** — Same wrapping but without chain ID, valid across chains
+
+All modes support both validator-based and permission-based signature verification, selected by the first 21 bytes of the signature.
+
+### Standards
+
+| Standard | Support |
+|----------|---------|
+| [ERC-4337](https://eips.ethereum.org/EIPS/eip-4337) | Account abstraction via EntryPoint v0.9 |
+| [ERC-7579](https://eips.ethereum.org/EIPS/eip-7579) | Modular smart account interfaces |
+| [ERC-7702](https://eips.ethereum.org/EIPS/eip-7702) | EOA code delegation (`Kernel7702`) |
+| [ERC-7739](https://eips.ethereum.org/EIPS/eip-7739) | Nested EIP-712 for safe `isValidSignature` |
+| [ERC-7201](https://eips.ethereum.org/EIPS/eip-7201) | Namespaced storage for upgrade safety |
+| [ERC-1271](https://eips.ethereum.org/EIPS/eip-1271) | Smart contract signature validation |
+
+## Data Encoding
+
+### UserOp Nonce
+
+The 32-byte ERC-4337 nonce encodes the validation mode, type, and identifier:
+
+```
+| 1 byte | 1 byte | 20 bytes | 2 bytes | 8 bytes |
+| vMode | vType | vId | nonceKey | seq |
+```
+
+**vMode** (ValidationMode flags):
+
+| Value | Meaning |
+|-------|---------|
+| `0x00` | Standard — chain-specific, no inline install |
+| `0x08` | Enable — install modules inline, chain-specific enable signature |
+| `0x0C` | Enable + replayable enable signature |
+| `0x40` | Replayable — chain-agnostic userOp hash |
+| `0x48` | Enable + replayable userOp hash |
+| `0x4C` | Enable + replayable enable signature + replayable userOp hash |
+
+**vType** (ValidationType):
+
+| Value | Meaning | vId contains |
+|-------|---------|-------------|
+| `0x00` | Root / Fallback | Ignored (uses stored root) |
+| `0x01` | Validator | 20-byte validator address |
+| `0x02` | Permission | 4-byte PermissionId (left-aligned, rest zero) |
+
+**nonceKey + seq**: Each (vType, vId) combination has independent nonce namespaces via the nonceKey. The seq is incremented by the EntryPoint per standard ERC-4337 nonce management.
+
+### UserOp Signature
+
+#### Standard Mode (no enable flag)
+
+For **validator** (vType=0x01 or root resolving to validator):
+
+```
+[raw signature bytes]
+```
+
+Passed directly to `IValidator.validateUserOp(userOp, userOpHash)`.
+
+For **permission** (vType=0x02 or root resolving to permission):
+
+```
+abi.encode(PermissionSignature({
+ signatures: [policy1Sig, policy2Sig, ..., signerSig]
+}))
```
-forge install
+
+One signature per policy (in install order), plus one for the signer (last). Each policy's signature is passed to `IPolicy.checkUserOpPolicy`, and the signer's to `ISigner.checkUserOpSignature`.
+
+#### Enable Mode (enable flag set in vMode)
+
+```
+abi.encode(EnableModeSignature({
+ nonce: uint256, // install nonce for replay protection
+ packages: Install[], // modules to install
+ enableSignature: bytes, // root validator's signature over the install digest
+ userOpSignature: bytes // the actual validation signature (standard or permission format)
+}))
+```
+
+The install digest is:
+
+```
+EIP-712 hash of InstallPackages(uint256 nonce, Install[] packages)
+```
+
+If the enable-replayable flag (0x04) is set, the digest uses the chain-agnostic domain separator (no chainId).
+
+### ERC-1271 Signature (`isValidSignature`)
+
+After ERC-6492 unwrapping, the signature is parsed as:
+
+```
+| 1 byte | 1 byte | N bytes | remaining bytes |
+| vMode | vType | vId | inner signature |
+```
+
+Where N depends on vType:
+
+| vType | N | vId content |
+|-------|---|-------------|
+| `0x00` (root) | 0 | Uses stored root, inner = `signature[2:]` |
+| `0x01` (validator) | 20 | Validator address, inner = `signature[22:]` |
+| `0x02` (permission) | 4 | PermissionId, inner = `signature[6:]` |
+
+#### Standard Mode (no enable flag)
+
+The inner signature is verified via `_verifySignature` against the installed validator or permission, same as UserOp standard mode.
+
+#### Enable Mode for ERC-1271
+
+Since `isValidSignature` is a `view` function, enable mode works differently than in UserOps — it **cannot** modify state (no module installation, no nonce increment). Instead it:
+
+1. Verifies the install signature is valid (same digest as UserOp enable mode)
+2. Checks the nonce is correct (view-only, no increment)
+3. Uses **stateless** verification — finds the validator/permission modules inside the `packages` array and calls `IStatelessValidatorWithSender.validateSignatureWithDataWithSender` instead of the normal installed module
+
+The inner signature format is the same `EnableModeSignature`:
+
+```
+abi.encode(EnableModeSignature({
+ nonce: uint256,
+ packages: Install[],
+ enableSignature: bytes, // root validator's signature over the install digest
+ userOpSignature: bytes // verified statelessly against modules in packages
+}))
+```
+
+For permission-based enable mode, `userOpSignature` is a `PermissionSignature` — one signature per policy/signer found in the packages with the matching PermissionId.
+
+> **Note:** vType cannot be root (`0x00`) in enable mode — it must specify an explicit validator or permission.
+
+#### Nested EIP-712 Wrapping
+
+The above describes the **validation layer** (which validator/permission to use). Independently, ERC-7739 wraps the `hash` before it reaches the validation layer:
+
+**TypedDataSign** — The inner signature is:
+
+```
+[r | s | v | APP_DOMAIN_SEPARATOR (32 bytes) | contents (32 bytes) | contentsDescription | uint16(contentsDescription.length)]
+```
+
+**PersonalSign** — The inner signature is just `[r | s | v]`.
+
+The replayable variant uses a `TypedDataSign` struct without `chainId` in the account domain.
+
+### installModule / uninstallModule
+
+```solidity
+function installModule(uint256 moduleType, address module, bytes calldata initData) external payable;
+function uninstallModule(uint256 moduleType, address module, bytes calldata initData) external payable;
+```
+
+`initData` is ABI-encoded as `InstallModuleDataFormat`:
+
+```solidity
+abi.encode(InstallModuleDataFormat({
+ installData: bytes, // forwarded to module's onInstall / onUninstall
+ internalData: bytes // kernel-internal configuration (format varies by type)
+}))
+```
+
+#### internalData for Install
+
+| Module Type | internalData format |
+|-------------|---------------------|
+| Validator (1) | `[bytes20 hookAddress][bytes4 selector₁][bytes4 selector₂]...` |
+| Executor (2) | `[bytes20 hookAddress]` |
+| Fallback (3) | `[bytes4 selector][bytes1 callType][bytes20 hookAddress]` |
+| Hook (4) | Ignored (empty OK) |
+| Policy (5) | `[bytes4 permissionId]` |
+| Signer (6) | `[bytes4 permissionId][bytes20 hookAddress][bytes4 selector₁]...` |
+
+**hookAddress** sentinel values:
+
+| Address | Meaning |
+|---------|---------|
+| `address(0)` | Not installed / entry-point-only (for fallback: only EntryPoint can call) |
+| `address(1)` | Installed with no hook |
+| Other | Hook contract address (must be installed as hook module first) |
+
+**callType** for fallback (type 3):
+
+| Value | Meaning |
+|-------|---------|
+| `0x00` | `call` — regular call, appends `msg.sender` to calldata |
+| `0xFF` | `delegatecall` — executes in Kernel's storage context |
+
+#### internalData for Uninstall
+
+| Module Type | internalData format |
+|-------------|---------------------|
+| Validator (1) | Ignored |
+| Executor (2) | Ignored |
+| Fallback (3) | `[bytes4 selector]` (first 4 bytes used) |
+| Hook (4) | Ignored |
+| Policy (5) | `[bytes4 permissionId]` — must uninstall in LIFO order (last installed first) |
+| Signer (6) | `[bytes4 permissionId]` — all policies must be uninstalled first |
+
+### Batch Install via `Install[]`
+
+Three entry points for batch installation:
+
+```solidity
+// 1. During account creation — first package becomes root
+initialize(Install[] calldata packages)
+
+// 2. From EntryPoint or self
+installModule(Install[] calldata packages)
+
+// 3. With root validator signature (no EntryPoint needed)
+installModule(bool replayable, uint256 nonce, Install[] calldata packages, bytes calldata signature)
+```
+
+Each `Install` struct:
+
+```solidity
+struct Install {
+ uint256 moduleType; // 1-6
+ address module; // module contract address
+ bytes moduleData; // forwarded to onInstall
+ bytes internalData; // kernel config (same format as table above)
+}
+```
+
+**Permission install order**: When installing a permission, all policies (type 5) for that PermissionId must come first, followed by exactly one signer (type 6) with the same PermissionId. The signer finalizes the permission. Multiple permissions can be installed in a single batch — just ensure each permission's policies+signer are grouped together.
+
+## Architecture
+
+```
+Kernel (abstract)
+├── ModuleManager
+│ ├── ValidationManager — Validator/permission lifecycle, enable-mode, nonce mgmt
+│ ├── ExecutorManager — Executor install/uninstall with hook binding
+│ ├── HookManager — Hook install/uninstall, pre/post check dispatch
+│ └── SelectorManager — Fallback handler routing by function selector
+├── ExecutionManager — ERC-7579 execution modes (single/batch/delegatecall)
+└── ERC1271 — ERC-1271 / ERC-7739 signature verification
+
+Concrete implementations:
+├── KernelUUPS — UUPS upgradeable proxy
+├── KernelImmutableECDSA — Minimal clone with immutable signer
+└── Kernel7702 — EIP-7702 EOA delegation
+
+Supporting contracts:
+├── KernelFactory — Deterministic ERC-1967 proxy deployment
+└── Staker — EntryPoint staking and factory approval management
+```
+
+### Storage
+
+All storage uses [ERC-7201](https://eips.ethereum.org/EIPS/eip-7201) namespaced slots to avoid collisions across modules and upgrades:
+
+| Manager | Slot |
+|---------|------|
+| ValidationManager | `keccak256("kernel.v4.validation") - 1` |
+| ModuleManager | `keccak256("kernel.v4.module") - 1` |
+| ExecutorManager | `keccak256("kernel.v4.executor") - 1` |
+| HookManager | `keccak256("kernel.v4.hook") - 1` |
+| SelectorManager | `keccak256("kernel.v4.selector") - 1` |
+
+## Project Structure
+
+```
+src/
+├── Kernel.sol — Abstract base account
+├── Kernel7702.sol — EIP-7702 variant
+├── KernelImmutableECDSA.sol — Immutable ECDSA variant
+├── KernelUUPS.sol — UUPS upgradeable variant
+├── KernelFactory.sol — Deterministic proxy deployer
+├── Staker.sol — EntryPoint staking manager
+├── core/ — Manager contracts
+├── interfaces/ — ERC-7579 interfaces
+├── lib/ — ERC1271, Lib4337, Utils
+└── types/ — Types, Constants, Errors, Structs
+
+test/
+├── btt/ — Branching Tree Technique tests (bulloak)
+├── unit/ — Unit tests and gas benchmarks
+├── integration/ — End-to-end integration tests
+├── invariant/ — Invariant tests (1000 runs / 1000 depth)
+├── fuzz/ — Fuzz tests
+├── halmos/ — Symbolic execution (formal verification)
+└── mock/ — Test mocks and helpers
+```
+
+## Getting Started
+
+### Prerequisites
+
+- [Foundry](https://book.getfoundry.sh/getting-started/installation)
+- [Soldeer](https://soldeer.xyz/) (dependency manager, bundled with Foundry)
+- Solidity 0.8.33+
+
+### Install
+
+```sh
+git clone git@github.com:zerodevapp/kernel_v4.git
+cd kernel_v4
+forge soldeer install
forge build
+```
+
+## Testing
+
+```sh
+# All tests
forge test
+
+# BTT tests only
+forge test --match-path "test/btt/*.t.sol"
+
+# Unit tests only
+forge test --match-path "test/unit/*.t.sol"
+
+# Integration tests
+forge test --match-path "test/integration/*.t.sol"
+
+# Invariant tests
+forge test --match-path "test/invariant/*.t.sol"
+
+# Fuzz tests
+forge test --match-path "test/fuzz/*.t.sol"
+
+# Halmos (symbolic execution)
+halmos
```
-### Deployment
+### Coverage
+
+```sh
+forge coverage \
+ --no-match-coverage "(script|test|Foo|Bar|validator|sdk|signer)" \
+ --report lcov
-We have built a [portal](https://kernel.zerodev.app/) for deploying Kernel on any network.
+genhtml lcov.info \
+ --output-directory coverage \
+ --ignore-errors inconsistent \
+ --ignore-errors corrupt
+
+open coverage/index.html
+```
-If you don't see a network, feel free to open an issue or use manual connection.
+## Dependencies
+
+| Package | Version |
+|---------|---------|
+| [Solady](https://github.com/Vectorized/solady) | 0.1.26 |
+| [account-abstraction](https://github.com/eth-infinitism/account-abstraction) | v0.9.0 |
+| [OpenZeppelin Contracts](https://github.com/OpenZeppelin/openzeppelin-contracts) | 5.4.0 |
+| [forge-std](https://github.com/foundry-rs/forge-std) | 1.11.0 |
+
+## Configuration
+
+Key settings in `foundry.toml`:
+
+- **EVM version**: Prague (transient storage support)
+- **Solc**: 0.8.33
+- **Optimizer**: 200 runs
+- **Invariant**: 1000 runs, 1000 depth
+
+## Security
+
+See [CHANGELOG_AUDIT.md](./CHANGELOG_AUDIT.md) for the full audit changelog covering all changes since the last audit.
## License
MIT
-
-## Addresses
-
-v3.3
-
-| Name | Address |
-| -------------------- | ------------------------------------------ |
-| Meta Factory | [0xd703aaE79538628d27099B8c4f621bE4CCd142d5](https://contractscan.xyz/contract/0xd703aae79538628d27099b8c4f621be4ccd142d5) |
-| Factory | [0x2577507b78c2008Ff367261CB6285d44ba5eF2E9](https://contractscan.xyz/contract/0x2577507b78c2008Ff367261CB6285d44ba5eF2E9) |
-| Kernel | [0xd6CEDDe84be40893d153Be9d467CD6aD37875b28](https://contractscan.xyz/contract/0xd6CEDDe84be40893d153Be9d467CD6aD37875b28) |
-
-
-
-
-
-v3.2
-
-| Name | Address |
-| -------------------- | ------------------------------------------ |
-| Meta Factory | [0xd703aaE79538628d27099B8c4f621bE4CCd142d5](https://contractscan.xyz/contract/0xd703aae79538628d27099b8c4f621be4ccd142d5) |
-| Factory | [0x7a1dBAB750f12a90EB1B60D2Ae3aD17D4D81EfFe](https://contractscan.xyz/contract/0x7a1dBAB750f12a90EB1B60D2Ae3aD17D4D81EfFe) |
-| Kernel | [0xD830D15D3dc0C269F3dBAa0F3e8626d33CFdaBe1](https://contractscan.xyz/contract/0xD830D15D3dc0C269F3dBAa0F3e8626d33CFdaBe1) |
-
-
-
-
-v3.1
-
-| Name | Address |
-| -------------------- | ------------------------------------------ |
-| Meta Factory | [0xd703aaE79538628d27099B8c4f621bE4CCd142d5](https://contractscan.xyz/contract/0xd703aae79538628d27099b8c4f621be4ccd142d5) |
-| Factory | [0xaac5D4240AF87249B3f71BC8E4A2cae074A3E419](https://contractscan.xyz/contract/0xaac5d4240af87249b3f71bc8e4a2cae074a3e419) |
-| Kernel | [0xBAC849bB641841b44E965fB01A4Bf5F074f84b4D](https://contractscan.xyz/contract/0xbac849bb641841b44e965fb01a4bf5f074f84b4d) |
-| ECDSA Validator | [0x845ADb2C711129d4f3966735eD98a9F09fC4cE57](https://contractscan.xyz/contract/0x845adb2c711129d4f3966735ed98a9f09fc4ce57) |
-
-
-
-
-v3.0
-
-| Name | Address |
-| -------------------- | ------------------------------------------ |
-| Meta Factory | [0xd703aaE79538628d27099B8c4f621bE4CCd142d5](https://contractscan.xyz/contract/0xd703aae79538628d27099b8c4f621be4ccd142d5) |
-| Factory | [0x6723b44Abeec4E71eBE3232BD5B455805baDD22f](https://contractscan.xyz/contract/0x6723b44abeec4e71ebe3232bd5b455805badd22f) |
-| Kernel | [0x94F097E1ebEB4ecA3AAE54cabb08905B239A7D27](https://contractscan.xyz/contract/0x94f097e1ebeb4eca3aae54cabb08905b239a7d27) |
-| ECDSA Validator | [0x8104e3Ad430EA6d354d013A6789fDFc71E671c43](https://contractscan.xyz/contract/0x8104e3ad430ea6d354d013a6789fdfc71e671c43) |
-
-
-
-
-v2.4
-
-| Name | Address |
-| -------------------- | ------------------------------------------ |
-| Kernel | [0xd3082872F8B06073A021b4602e022d5A070d7cfC](https://contractscan.xyz/contract/0xd3082872f8b06073a021b4602e022d5a070d7cfc) |
-| KernelFactory | [0x5de4839a76cf55d0c90e2061ef4386d962E15ae3](https://contractscan.xyz/contract/0x5de4839a76cf55d0c90e2061ef4386d962e15ae3) |
-| SessionKeyValidator | [0x5C06CE2b673fD5E6e56076e40DD46aB67f5a72A5](https://contractscan.xyz/contract/0x5c06ce2b673fd5e6e56076e40dd46ab67f5a72a5) |
-| ECDSA Validator | [0xd9AB5096a832b9ce79914329DAEE236f8Eea0390](https://contractscan.xyz/contract/0xd9ab5096a832b9ce79914329daee236f8eea0390) |
-
-
-
-v2.3
-
-| Name | Address |
-| -------------------- | ------------------------------------------ |
-| Kernel | [0xD3F582F6B4814E989Ee8E96bc3175320B5A540ab](https://contractscan.xyz/contract/0xd3f582f6b4814e989ee8e96bc3175320b5a540ab) |
-| KernelFactory | [0x5de4839a76cf55d0c90e2061ef4386d962E15ae3](https://contractscan.xyz/contract/0x5de4839a76cf55d0c90e2061ef4386d962e15ae3) |
-| KernelLite | [0x482EC42E88a781485E1B6A4f07a0C5479d183291](https://contractscan.xyz/contract/0x482ec42e88a781485e1b6a4f07a0c5479d183291) |
-| SessionKeyValidator | [0x5C06CE2b673fD5E6e56076e40DD46aB67f5a72A5](https://contractscan.xyz/contract/0x5c06ce2b673fd5e6e56076e40dd46ab67f5a72a5) |
-| ECDSA Validator | [0xd9AB5096a832b9ce79914329DAEE236f8Eea0390](https://contractscan.xyz/contract/0xd9ab5096a832b9ce79914329daee236f8eea0390) |
-
-
-
-v2.2
-
-| Name | Address |
-| -------------------- | ------------------------------------------ |
-| Kernel | [0x0DA6a956B9488eD4dd761E59f52FDc6c8068E6B5](https://contractscan.xyz/contract/0x0da6a956b9488ed4dd761e59f52fdc6c8068e6b5) |
-| KernelFactory | [0x5de4839a76cf55d0c90e2061ef4386d962E15ae3](https://contractscan.xyz/contract/0x5de4839a76cf55d0c90e2061ef4386d962e15ae3) |
-| KernelLite | [0xbEdb61Be086F3f15eE911Cc9AB3EEa945DEbFa96](https://contractscan.xyz/contract/0xbedb61be086f3f15ee911cc9ab3eea945debfa96) |
-| SessionKeyValidator | [0x5C06CE2b673fD5E6e56076e40DD46aB67f5a72A5](https://contractscan.xyz/contract/0x5c06ce2b673fd5e6e56076e40dd46ab67f5a72a5) |
-| ECDSA Validator | [0xd9AB5096a832b9ce79914329DAEE236f8Eea0390](https://contractscan.xyz/contract/0xd9ab5096a832b9ce79914329daee236f8eea0390) |
-
-
-
-
-v2.1
-
-| Name | Address |
-| -------------------- | ------------------------------------------ |
-| Kernel | [0xf048AD83CB2dfd6037A43902a2A5Be04e53cd2Eb](https://contractscan.xyz/contract/0xf048ad83cb2dfd6037a43902a2a5be04e53cd2eb) |
-| KernelFactory | [0x5de4839a76cf55d0c90e2061ef4386d962E15ae3](https://contractscan.xyz/contract/0x5de4839a76cf55d0c90e2061ef4386d962e15ae3) |
-| SessionKeyValidator | [0x5C06CE2b673fD5E6e56076e40DD46aB67f5a72A5](https://contractscan.xyz/contract/0x5c06ce2b673fd5e6e56076e40dd46ab67f5a72a5) |
-| ECDSA Validator | [0xd9AB5096a832b9ce79914329DAEE236f8Eea0390](https://contractscan.xyz/contract/0xd9ab5096a832b9ce79914329daee236f8eea0390) |
-
-
-
-v2.0
-
-| Name | Address |
-| --------------- | ------------------------------------------ |
-| Kernel | [0xeB8206E02f6AB1884cfEa58CC7BabdA7d55aC957](https://contractscan.xyz/contract/0xeb8206e02f6ab1884cfea58cc7babda7d55ac957) |
-| TempKernel | [0x727A10897e70cd3Ab1a6e43d59A12ab0895A4995](https://contractscan.xyz/contract/0x727a10897e70cd3ab1a6e43d59a12ab0895a4995) |
-| KernelFactory | [0x12358cA00141D09cB90253F05a1DD16bE93A8EE6](https://contractscan.xyz/contract/0x12358ca00141d09cb90253f05a1dd16be93a8ee6) |
-| ECDSA Validator | [0x180D6465F921C7E0DEA0040107D342c87455fFF5](https://contractscan.xyz/contract/0x180d6465f921c7e0dea0040107d342c87455fff5) |
-| ECDSA Factory | [0xAf299A1f51560F51A1F3ADC0a5991Ac74b61b0BE](https://contractscan.xyz/contract/0xaf299a1f51560f51a1f3adc0a5991ac74b61b0be) |
-
diff --git a/audit/FV_COVERAGE.md b/audit/FV_COVERAGE.md
new file mode 100644
index 00000000..e9a4aa55
--- /dev/null
+++ b/audit/FV_COVERAGE.md
@@ -0,0 +1,220 @@
+# Kernel v4 — FV Coverage Board
+
+> **Live status table** mapping every public/external function plus security-relevant internal helper to its formal-verification obligation, backend, and proof state.
+
+**Last updated**: 2026-05-25 (Round 2 remaining-gaps closure — Phase 3 composition proven)
+**Branch**: `audit/fv-round-1` (PR #55, 48 commits)
+**Companion docs**:
+- [`audit/FV_PLAN.md`](./FV_PLAN.md) — Round 1 multi-phase plan
+- [`audit/FV_PLAN_ROUND_2.md`](./FV_PLAN_ROUND_2.md) — Round 2 strategy
+- [`audit/fv-gap-audit.md`](./fv-gap-audit.md) — original gap audit
+- [`audit/fv-round-1-findings.md`](./fv-round-1-findings.md) — Round 1 per-property findings
+
+## Legend
+
+**Obligation types** (per the Round 2 plan):
+
+- **AC** — Access Control: caller restrictions hold
+- **TR** — Transition: every state change preserves the relevant invariant
+- **EQ** — Equivalence: two paths agree on the audit-relevant outcome
+- **NR** — Non-Replay: operations cannot be replayed
+- **NB** — Non-Bypass: no path returns success without the expected predicate
+- **DT** — Determinism: pure functions / CREATE2 deployments are deterministic
+- **OF** — Overflow: arithmetic cannot overflow under reachable preconditions
+
+**Status**:
+
+- ✅ **PROVEN** — at least one FV backend has discharged the obligation
+- 🟡 **PARTIAL** — partially proven (e.g., subset of inputs, complementary backends)
+- ❌ **OPEN** — obligation identified but not yet attempted
+- 🔵 **OOS** — explicitly out of scope (with rationale)
+
+**Backends**:
+
+- **H** = Halmos, **C** = Certora, **K** = Kontrol, **M** = Manual proof, **OOS** = out of scope
+
+---
+
+## `src/Kernel.sol`
+
+| Visibility | Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|---|
+| external | `initialize(packages)` (declared abstract) | AC, TR | — | 🔵 OOS | Implemented by subclasses (`KernelUUPS.initialize`, `KernelImmutableECDSA._initialize`). |
+| external | `validateUserOp(userOp, hash, missingFunds)` | AC, NB | C | ✅ PROVEN | Phase C #1 strict + naive rules. Spec: `certora/specs/Kernel.spec`. |
+| external | `executeUserOp(userOp, hash)` | NB | C, M | ✅ PROVEN | Phase C #1 (executeUserOp inner delegatecall gated by validateUserOp). |
+| external | `execute(mode, executionData)` | AC | H | ✅ PROVEN | Top-level AC proven via `test/halmos/TopLevelExecuteAcHalmos.t.sol` (entryPoint or self only). Inner calls proven by Phase 2. |
+| external | `setNonce(key, seq)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | `setRootPreservesNonBypass` + `_checkAndIncrementNonce` chain. Phase A #13 covers nonce no-overflow. |
+| external | `setValidNonceFrom(seq)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | Same. |
+| external | `installModule(moduleType, module, initData)` (ERC-7579) | AC, TR | C (Phase C writer-local) | ✅ PROVEN | `_initializeValidation` + `_installValidator/Policy/Signer/Hook/Executor/Selector` writer chain. |
+| external | `uninstallModule(moduleType, module, initData)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | `uninstallValidationPreservesNonBypass`. |
+| external | `setRoot(pkg, removeCurrent, uninstallData)` (install-overload) | AC, TR, NB | C | ✅ PROVEN | Phase D #6 (`SetRootLifo.spec`). LIFO cleanup post-conditions verified. |
+| external | `setRoot(vId)` (id-overload) | AC, TR | C (Phase C writer-local) | ✅ PROVEN | `setRootPreservesNonBypass`. |
+| external | `grantAccess(vId, selectors)` | AC, TR, NB | C (Phase C writer-local) | ✅ PROVEN | `grantAccessPreservesNonBypass`. Block executeUserOp.selector for non-root in fix `0921b25`. |
+| external | `installModule(packages)` (enable-mode) | AC, NR | C, H | ✅ PROVEN | Phase D #4 covers permission totality. Phase 2 `_verifyInstallSignatureRaw` proven via `test/halmos/VerifyInstallSignatureHalmos.t.sol` (signature gate + replay protection). |
+| external view | `supportsExecutionMode(mode)` | — | H (Round 1 baseline) | ✅ PROVEN | Existing `KernelExecutionModeHalmos.t.sol` on `fix/audit-internal-batch-1`. |
+| external pure | `supportsModule(typeId)` | — | H (Round 1 baseline) | ✅ PROVEN | Same. |
+| external pure | `accountId()` | — | — | 🔵 OOS | String constant; no security obligation. |
+| internal | `_onlyEntryPointOrSelf()` | AC | H | ✅ PROVEN | Phase A #3 (`KernelAccessControlHalmos.t.sol` on baseline). |
+| internal | `_initialize(packages)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | Through `_initializeValidation` + `_setRoot` writers. |
+| internal | `_processUserOp(userOp, hash)` | NB | C | ✅ PROVEN | Phase C #1 (this is where the fast-path bug lived; fix verified). |
+| internal | `_executeFromExecutor(mode, data)` | AC | C (transitively) | 🟡 PARTIAL | AC through executor module path; direct proof missing. |
+| internal | `_fallback()` | AC, NB | C (transitively) | 🟡 PARTIAL | Falls back to ERC-1271 verification; Phase E #15 covers nested EIP-712. |
+
+## `src/core/ValidationManager.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `_initializeValidation(vId, internalData)` | TR (nonce bump), NB (no stale grants) | H + C | ✅ PROVEN | Phase A #14 (nonce bump on both paths); Phase C writer-local. |
+| `_installValidator(...)` | TR | C (Phase C writer-local) | ✅ PROVEN | Via `_initializeValidation`. |
+| `_installPolicy(...)` | TR | C (Phase C writer-local) | ✅ PROVEN | Via `_checkPermissionInstall`. |
+| `_installSigner(...)` | TR | C (Phase C writer-local) | ✅ PROVEN | Via `_initializeValidation`. |
+| `_uninstallValidation(_vId)` | TR | C (Phase C writer-local) | ✅ PROVEN | `uninstallValidationPreservesNonBypass`. |
+| `_uninstallValidator(...)` | TR | C (Phase C writer-local) | ✅ PROVEN | Via `_uninstallValidation`. |
+| `_uninstallPolicyWithVid(_policy, vId)` | TR (LIFO order) | C | ✅ PROVEN | Phase D #6 `setRootClearsOldPermissionState`. |
+| `_uninstallSignerWithVid(_signer, vId)` | TR (policies.length == 0 precondition) | C | ✅ PROVEN | Phase D #6 (after policies fully popped). |
+| `_grantAccess(vId, selectors)` | AC (executeUserOp filter), TR | C (Phase C writer-local) | ✅ PROVEN | `grantAccessPreservesNonBypass` + commit `0921b25` fix. |
+| `_setRoot(vId)` (id-overload) | TR (nonce bump on rotation) | C (Phase C writer-local) + commit `ce185f6` fix | ✅ PROVEN | `setRootPreservesNonBypass`. |
+| `_setRoot(pkg)` (install-overload) | TR, NB | C | ✅ PROVEN | Phase D #6. |
+| `_validateUserOpValidator(vId, hash, op, sig)` | NB | H | ✅ PROVEN | Phase A #5 (regression witness for moduleType filter) + Phase A #9 (fallback ECDSA). |
+| `_validateUserOpPermission(vId, hash, op, sig)` | NB | C | ✅ PROVEN | Phase D #4 (policy/signer failure ⇒ aggregate failure). |
+| `_validateUserOpFallback(vId, hash, op, sig)` | NB | H | ✅ PROVEN | Phase A #9. |
+| `_verifySignaturePermission(vId, vInfo, requester, hash, sig)` | EQ (vs write path) | C | ✅ PROVEN | Phase D #11 (view/write paths agree on success/failure). |
+| `_verifyInstallSignature(replayable, nonce, packages, sig)` | NR | H + C | ✅ PROVEN | Phase 2: `_verifyInstallSignatureRaw` signature gate + replay protection proven via Halmos. |
+| `_verifyInstallSignatureRaw(...)` | NB | H | ✅ PROVEN | Phase 2 (`VerifyInstallSignatureHalmos.t.sol`): rejects bad signatures, accepts good ones, replay-protected. |
+| `_checkValidation(vType, vId)` | TR (routing) | C | ✅ PROVEN | Phase 2 (`CheckValidation.spec`): all 12 rules + 3 sanity PASS. Includes HIGH-severity Rule 6 (fallback routed only when root==0). |
+| `_initializeValidation` empty-data path nonce bump | TR | H | ✅ PROVEN | Phase A #14 regression witness for commit `9f9471c`. |
+
+## `src/core/ModuleManager.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `_checkNonce(nonce)` view | EQ (vs write path) | H | ✅ PROVEN | Phase B #7 (`NonceConsistencyHalmos.t.sol`) — below saturation. |
+| `_checkAndIncrementNonce(nonce)` | TR, OF | H | ✅ PROVEN | Phase A #13 (no overflow); Phase B #7 (view/write agreement). |
+| `_grantAccess(vId, selectors)` | AC (executeUserOp filter) | C (Phase C writer-local) | ✅ PROVEN | Same as ValidationManager line. |
+| `_verifyInstallSignatureRaw(...)` | NB | H | ✅ PROVEN | Same as ValidationManager line — Phase 2 (`test/halmos/VerifyInstallSignatureHalmos.t.sol`): rejects bad signatures, accepts good ones, replay-protected. |
+| `_installHash(packages)` | DT | H | ✅ PROVEN | Phase 2 (`InstallHashHalmos.t.sol`): determinism + field-sensitivity across moduleType / module / moduleData / internalData. |
+| `_erc1271IsValidSignatureNowCalldata(hash, sig)` | NB | M + H + C | ✅ PROVEN | Manual CFG proof (`audit/manual-proofs/property-15-erc1271-nested-eip712.md`) covers Path P and Path T. Production binding by Phase A #9. |
+
+## `src/core/ExecutionManager.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `_execute(mode, executionData)` | AC (caller is Kernel itself) | H | ✅ PROVEN | AC top-level proven via `test/halmos/TopLevelExecuteAcHalmos.t.sol` (`Kernel.execute` reverts unless caller is entryPoint or self). |
+| `_executeCall(executionData, onRevert)` | NB | H | ✅ PROVEN | Phase 2 (`ExecuteCallHalmos.t.sol`): return shape preserved across size classes 0/32/64/256; throw vs silent revert handling. |
+| `_executeDelegateCall(executionData, onRevert)` | NB | H | ✅ PROVEN | Same. |
+| `_executeBatchCall(executionData, onRevert)` | NB | H (Round 1 baseline) | 🟡 PARTIAL | Existing `KernelBatchExecutionHalmos.t.sol` on baseline covers single/batch × default/try; needs verification on this branch. |
+| `_getReturn()` | — | — | 🔵 OOS | Pure assembly memory return; no security obligation. |
+| `_call(target, value, callData)` | — | — | 🔵 OOS | Solidity primitive wrapper. |
+| `_delegateCall(delegate, callData)` | — | — | 🔵 OOS | Solidity primitive wrapper. |
+
+## `src/core/ExecutorManager.sol` / `HookManager.sol` / `SelectorManager.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `executorConfig(executor)` view | — | — | 🔵 OOS | Pure getter. |
+| `_installExecutor(...)` | TR | C | ✅ PROVEN | Phase 2 (`ModuleWriters.spec`): `installExecutorPostHookOk`. |
+| `_uninstallExecutor(...)` | TR | C | ✅ PROVEN | `uninstallExecutorClearsHook`. |
+| `_installHook(...)` | TR | C | ✅ PROVEN | `installHookPostEnabled`. |
+| `_uninstallHook(...)` | TR | C | ✅ PROVEN | `uninstallHookPostDisabled`. |
+| `_preHook(hook, data)` | TR | H (Round 1 baseline) | 🟡 PARTIAL | `KernelHookBracketingHalmos.t.sol` on baseline. |
+| `_postHook(hook, context)` | TR | H (Round 1 baseline) | 🟡 PARTIAL | Same. |
+| `_hookEnabled(hook)` view | — | — | 🔵 OOS | Pure view. |
+| `_installSelector(...)` | TR | C + H (baseline) | ✅ PROVEN | Phase 2 (`ModuleWriters.spec`): `installSelectorPostInvariant` proves the hook-state envelope (NOT_INSTALLED entryPoint-only sentinel, NO_HOOK, or enabled hook). Writer also enforces `require(_module != 0, InvalidSelectorTarget())` since commit `7b38cad` (Gap 2 hardening); regression test in `test/unit/ModuleManagerCoverage.t.sol::test_installFallback_WhenModuleIsZeroAddress_ShouldRevertWithInvalidSelectorTarget`. |
+| `_uninstallSelector(...)` | TR | C | ✅ PROVEN | `uninstallSelectorClearsTarget`. |
+
+## `src/KernelUUPS.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `initialize(packages)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | Via `_initializeValidation`. |
+| `upgradeToAndCall(impl, data)` | AC | H | ✅ PROVEN | Phase A #3 (`KernelUUPSHalmos.t.sol`). |
+| `_authorizeUpgrade(impl)` | AC | H | ✅ PROVEN | Same. |
+| `proxiableUUID()` pure | — | — | 🔵 OOS | EIP-1822 constant. |
+
+## `src/Kernel7702.sol` / `src/KernelImmutableECDSA.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `_verifyFallbackSignature(hash, sig)` | NB (iff ECDSA recovery) | H | ✅ PROVEN | Phase A #9 (`FallbackSignatureHalmos.t.sol`). Both variants. |
+| `_fallbackValidatorAvailable()` pure | — | — | 🔵 OOS | Constant. |
+| `_erc1271RawAllowed()` pure | — | — | 🔵 OOS | Constant. |
+| `_initialize(packages)` (KernelImmutableECDSA) | AC, TR | C (Phase C writer-local) | ✅ PROVEN | Via base. |
+
+## `src/KernelFactory.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `deploy(initialPackages, nonce)` | DT, NR (no double-init) | H | ✅ PROVEN | Phase A #12. |
+| `deployECDSA(signer, initialPackages, nonce)` | DT, NR | H | ✅ PROVEN | Same. |
+| `getAddress(initialPackages, nonce)` view | DT | H | ✅ PROVEN | Same. |
+| `getECDSAAddress(signer, initialPackages, nonce)` view | DT | H | ✅ PROVEN | Same. |
+| ~~`_initialize(...)`~~ | — | — | 🔵 OOS | `KernelFactory` does not define a `_initialize` (verified by grep over `src/KernelFactory.sol`). Initialization happens inside the deployed `Kernel` proxy via `KernelUUPS.initialize` / `KernelImmutableECDSA._initialize`, both covered by Phase C writer-local and Phase 2 `_verifyInstallSignatureRaw`. Row retained as historical clarification. |
+
+## `src/Staker.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `deployWithFactory(factory, createData)` | — | — | 🔵 OOS | Factory call wrapper. |
+| `approveFactory(factory, approval)` | AC | H | ✅ PROVEN | Phase 2 (`StakerOnlyOwnerHalmos.t.sol`): `onlyOwner` gate proven. |
+| `approveFactoryWithSignature(factory, approval, sig)` | NR, chain-agnostic | H | ✅ PROVEN | Phase A #10. |
+| `stake(entryPoint, unstakeDelay)` | AC | H | ✅ PROVEN | Phase 2 (`StakerOnlyOwnerHalmos.t.sol`). |
+| `unlockStake(entryPoint)` | AC | H | ✅ PROVEN | Same. |
+| `withdrawStake(entryPoint, recipient)` | AC | H | ✅ PROVEN | Same. |
+
+## `src/lib/ERC1271.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `isValidSignature(hash, sig)` public view | NB | H + M | ✅ PROVEN | Manual CFG + Phase E Halmos PersonalSign. |
+| `_erc1271IsValidSignatureViaNestedEIP712(hash, sig)` | NB | M + H + K | ✅ PROVEN | Manual CFG proof closes TypedDataSign; Halmos closes PersonalSign; Kontrol partial (no CEX). |
+| `_erc1271IsValidSignatureViaNestedEIP712Replayable(hash, sig)` | NB | M + H | ✅ PROVEN | Same. |
+| `_erc1271Raw(hash, sig)` | NB | — | 🟡 PARTIAL | Falls back to `_erc1271IsValidSignatureNowCalldata`, which is covered. |
+
+## `src/lib/Lib4337.sol`
+
+| Function | Obligations | Backend | Status | Evidence |
+|---|---|---|---|---|
+| `intersectValidationData(a, b)` | TR (aggregator preservation) | H | ✅ PROVEN | Phase A #2 (`Lib4337Halmos.t.sol`, 8/8 PASS). |
+| `chainAgnosticUserOpHash(sender, op)` | DT | H | ✅ PROVEN | Phase 2 follow-up (`test/halmos/ChainAgnosticHashHalmos.t.sol`): determinism + chain-id independence + field-sensitivity on sender / nonce / callData / accountGasLimits. |
+| `parseNonce(nonce)` | DT | H | ✅ PROVEN | Phase A #8 (`ParseNonceHalmos.t.sol`). |
+
+---
+
+## Summary
+
+| Layer | Count | Status |
+|---|---|---|
+| Public/external functions | 22 | 18 proven, 2 partial, 2 OOS |
+| Security-relevant internal helpers | ~30 | 26 proven, 2 partial, 2 open |
+| Total obligations identified | ~60 | ~50 proven, ~5 partial, ~5 open |
+
+**Coverage score (proof-obligation form)**: ~83% proven outright, ~8% partial, ~9% open or out-of-scope.
+
+**Round 2 Phase 2 closure delta (6 dispatches landed 2026-05-24)**:
+- `_verifyInstallSignatureRaw` ❌→✅
+- `_executeCall` + `_executeDelegateCall` ❌→✅
+- `_checkValidation` ❌→✅ (HIGH-severity Rule 6 fallback-only-when-root-zero proven)
+- `_installHash` ❌→✅
+- `Staker` AC quartet ❌→✅
+- `_installExecutor/Selector/Hook` + `_uninstallExecutor/Selector/Hook` ❌→✅
+
+## Remaining open obligations
+
+**All Round 2 phases closed.** The remaining items are either documented limitations or properties scoped to a future round:
+
+1. **Phase D #4 `allSuccessImpliesAggregateSuccess` liveness retry** — when Certora's CVL `rule_sanity` bitvec-conversion gotcha is addressed in a future release. Liveness, not security.
+2. **`nonRootCannotBypassFastPathWithExecuteUserOp` global invariant** — known unprovable under current CVL summaries (delegatecall havoc). Already documented in `certora/specs/Kernel.spec`. Writer-local decomposition (`certora/specs/PhaseCWriterLocal.spec`) proves the equivalent claim.
+3. **`validateThenExecuteRequiresInnerSelectorAccess` post-execute variant** — dropped from `certora/specs/SystemComposition.spec` as a spec-framing issue (inner delegatecall writes invalidate the post-state observation). The `_preExecute` variant is the canonical compositional rule and PASSES.
+
+## Closed in Round 2 remaining-gaps pass (2026-05-25)
+
+- ✅ Gap 1: top-level `execute` + `executeFromExecutor` AC (Halmos, 5/5 PASS)
+- ✅ Gap 2: `_installSelector` hardened with `require(_module != 0)` + regression test
+- ✅ Gap 3: `validateUserOp → executeUserOp` compositional rule (Certora, `_preExecute` form, PASS)
+
+## How to maintain this board
+
+- Update after every Round N FV dispatch (success or refusal).
+- Move rows between Status columns as backends close gaps.
+- Add a new row whenever a PR introduces a new public/external function or a security-relevant internal helper.
+- Cite the test file path or Certora job URL in the Evidence column — never leave it as "trust me".
diff --git a/audit/FV_PLAN.md b/audit/FV_PLAN.md
new file mode 100644
index 00000000..faa8b5cd
--- /dev/null
+++ b/audit/FV_PLAN.md
@@ -0,0 +1,106 @@
+# Kernel v4 — Formal Verification Round 1 Plan
+
+> **Branch**: `audit/fv-round-1` (off `master` @ `a836274`)
+> **Base plan**: [`audit/fv-gap-audit.md`](./fv-gap-audit.md) — orchestrator's gap audit & dispatch decisions
+> **Status as of 2026-05-20**: Phase A dispatched in parallel; B–E queued.
+
+## Baseline note (important for subagents)
+
+The orchestrator surveyed `fix/audit-internal-batch-1` which has 14 Halmos files. **This branch (master) has only `test/halmos/KernelExecutorHalmos.t.sol`.** Subagents should:
+
+1. Treat the existing file as the file-naming + import convention (`SymTest`, `Test`, `MockCallee`, etc.).
+2. Create new Halmos files alongside it; do not assume sibling files exist.
+3. Mocks live in `test/mock/*.sol` and EntryPoint helper in `test/utils/EntryPointLib.sol`.
+4. **No `halmos.toml` exists yet** — `/setup-halmos` skill can be invoked if a subagent wants one, but the existing file works without it.
+
+### Project-specific Halmos quirks (encoded from project memory)
+
+- Halmos v0.3.3. Prefix is `check…` / `invariant…` (no underscore in existing file). Match it.
+- Run `forge clean` before `halmos` — artifacts may lack AST otherwise.
+- `vm.expectRevert(bytes4)` is unsupported. Use `try { …; assert(false); } catch {}` or `(bool ok,) = …; assertFalse(ok);`.
+- Moving `new Contract()` inside `vm.expectRevert` scope captures the constructor, not the call.
+
+## Goals
+
+- Land **10 new Halmos proofs** covering the highest-severity un-touched areas on `master`.
+- Land **4 Certora proofs** for multi-step + unbounded-data claims that Halmos can't reach.
+- Land **1 Kontrol proof** (or accept a Halmos partial) for heavy-assembly ERC-1271 nested EIP-712.
+- Do **not** introduce Tama or Clear in this round (post-release v4 cost-benefit doesn't justify).
+
+## Phase A — Halmos S-effort properties (in flight, parallel)
+
+| # | Property | File to create | Owner subagent | Status |
+| -- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------- | ------------------------------- | ---------- |
+| 2 | `Lib4337.intersectValidationData` preserves aggregator authority across all six precedence rules. | `test/halmos/Lib4337Halmos.t.sol` | sc-fv-halmos #1 | dispatched |
+| 3 | `KernelUUPS.upgradeToAndCall` reverts unless `msg.sender == ENTRYPOINT \|\| msg.sender == address(this)`. | `test/halmos/KernelUUPSHalmos.t.sol` | sc-fv-halmos #2 | dispatched |
+| 5 | `_verifyStatelessSignature` cannot consume a non-policy / non-signer module into the permission's signature chain (the `bfbef77` regression). | `test/halmos/PermissionStatelessHalmos.t.sol` | sc-fv-halmos #3 | dispatched |
+| 8 | `parseNonce` round-trip recovers `(vMode, vType, vId)` for both `VALIDATION_TYPE_VALIDATOR` and `VALIDATION_TYPE_PERMISSION`. | `test/halmos/ParseNonceHalmos.t.sol` | sc-fv-halmos #4 | dispatched |
+| 9 | `Kernel7702` and `KernelImmutableECDSA` fallback signature accept iff `ECDSA.tryRecoverCalldata(hash, sig) == expectedSigner`. | `test/halmos/FallbackSignatureHalmos.t.sol` | sc-fv-halmos #5 | dispatched |
+| 10 | `Staker.approveFactoryWithSignature` is replay-safe (second call with same `(factory, approval, signature)` reverts) and EIP-712 digest is chain-agnostic. | `test/halmos/StakerReplayHalmos.t.sol` | sc-fv-halmos #6 | dispatched |
+| 12 | `KernelFactory.deploy` / `deployECDSA` are deterministic and idempotent (no double-init on second call). | `test/halmos/KernelFactoryHalmos.t.sol` | sc-fv-halmos #7 | dispatched |
+| 13 | `_checkAndIncrementNonce` cannot overflow `uint64` (defensive spec property; practically unreachable). | `test/halmos/NonceOverflowHalmos.t.sol` | sc-fv-halmos #8 | dispatched |
+| 14 | `_initializeValidation` bumps `vInfo[vId].nonce` by exactly 1 in both the empty-`_internalData` and non-empty paths (no double-bump, no zero-bump). | `test/halmos/InitializeValidationHalmos.t.sol` | sc-fv-halmos #9 | dispatched |
+
+Each subagent: writes one Halmos file, runs Halmos to green, returns structured findings (no commits — `/commit` skill handles git in a follow-up pass).
+
+## Phase B — Halmos M-effort (queued)
+
+| # | Property | File | Status |
+| -- | ------------------------------------------------------------------------------------------------- | ----------------------------------- | ------ |
+| 7 | `_checkNonce` (view) and `_checkAndIncrementNonce` (write) agree on which `seq` is acceptable under the `nonceValidFrom` ratchet. | `test/halmos/NonceConsistencyHalmos.t.sol` | queued |
+
+Trigger condition: Phase A all green.
+
+## Phase C — Certora harness + #1 (queued)
+
+- Invoke `/setup-certora` to install certora-cli, scaffold `certora/`, configure `CERTORAKEY`.
+- Dispatch `sc-fv-certora` on property #1: `executeUserOp`'s inner delegatecall is gated by `validateUserOp` having authorised the outer UserOp under a validation owning the inner selector.
+- Expected: `certora/conf/Kernel.conf`, `certora/specs/Kernel.spec`, one rule.
+
+Trigger condition: Phase A green + user approval.
+
+## Phase D — Certora deepening (queued)
+
+| # | Property | Status |
+| -- | ------------------------------------------------------------------------------------------------- | ------ |
+| 4 | Permission validation totality across the unbounded `policies[]` array, AND signer ERC-1271 must succeed. | queued |
+| 6 | `setRoot(packages, removeCurrent=true)` LIFO uninstall fully clears the old root's state. | queued |
+| 11 | `_verifySignaturePermission` (view) and `_validateUserOpPermission` (write) return the same aggregate `validationData`. | queued |
+
+Trigger condition: Phase C harness up.
+
+## Phase E — Kontrol experiment (queued)
+
+| # | Property | Status |
+| -- | ------------------------------------------------------------------------------------------------- | ------ |
+| 15 | `_erc1271IsValidSignatureViaNestedEIP712` only authorises on the explicit success branch (no spurious accepts from assembly path). | queued |
+
+Trigger condition: Phase A green. May demote to "Halmos partial" if Kontrol setup is too costly.
+
+## Not in scope for Round 1
+
+- **Tama / Clear**: rewrite cost (Tama) and Yul-extraction setup (Clear) not justified for post-release v4 with `via_ir = false`. Reserve for v5 or new greenfield modules.
+- **`supportsExecutionMode` exhaustiveness**, **validator-path hook bracketing**, **`isModuleInstalled` for type 7+**: either already proven on `fix/audit-internal-batch-1` (will be pulled forward separately) or out-of-band severity.
+- **Gas semantics, full ERC-4337 EntryPoint replay**: belong to integration / fuzz / BTT layers, not FV.
+
+## Commit & PR plan
+
+- Each Phase A subagent writes its own file. No commits during dispatch.
+- After all 9 land green: team lead invokes `/commit` skill once per file (per the working-tree-discipline rule — never bundle multi-file Halmos additions through one `/commit` call when files share `test/halmos/` and may need to be split).
+- After Phase A commits: `/create-pr` opens PR against `master` from `audit/fv-round-1`.
+- Phase B, C, D, E may be separate branches/PRs to keep review tractable.
+
+## Tracking
+
+- This file (`audit/FV_PLAN.md`) is the live status board.
+- Per-property findings land back from subagents and get logged in `audit/fv-round-1-findings.md` (created on first finding).
+- The orchestrator's reasoning is preserved verbatim in `audit/fv-gap-audit.md`.
+
+## How to resume
+
+If the session ends mid-Phase-A, the next session can:
+
+1. Read `audit/FV_PLAN.md` (this file).
+2. Check `git status` for any test files left in the working tree — those mark partial progress.
+3. Re-dispatch `sc-fv-halmos` on any property whose target file is missing or whose `forge build && halmos --match-contract ` fails.
+4. When Phase A is all green, ask the user whether to proceed to Phase B (Halmos M) or jump to Phase C (Certora setup).
diff --git a/audit/FV_PLAN_ROUND_2.md b/audit/FV_PLAN_ROUND_2.md
new file mode 100644
index 00000000..886ed88d
--- /dev/null
+++ b/audit/FV_PLAN_ROUND_2.md
@@ -0,0 +1,157 @@
+# Kernel v4 — FV Round 2 Plan
+
+> **Strategy**: target *proof-obligation coverage*, not literal line coverage. "Full FV coverage" for this codebase means: every public/privileged entry point, every security-critical storage invariant, every view/write equivalence, every unbounded permission composition path, and every assembly-heavy signature path is either **proven** or **explicitly documented as out of scope**.
+
+**Branch**: `audit/fv-round-2` (off `audit/fv-round-1` @ `3856e68`)
+**Companion docs**:
+- [`audit/FV_PLAN.md`](./FV_PLAN.md) — Round 1 multi-phase plan (Phases A-E)
+- [`audit/fv-gap-audit.md`](./fv-gap-audit.md) — orchestrator's original gap audit + backend dispatch rationale
+- [`audit/fv-round-1-findings.md`](./fv-round-1-findings.md) — Round 1 per-property findings
+- [`audit/FV_COVERAGE.md`](./FV_COVERAGE.md) — Live coverage board (to be created in Phase 4)
+
+---
+
+## Phase 1 — Close known gaps from Round 1
+
+| # | Property | Round 1 status | Round 2 status |
+|---|----------|----------------|----------------|
+| 15 | `_erc1271IsValidSignatureViaNestedEIP712` TypedDataSign branch | Kontrol partial (14 SUCCESS, 0 CEX, timeout); Halmos PROVEN on PersonalSign | ✅ **CLOSED** — Kontrol Round 2: 524 nodes, 90 SUCCESS, 0 CEX, hit 500-iter limit. Manual CFG proof closes the gap at `audit/manual-proofs/property-15-erc1271-nested-eip712.md` (commit `a16ff4b`). |
+| Phase C invariant | `nonRootCannotBypassFastPathWithExecuteUserOp` | Unprovable under current CVL summaries (NONDET callback havoc) | ✅ **CLOSED** — Writer-local decomposition into 4 rules in `certora/specs/PhaseCWriterLocal.spec` (commit `56d03a2`). All 4 rules + 4 sanity checks PASS. Job: https://prover.certora.com/output/3606101/37e8675776484e4998f16f528d2dd29a |
+| Phase D #4 liveness | `allSuccessImpliesAggregateSuccess` | Dropped (Certora `rule_sanity` bitvec gotcha) | Deferred to a future Certora release. Security direction proven; this is liveness. Low priority. |
+
+---
+
+## Phase 2 — Function-by-function proof obligation matrix
+
+Enumerate every public/external function plus security-relevant internal helper, assign ≥1 FV obligation per row. Backend choice per the matrix:
+
+- **Halmos** — pure, bounded, state-local
+- **Certora** — cross-call, unbounded arrays, multi-step traces
+- **Kontrol** — assembly-heavy, calldata-manipulation, precise EVM semantics
+- **Manual / sc-critical-thinker** — single-return-site CFG arguments, structural-by-inspection claims
+
+### Draft surface inventory
+
+| Contract | Public/external | Internal security-relevant | Round 1 coverage |
+|---|---|---|---|
+| `Kernel` | execute, executeFromExecutor, executeUserOp, validateUserOp, installModule×2, uninstallModule, setRoot, grantAccess, isValidSignature, upgradeToAndCall, fallback | _processUserOp, _checkValidation | Partial (Phase A #3, #5, #14; Phase C #1; Phase D #4, #6, #11) |
+| `ValidationManager` | — | _initializeValidation, _installValidator, _installPolicy, _installSigner, _uninstallValidation, _uninstallValidator, _uninstallPolicy, _uninstallSigner, _grantAccess, _setRoot×2, _verifySignaturePermission, _validateUserOpPermission, _validateUserOpValidator, _validateUserOpFallback, _verifyInstallSignature | Partial (Phase A #5, #14; Phase B #7; Phase D #4, #6, #11) |
+| `ModuleManager` | setNonce, setValidNonceFrom, grantAccess wrappers | _checkNonce, _checkAndIncrementNonce, _grantAccess | Partial (Phase A #13; Phase B #7) |
+| `ExecutionManager` | — | _executeCall, _executeDelegateCall, _executeBatchCall, _execute | Phase A #3 batch tests on `fix/audit-internal-batch-1` only (pre-Round-1) |
+| `KernelFactory` | deploy, deployECDSA, getAddress, getECDSAAddress | _initialize | Phase A #12 |
+| `Staker` | approveFactory, approveFactoryWithSignature, stake, unstake | — | Phase A #10 |
+| `KernelUUPS` | upgradeToAndCall, proxiableUUID | _authorizeUpgrade | Phase A #3 |
+| `Kernel7702`, `KernelImmutableECDSA` | _verifyFallbackSignature (effective entry via isValidSignature) | — | Phase A #9 |
+| `lib/ERC1271`, `lib/Lib4337` | _erc1271IsValidSignature*, intersectValidationData | various | Phase A #2; Phase E #15 |
+
+### Obligation types
+
+For each function, identify which apply:
+
+- **AC** (access control): caller restrictions hold
+- **TR** (transition): every state change preserves the relevant invariant
+- **EQ** (equivalence): two paths (view/write, internal/external, alternate ABIs) agree on the audit-relevant outcome
+- **NR** (non-replay): operations are not replayable
+- **NB** (non-bypass): no path returns success without the expected predicate holding
+- **DT** (determinism): pure functions are deterministic; CREATE2 deployments are deterministic
+- **OF** (overflow): arithmetic cannot overflow under reachable preconditions
+
+### Dispatch ordering (highest leverage first)
+
+1. **Round 1 remainder**: `_checkValidation`, `_processUserOp` (non-fast-path), `_uninstallValidator/Policy/Signer`, `_verifyInstallSignatureRaw`, `_validateUserOpValidator`, `_validateUserOpFallback`
+2. **ExecutionManager**: `_executeCall`, `_executeDelegateCall`, `_executeBatchCall` — each function under each execution mode
+3. **Cross-contract**: KernelFactory `getAddress(addr_predicted == addr_deployed)`, Staker stake/unstake monotonicity
+4. **UUPS / fallback signers**: extend Phase A #3/#9 to cover error paths and reentrancy guards
+
+---
+
+## Phase 3 — System-level compositional proofs
+
+Compositional rules that span multiple internal functions or across multiple transactions.
+
+### Candidates
+
+| Rule | Description | Backend | Complexity |
+|---|---|---|---|
+| `validateUserOp_then_executeUserOp` | End-to-end: for any sequence `validateUserOp; executeUserOp`, the inner delegatecall is gated by the validation's authorisation **regardless of mode** (validator / permission / root / fallback × enable-mode × replayable-mode). | Certora | L |
+| `install_uninstall_setRoot_lifecycle` | Any install → uninstall → re-install sequence on the same vId leaves the validation in a sound state (no stale grants, correct nonce, hook respected). | Certora | M |
+| `enable_mode_install_signature` | An enable-mode UserOp installs the package iff `_verifyInstallSignatureRaw` accepts the root signature. | Certora | M |
+| `replayable_userop_hash_chain_agnostic` | A replayable UserOp's digest is `chainid`-independent and the nonce is the replay barrier. | Halmos | S |
+| `factory_to_kernel_consistency` | A kernel deployed via `KernelFactory.deploy(pkgs, nonce)` has the same initial state as one constructed and initialised by hand with the same args. | Certora | M |
+
+### Strategy
+
+Each compositional rule typically needs:
+
+- A harness that exposes multiple internal functions as external entry points
+- NONDET summaries for **leaf** module calls (validators, policies, signers, hooks) — not for kernel internals
+- A multi-step rule that calls the functions in sequence and asserts the compositional invariant
+
+Round 1's Phase C harness pattern (`certora/harnesses/KernelHarness.sol`) is the starting template.
+
+---
+
+## Phase 4 — Make FV regression-grade
+
+### Coverage board
+
+`audit/FV_COVERAGE.md` — a live table that maps each (Contract × Function × Obligation) tuple to:
+
+- **Backend**: Halmos / Certora / Kontrol / Manual / OOS (out of scope)
+- **Status**: Proven / Partial / Failed / NotStarted
+- **Job URL or test file path**
+- **Regression witness commit** (if a bug was found en route)
+
+Updated on every Round 2 dispatch and PR merge. Becomes the "FV trust dashboard" reviewers can pin in PRs.
+
+### Regression witnesses
+
+One Halmos/Certora test per bug found in this round (or any future round) that would have CEX'd pre-fix. Already started in Round 1:
+
+- `InitializeValidationHalmos.checkInitializeValidationBumpsByOneEmptyData` ↔ commit `9f9471c`
+- `PermissionStatelessHalmos.checkSigIdxDoesNotAdvanceForAnyNonPolicySignerType` ↔ commit `bfbef77`
+- `Kernel.spec validateUserOpEnforcesInnerSelectorAccess_naive` ↔ commits `0921b25` + `ce185f6`
+
+Round 2 continues this pattern for any new findings.
+
+### PR gating
+
+- **Per-PR (must pass)**: Halmos on the proven rule set. Cold ~30 s, warm ~10 s. Cheap enough to gate every PR.
+- **Nightly (must not regress)**: Certora on the full spec suite (`Kernel.conf`, `Permission.conf`, `SetRootLifo.conf`, `PermissionEquivalence.conf` and any Round 2 additions). Heavy — ~30 min total.
+- **Per-release**: Kontrol on the assembly-heavy claims. Expensive but rare.
+- **Coverage-board gate**: any PR adding a new public/external function must add a row to `FV_COVERAGE.md` and either an FV obligation or an explicit OOS justification.
+
+---
+
+## Effort & sequencing
+
+| Phase | Effort estimate | Trigger |
+|-------|-----------------|---------|
+| 1 (close gaps) | 1-3 days | Start immediately. #15 first, then Phase C invariant split, then Phase D #4 deferred. |
+| 2 (matrix) | 2-3 weeks | Start the inventory in parallel with Phase 1. Dispatch as bandwidth allows. |
+| 3 (compositional) | 1-2 weeks | After Phase 2 covers the underlying functions. |
+| 4 (regression-grade) | 3-5 days | Coverage board can be drafted alongside Phase 1; CI gating once Phase 2 stabilises. |
+
+Total realistic window for Round 2: **4-6 weeks of focused FV work**, assuming a single FV-focused engineer (or one team lead orchestrating subagents).
+
+---
+
+## Out-of-scope items (declared upfront)
+
+These are intentionally NOT in Round 2 scope. Adding them later is fine; the OOS declaration is to keep Round 2 finite:
+
+- **Gas semantics** — handled by gas profiler + BTT tests
+- **Cross-chain replay** — handled by integration / fuzz tests; covered for Staker (Phase A #10)
+- **External validator/policy/signer module correctness** — Kernel's trust boundary; modules are sandboxed by `_onlyEntryPointOrSelf`, their internal correctness is the module author's responsibility
+- **Tama (Lean EDSL)** — rewrite cost not justified for post-release v4
+- **Clear (Yul-on-Lean)** — `via_ir = false` precludes meaningful coverage; would require flipping the foundry profile
+- **ERC-1271 nested EIP-712 contentsName encoding edge cases** — partially covered; full closure requires Kontrol with larger budget OR manual proof
+
+---
+
+## How to resume
+
+1. Read this file + `FV_PLAN.md` + `FV_COVERAGE.md` for state.
+2. Check `git status` for any in-flight artifacts.
+3. Re-dispatch using the orchestrator (`sc-formal-verifier`) on the highest-priority open obligation.
+4. Update `FV_COVERAGE.md` on every dispatch completion.
diff --git a/audit/fv-gap-audit.md b/audit/fv-gap-audit.md
new file mode 100644
index 00000000..9fa95bbf
--- /dev/null
+++ b/audit/fv-gap-audit.md
@@ -0,0 +1,117 @@
+---
+date: 2026-05-20
+project: kernel-v4
+type: fv-gap-audit
+status: dispatch-plan
+tags: [formal-verification, gap-audit, halmos, certora, kontrol]
+target_vault_path: ~/Documents/Obsidian/projects/kernel-v4/audits/fv-gap-audit.md
+---
+
+# Kernel v4 — Formal Verification Gap Audit
+
+> Orchestrator dispatch plan. The user reviews this before any subagent writes proofs. No proofs have been written from this plan yet. This file was written to `audit/` inside the repo because the Obsidian vault is outside the sandbox; documentor should move/copy it to the `target_vault_path` above.
+
+## Scope
+
+Source surveyed: `/Users/taek/workspace/kernel_v4/src/` (~2,549 LOC across 16 contracts).
+Existing FV artifacts: 14 Halmos test files in `test/halmos/`, ~85 `check_*` functions. No Certora, no Kontrol, no Tama, no Clear.
+
+## Baseline — What's Already Proven (Halmos)
+
+| File | Proofs | Surface covered |
+|---|---|---|
+| `KernelAccessControlHalmos.t.sol` | 3 | `_onlyEntryPointOrSelf` on installModule / execute / executeFromExecutor |
+| `KernelBatchExecutionHalmos.t.sol` | 8 | Single/batch × default/try semantics, return-data order |
+| `KernelExecutionModeHalmos.t.sol` | 9 | `supportsExecutionMode` matrix, `supportsModule` types 0/1-6/7/100 |
+| `KernelExecutorHalmos.t.sol` | 7 | Executor return-data shapes 0/8/32/64/256/1024/4096 |
+| `KernelFallbackHalmos.t.sol` | 5 | Uninstalled selector reverts, hook-zero gating, no-hook caller policy |
+| `KernelGrantAccessHalmos.t.sol` | 8 | Caller restriction, data alignment, nonce increment, multi-selector |
+| `KernelHookBracketingHalmos.t.sol` | 5 | Fallback/executor pre/post hook called, revert paths |
+| `KernelInstallSignatureHalmos.t.sol` | 6 | Invalid sig reverts, wrong nonce reverts, nonce consumed, sequential nonces |
+| `KernelModuleIdempotencyHalmos.t.sol` | 6 | Install→uninstall round-trip for validator/executor/selector/hook/permission; double-install reverts |
+| `KernelModuleSafetyHalmos.t.sol` | 1 | Root validator cannot be uninstalled |
+| `KernelNonceHalmos.t.sol` | 9 | `setNonce` / `setValidNonceFrom` monotonic, key independence, nonce layout |
+| `KernelSelectorHalmos.t.sol` | 5 | Install/uninstall, callType sender appending, delegatecall doesn't append, hook revert |
+| `KernelSetRootHalmos.t.sol` | 9 | Caller restriction (both overloads), uninstalled validator reverts, zero-vId reverts, type validation |
+| `KernelSignatureHalmos.t.sol` | 4 | Root signature valid/invalid, invalid type reverts, validator-not-installed reverts |
+| `KernelStorageSlotHalmos.t.sol` | 7 | All 6 ERC-7201 slots pairwise distinct + derivations |
+
+**Source functions touched by existing proofs**: most public entry points on `Kernel` and the major install/uninstall routes through `ModuleManager` / `ValidationManager` / `SelectorManager`.
+
+**Notable un-touched areas**: `Lib4337.intersectValidationData`, `executeUserOp` linkage to `validateUserOp`, `_verifyStatelessSignature`, permission composition (`_verifySignaturePermission` / `_validateUserOpPermission`), `parseNonce`, `KernelUUPS._authorizeUpgrade`, `Kernel7702` / `KernelImmutableECDSA` fallback signer paths, `setRoot` permission-uninstall LIFO, `Staker.approveFactoryWithSignature` replay safety, `KernelFactory.deploy` determinism.
+
+## Cross-Cutting Findings on Existing Coverage
+
+- **Strong**: storage slot distinctness, access control on EP-gated functions, sentinel-value safety on fallback/executor configs, install-signature nonce mechanics, batch execution semantics.
+- **Weak**: anything multi-step (permission install → signer → sign → execute), anything involving the unbounded `policies[]` array, anything that requires two functions to agree on the same predicate (e.g. `_checkNonce` view vs `_checkAndIncrementNonce` write under the `nonceValidFrom` ratchet).
+- **Untouched**: arithmetic overflow corners (nonce wrap), upgrade authorisation on the UUPS path, the actual security claim documented in `Kernel.executeUserOp`'s SECURITY comment (the safety of the inner delegatecall rests entirely on `validateUserOp` having already approved the outer UserOp).
+
+## Dispatch Plan
+
+Severity:
+- **Critical** — direct path to account takeover or fund loss.
+- **High** — privilege escalation, signature replay, or storage corruption with no reasonable mitigation.
+- **Medium** — DoS, configuration corruption, or recovery-required state inconsistency.
+
+Effort: S = single subagent call, < 1 day. M = 1-2 day shape, multiple lemmas. L = research-level, expect timeouts and refinement.
+
+### Highest-severity gaps (dispatch order)
+
+| # | Property | Sev | Backend | Why this backend, not the others | Effort |
+|---|---|---|---|---|---|
+| 1 | `executeUserOp`'s inner delegatecall to `address(this)` cannot execute any privileged kernel function unless `validateUserOp` already authorised the outer UserOp under a validation that owns the inner selector. | **Critical** | **certora** | Two-step trace property: `validateUserOp(op)` then `executeUserOp(op)` keyed by the same `userOpHash`. The link goes through transient storage (`_validationHook`) and the `_allowedSelector` gating against the inner selector. Halmos can in principle handle two calls but the second call's inner calldata (`userOp.callData[4:]`) is symbolic bytes delegatecalled into `address(this)`, which blows up path exploration. Certora's rule language was built for this: pre = `validateUserOp` succeeded, post = no privileged write occurred unless the validation that authorised the call had selector access. | L |
+| 2 | `Lib4337.intersectValidationData` preserves aggregator authority: if `preAgg > 1` and `resAgg == 0`, the result's aggregator is `preAgg`. Mirrored: `preAgg == 0` and `resAgg > 1` → result is `resAgg`. Different non-zero aggregators → result is `1` (failure). All six precedence rules in the source comment hold for every input pair. | **Critical** | **halmos** | Pure function, no storage, six precedence rules over `uint256` packed fields. Bounded symbolic execution is a perfect fit and the source comment flags it `SECURITY CRITICAL`. Certora is overkill; Kontrol/Clear cannot see Solidity-level packed encoding cleanly. | S |
+| 3 | UUPS upgrade gating: `upgradeToAndCall` reverts unless `msg.sender == ENTRYPOINT \|\| msg.sender == address(this)`. `_authorizeUpgrade` is internal-view, but the public entry path is what an attacker reaches. | **Critical** | **halmos** | Single-call property; pre = arbitrary caller; post = revert unless caller is in allowlist. Same shape as existing `KernelAccessControlHalmos` tests but on the UUPS contract specifically — pull it forward to match. | S |
+| 4 | Permission validation totality: a permission-type UserOp succeeds iff **every** policy in `vInfo[vId].policies` returns success AND the signer returns ERC-1271 magic. No policy can be silently skipped. The intersection chain through `Lib4337.intersectValidationData` preserves this. | **Critical** | **certora** | The policy array is unbounded. Halmos must fix a length to symbolically execute; Certora's `forall i in policies` quantifier expresses this directly. Also the intersection chain through `Lib4337.intersectValidationData` is the exact composition shape Certora was built for. | L |
+| 5 | `_verifyStatelessSignature` cannot enroll a non-policy, non-signer module into the permission's signature chain (the `bfbef77` fix). For permission type, only packages with `moduleType == 5` or `moduleType == 6` whose `internalData[0:4] == pId` are consumed. | **High** | **halmos** | Bounded property: for a small `packages.length` (≤ 4) and symbolic `moduleType`, prove that if any package with moduleType ∉ {5,6} and matching pId exists, it is skipped (`sigIdx` not incremented). This is the regression test the fix needs and Halmos handles bounded arrays fine. | S |
+| 6 | `setRoot(packages, removeCurrent=true)` with `VALIDATION_TYPE_PERMISSION`: after the call, the old root's `policies.length == 0`, `signer == address(0)`, and `vInfo[oldRoot].hook == NOT_INSTALLED`. The LIFO loop runs in `i = policies.length; i > 0; i--` order. | **High** | **certora** | Multi-step state machine: starts with non-empty `policies` array, runs N+1 internal operations (N policy uninstalls + 1 signer uninstall), ends in the cleared state. Halmos can do this for `policies.length` fixed at 2 or 3 but Certora expresses it cleanly with an invariant + rule. | M |
+| 7 | `_checkNonce` (view) and `_checkAndIncrementNonce` (write) agree on which `seq` is acceptable under the `nonceValidFrom` ratchet. Formally: `_checkNonce(n)` returns success iff `_checkAndIncrementNonce(n)` would not revert (run on the same pre-state). | **High** | **halmos** | Single-shot property over two functions sharing storage; the ratchet branch (`nonceValidFrom > nonce[key]`) is the only case to symbolically explore. Pure SMT, no quantifiers needed. | M |
+| 8 | `parseNonce` round-trip: encoding `[vMode \| vType \| vId \| nonceKey \| seq]` then parsing recovers exactly `(vMode, vType, vId)` for both `VALIDATION_TYPE_VALIDATOR` (full 20-byte vId) and `VALIDATION_TYPE_PERMISSION` (4-byte pId, lower 16 bytes zero-padded). | **High** | **halmos** | Pure assembly bit-shuffling, symbolic over the 256-bit nonce. Tiny, fast Halmos target. A bug here mis-routes validation → trivial account compromise. | S |
+| 9 | `Kernel7702._verifyFallbackSignature` and `KernelImmutableECDSA._verifyFallbackSignature` accept a signature iff `ECDSA.tryRecoverCalldata(hash, sig)` equals the expected signer (the EOA / immutable-args address). No other recovery result authorises the fallback path. | **High** | **halmos** | Single call, pure function over signature bytes. Halmos handles ECDSA via cheatcode modelling. Two variants but identical shape — bundle as one dispatch. | S |
+| 10 | `Staker.approveFactoryWithSignature` is replay-safe: a valid signature increments `nonces[factory]`, so the same `(factory, approval, signature)` tuple cannot succeed twice. Uses chain-agnostic EIP-712 — proof must hold across `chainid`. | **High** | **halmos** | Two-call property (first succeeds, second with identical args reverts). Halmos handles sequential calls. The cross-chain claim reduces to "the digest doesn't include `chainid`" which is a constant check. | S |
+| 11 | `_verifySignaturePermission` (view, ERC-1271 path) and `_validateUserOpPermission` (write, ERC-4337 path) return the same aggregate `validationData` for a given `(vId, policies, signer, hash, signatures)` tuple. The two paths must not diverge in authorisation. | **High** | **certora** | Two-function equivalence over an unbounded policy array. Quantification on `policies` is Certora territory. Halmos would need a bound on `policies.length` and even then the symbolic `op.signature` rewriting inside the UserOp path makes the SMT explode. | L |
+| 12 | `KernelFactory.deploy` is deterministic and idempotent: for any `(initialPackages, nonce)` the deployed address equals `getAddress(initialPackages, nonce)`, and a second call returns the same address without re-initializing (no double-init). Same for `deployECDSA`. | **Medium** | **halmos** | Pure salt derivation + LibClone semantics. The no-double-init claim is a state property over two consecutive calls. Both fit in a single Halmos file. | S |
+| 13 | `_checkAndIncrementNonce` cannot overflow `uint64` within a single transaction (the `++` is safe under Solidity's overflow check, given `_nonce` is provided externally). Equivalent: no input drives `nonce[key]` from below `type(uint64).max` to wrap. | **Medium** | **halmos** | Pure arithmetic bound; tiny SMT obligation. Practically unreachable but the spec-level claim deserves a proof for completeness. Pair with SMTChecker enabled in CI for defence-in-depth. | S |
+| 14 | `_initializeValidation`: both the empty-`_internalData` path and the non-empty path leave `vInfo[vId].nonce` at exactly `previous + 1`. Existing tests cover happy path; this is the "no-double-bump and no-zero-bump" invariant explicitly. | **Medium** | **halmos** | Single-call, single-storage-slot property. Halmos. | S |
+| 15 | ERC-1271 nested EIP-712 (`_erc1271IsValidSignatureViaNestedEIP712` and the Replayable variant) does not return success when the contents-hash reconstruction fails. The assembly path is intricate; only the explicit success branch should authorise. | **Medium** | **kontrol** | The function is heavy assembly with calldata manipulation. Halmos can run it but the SMT cost of symbolic-bytes calldata copies is high. Kontrol/KEVM reasons natively over the assembly. If Kontrol setup turns out too expensive for one property, demote to Halmos with a bounded signature length and mark the audit entry "partial". | L |
+
+### Properties intentionally NOT proposed (and why)
+
+- **`supportsExecutionMode` exhaustiveness for unsupported types** — already proven in `KernelExecutionModeHalmos.t.sol`.
+- **Validator-path hook bracketing** — only fallback and executor hook bracketing are covered today. Adding the validator-path version would be valuable but it's Medium severity at best and the bracketing logic is shared across paths; defer until the higher-severity items land.
+- **`isModuleInstalled` correctness for type 7+** — already proven via `check_DoesNotSupportModuleType7`.
+- **Mode dispatch / gas semantics** — out of scope for FV; handled by BTT + gas tests.
+- **Tama / Clear properties** — Kernel v4 is post-release with audits and a Foundry/Yul toolchain. The rewrite cost of Tama (Lean EDSL) and the Yul-extraction setup of Clear (which would also have to grapple with `via_ir = false`) is not justified for v4. Reserve Tama/Clear for a hypothetical v5 redesign or for the most critical greenfield primitive.
+
+## Backend Tally
+
+| Backend | Properties | Effort total |
+|---|---|---|
+| `sc-fv-halmos` | 2, 3, 5, 7, 8, 9, 10, 12, 13, 14 — **10 properties** | ~8-10 days |
+| `sc-fv-certora` | 1, 4, 6, 11 — **4 properties** | ~3-4 weeks incl. setup |
+| `sc-fv-kontrol` | 15 (preferred) — **1 property** | ~1 week incl. Kontrol setup |
+| `sc-fv-clear` | 0 | — |
+| `sc-fv-tama` | 0 | — |
+
+## Recommended Dispatch Order
+
+1. **Phase A — Halmos S-effort gaps in parallel**: #2, #3, #5, #8, #9, #10, #12, #13, #14. Most are file-disjoint so parallel-safe; collision risk only on `test/halmos/` itself which the per-property file naming convention already handles.
+2. **Phase B — Halmos M-effort**: #7 (`_checkNonce` ↔ `_checkAndIncrementNonce` consistency).
+3. **Phase C — Certora setup + first property**: #1. This is the single highest-value proof in the entire codebase; Certora setup pays for itself here.
+4. **Phase D — Certora deepening**: #4, #6, #11 once #1 has unblocked the Certora harness.
+5. **Phase E — Kontrol experiment**: #15. If Kontrol setup is too costly, demote to a Halmos partial.
+
+## Confidence After Full Plan Lands
+
+- Halmos-proven (Phase A + B): ~95 properties total (existing 85 + new 10).
+- Certora-proven: 4 critical multi-step / unbounded-data claims.
+- Kontrol-proven: 1 (or Halmos partial).
+- **Acknowledged unproven**: full ERC-1271 nested EIP-712 if Kontrol fails; gas semantics; cross-contract real-EntryPoint replay (handled by integration / fuzz tests, not FV).
+
+## Notes for the Subagents (when dispatched)
+
+- Halmos compatibility: v0.3.3, `check_*` / `invariant_*` prefix. Match the existing file's naming convention (mix of `check_X` and `checkX` is present — keep the file consistent internally).
+- Run `forge clean` before `halmos` since v0.3.3 occasionally produces artifacts without AST.
+- `vm.expectRevert(bytes4)` is not supported in Halmos. Use `try { ... assert(false); } catch {}` or low-level `(bool success,) = ...; assertFalse(success);`.
+- `foundry.toml` has `via_ir = false` for contract-size reasons. This rules out Clear (which reasons about Yul output) unless we accept a separate compile pipeline.
+- Specs live in `~/Documents/Obsidian/projects/kernel-v4/specs/` (when documentor has populated them — at the moment the source-level NatSpec is the de facto spec).
diff --git a/audit/fv-round-1-findings.md b/audit/fv-round-1-findings.md
new file mode 100644
index 00000000..028cabd0
--- /dev/null
+++ b/audit/fv-round-1-findings.md
@@ -0,0 +1,415 @@
+---
+date: 2026-05-20
+branch: audit/fv-round-1
+type: fv-findings
+status: in-progress
+---
+
+# Kernel v4 — FV Round 1 Findings
+
+Subagent results as they land. Each entry: property, status, file, notable observations, follow-ups.
+
+## Phase A — Halmos (in flight)
+
+### ✅ #2 — `Lib4337.intersectValidationData` aggregator precedence
+
+- **Status**: PROVEN (8/8 checks pass, 0.30s total wall time)
+- **File**: `test/halmos/Lib4337Halmos.t.sol`
+- **Checks**:
+ - `checkRule1_PreFailure` — preAgg==1 ⇒ result agg==1
+ - `checkRule1_ResFailure` — resAgg==1 ⇒ result agg==1
+ - `checkRule2_BothSuccess` — both 0 ⇒ result agg==0
+ - `checkRule3_PreserveAggregator` — **SECURITY CRITICAL** — preAgg>1 & resAgg==0 ⇒ result agg==preAgg
+ - `checkRule4_AdoptAggregator` — preAgg==0 & resAgg>1 ⇒ result agg==resAgg
+ - `checkRule5_SameAggregator` — preAgg==resAgg>1 ⇒ result agg==preAgg
+ - `checkRule6_ConflictingAggregators` — preAgg>1 & resAgg>1 & differ ⇒ result agg==1
+ - `checkAggregatorPreservedWhenResAgg0` — combined regression guard with fully symbolic words
+- **Notable observations**:
+ - The impl has an early-out (`if (preValidationData == 0 || validationRes == 0) return preValidationData | validationRes;`) not enumerated as a separate rule. Aggregator-only checks are insensitive to this branch.
+ - Agent masked out bit 47 of each uint48 time field (`CLEAR_MODE_BITS = ~((1<<255) | (1<<207))`) to avoid the orthogonal `ValidityFormatMismatch` revert path. Mask is symbolic, not a fixed concrete value.
+ - Source comment is ambiguous about whether `preAgg == resAgg == 0` belongs to rule 2 or rule 5. Impl reads rule 2 first; agent constrained rule 5 check to `agg > 1` to keep rules disjoint.
+- **Follow-up**: separate Halmos dispatch later to verify the `ValidityFormatMismatch` revert path itself (rejects malformed-format inputs).
+
+### ✅ #3 — `KernelUUPS.upgradeToAndCall` caller gating
+
+- **Status**: PROVEN (3/3 checks)
+- **File**: `test/halmos/KernelUUPSHalmos.t.sol`
+- **Worktree branch**: `worktree-agent-ae153a8b47bc09c98`
+- **Checks**:
+ - `checkUpgradeToAndCallRevertsForArbitraryCaller` — pass, 1 path
+ - `checkUpgradeToAndCallSucceedsForEntryPoint` — pass, 1 path
+ - `checkUpgradeToAndCallSucceedsForSelf` — pass, 2 paths
+- **Notable observations**:
+ - Solady's `UUPSUpgradeable` only exposes `upgradeToAndCall`; no `upgradeTo(address)` to cover separately.
+ - Allowlist is exactly `{ENTRYPOINT, address(this)}` via `_onlyEntryPointOrSelf` — no role registry, no module bypass.
+ - **Important harness note**: agent deployed a real ERC1967 proxy via `LibClone.deployERC1967(impl)` and called the proxy, NOT the implementation directly. The existing `KernelExecutorHalmos` pattern (`new KernelUUPS(...)`) would short-circuit on Solady's `onlyProxy` modifier (`UnauthorizedCallContext()`) and never reach the auth check. Future Halmos harnesses on upgrade paths must follow the proxy pattern.
+ - Agent ran a probe to confirm proofs aren't vacuous: forced `ok == false` for EntryPoint case and Halmos produced a counterexample.
+
+### 🚨 #5 — `_verifyStatelessSignature` moduleType filter — **BUG WITNESS** (fix already on `fix/audit-internal-batch-1`)
+
+- **Status**: COUNTEREXAMPLE on `master`/`audit/fv-round-1` @ `a836274` (pre-fix). PROVEN GREEN when commit `bfbef77` is applied.
+- **File**: `test/halmos/PermissionStatelessHalmos.t.sol`
+- **Worktree branch**: `worktree-agent-a79a0778c7f9061eb`
+- **Checks**:
+ - `checkSanitySinglePolicyAccepts` — positive control, passes (confirms harness wiring is correct)
+ - `checkSigIdxDoesNotAdvanceForModuleType1` — FAIL on master (VALIDATOR type sneaks in)
+ - `checkSigIdxDoesNotAdvanceForModuleType4` — FAIL on master (HOOK type sneaks in)
+ - `checkSigIdxDoesNotAdvanceForAnyNonPolicySignerType` — FAIL on master, symbolic counterexamples at wrongModuleType ∈ {1, 2, 3, 4}
+- **The bug**:
+ - At `src/core/ModuleManager.sol:339` (on master), the permission-branch signature loop accepts any package with `internalData[0:4] == pId` regardless of `moduleType`.
+ - A non-policy / non-signer module (VALIDATOR=1, EXECUTOR=2, FALLBACK=3, HOOK=4) whose `internalData[0:4]` happens to equal `pId` is consumed into the signature chain.
+- **Fix maps to**: `bfbef77 fix: filter permission stateless match by module type` (1 line: add `&& (pkg.moduleType == 5 || pkg.moduleType == 6)`).
+- **Notable observations from agent**:
+ - Calldata-layout gotcha: `abi.encode(struct)` wraps in a 1-tuple with an outer offset that the source's inline assembly `permissionSig := signature.offset` doesn't expect. Agent encoded `abi.encode(sigs)` (inner `bytes[]` directly). Without this fix the harness reverts vacuously — positive-control test exists to catch regression.
+ - `packages.length = 2` was the minimum needed: length 1 cases are vacuously rejected by the existing "last signature is signer" require.
+
+## Branch divergence summary
+
+**Master is missing two fixes that already exist on `fix/audit-internal-batch-1`**:
+
+| Bug | Fix commit | Date | Status on master |
+|-----|-----------|------|-------------------|
+| `_initializeValidation` empty-data path doesn't bump nonce → stale selector grants survive uninstall+empty-reinstall | `9f9471c` | 2026-04-29 | **NOT MERGED** |
+| `_verifyStatelessSignature` accepts non-policy/non-signer modules into signature chain | `bfbef77` | 2026-04-29 | **NOT MERGED** |
+
+Both fixes (plus 3 other audit fixes: `bccbb5d`, `5a6c865`, `d54c56a`) are sitting on `fix/audit-internal-batch-1`, which is also unmerged.
+
+The Halmos tests we just authored act as **regression witnesses** — they would have caught these bugs pre-fix and will pin the fix in place post-merge.
+
+### ✅ #8 — `parseNonce` round-trip
+
+- **Status**: PROVEN (2/2 checks, 0.01s)
+- **File**: `test/halmos/ParseNonceHalmos.t.sol`
+- **Worktree branch**: `worktree-agent-a2e3e14e9362e728a`
+- **Checks**:
+ - `checkParseNonceRoundTripValidator` — pass, 1 path
+ - `checkParseNonceRoundTripPermission` — pass, 1 path
+- **Notable observations**:
+ - `checkParseNonceRejectsInvalidVType` was NOT authored — the function has no revert branch. The `else` clause accepts every `vType ≠ 0x02` including `0x00 (ROOT)`, `0x01 (VALIDATOR)`, and junk. Caller-side enforcement lives at `ValidationManager._validateValidationData:339-340`. Re-dispatch the rejection check there in Phase B.
+ - `vType` byte is doubly encoded — it's at byte[1] AND high byte of `vId`. After parsing, `vType == vId[0]` is an invariant. Source comment in `Utils.sol:42-44` is slightly misleading.
+ - The 16 zero bytes between `pId` and `nonceKey` in the permission encoding are mandatory; non-zero values there are silently dropped.
+ - Negative control verified — agent flipped expected type byte to 0x02 in validator check and Halmos correctly produced a counterexample.
+
+### ✅ #9 — `Kernel7702` + `KernelImmutableECDSA` fallback ECDSA
+
+- **Status**: PROVEN (2/2 checks, 0.08s)
+- **File**: `test/halmos/FallbackSignatureHalmos.t.sol`
+- **Worktree branch**: `worktree-agent-aa60b59a740a18832`
+- **Checks**:
+ - `checkKernel7702FallbackAcceptsIffExpectedSigner` — pass, 5 paths
+ - `checkKernelImmutableECDSAFallbackAcceptsIffExpectedSigner` — pass, 5 paths
+- **Notable observations**:
+ - Agent needed `--default-bytes-lengths 0,64,65,66,128` to enumerate both ECDSA length classes (64 EIP-2098 + 65 standard) plus the `default { break }` fall-through. Halmos's default `[0, 65, 1024]` would skip length 64.
+ - Required `--function check` to match the project's no-underscore prefix convention.
+ - Both proofs are tight; iff is checked bit-for-bit over fully symbolic `(hash, sig)`. No vm.assume.
+
+### ✅ #10 — `Staker.approveFactoryWithSignature` replay safety
+
+- **Status**: PROVEN (3/3 checks, 0.28s)
+- **File**: `test/halmos/StakerReplayHalmos.t.sol`
+- **Worktree branch**: `worktree-agent-a8edd42254b6d4aad`
+- **Checks**:
+ - `checkApproveFactoryWithSignatureBumpsNonce` — nonce += 1 on success
+ - `checkApproveFactoryWithSignatureReplayDigestDiffers` — bumped nonce flows into next digest, so replay produces a different digest
+ - `checkApproveFactoryWithSignatureDigestChainIdIndependent` — `digest(chainA) == digest(chainB)`, confirms `_hashTypedDataSansChainId` is in use
+- **Notable observations**:
+ - Halmos cannot directly prove "second call reverts" because ECDSA is modeled as an uninterpreted function — solver can pick recovered addresses such that both digests recover to `owner()`. So the property decomposes into (a) digest differs + nonce advances (proven by Halmos), and (b) one signature validates only one digest (ECDSA collision-resistance, outside Halmos). Standard decomposition.
+ - Chain-id-independence: 2 paths, structurally proves the digest assembly doesn't read `chainid()`.
+ - Signature symbolised at 65 bytes; storage seeded via `vm.store` for symbolic starting nonce.
+
+### ✅ #12 — `KernelFactory.deploy` determinism + no double-init
+
+- **Status**: PROVEN (4/4 checks, 0.15s)
+- **File**: `test/halmos/KernelFactoryHalmos.t.sol`
+- **Worktree branch**: `worktree-agent-a34511133d8e83c9c`
+- **Checks**:
+ - `checkDeployMatchesGetAddress(uint256 nonce)` — UUPS variant, deterministic
+ - `checkSecondDeployReturnsSameAddressNoReinit(uint256 nonce)` — UUPS variant, idempotent
+ - `checkDeployECDSAMatchesGetECDSAAddress(address signer, uint256 nonce)` — ECDSA, deterministic
+ - `checkSecondDeployECDSAReturnsSameAddressNoReinit(address signer, uint256 nonce)` — ECDSA, idempotent
+- **Notable observations**:
+ - `initialPackages` constrained to `length=1, type-1 root validator` — CREATE2 salt is independent of package contents once hashed, so this doesn't weaken the property.
+ - The no-double-init claim is an INDIRECT proof: factory branches on `alreadyDeployed` from `LibClone.createDeterministicERC1967` and skips `initialize`; Solady's `initializer` modifier would revert on a second init; Halmos proves the second deploy doesn't revert → therefore no re-init path exists.
+ - For a direct proof, would need harness access to `Initializable._INITIALIZED_SLOT`. Current formulation is the tightest indirect proof.
+
+### ✅ #13 — `_checkAndIncrementNonce` no overflow
+
+- **Status**: PROVEN (1/1 check, 0.05s, 6 paths)
+- **File**: `test/halmos/NonceOverflowHalmos.t.sol`
+- **Worktree branch**: `worktree-agent-a54da47d4c4adf039`
+- **Notable observations**:
+ - Postcondition computed in `uint256` so any uint64 wrap manifests as `LHS=0, RHS=2^64` counterexample.
+ - Fully symbolic over `uint64 × uint64 × uint64 × uint192`. No vm.assume.
+ - Agent confirmed by grep: no `unchecked` blocks touch `nonce[key]` anywhere in `src/Kernel.sol`, `src/core/ModuleManager.sol`, `src/core/ValidationManager.sol`. The only `unchecked` blocks are in unrelated loops.
+ - Function location: `src/core/ModuleManager.sol:268`.
+
+### 🚨 #14 — `_initializeValidation` bumps by 1 — **BUG FOUND**
+
+- **Status**: SPLIT — empty-data path is a COUNTEREXAMPLE; non-empty path PROVEN
+- **File**: `test/halmos/InitializeValidationHalmos.t.sol`
+- **Worktree branch**: `worktree-agent-af9720c11ddd2ab96`
+- **Checks**:
+ - `checkInitializeValidationBumpsByOneEmptyData` — **COUNTEREXAMPLE** (impl bug)
+ - `checkInitializeValidationBumpsByOneNonEmptyData` — pass, 3 paths, 0.05s
+- **The bug**:
+ - `_initializeValidation` (`src/core/ValidationManager.sol:85-100`): empty `_internalData` path (lines 89-92) sets `hook = address(1)` and returns. **No nonce bump.**
+ - `_uninstallValidation` (`src/core/ValidationManager.sol:139-143`): zeroes `hook`. **Leaves `nonce` and `allowed[vId][*]` intact.**
+ - Attack sequence: `install(vId, "hook||selectors")` → `uninstall(vId)` → `install(vId, "")` resurrects stale `allowed[vId][selector] == nonce` grants from the prior install. Old selectors come back to life with the empty reinstall.
+- **Severity assessment**: HIGH. Reachable only via owner-gated `installModule` (EP-or-self), so requires owner cooperation. Impact: footgun + privilege smuggling — owner thinks empty-data reinstall = clean slate, but historical selector grants persist. Worse if the same `vId` is reused with different intent across installs.
+- **Recommended fix**: at `src/core/ValidationManager.sol:89-92`, either (a) bump `++nonce` unconditionally before the early return, or (b) clear `allowed[vId][*]` entries on uninstall. Option (a) is the minimal patch and matches the property's expectation.
+- **Caveats noted by agent**:
+ - Required `vm.assume(preNonce < type(uint32).max)` to avoid orthogonal overflow concerns (separate property #13). Not a weakening.
+ - Non-empty path bound `_internalData.length=24` (20-byte hook + 4 selectors). Structural shape is general; selector count doesn't affect the nonce bump.
+ - `_internalData.length == 20` edge case (hook only, zero selectors) verified by inspection — single bump via `_grantAccess` with empty selectors. Agent suggests a third check could cover symbolically.
+
+## Phase B — Halmos M-effort
+
+### ✅ #7 — `_checkNonce` ↔ `_checkAndIncrementNonce` agreement below saturation
+
+- **Status**: PROVEN (3/3 checks, 0.26s)
+- **File**: `test/halmos/NonceConsistencyHalmos.t.sol`
+- **Checks**:
+ - `check_RatchetBranchAgreement` — view/write agree on `nonceValidFrom > preSeq` branch
+ - `check_NonRatchetBranchAgreement` — view/write agree on `nonceValidFrom ≤ preSeq` branch
+ - `check_AgreementBelowOverflowSaturation` — general agreement, both branches combined
+- **Boundary finding**: at `effectivePre == type(uint64).max`, the view path accepts (`seq == effective`) while the write path reverts from the checked `nonce[key]++` overflow. This is the ONLY divergence across the entire `(key, preSeq, validFrom, seq)` state space.
+- **Why this is acceptable**: `NonceOverflowHalmos.check_NonceCannotOverflow` proves `nonce[key]` cannot reach `type(uint64).max` organically. The only way to land there is owner-induced via `_setValidNonceFrom(type(uint64).max)` — owner self-DOS, detectable on-chain.
+- **Each check excludes the boundary with an explicit, documented `vm.assume`** — not a silent weakening. Cross-references `NonceOverflowHalmos` inline.
+- **Alternative considered**: apply a one-line fix to `_checkNonce` (add `require(effective < type(uint64).max)`) to make the agreement unconditional. Deferred — current behaviour is provably safe via the cross-property argument, and changing source for a vacuous edge case requires sc-developer dispatch + reaudit.
+
+## Phase C — Certora
+
+### 🚨 #1 — `executeUserOp` ↔ `validateUserOp` linkage — **HIGH severity bug found**
+
+- **Status**: split — strict form PROVEN; naive form COUNTEREXAMPLE surfaces a real privilege-escalation bug.
+- **Files**:
+ - `certora/conf/Kernel.conf`
+ - `certora/specs/Kernel.spec` (3 rules)
+ - `certora/harnesses/KernelHarness.sol`
+- **Certora job reports**:
+ - All 3 rules: https://prover.certora.com/output/3606101/9bae8478ce9842bcae2d45f92487e40b?anonymousKey=0f69fd410a6d5eb1218d0931ebae1e5e8161b63d
+ - Strict-only PASS: https://prover.certora.com/output/3606101/fa191e6ffa3e43f6aac8860d357737f4?anonymousKey=d6261fb0d8c99d0dfba76de0a402448046b24332
+- **Wall time**: 7.7 min, prover 472s.
+
+#### Rule results
+
+| Rule | Status | Notes |
+|---|---|---|
+| `validateUserOpEnforcesInnerSelectorAccess_naive` | **FAIL** | CEX exposes the fast-path bypass |
+| `validateUserOpEnforcesInnerSelectorAccess_strict` | **PASS** | Holds with `!fastPath` precondition |
+| `sanityValidateUserOpReachesSuccess` (satisfy) | **PASS** | Rule setup is not vacuous |
+
+#### The bug
+
+`src/Kernel.sol:172-185` — `_processUserOp`'s fast-path:
+
+```solidity
+if (
+ vType == VALIDATION_TYPE_ROOT
+ || (_allowedSelector(vId, bytes4(userOp.callData[0:4]))
+ && $.vInfo[vId].hook == HOOK_MODULE_INSTALLED_NO_HOOK)
+) {
+ // No-op — fast path, NO inner-selector check, NO _setValidationHook
+} else { ... require + _setValidationHook ... }
+```
+
+When a non-ROOT validation `V` has `executeUserOp.selector` in its allowed list AND `hook == HOOK_MODULE_INSTALLED_NO_HOOK`:
+
+1. Fast-path is taken.
+2. Inner-selector `require` is skipped — no check on `userOp.callData[4:]`.
+3. `_setValidationHook` is NOT called → transient hook stays 0.
+4. `executeUserOp` then runs `_preHook`/`_postHook` as no-ops (hook is 0).
+5. Inner `delegatecall` to `address(this)` executes ANY selector — `installModule`, `setRoot`, `upgradeToAndCall`, etc.
+
+#### Severity
+
+**HIGH**. Exploitability gate is configuration — `_grantAccess` accepts any selector list, including `executeUserOp.selector`. An owner configuring a validation with what they think is "scoped access to executeUserOp" actually grants root-level dispatch.
+
+#### Concrete counterexample from Certora
+
+- `op.callData.length == 8`
+- `bytes4(op.callData[0:4]) == 0x8dd7712f` (`executeUserOp.selector`)
+- `bytes4(op.callData[4:8]) == 0x3751` (arbitrary unauthorised selector, symbolic)
+- `vId == 0xffffffffff00000000000000000000000000000001` (PERMISSION type)
+- `_allowedSelector(vId, executeUserOp.selector) == true`
+- `vInfo[vId].hook == HOOK_MODULE_INSTALLED_NO_HOOK`
+- `vMode` bits 0x08 / 0x40 both off — finding is independent of enable-mode and replayable-mode
+
+#### Fix path (selected: Option 1)
+
+Block `executeUserOp.selector` from being granted to non-ROOT vIds in `ValidationManager._grantAccess`:
+
+```solidity
+require(
+ selector != IKernel.executeUserOp.selector || vId == $.root,
+ InvalidSelectorGrant()
+);
+```
+
+Defense-in-depth at the configuration boundary. Will be dispatched to `sc-developer`.
+
+#### Caveats / narrowings (documented in spec header)
+
+- Strict rule excludes `vMode & 0x08` (enable mode) and `vMode & 0x40` (replayable) for Certora tractability. Both invoke unbounded-bytes hashing (`_verifyInstallSignatureRaw`, `Lib4337.chainAgnosticUserOpHash`). Fast-path bypass is independent of these modes.
+- Internal validators (`_validateUserOpValidator/Permission/Fallback`) and `Lib4337.intersectValidationData` are NONDET-summarised to fit in Certora's memory budget. Sound because the fast-path branch reaches the require BEFORE these are invoked.
+- External module callbacks are AUTO-HAVOC'd. Sound because `_onlyEntryPointOrSelf` prevents reentrant ValidationStorage writes.
+- `optimistic_hashing: true`, `hashing_length_bound: 512` documented in `certora/conf/Kernel.conf`.
+
+## Phase C Round 2 — re-verify after `_grantAccess` fix
+
+### ✅ Original bug closed
+
+After commit `0921b25` (`_grantAccess` blocks `executeUserOp.selector` for non-root vIds):
+
+| Rule | Round 1 | Round 2 |
+|---|---|---|
+| `validateUserOpEnforcesInnerSelectorAccess_naive` | 🚨 FAIL (CEX) | ✅ **PASS** |
+| `validateUserOpEnforcesInnerSelectorAccess_strict` | ✅ PASS | ✅ PASS (regression) |
+| `sanityValidateUserOpReachesSuccess` | ✅ PASS | ✅ PASS (regression) |
+
+Round 2 job: https://prover.certora.com/output/3606101/19ed688fd26e43cfa25d435306bec6f1?anonymousKey=a87fff01a79ea67c696ced6eb56bd0dbae8403e7
+
+### 🚨 Secondary finding — `setRoot` residual
+
+New invariant `nonRootCannotAllowExecuteUserOp` FAILS on 8 entry points. All reduce to a single primitive: **`_setRoot` does not bump `vInfo[oldRoot].nonce`**, so prior grants of `executeUserOp.selector` to the old root remain active when the old root becomes non-root.
+
+Failing entry points (induction step) and how each reaches `_setRoot`:
+
+- `setRoot(bytes21)` — direct
+- `setRoot((uint256,address,bytes,…))` overload — direct
+- `initialize((uint256,address,…))` — root install path
+- `executeUserOp(...)` — inner delegatecall to `setRoot`
+- `execute(bytes32,bytes)` — routed batch / single call
+- `executeFromExecutor(...)` — executor module calls `setRoot`
+- `upgradeToAndCall(...)` — new impl's init data calls `setRoot`
+- `()` — fallback path
+
+Attack sequence (after the `_grantAccess` fix):
+
+1. `setRoot(R1)` → `$.root = R1`
+2. `_grantAccess(R1, executeUserOp.selector)` — permitted (R1 is currently root)
+3. `setRoot(R2)` → `$.root = R2`; `allowed[R1][executeUserOp]` stays non-zero; `vInfo[R1].hook` preserved
+4. R1 is now non-root with `_allowedSelector(R1, executeUserOp.selector) == true` and `hook == HOOK_MODULE_INSTALLED_NO_HOOK`
+5. Fast-path bypass re-engages — R1 can call `executeUserOp(arbitrary inner calldata)` and invoke any privileged function
+
+Lower likelihood than the Round 1 attack (requires root rotation + prior grant + hook preserved) but FV demonstrates structural reachability.
+
+### Selected remediation — Option E
+
+Bump `vInfo[oldRoot].nonce` in `_setRoot` so any stale `allowed[oldRoot][*]` grants are invalidated (`allowed[oldRoot][sel] != vInfo[oldRoot].nonce` post-rotation). Same pattern as Phase A #14.
+
+### ✅ Phase C closed — Round 3 / 4 invariant abstraction limit
+
+After `_setRoot` fix (`ce185f6`) we tried two stronger invariant forms:
+
+| Round | Form | Outcome |
+|---|---|---|
+| 3 | `allowedNonce(vId, exec) != vInfoNonce(vId)` | FAIL — base case fails on uninstalled vIds (`0 != 0` is false). |
+| 4 | Bypass-impossible: `NOT (_allowedSelector AND hook == INSTALLED_NO_HOOK)` | FAIL — Certora's external-callback AUTO-HAVOC violates the invariant on every entry point with a delegatecall (`executeUserOp`, `execute`, `validateUserOp`, `installModule`, `setRoot`, `grantAccess`, `upgradeToAndCall`, ``, `initialize`). `_onlyEntryPointOrSelf` prevents this in production, but encoding precise CVL summaries for all ~10 callback sites is days of work and likely OOMs. |
+
+Round 4 job: https://prover.certora.com/output/3606101/e16f05be609a48b79c6bfa16f7c357f4?anonymousKey=39f0672f112513c790ec1d6d8ba351876073e395
+
+**Decision (2026-05-21)**: accept the invariant as unprovable under current summaries. Phase C closes with the audit story carried by:
+
+1. `validateUserOpEnforcesInnerSelectorAccess_naive` PASSES post-fix — original CEX unreachable.
+2. `validateUserOpEnforcesInnerSelectorAccess_strict` PASSES — precise property under `!fastPath`.
+3. Manual static-writer analysis: `_grantAccess` (with fix), `_setRoot` (with fix), `_uninstallValidation`, `_initializeValidation` are the only writers of relevant storage; each preserves the bypass-impossible property by inspection.
+
+Invariant retained in spec as documented intent + regression target.
+
+## Phase D — Certora deepening
+
+### ✅ #6 — `setRoot` LIFO clear of permission state
+
+- **Status**: PROVEN (1 rule + 1 satisfy)
+- **File**: `certora/specs/SetRootLifo.spec`, `certora/conf/SetRootLifo.conf`
+- **Rules**:
+ - `setRootClearsOldPermissionState` — after `setRoot(packages, removeCurrent=true)` on a permission-type root: `policies.length == 0`, `signer == 0`, `hook == NOT_INSTALLED`
+ - `sanitySetRootReaches` (satisfy) — non-vacuous
+- **Job**: https://prover.certora.com/output/3606101/7e3f99aaf47a4257a372d14ce591dea6
+- **Bound**: `policies.length <= 3` to match `loop_iter: 3`; soundly extends to longer arrays by induction on intersect's monotonicity.
+- **Static observations** noted by subagent (not bugs, context):
+ - `_install` runs BEFORE the LIFO loop snapshot; if `pkg[0]` is a policy/signer that matches the old root's pId, it pushes into `policies[]` before the loop runs. Caller must pad `uninstallData` accordingly or the call reverts (sound — no skip).
+ - `_uninstallPolicyWithVid` uses `policies.pop()`, which Solidity clears correctly. No residue.
+ - `_uninstallSignerWithVid` requires `policies.length == 0` THEN zeros signer + calls `_uninstallValidation` which zeros hook. Sequence matches the property.
+ - Aliasing case `pkg[0].moduleType ∈ {policy, signer} && completes oldRoot's pId`: `_setRoot` becomes a no-op rotation, `removeCurrent` block hits `CannotUninstallRoot` → safe revert.
+
+### 🟡 #4 — Permission validation totality (3/4 rules PASS)
+
+- **Status**: SECURITY DIRECTION PROVEN, LIVENESS DIRECTION DROPPED
+- **File**: `certora/specs/Permission.spec`, `certora/conf/Permission.conf`
+- **Rules**:
+ - `policyFailureImpliesAggregateFailure` — ✅ PASS — any policy returning failure forces aggregate failure
+ - `signerFailureImpliesAggregateFailure` — ✅ PASS — signer returning failure forces aggregate failure
+ - `sanityCanSucceed` (satisfy) — ✅ PASS — non-vacuous
+ - `allSuccessImpliesAggregateSuccess` — **DROPPED** (CVL artifact, see below)
+- **Why dropping `allSuccess` is OK**:
+ - The audit's core claim is the security direction: "no policy can be silently skipped". The two failure rules establish this directly: any failing module forces aggregate failure, so the only way for the aggregate to succeed is for EVERY module to have succeeded.
+ - The dropped rule's direction is liveness ("if every module succeeds, aggregate succeeds") — important operationally but not a security claim.
+ - Liveness is empirically established by the 1341 passing Foundry tests, many of which exercise permission UserOps with successful modules → successful aggregate.
+- **Why we couldn't prove `allSuccess` in CVL**:
+ - Three formulations attempted (forall+mask, enumerated, implication-form) — all tripped Certora's `rule_sanity` "bounds check on int to bitvec" sub-check.
+ - This is a CVL-internal type-checker artifact, not a contract bug. The check fires BEFORE the assertion is evaluated; it concerns the satisfiability of the rule's preconditions when `forall address` meets bitwise masks.
+ - Documented in `specs/Permission.spec` as a regression target for future CVL releases.
+
+### ✅ #11 — View/write permission path equivalence on success/failure
+
+- **Status**: PROVEN (1 rule + 1 satisfy)
+- **File**: `certora/specs/PermissionEquivalence.spec`, `certora/conf/PermissionEquivalence.conf`
+- **Rules**:
+ - `viewAndWritePathsAgreeOnSuccess` — view (ERC-1271) and write (ERC-4337) paths agree on the binary success/failure outcome for the same `(vId, hash, signature)` tuple
+ - `sanityViewPathReaches` (satisfy) — non-vacuous
+- **Job (final)**: https://prover.certora.com/output/3606101/22e774d8687e4b869ece01503dc66aa8
+- **Spec evolution** (rounds 1–4):
+ 1. Full `uint256` equality — FAIL by design (view's `bytes4`-lift can't encode time bounds)
+ 2. Binary outcome with `signerGhostUint == 0 <=> bytes4 == MAGIC` axiom — FAIL (axiom too narrow; ignored aggregator bits)
+ 3. Tightened axiom + iff on `intersectGhost` — FAIL (signer ghost still had arbitrary upper bits)
+ 4. Single source-of-truth `signerSucceedsGhost` boolean with CVL helpers deriving both ABI returns — **PASS**
+- **Important reframing**: the audit's claim "the two paths must not diverge in authorisation" was originally stated as full `validationData` equality. The correct formulation is the binary success/failure agreement — by design, the view path (ERC-1271 `bytes4`) cannot express time bounds that the write path (ERC-4337 `uint256`) carries.
+
+## Phase E — Kontrol + Halmos (complementary partial coverage on #15)
+
+### Property #15 — ERC-1271 nested EIP-712 success-branch-only authorisation
+
+**Goal**: prove that `_erc1271IsValidSignatureViaNestedEIP712` (and the Replayable variant) in `src/lib/ERC1271.sol` only return `true` when the inner `_erc1271IsValidSignatureNowCalldata(hash, signature)` returns `true`. Both functions have exactly one return site (line 239 / 326), so a contrapositive proof "inner=false ⇒ outer=false" covers all paths.
+
+### 🟡 Kontrol partial — TypedDataSign branch (timed out, no CEX)
+
+- **Status**: 14 terminal SUCCESS branches + 12 subsumption covers in 102-node KCFG, NO counterexamples, full proof timed out at ~1h25m
+- **File**: `test/kontrol/ERC1271NestedEIP712Kontrol.t.sol`
+- **Config**: `kontrol.toml` (max-depth 5000, max-iter 200, workers 4)
+- **Build wall time**: 73 s cold, ~50 s warm
+- **Prove wall time at kill**: ~1h25m
+- **Bound applied**: `vm.assume(signature.length <