Merge branch 'master' into fix/specs

.github/CODEOWNERS

@@ -0,0 +1,5 @@
+# Specify the owners of the code in the src directory
+src/ @dglowinski @kasperpawlowski @hoytech
+
+# Specify the owners of the code in the certora directory
+certora/ @dglowinski @kasperpawlowski @hoytech

.gitmodules

@@ -1,12 +1,12 @@
 [submodule "lib/forge-std"]
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
-[submodule "lib/ethereum-vault-connector"]
-	path = lib/ethereum-vault-connector
-	url = https://github.com/euler-xyz/ethereum-vault-connector
 [submodule "lib/permit2"]
 	path = lib/permit2
 	url = https://github.com/Uniswap/permit2
 [submodule "lib/openzeppelin-contracts"]
 	path = lib/openzeppelin-contracts
 	url = https://github.com/OpenZeppelin/openzeppelin-contracts
+[submodule "lib/ethereum-vault-connector"]
+	path = lib/ethereum-vault-connector
+	url = https://github.com/euler-xyz/ethereum-vault-connector

README.md

@@ -61,8 +61,6 @@ This software is **experimental** and is provided "as is" and "as available".
 
 Always include thorough tests when using the Euler Vault Kit to ensure it interacts correctly with your code.
 
-The Euler Vault Kit is currently undergoing security audits and should not be used in production.
-
 ## Known limitations
 
 Refer to the [whitepaper](https://docs.euler.finance/euler-vault-kit-white-paper/) for a list of known limitations and security considerations.

certora/conf/Cache.conf

@@ -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"
+}

certora/conf/ERC4626Split/README.md

@@ -0,0 +1 @@
+To run all of these conf files easily, use the certora/scripts/runERC4626RulesSplitConfs.py

certora/conf/ERC4626Split/VaultERC4626-assetsMoreThanSupply.conf

@@ -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"
+}
+

certora/conf/ERC4626Split/VaultERC4626-convertToAssetsWeakAdditivity.conf

@@ -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",
+}
+

certora/conf/ERC4626Split/VaultERC4626-convertToSharesWeakAdditivity.conf

@@ -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",
+}
+

certora/conf/ERC4626Split/VaultERC4626-depositMonotonicity.conf

@@ -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"
+}
+

certora/conf/ERC4626Split/VaultERC4626-dustFavorsTheHouse.conf

@@ -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"
+}
+

certora/conf/ERC4626Split/VaultERC4626-dustFavorsTheHouseAssets.conf

@@ -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"
+}
+

certora/conf/ERC4626Split/VaultERC4626-noAssetsIfNoSupply.conf

@@ -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"
+}
+