euler-xyz · andrew-certora · Aug 20, 2024 · Mar 11, 2024 · Mar 11, 2024 · Mar 11, 2024
@@ -0,0 +1,27 @@
+{
+  "files": [
+    "certora/harness/CacheHarness.sol"
+  ],
+  "verify": "CacheHarness:certora/specs/Cache.spec",
+  "solc": "solc8.23",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "prover_version": "master",
+  "server" : "production",
+  "parametric_contracts": ["CacheHarness"],
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "rule_sanity": "basic",
+  "function_finder_mode" : "relaxed",
+  "finder_friendly_optimizer" : false,
+	"prover_args": [
+		"-smt_nonLinearArithmetic true",
+		"-adaptiveSolverConfig false",
+		"-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
+	],
+  "smt_timeout": "7000"
+}
@@ -0,0 +1 @@
+To run all of these conf files easily, use the certora/scripts/runERC4626RulesSplitConfs.py
@@ -0,0 +1,34 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "rule": ["assetsMoreThanSupply",],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+	"prover_args": [
+    "-maxConcurrentTransforms INLINED_HOOKS:8",
+		"-smt_nonLinearArithmetic true -adaptiveSolverConfig false -splitParallel true -splitParallelInitialDepth 2 -depth 15 -s [z3:arith1,yices:def] -mediumTimeout 2 -splitParallelTimelimit 7200"
+	],
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+  "smt_timeout": "7200"
+}
+
@@ -0,0 +1,31 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "rule": ["convertToAssetsWeakAdditivity"],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+	"disable_auto_cache_key_gen": true,
+	"fe_version": "latest",
+}
+
@@ -0,0 +1,31 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "rule": ["convertToSharesWeakAdditivity"],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+	"disable_auto_cache_key_gen": true,
+	"fe_version": "latest",
+}
+
@@ -0,0 +1,32 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "rule": ["depositMonotonicity",],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+	"disable_auto_cache_key_gen": true,
+	"fe_version": "latest",
+  "smt_timeout": "7200"
+}
+
@@ -0,0 +1,32 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "rule": ["dustFavorsTheHouse",],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+	"disable_auto_cache_key_gen": true,
+	"fe_version": "latest",
+  "smt_timeout": "7200"
+}
+
@@ -0,0 +1,32 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "rule": ["dustFavorsTheHouseAssets",],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+	"disable_auto_cache_key_gen": true,
+	"fe_version": "latest",
+  "smt_timeout": "7200"
+}
+
@@ -0,0 +1,36 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "rule": ["noAssetsIfNoSupply",],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+	"disable_auto_cache_key_gen": true,
+	"fe_version": "latest",
+  "prover_args": [
+    "-maxConcurrentTransforms INLINED_HOOKS:6",
+    "-smt_nonLinearArithmetic true -adaptiveSolverConfig false -depth 0 "
+  ],
+  "smt_timeout": "7200"
+}
+
@@ -0,0 +1,32 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "rule": ["noSupplyIfNoAssets",],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+	"disable_auto_cache_key_gen": true,
+	"fe_version": "latest",
+  "smt_timeout": "7200"
+}
+
@@ -0,0 +1,33 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "prover_args": [
+    "-maxConcurrentTransforms INLINED_HOOKS:8"
+  ],
+  "rule": ["onlyContributionMethodsReduceAssets"],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+  "smt_timeout": "7200"
+}
+
@@ -0,0 +1,33 @@
+{
+  "files": [
+    "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+    "src/EVault/modules/Vault.sol",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol",
+    "certora/harness/EVCHarness.sol",
+    "certora/harness/BaseHarness.sol",
+    "certora/harness/ERC4626Harness.sol",
+  ],
+  "verify": "ERC4626Harness:certora/specs/VaultERC4626.spec",
+  "solc": "solc8.23",
+  "rule_sanity": "basic",
+  "msg": "Vault ERC4626",
+  "packages": [
+      "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+      "forge-std=lib/forge-std/src"
+  ],
+  "prover_args": [
+    "-maxConcurrentTransforms INLINED_HOOKS:8"
+  ],
+  "rule": ["totalsMonotonicity"],
+  "parametric_contracts": ["ERC4626Harness"],
+  "build_cache": true,
+  "prover_version" : "master",
+  // Performance tuning options below this line
+  "solc_via_ir": true,
+  "solc_optimize": "10000",
+  "optimistic_loop": true, 
+  "loop_iter": "2",
+  "smt_timeout": "7200"
+}
+
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		To run all of these conf files easily, use the certora/scripts/runERC4626RulesSplitConfs.py