Certora specs

.gitignore

@@ -27,6 +27,7 @@ broadcast
 # Certora Outputs
 .certora_internal/
 .certora_recent_jobs.json
+emv*certora*/*
 
 #script config file
 # script/M1_deploy.config.json
@@ -44,4 +45,4 @@ test.sh
 InheritanceGraph.png
 surya_report.md
 
-.idea
+.idea

certora/confs/beaconChainProofs.conf

@@ -0,0 +1,54 @@
+
+
+{
+    //"assert_autofinder_success": true,
+    "files": [ 
+        "src/test/utils/BeaconChainProofsWrapper.sol",
+        "src/contracts/libraries/BeaconChainProofs.sol",
+    ],
+    "link": [
+    ],
+    "struct_link": [
+
+    ],
+    //"java_args": [ " -ea -Dlevel.setup.helpers=info" ],
+
+    "hashing_length_bound": "320",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "solc": "solc8.12",
+    "solc_optimize": "200",
+    "cache": "false",
+    "solc_via_ir": false,
+    "server": "production",
+    "prover_version": "master",
+    "packages": [
+    ],
+    //"process": "emv",
+    "smt_timeout": "6000",
+    //"auto_nondet_difficult_internal_funcs": true, 
+    "prover_args": [
+        //"-maxBlockCount 130000",  //if running with high loop iter
+        //"-verifyCache true",
+        //"-verifyTACDumps true",
+        //"-testMode true",
+        //"-checkRuleDigest true",
+        //"-callTraceHardFail on",
+        //"-recursionEntryLimit 3",
+        "-enableCopyLoopRewrites true", 
+        //"-summaryResolutionMode tiered", 
+        //"-enableEqualityReasoning true",
+        //"-mediumTimeout 5",
+        //"-depth 0",
+		//"-smt_initialSplitDepth 3",
+		//"-s [z3:lia1,yices:def]",
+		//"-splitParallel true",
+		//"-splitParallelInitialDepth 6",
+		//"-splitParallelTimelimit 7200",
+    ],
+    "loop_iter": "24",
+
+    "verify": "BeaconChainProofsWrapper:certora/specs/libraries/BeaconChainProofs.spec",
+
+    "msg": "BeaconChainProofs",
+}

certora/confs/endian.conf

@@ -0,0 +1,69 @@
+{
+    //"assert_autofinder_success": true,
+    "files": [ 
+        "certora/harnesses/EndianCaller.sol",
+        "src/contracts/libraries/Endian.sol",
+    ],
+    "link": [
+    ],
+    "struct_link": [
+
+    ],
+    //"java_args": [ " -ea -Dlevel.setup.helpers=info" ],
+
+    "hashing_length_bound": "320",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "solc": "solc8.12",
+    "solc_optimize": "200",
+    "cache": "false",
+    "solc_via_ir": false,
+    "server": "production",
+    //"server": "staging",  // switch to staging when running mutations
+    "prover_version": "master",
+    "packages": [
+    ],
+    //"process": "emv",
+    "smt_timeout": "6000",
+    //"auto_nondet_difficult_internal_funcs": true, 
+    "prover_args": [
+        //"-maxBlockCount 130000",  //if running with loop iter >=32
+        //"-verifyCache true",
+        //"-verifyTACDumps true",
+        //"-testMode true",
+        //"-checkRuleDigest true",
+        //"-callTraceHardFail on",
+        //"-recursionEntryLimit 3",
+        //"-enableCopyLoopRewrites true", 
+        //"-summaryResolutionMode tiered", 
+        //"-enableEqualityReasoning true",
+        //"-mediumTimeout 5",
+        //"-depth 0",
+		//"-smt_initialSplitDepth 3",
+		//"-s [z3:lia1,yices:def]",
+		//"-splitParallel true",
+		//"-splitParallelInitialDepth 6",
+		//"-splitParallelTimelimit 7200",
+        "-useBitVectorTheory true", 
+        //"-allowSolidityCallsInQuantifiers true", //needed for fromLittleEndianUint64_isSurjective 
+        //"-smt_groundQuantifiers false",          //needed for fromLittleEndianUint64_isSurjective 
+    ],
+    //"disable_local_typechecking": true,   //needed for fromLittleEndianUint64_isSurjective 
+    "loop_iter": "4",
+    "verify": "EndianCaller:certora/specs/libraries/Endian.spec",
+
+    "rule": [ "fromLittleEndianUint64_correctness" ],
+    //"rule": [ "transformationsAreInverse1", "transformationsAreInverse2", ],
+    "msg": "Endian inverse 4",
+
+    "mutations": {
+        "manual_mutants": [
+            {
+                "file_to_mutate": "src/contracts/libraries/Endian.sol",
+                "mutants_location": "certora/mutations/Edian"
+            }
+            ]
+    }
+}
+
+

certora/confs/full.conf

@@ -0,0 +1,124 @@
+{
+    //"assert_autofinder_success": true,
+    "files": [
+        "certora/harnesses/StrategyManagerHarness.sol",
+        "certora/harnesses/EigenPodManagerHarness.sol",
+        "certora/harnesses/DummyEigenPodA.sol",
+        "certora/harnesses/DummyEigenPodB.sol",
+        "certora/harnesses/ERC20Like/DummyERC20A.sol",
+        "certora/harnesses/ERC20Like/DummyERC20B.sol",
+        "certora/harnesses/DelegationManagerHarness.sol",
+        //"certora/harnesses/SlasherHarness.sol",
+        "src/contracts/strategies/EigenStrategy.sol",
+        //"certora/harnesses/PausableHarness.sol",
+        "src/contracts/permissions/Pausable.sol",
+        "src/test/mocks/ETHDepositMock.sol:ETHPOSDepositMock",
+        "lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol",
+        "src/contracts/permissions/PauserRegistry.sol",
+    ],
+    "link": [
+        "EigenPodManagerHarness:delegationManager=DelegationManagerHarness",
+        //"EigenPodManagerHarness:pauserRegistry=PauserRegistry",
+        //"SlasherHarness:_delegation=DelegationManagerHarness",
+        "DelegationManagerHarness:pauserRegistry=PauserRegistry",
+        "DelegationManagerHarness:eigenPodManager=EigenPodManagerHarness",
+        "DelegationManagerHarness:strategyManager=StrategyManagerHarness",
+        //"PausableHarness:pauserRegistry=PauserRegistry",
+        //"EigenPodManagerHarness:beaconChainOracle=TODO",
+        "EigenStrategy:underlyingToken=DummyERC20A",
+        //"EigenStrategy:EIGEN=TODO",
+        //"StrategyManagerHarness:pauserRegistry=PauserRegistry",
+
+        "StrategyManagerHarness:delegation=DelegationManagerHarness",
+        "StrategyManagerHarness:eigenPodManager=EigenPodManagerHarness",
+        "DummyEigenPodA:ethPOS=ETHPOSDepositMock",
+        "DummyEigenPodA:eigenPodManager=EigenPodManagerHarness",
+        "DummyEigenPodB:ethPOS=ETHPOSDepositMock",
+        "DummyEigenPodB:eigenPodManager=EigenPodManagerHarness",
+
+    ],
+    "struct_link": [
+        "DelegationManagerHarness:delegationApprover=ERC1271WalletMock",
+
+    ],
+    //"java_args": [ " -ea -Dlevel.setup.helpers=info" ],
+
+    "loop_iter": "3",
+    "hashing_length_bound": "3200",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "solc": "solc8.12",
+    "solc_optimize": "200",
+    "cache": "false",
+    "solc_via_ir": false,
+    "server": "production",
+    //"server": "staging",  // switch to staging when running mutations
+    "prover_version": "master",
+    "packages": [
+        "@commitlint/cli=node_modules/@commitlint/cli",
+        "@commitlint/config-conventional=node_modules/@commitlint/config-conventional",
+        "@types/yargs=node_modules/@types",
+        "chalk=node_modules/chalk",
+        "dotenv=node_modules/dotenv",
+        "fs=node_modules/fs",
+        "hardhat=node_modules/hardhat",
+        "hardhat-preprocessor=node_modules/hardhat-preprocessor",
+        "husky=node_modules/husky",
+        "ts-node=node_modules/ts-node",
+        "typescript=node_modules/typescript",
+        "yargs=node_modules/yargs",
+        "@openzeppelin-upgrades/=lib/openzeppelin-contracts-upgradeable",
+        "@openzeppelin/=lib/openzeppelin-contracts",
+        "@openzeppelin-v4.9.0/=lib/openzeppelin-contracts-v4.9.0",
+        "@openzeppelin-upgrades-v4.9.0/=lib/openzeppelin-contracts-upgradeable-v4.9.0",
+        "ds-test/=lib/ds-test/src",
+        "forge-std/=lib/forge-std/src"
+    ],
+    "rule_sanity": "basic",
+    //"process": "emv",
+    "smt_timeout": "6000",
+    //"auto_nondet_difficult_internal_funcs": true, 
+    "prover_args": [
+        //"-verifyCache true",
+        //"-verifyTACDumps true",
+        //"-testMode true",
+        //"-checkRuleDigest true",
+        //"-callTraceHardFail on",
+        "-recursionEntryLimit 3",
+        "-enableCopyLoopRewrites true", 
+        //"-summaryResolutionMode tiered", 
+        //"-enableEqualityReasoning true",
+        //"-mediumTimeout 5",
+        //"-depth 0",
+		//"-smt_initialSplitDepth 3",
+		//"-s [z3:lia1,yices:def]",
+		//"-splitParallel true",
+		//"-splitParallelInitialDepth 6",
+		//"-splitParallelTimelimit 7200",
+        "-useBitVectorTheory true", 
+    ],
+    //"coverage_info": "advanced",    //for unsat cores
+    "build_cache": true,  //to speed up if there were no changes in .sol files
+    "parametric_contracts": ["DummyEigenPodA", "DummyEigenPodB", "EigenPodManagerHarness", ],
+
+    //"verify": "PausableHarness:certora/specs/permissions/Pausable.spec",
+    //"verify": "DummyEigenPodA:certora/specs/pods/EigenPod.spec",
+    //"verify": "DummyEigenPodA:certora/specs/pods/EigenPodHooks.spec",
+    "verify": "EigenPodManagerHarness:certora/specs/pods/EigenPodManager.spec",
+    //"verify": "EigenPodManagerHarness:certora/specs/globalRules.spec",
+
+    //"exclude_rule": [ "methodsOnlyChangeOneValidatorStatus", "activeValidatorsCount_correctness"],
+    "rule": [ "methodsDontAlwaysRevert",  ],
+    //"rule": [ "verifyWithdrawalCredentials_alwaysReverts", ],
+
+    "msg": "methodsAlwaysRevert OL LI3, HB320, OH UC",
+
+    "mutations": {
+        "manual_mutants": [
+            {
+                "file_to_mutate": "src/contracts/pods/EigenPod.sol",
+                "mutants_location": "certora/mutations/EigenPodTest"
+            }
+            ]
+    }
+}

certora/confs/merkle.conf

@@ -0,0 +1,66 @@
+{
+    //"assert_autofinder_success": true,
+    "files": [ 
+        "certora/harnesses/MerkleCaller.sol",
+        "src/contracts/libraries/Merkle.sol",
+    ],
+    "link": [
+    ],
+    "struct_link": [
+
+    ],
+    //"java_args": [ " -ea -Dlevel.setup.helpers=info" ],
+
+    "hashing_length_bound": "3200",
+    //"optimistic_loop": true,
+    //"optimistic_hashing": true,
+    "solc": "solc8.12",
+    "solc_optimize": "200",
+    "cache": "false",
+    "solc_via_ir": false,
+    "server": "production",
+    //"server": "staging",  // switch to staging when running mutations
+    "prover_version": "master",
+    "packages": [
+    ],
+    //"process": "emv",
+    "smt_timeout": "6000",
+    //"auto_nondet_difficult_internal_funcs": true, 
+    "prover_args": [
+        "-maxBlockCount 130000",  //needed when running with loop iter > ~30
+        //"-verifyCache true",
+        //"-verifyTACDumps true",
+        //"-testMode true",
+        //"-checkRuleDigest true",
+        //"-callTraceHardFail on",
+        //"-recursionEntryLimit 3",
+        "-enableCopyLoopRewrites true", 
+        //"-summaryResolutionMode tiered", 
+        //"-enableEqualityReasoning true",
+        //"-mediumTimeout 5",
+        //"-depth 0",
+		//"-smt_initialSplitDepth 3",
+		//"-s [z3:lia1,yices:def]",
+		//"-splitParallel true",
+		//"-splitParallelInitialDepth 6",
+		//"-splitParallelTimelimit 7200",
+        "-useBitVectorTheory true", 
+    ],
+    "loop_iter": "32",
+    //"coverage_info": "advanced",    //for unsat cores
+
+    "verify": "MerkleCaller:certora/specs/libraries/Merkle.spec",
+
+    //"exclude_rule": [ "merkleizeSha256IsInjective_onSameLengths", "merkleizeSha256IsInjective" ],
+    //"rule": [ "processInclusionProofSha256_SingleValue", ],
+    "msg": "Merkle processInclusionProofSha256_SingleValue 2",
+
+    "mutations": {
+        "manual_mutants": [
+            {
+                "file_to_mutate": "src/contracts/libraries/Merkle.sol",
+                "mutants_location": "certora/mutations/Merkle"
+            }
+            ]
+    }
+}

certora/harnesses/DummyEigenPodA.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: BUSL-1.1
+pragma solidity ^0.8.12;
+
+import "../../src/contracts/pods/EigenPod.sol";
+import "./EigenPodHarness.sol";
+
+contract DummyEigenPodA is EigenPodHarness {
+    constructor(
+        IETHPOSDeposit _ethPOS,
+        IEigenPodManager _eigenPodManager,
+        uint64 _GENESIS_TIME
+    )
+    EigenPodHarness(_ethPOS, _eigenPodManager, _GENESIS_TIME) {}
+
+}

certora/harnesses/DummyEigenPodB.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: BUSL-1.1
+pragma solidity ^0.8.12;
+
+import "../../src/contracts/pods/EigenPod.sol";
+import "./EigenPodHarness.sol";
+
+contract DummyEigenPodB is EigenPodHarness {
+
+    constructor(
+        IETHPOSDeposit _ethPOS,
+        IEigenPodManager _eigenPodManager,
+        uint64 _GENESIS_TIME
+    )
+    EigenPodHarness(_ethPOS, _eigenPodManager, _GENESIS_TIME) {}
+}