diff --git a/.github/workflows/echidna-enigma-invariants.yml b/.github/workflows/echidna-enigma-invariants.yml
new file mode 100644
index 0000000..51b7909
--- /dev/null
+++ b/.github/workflows/echidna-enigma-invariants.yml
@@ -0,0 +1,46 @@
+name: Echidna Enigma Invariants
+
+on:
+ push:
+ branches:
+ - master
+ pull_request:
+
+env:
+ FOUNDRY_PROFILE: ci
+
+concurrency:
+ group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+ cancel-in-progress: true
+
+jobs:
+ echidna:
+ runs-on: ubuntu-latest
+
+ strategy:
+ matrix:
+ mode: [property, assertion] # Define the modes here
+
+ steps:
+ - name: Checkout repository
+ uses: actions/checkout@v3
+ with:
+ submodules: recursive
+
+ - name: Install Foundry
+ uses: foundry-rs/foundry-toolchain@v1
+ with:
+ version: nightly
+
+ - name: Compile contracts
+ run: |
+ forge build --build-info
+
+ - name: Run Echidna ${{ matrix.mode == 'property' && 'Property' || 'Assertion' }} Mode
+ uses: crytic/echidna-action@v2
+ with:
+ files: .
+ contract: Tester
+ config: test/enigma-dark-invariants/_config/echidna_config_ci.yaml
+ crytic-args: --ignore-compile
+ test-mode: ${{ matrix.mode == 'assertion' && 'assertion' || '' }}
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 27666da..2f8b700 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -2,8 +2,9 @@ name: CI
on:
push:
+ branches:
+ - master
pull_request:
- workflow_dispatch:
env:
FOUNDRY_PROFILE: ci
diff --git a/.gitignore b/.gitignore
index 29fa0d2..8dd01d5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,6 +15,13 @@ script/json/out/
# Coverage file
lcov.info
+# echidna
+_corpus/
+crytic-export/
+
+# VSCode files
+.vscode/
+
# MAC files
.DS_Store
-__MACOSX
\ No newline at end of file
+__MACOSX
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..aa5b0e5
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,18 @@
+# Invariants
+echidna:
+ echidna test/enigma-dark-invariants/Tester.t.sol --contract Tester --config ./test/enigma-dark-invariants/_config/echidna_config.yaml --corpus-dir ./test/enigma-dark-invariants/_corpus/echidna/default/_data/corpus
+
+echidna-assert:
+ echidna test/enigma-dark-invariants/Tester.t.sol --contract Tester --test-mode assertion --config ./test/enigma-dark-invariants/_config/echidna_config.yaml --corpus-dir ./test/enigma-dark-invariants/_corpus/echidna/default/_data/corpus
+
+echidna-explore:
+ echidna test/enigma-dark-invariants/Tester.t.sol --contract Tester --test-mode exploration --config ./test/enigma-dark-invariants/_config/echidna_config.yaml --corpus-dir ./test/enigma-dark-invariants/_corpus/echidna/default/_data/corpus
+
+# Invariants
+echidna-docker:
+ echidna test/enigma-dark-invariants/Tester.t.sol --contract Tester --config ./test/enigma-dark-invariants/_config/echidna_config_runner.yaml --corpus-dir ./test/enigma-dark-invariants/_corpus/echidna/default/_data/corpus
+
+
+# Medusa
+medusa:
+ medusa fuzz --config ./medusa.json
\ No newline at end of file
diff --git a/lib/openzeppelin-contracts b/lib/openzeppelin-contracts
index acd4ff7..a3a6db8 160000
--- a/lib/openzeppelin-contracts
+++ b/lib/openzeppelin-contracts
@@ -1 +1 @@
-Subproject commit acd4ff74de833399287ed6b31b4debf6b2b35527
+Subproject commit a3a6db86d5b4d7ef003b6f71e6504867d2679a7f
diff --git a/test/enigma-dark-invariants/CryticToFoundry.t.sol b/test/enigma-dark-invariants/CryticToFoundry.t.sol
new file mode 100644
index 0000000..0fd195c
--- /dev/null
+++ b/test/enigma-dark-invariants/CryticToFoundry.t.sol
@@ -0,0 +1,165 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IEulerSwap} from "src/interfaces/IEulerSwap.sol";
+
+// Libraries
+import "forge-std/Test.sol";
+import "forge-std/console.sol";
+
+// Contracts
+import {Invariants} from "./Invariants.t.sol";
+import {Setup} from "./Setup.t.sol";
+
+/*
+ * Test suite that converts from "fuzz tests" to foundry "unit tests"
+ * The objective is to go from random values to hardcoded values that can be analyzed more easily
+ */
+contract CryticToFoundry is Invariants, Setup {
+ CryticToFoundry Tester = this;
+
+ modifier setup() override {
+ _;
+ }
+
+ function setUp() public {
+ // Deploy protocol contracts
+ _setUp();
+
+ // Initialize handler contracts
+ _setUpHandlers();
+
+ // Initialize hook contracts
+ _setUpHooks();
+
+ /// @dev fixes the actor to the first user
+ actor = actors[USER1];
+
+ vm.warp(101007);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // POSTCONDITIONS REPLAY //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /* function test_replay_swap() public {
+ //@audit-issue is possible to extract value from the protocol 1 wei of value
+ Tester.setupMaglev(10, 50e18, 50e18, 0, Curve(0), MaglevEulerSwap.EulerSwapParams(1e18, 1e18, 0.4e18, 0.85e18));
+ Tester.mint(2000000, 0, 0);
+ Tester.swap(1, 0, 0, 0, 0);
+ }
+
+ function test_replay_nav() public {
+ //@audit-issue when price changes user lp looses nav after a trade
+ Tester.setupMaglev(10, 50e18, 50e18, 0, Curve(0), MaglevEulerSwap.EulerSwapParams(1e18, 1e18, 0.4e18, 0.85e18));
+ Tester.setPrice(1, 0.1 ether);
+ Tester.swap(10, 0, 0, 10, 0);
+ }
+
+ function test_replay_roundtripswap() public {
+ // @audit-ok user receives the amount donated -> HSPOST_SWAP_B -> expected functionality
+ Tester.setupMaglev(10, 50e18, 50e18, 0, Curve(0), MaglevEulerSwap.EulerSwapParams(1e18, 1e18, 0.4e18, 0.85e18));
+ Tester.donateUnderlying(300000000000, 0);
+ Tester.roundtripSwap(100000000, 0);
+ }
+
+ function test_replay_2roundtripswap() public {
+ //@audit-issue user gets 1 wei more one the swap back -> HSPOST_SWAP_B
+ Tester.setupMaglev(10, 50e18, 50e18, 0, Curve(0), MaglevEulerSwap.EulerSwapParams(1e18, 1e18, 0.4e18, 0.85e18));
+ Tester.swap(1516752036338334875613876384, 1645511910635276617001867226888, 2, 0, 0);
+ Tester.roundtripSwap(200000000, 0);
+ } */
+
+ /* function test_replay_setupEulerSwap() public {
+ //@audit-ok fixed by clamping fee
+ Tester.setupEulerSwap(
+ 0,
+ 0,
+ 0,
+ 1003720677821071739,
+ IEulerSwap.CurveParams(
+ 0, 12246676942863640986141097041882032371945, 31951643412123143093714293698540253070340823296393767, 0
+ )
+ );
+ }
+
+ function test_replay_swapExactOut() public {
+ //@audit-ok Invalid: 1!=0, reason: HSPOST_RESERVES_C: If amountIn tokenOut collateral, a specific amountOut is borrowed
+ Tester.setupEulerSwap(0, 0, 0, 0, IEulerSwap.CurveParams(0, 0, 0, 0));
+ Tester.swap(0, 0, 1, 0, 0);
+ Tester.mint(1, 1, 0);
+ Tester.redeem(115792089237316195423570985008687907853269984665640564039457584007913129639935, 0, 0);
+ console.log("########################");
+ console.log("debt2", eTST.debtOf(address(holder)));
+ Tester.swapExactOut(0, 0, false);
+ }
+
+ function test_replay_swapExactIn() public {
+ //@audit-ok Invalid: 1!=0, reason: HSPOST_RESERVES_C: If amountIn tokenOut collateral, a specific amountOut is borrowed
+ Tester.setupEulerSwap(0, 0, 0, 0, IEulerSwap.CurveParams(0, 0, 0, 0));
+ Tester.mint(1, 1, 0);
+ Tester.redeem(115792089237316195423570985008687907853269984665640564039457584007913129639935, 0, 0);
+ Tester.donateUnderlying(2, 1);
+ Tester.swapExactIn(0, 0, true);
+ } */
+
+ /* function test_replay_swap() public {
+ //@audit-ok Invalid: 1!=0, reason: HSPOST_RESERVES_A: If there is debt in tokenIn, the debt must be repaid
+ Tester.setupEulerSwap(0, 0, 0, 0, IEulerSwap.CurveParams(0, 0, 0, 0));
+ Tester.redeem(115792089237316195423570985008687907853269984665640564039457584007913129639935, 0, 1);
+ Tester.mint(1, 1, 1);
+ console.log("########################");
+ console.log("debt2", eTST2.debtOf(address(holder)));
+ console.log("balance2", eTST2.balanceOf(address(holder)));
+ Tester.swap(0, 1, 2, 0, 0);
+ } */
+
+ function test_replay_roundtripSwap() public {
+ //@audit Invalid: 1999999999999999999999<2000000000000000000000 failed, reason: HSPOST_SWAP_A: Holder's NAV should increase monotonically
+ Tester.setupEulerSwap(0, 0, 0, 0, IEulerSwap.CurveParams(2069895513206400, 0, 0, 77696590));
+ Tester.roundtripSwap(1, 0);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // INVARIANTS REPLAY //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // BROKEN INVARIANTS REPLAY //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Fast forward the time and set up an actor,
+ /// @dev Use for ECHIDNA call-traces
+ function _delay(uint256 _seconds) internal {
+ vm.warp(block.timestamp + _seconds);
+ }
+
+ /// @notice Set up an actor
+ function _setUpActor(address _origin) internal {
+ actor = actors[_origin];
+ }
+
+ /// @notice Set up an actor and fast forward the time
+ /// @dev Use for ECHIDNA call-traces
+ function _setUpActorAndDelay(address _origin, uint256 _seconds) internal {
+ actor = actors[_origin];
+ vm.warp(block.timestamp + _seconds);
+ }
+
+ /// @notice Set up a specific block and actor
+ function _setUpBlockAndActor(uint256 _block, address _user) internal {
+ vm.roll(_block);
+ actor = actors[_user];
+ }
+
+ /// @notice Set up a specific timestamp and actor
+ function _setUpTimestampAndActor(uint256 _timestamp, address _user) internal {
+ vm.warp(_timestamp);
+ actor = actors[_user];
+ }
+}
diff --git a/test/enigma-dark-invariants/HandlerAggregator.t.sol b/test/enigma-dark-invariants/HandlerAggregator.t.sol
new file mode 100644
index 0000000..ca7a945
--- /dev/null
+++ b/test/enigma-dark-invariants/HandlerAggregator.t.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// modules Actions Handler contracts,
+import {EVCHandler} from "./handlers/euler/EVCHandler.t.sol";
+import {ERC20Handler} from "./handlers/standard/ERC20Handler.t.sol";
+import {ERC4626Handler} from "./handlers/standard/ERC4626Handler.t.sol";
+import {EulerSwapHandler} from "./handlers/swap/EulerSwapHandler.t.sol";
+import {EulerSwapPeripheryHandler} from "./handlers/swap/EulerSwapPeripheryHandler.t.sol";
+import {EulerSwapSetupHandler} from "./handlers/setup/EulerSwapSetupHandler.t.sol";
+
+// Simulator Handler contracts,
+import {DonationAttackHandler} from "./handlers/simulators/DonationAttackHandler.t.sol";
+import {PriceOracleHandler} from "./handlers/simulators/PriceOracleHandler.t.sol";
+
+/// @notice Helper contract to aggregate all handler contracts, inherited in BaseInvariants
+abstract contract HandlerAggregator is
+ EVCHandler, // Euler handlers
+ ERC20Handler, // Standard Handlers
+ ERC4626Handler,
+ EulerSwapHandler, // Swap Handlers
+ EulerSwapPeripheryHandler,
+ EulerSwapSetupHandler, // Setup Handlers
+ DonationAttackHandler, // Simulator handlers
+ PriceOracleHandler
+{
+ /// @notice Helper function in case any handler requires additional setup
+ function _setUpHandlers() internal {}
+}
diff --git a/test/enigma-dark-invariants/Invariants.t.sol b/test/enigma-dark-invariants/Invariants.t.sol
new file mode 100644
index 0000000..7076d1c
--- /dev/null
+++ b/test/enigma-dark-invariants/Invariants.t.sol
@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+
+// Invariant Contracts
+import {BaseInvariants} from "./invariants/BaseInvariants.t.sol";
+
+/// @title Invariants
+/// @notice Wrappers for the protocol invariants implemented in each invariants contract
+/// @dev recognised by Echidna when property mode is activated
+/// @dev Inherits BaseInvariants
+abstract contract Invariants is BaseInvariants {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // BASE INVARIANTS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function echidna_CORE_INVARIANTS() public returns (bool) {
+ if (address(eulerSwap) != address(0)) {
+ assert_INV_CORE_A();
+ assert_INV_CORE_C();
+ }
+
+ return true;
+ }
+
+ function echidna_STATE_INVARIANTS() public returns (bool) {
+ if (address(eulerSwap) != address(0)) {
+ assert_INV_STATE_A();
+ assert_INV_STATE_B();
+ assert_INV_STATE_C();
+ }
+
+ return true;
+ }
+
+ function echidna_DEBT_LIMIT_INVARIANTS() public returns (bool) {
+ if (address(eulerSwap) != address(0)) {
+ assert_INV_DL_A();
+ }
+
+ return true;
+ }
+}
diff --git a/test/enigma-dark-invariants/README.md b/test/enigma-dark-invariants/README.md
new file mode 100644
index 0000000..359f0ef
--- /dev/null
+++ b/test/enigma-dark-invariants/README.md
@@ -0,0 +1,37 @@
+# Actor Based Invariant Testing Suite
+
+
+
+
+
+Developed by [vnmrtz.eth](https://x.com/vn_martinez_) from [Enigma Dark](https://www.enigmadark.com/).
+
+
+
+The Actor Based Invariant Testing Suite is a framework for performing comprehensive invariant testing of the EulerSwap protocol. Using an actor-based model, it simulates realistic scenarios with various entities interacting with the system, ensuring that protocol invariants and postconditions hold under an extensive range of conditions.
+
+The suite is designed to support multi-actor tooling, randomizing actions, parameters, actor roles, and asset selection to explore edge cases and ensure the robustness of a protocol.
+
+# Specifications
+
+Extensive documentation regarding the architecture and design of the suite can be found [HERE](./docs/overview.md).
+
+Further documentation outlining the properties of the system (both invariants and postconditions) can be found [HERE](./specs/).
+
+# Tooling
+
+The suite has been developed and tested using the following tools:
+
+- [Echidna](https://github.com/crytic/echidna): A battle tested property-based testing tool for Ethereum smart contracts.
+
+# Setup Instructions:
+
+Instructions for setting up the project and running the testing suite with echidna are available [HERE](./docs/internal-docs.md).
+
+## Additional notes
+
+- Ensure you have the latest version of dependencies both tooling and protocol dependencies installed before running the tests.
+- The suite is designed to be modular and extensible, allowing for easy integration of new properties and actors.
+- The suite supports integration with github actions, allowing for automated testing as part of the development workflow.
+
+This suite was developed by Enigma Dark after being engaged by Euler Labs to provide security services for the Euler v2 protocol, ensuring that best practices in security and testing are satisfied.
diff --git a/test/enigma-dark-invariants/Setup.t.sol b/test/enigma-dark-invariants/Setup.t.sol
new file mode 100644
index 0000000..285a00b
--- /dev/null
+++ b/test/enigma-dark-invariants/Setup.t.sol
@@ -0,0 +1,222 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Utils
+import "forge-std/console.sol";
+
+// Libraries
+import {DeployPermit2} from "./utils/DeployPermit2.sol";
+
+// Contracts
+import {EthereumVaultConnector} from "ethereum-vault-connector/EthereumVaultConnector.sol";
+import {GenericFactory} from "evk/GenericFactory/GenericFactory.sol";
+import {ProtocolConfig} from "evk/ProtocolConfig/ProtocolConfig.sol";
+import {SequenceRegistry} from "evk/SequenceRegistry/SequenceRegistry.sol";
+import {Base} from "evk/EVault/shared/Base.sol";
+import {Dispatch} from "evk/EVault/Dispatch.sol";
+import {EVault} from "evk/EVault/EVault.sol";
+import {EulerSwap} from "src/EulerSwap.sol";
+import {EulerSwapPeriphery} from "src/EulerSwapPeriphery.sol";
+import {EulerSwapFactory} from "src/EulerSwapFactory.sol";
+
+// Modules
+import {Initialize} from "evk/EVault/modules/Initialize.sol";
+import {Token} from "evk/EVault/modules/Token.sol";
+import {Vault} from "evk/EVault/modules/Vault.sol";
+import {Borrowing} from "evk/EVault/modules/Borrowing.sol";
+import {Liquidation} from "evk/EVault/modules/Liquidation.sol";
+import {BalanceForwarder} from "evk/EVault/modules/BalanceForwarder.sol";
+import {Governance} from "evk/EVault/modules/Governance.sol";
+import {RiskManager} from "evk/EVault/modules/RiskManager.sol";
+import {MockBalanceTracker} from "evk/../test/mocks/MockBalanceTracker.sol";
+
+// Interfaces
+import {IEVault} from "evk/EVault/IEVault.sol";
+import {IRMTestDefault} from "evk-test/mocks/IRMTestDefault.sol";
+
+// Test Contracts
+import {TestERC20} from "test/enigma-dark-invariants/utils/mocks/TestERC20.sol";
+import {BaseTest} from "test/enigma-dark-invariants/base/BaseTest.t.sol";
+import {MockPriceOracle} from "./utils/mocks/MockPriceOracle.sol";
+import {Actor} from "./utils/Actor.sol";
+
+/// @notice Setup contract for the invariant test Suite, inherited by Tester
+contract Setup is BaseTest {
+ function _setUp() internal {
+ // Deploy protocol contracts
+ _deployEulerEVCContracts();
+
+ // Deploy suite assets
+ _deployAssets();
+
+ // Deploy vaults
+ _deployEVaults();
+
+ // Deploy actors
+ _setUpActors();
+
+ // Setup eulerswap holder and periphery
+ _setUpEulerSwap();
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // EVC //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Deploy euler EVC & Environment contracts
+ function _deployEulerEVCContracts() internal {
+ // Deploy the EVC
+ evc = new EthereumVaultConnector();
+
+ // Deploy the factory
+ factory = new GenericFactory(address(this));
+
+ // Deploy permit2 contract
+ permit2 = DeployPermit2.deployPermit2();
+
+ // Setup fee recipient
+ feeRecipient = _makeAddr("feeRecipient");
+ protocolConfig = new ProtocolConfig(address(this), feeRecipient);
+
+ // Deploy the oracle and integrations
+ balanceTracker = address(new MockBalanceTracker());
+ oracle = new MockPriceOracle();
+ sequenceRegistry = address(new SequenceRegistry());
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // VAULTS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function _deployEVaults() internal {
+ // Deploy the modules
+ Base.Integrations memory integrations =
+ Base.Integrations(address(evc), address(protocolConfig), sequenceRegistry, balanceTracker, permit2);
+
+ Dispatch.DeployedModules memory modules = Dispatch.DeployedModules({
+ initialize: address(new Initialize(integrations)),
+ token: address(new Token(integrations)),
+ vault: address(new Vault(integrations)),
+ borrowing: address(new Borrowing(integrations)),
+ liquidation: address(new Liquidation(integrations)),
+ riskManager: address(new RiskManager(integrations)),
+ balanceForwarder: address(new BalanceForwarder(integrations)),
+ governance: address(new Governance(integrations))
+ });
+
+ // Deploy the vault implementation
+ address evaultImpl = address(new EVault(integrations, modules));
+
+ // Deploy the vault factory and set the implementation
+ factory.setImplementation(evaultImpl);
+
+ // Deploy the vaults
+ eTST = _deployEVault(address(assetTST));
+ vaults.push(address(eTST));
+
+ eTST2 = _deployEVault(address(assetTST2));
+ vaults.push(address(eTST2));
+
+ // Set LTVs
+ eTST.setLTV(address(eTST2), BORROW_LTV, LIQUIDATION_LTV, 0);
+ eTST2.setLTV(address(eTST), BORROW_LTV, LIQUIDATION_LTV, 0);
+
+ // Set pricing
+ oracle.setPrice(address(assetTST), unitOfAccount, 1e18);
+ oracle.setPrice(address(assetTST2), unitOfAccount, 1e18);
+
+ oracle.setPrice(address(assetTST), unitOfAccount, 1e18);
+ oracle.setPrice(address(assetTST2), unitOfAccount, 1e18);
+
+ oracle.setPrice(address(assetTST), address(assetTST2), 1e18);
+ oracle.setPrice(address(assetTST2), address(assetTST), 1e18);
+ }
+
+ function _deployEVault(address asset) internal returns (IEVault eVault) {
+ // Deploy the eTST
+ eVault = IEVault(factory.createProxy(address(0), true, abi.encodePacked(asset, address(oracle), address(1))));
+
+ // Configure the vault
+ eVault.setHookConfig(address(0), 0);
+ eVault.setInterestRateModel(address(new IRMTestDefault()));
+ eVault.setMaxLiquidationDiscount(MAX_LIQUIDATION_DISCOUNT);
+ eVault.setFeeReceiver(feeRecipient);
+ }
+
+ function _deployAssets() internal {
+ // Deploy base assets
+ TestERC20 asset0 = new TestERC20("Test Token", "TST", 18);
+ TestERC20 asset1 = new TestERC20("Test Token 2", "TST2", 6);
+ (assetTST, assetTST2) = (address(asset0) < address(asset1) ? (asset0, asset1) : (asset1, asset0));
+
+ baseAssets.push(address(assetTST));
+ baseAssets.push(address(assetTST2));
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // EULER SWAP //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function _setUpEulerSwap() internal {
+ // Deploy the periphery
+ periphery = new EulerSwapPeriphery();
+
+ // Deploy the euler swap factory
+ eulerSwapfactory = new EulerSwapFactory(address(evc));
+
+ // Setup eulerswap lp as the first actor
+ holder = address(actors[USER1]);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTORS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Deploy protocol actors and initialize their balances
+ function _setUpActors() internal {
+ // Initialize the three actors of the fuzzers
+ address[] memory addresses = new address[](3);
+ addresses[0] = USER1;
+ addresses[1] = USER2;
+ addresses[2] = USER3;
+
+ // Initialize the tokens array
+ address[] memory tokens = new address[](2);
+ tokens[0] = address(assetTST);
+ tokens[1] = address(assetTST2);
+
+ address[] memory contracts_ = new address[](3);
+ contracts_[0] = address(eTST);
+ contracts_[1] = address(eTST2);
+ contracts_[2] = address(periphery);
+
+ for (uint256 i; i < NUMBER_OF_ACTORS; i++) {
+ // Deploy actor proxies and approve system contracts_
+ address _actor = _setUpActor(addresses[i], tokens, contracts_);
+
+ // Mint initial balances to actors
+ for (uint256 j = 0; j < tokens.length; j++) {
+ TestERC20 _token = TestERC20(tokens[j]);
+ _token.mint(_actor, INITIAL_BALANCE);
+ }
+ actorAddresses.push(_actor);
+ }
+ }
+
+ /// @notice Deploy an actor proxy contract for a user address
+ /// @param userAddress Address of the user
+ /// @param tokens Array of token addresses
+ /// @param contracts_ Array of contract addresses to aprove tokens to
+ /// @return actorAddress Address of the deployed actor
+ function _setUpActor(address userAddress, address[] memory tokens, address[] memory contracts_)
+ internal
+ returns (address actorAddress)
+ {
+ bool success;
+ Actor _actor = new Actor(tokens, contracts_);
+ actors[userAddress] = _actor;
+ (success,) = address(_actor).call{value: INITIAL_ETH_BALANCE}("");
+ assert(success);
+ actorAddress = address(_actor);
+ }
+}
diff --git a/test/enigma-dark-invariants/SpecAggregator.t.sol b/test/enigma-dark-invariants/SpecAggregator.t.sol
new file mode 100644
index 0000000..09b29a9
--- /dev/null
+++ b/test/enigma-dark-invariants/SpecAggregator.t.sol
@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Test Contracts
+import {InvariantsSpec} from "./specs/InvariantsSpec.t.sol";
+import {PostconditionsSpec} from "./specs/PostconditionsSpec.t.sol";
+import {NonRevertPropertiesSpec} from "./specs/NonRevertPropertiesSpec.t.sol";
+
+/// @title SpecAggregator
+/// @notice Helper contract to aggregate all spec contracts, inherited in BaseHooks
+/// @dev inherits InvariantsSpec, PostconditionsSpec
+abstract contract SpecAggregator is InvariantsSpec, PostconditionsSpec, NonRevertPropertiesSpec {
+///////////////////////////////////////////////////////////////////////////////////////////////
+// PROPERTY TYPES //
+///////////////////////////////////////////////////////////////////////////////////////////////
+
+/// In this invariant testing framework, there are two types of properties:
+
+/// - INVARIANTS (INV):
+/// - Properties that should always hold true in the system.
+/// - Implemented in the /invariants folder.
+
+/// - POSTCONDITIONS:
+/// - Properties that should hold true after an action is executed.
+/// - Implemented in the /hooks and /handlers folders.
+
+/// - There are two types of POSTCONDITIONS:
+
+/// - GLOBAL POSTCONDITIONS (GPOST):
+/// - Properties that should always hold true after any action is executed.
+/// - Checked in the `_checkPostConditions` function within the HookAggregator contract.
+
+/// - HANDLER-SPECIFIC POSTCONDITIONS (HSPOST):
+/// - Properties that should hold true after a specific action is executed in a specific context.
+/// - Implemented within each handler function, under the HANDLER-SPECIFIC POSTCONDITIONS section.
+
+/// - ERC4626 PROPERTIES:
+/// - Properties that should always hold true in the system, which check compliance with the ERC4626 standard.
+/// - Implemented across the testing suite as invariants, postconditions and specific custom handlers.
+
+/// - NON REVERT (NR):
+/// - Properties that assert a specific function should never revert, or only revert under
+/// certain defined conditions.
+}
diff --git a/test/enigma-dark-invariants/Tester.t.sol b/test/enigma-dark-invariants/Tester.t.sol
new file mode 100644
index 0000000..7697912
--- /dev/null
+++ b/test/enigma-dark-invariants/Tester.t.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+import {Invariants} from "./Invariants.t.sol";
+import {Setup} from "./Setup.t.sol";
+
+/// @title Tester
+/// @notice Entry point for invariant testing, inherits all contracts, invariants & handler
+/// @dev Mono contract that contains all the testing logic
+contract Tester is Invariants, Setup {
+ bool public IS_TEST = true;
+
+ constructor() payable {
+ // Deploy protocol contracts and protocol actors
+ setUp();
+ }
+
+ /// @dev Foundry compatibility faster setup debugging
+ function setUp() internal {
+ // Deploy protocol contracts and protocol actors
+ _setUp();
+
+ // Initialize handler contracts
+ _setUpHandlers();
+
+ // Initialize the actor to the first user
+ _setUpHooks();
+ }
+}
diff --git a/test/enigma-dark-invariants/_config/echidna_config.yaml b/test/enigma-dark-invariants/_config/echidna_config.yaml
new file mode 100644
index 0000000..099e1b3
--- /dev/null
+++ b/test/enigma-dark-invariants/_config/echidna_config.yaml
@@ -0,0 +1,60 @@
+#codeSize max code size for deployed contratcs (default 24576, per EIP-170)
+codeSize: 224576
+
+#whether ot not to use the multi-abi mode of testing
+#it’s not working for us, see: https://github.com/crytic/echidna/issues/547
+#multi-abi: true
+
+#balanceAddr is default balance for addresses
+balanceAddr: 0x1000000000000000000000000
+#balanceContract overrides balanceAddr for the contract address (2^128 = ~3e38)
+balanceContract: 0x1000000000000000000000000000000000000000000000000
+
+#testLimit is the number of test sequences to run
+testLimit: 20000000
+
+#seqLen defines how many transactions are in a test sequence
+seqLen: 300
+
+#shrinkLimit determines how much effort is spent shrinking failing sequences
+shrinkLimit: 2500
+
+#propMaxGas defines gas cost at which a property fails
+propMaxGas: 1000000000
+
+#testMaxGas is a gas limit; does not cause failure, but terminates sequence
+testMaxGas: 1000000000
+
+# list of methods to filter
+#filterFunctions: ["openCdpExt"]
+# by default, blacklist methods in filterFunctions
+#filterBlacklist: false
+
+#stopOnFail makes echidna terminate as soon as any property fails and has been shrunk
+stopOnFail: false
+
+#coverage controls coverage guided testing
+coverage: true
+
+# list of file formats to save coverage reports in; default is all possible formats
+coverageFormats: [ "txt", "html" ]
+
+#directory to save the corpus; by default is disabled
+corpusDir: "test/invariants/_corpus/echidna/default/_data/corpus"
+# constants for corpus mutations (for experimentation only)
+#mutConsts: [100, 1, 1]
+
+#remappings
+cryticArgs: [ "--solc-remaps", "@crytic/properties/=lib/properties/ forge-std/=lib/forge-std/src/ ds-test/=lib/forge-std/lib/ds-test/src/ openzeppelin/=lib/openzeppelin-contracts/contracts/" ]
+
+# maximum value to send to payable functions
+maxValue: 1e+23 # 100000 eth
+
+#quiet produces (much) less verbose output
+quiet: false
+
+# format: "text" or "json"
+format: "text"
+
+# concurrent workers
+workers: 10
diff --git a/test/enigma-dark-invariants/_config/echidna_config_ci.yaml b/test/enigma-dark-invariants/_config/echidna_config_ci.yaml
new file mode 100644
index 0000000..cfd37a9
--- /dev/null
+++ b/test/enigma-dark-invariants/_config/echidna_config_ci.yaml
@@ -0,0 +1,57 @@
+#codeSize max code size for deployed contratcs (default 24576, per EIP-170)
+codeSize: 224576
+
+#whether ot not to use the multi-abi mode of testing
+#it’s not working for us, see: https://github.com/crytic/echidna/issues/547
+#multi-abi: true
+
+#balanceAddr is default balance for addresses
+balanceAddr: 0x1000000000000000000000000
+#balanceContract overrides balanceAddr for the contract address (2^128 = ~3e38)
+balanceContract: 0x1000000000000000000000000000000000000000000000000
+
+#testLimit is the number of test sequences to run
+testLimit: 40000
+
+#seqLen defines how many transactions are in a test sequence
+seqLen: 200
+
+#shrinkLimit determines how much effort is spent shrinking failing sequences
+shrinkLimit: 1500
+
+#propMaxGas defines gas cost at which a property fails
+propMaxGas: 1000000000
+
+#testMaxGas is a gas limit; does not cause failure, but terminates sequence
+testMaxGas: 1000000000
+
+# list of methods to filter
+#filterFunctions: ["openCdpExt"]
+# by default, blacklist methods in filterFunctions
+#filterBlacklist: false
+
+#stopOnFail makes echidna terminate as soon as any property fails and has been shrunk
+stopOnFail: false
+
+#coverage controls coverage guided testing
+coverage: true
+
+# list of file formats to save coverage reports in; default is all possible formats
+coverageFormats: [ "lcov", "html" ]
+
+#directory to save the corpus; by default is disabled
+corpusDir: "corpus"
+# constants for corpus mutations (for experimentation only)
+#mutConsts: [100, 1, 1]
+
+#remappings
+cryticArgs: [ "--solc-remaps", "@crytic/properties/=lib/properties/ forge-std/=lib/forge-std/src/ ds-test/=lib/forge-std/lib/ds-test/src/ openzeppelin/=lib/openzeppelin-contracts/contracts/" ]
+
+# maximum value to send to payable functions
+maxValue: 1e+23 # 100000 eth
+
+#quiet produces (much) less verbose output
+quiet: false
+
+# concurrent workers
+workers: 10
diff --git a/test/enigma-dark-invariants/_config/echidna_config_runner.yaml b/test/enigma-dark-invariants/_config/echidna_config_runner.yaml
new file mode 100644
index 0000000..4c7c00f
--- /dev/null
+++ b/test/enigma-dark-invariants/_config/echidna_config_runner.yaml
@@ -0,0 +1,57 @@
+#codeSize max code size for deployed contratcs (default 24576, per EIP-170)
+codeSize: 224576
+
+#whether ot not to use the multi-abi mode of testing
+#it’s not working for us, see: https://github.com/crytic/echidna/issues/547
+#multi-abi: true
+
+#balanceAddr is default balance for addresses
+balanceAddr: 0x1000000000000000000000000
+#balanceContract overrides balanceAddr for the contract address (2^128 = ~3e38)
+balanceContract: 0x1000000000000000000000000000000000000000000000000
+
+#testLimit is the number of test sequences to run
+testLimit: 20000000
+
+#seqLen defines how many transactions are in a test sequence
+seqLen: 300
+
+#shrinkLimit determines how much effort is spent shrinking failing sequences
+shrinkLimit: 2500
+
+#propMaxGas defines gas cost at which a property fails
+propMaxGas: 1000000000
+
+#testMaxGas is a gas limit; does not cause failure, but terminates sequence
+testMaxGas: 1000000000
+
+# list of methods to filter
+#filterFunctions: ["openCdpExt"]
+# by default, blacklist methods in filterFunctions
+#filterBlacklist: false
+
+#stopOnFail makes echidna terminate as soon as any property fails and has been shrunk
+stopOnFail: false
+
+#coverage controls coverage guided testing
+coverage: true
+
+# list of file formats to save coverage reports in; default is all possible formats
+coverageFormats: [ "txt", "html" ]
+
+#directory to save the corpus; by default is disabled
+corpusDir: "test/invariants/_corpus/echidna/default/_data/corpus"
+# constants for corpus mutations (for experimentation only)
+#mutConsts: [100, 1, 1]
+
+#remappings
+cryticArgs: [ "--ignore-compile", "--solc-remaps", "@crytic/properties/=lib/properties/ forge-std/=lib/forge-std/src/ ds-test/=lib/forge-std/lib/ds-test/src/ openzeppelin/=lib/openzeppelin-contracts/contracts/" ]
+
+# maximum value to send to payable functions
+maxValue: 1e+23 # 100000 eth
+
+#quiet produces (much) less verbose output
+quiet: false
+
+# concurrent workers
+workers: 10
diff --git a/test/enigma-dark-invariants/base/BaseHandler.t.sol b/test/enigma-dark-invariants/base/BaseHandler.t.sol
new file mode 100644
index 0000000..66d52ff
--- /dev/null
+++ b/test/enigma-dark-invariants/base/BaseHandler.t.sol
@@ -0,0 +1,221 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+
+// Libraries
+import {EnumerableSet} from "@openzeppelin/contracts/utils/structs/EnumerableSet.sol";
+import {TestERC20} from "../utils/mocks/TestERC20.sol";
+import {Math} from "@openzeppelin/contracts/utils/math/Math.sol";
+
+// Contracts
+import {Actor} from "../utils/Actor.sol";
+import {HookAggregator} from "../hooks/HookAggregator.t.sol";
+
+import "forge-std/console.sol";
+
+/// @title BaseHandler
+/// @notice Contains common logic for all handlers
+/// @dev inherits all suite assertions since per action assertions are implmenteds in the handlers
+contract BaseHandler is HookAggregator {
+ using EnumerableSet for EnumerableSet.UintSet;
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ address receiver;
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // MODIFIERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ modifier eulerSwapNotDeployed() {
+ if (address(eulerSwap) != address(0)) revert("BaseHandler: EulerSwap already deployed on this trace");
+ _;
+ }
+
+ modifier eulerSwapDeployed() {
+ if (address(eulerSwap) == address(0)) revert("BaseHandler: EulerSwap has not been deployed on this trace");
+ _;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // SHARED VARAIBLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ // ERC4626
+
+ /// @notice Track of the total amount borrowed
+ uint256 internal ghost_totalBorrowed;
+
+ /// @notice Track of the total amount borrowed per user
+ mapping(address => uint256) internal ghost_owedAmountPerUser;
+
+ /// @notice Track the enabled collaterals per user
+ mapping(address => EnumerableSet.AddressSet) internal ghost_accountCollaterals;
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS: RANDOM GETTERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Get a random asset address
+ function _getRandomBaseAsset(uint256 _i) internal view returns (address) {
+ uint256 _assetIndex = _i % baseAssets.length;
+ return baseAssets[_assetIndex];
+ }
+
+ /// @notice Get a random actor proxy address
+ function _getRandomActor(uint256 _i) internal view returns (address) {
+ uint256 _actorIndex = _i % NUMBER_OF_ACTORS;
+ return actorAddresses[_actorIndex];
+ }
+
+ /// @notice Get a random vault address
+ function _getRandomVault(uint8 i) internal view returns (address) {
+ uint256 _vaultIndex = i % vaults.length;
+ return vaults[_vaultIndex];
+ }
+
+ function _getAssetsByDir(bool dir) internal view returns (address asset0, address asset1) {
+ asset0 = eulerSwap.asset0();
+ asset1 = eulerSwap.asset1();
+ return dir ? (asset0, asset1) : (asset1, asset0);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Helper function to randomize a uint256 seed with a string salt
+ function _randomize(uint256 seed, string memory salt) internal pure returns (uint256) {
+ return uint256(keccak256(abi.encodePacked(seed, salt)));
+ }
+
+ /// @notice Helper function to get a random value
+ function _getRandomValue(uint256 modulus) internal view returns (uint256) {
+ uint256 randomNumber = uint256(keccak256(abi.encode(block.timestamp, block.prevrandao, msg.sender)));
+ return randomNumber % modulus; // Adjust the modulus to the desired range
+ }
+
+ /// @notice Helper function to mint an amount of tokens to an address
+ function _mint(address token, address receiver_, uint256 amount) internal {
+ TestERC20(token).mint(receiver_, amount);
+ }
+
+ /// @notice Helper function to mint an amount of tokens to an address and approve them to a spender
+ /// @param token Address of the token to mint
+ /// @param owner Address of the new owner of the tokens
+ /// @param spender Address of the spender to approve the tokens to
+ /// @param amount Amount of tokens to mint and approve
+ function _mintAndApprove(address token, address owner, address spender, uint256 amount) internal {
+ _mint(token, owner, amount);
+ _approve(token, owner, spender, amount);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HSPOST: SWAP //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Postconditions common to all three curves
+ function _eulerSwapPostconditions(uint256 amount0Out, uint256 amount1Out, uint256 amount0In, uint256 amount1In)
+ internal
+ {
+ // SWAP POSTCONDITIONS
+
+ assertGe(defaultVarsAfter.holderNAV, defaultVarsBefore.holderNAV, HSPOST_SWAP_A);
+
+ if (amount0Out > 0) {
+ assertEq(
+ defaultVarsAfter.users[receiver].assetTSTBalance,
+ defaultVarsBefore.users[receiver].assetTSTBalance + amount0Out,
+ HSPOST_SWAP_C
+ );
+ }
+
+ if (amount1Out > 0) {
+ assertEq(
+ defaultVarsAfter.users[receiver].assetTST2Balance,
+ defaultVarsBefore.users[receiver].assetTST2Balance + amount1Out,
+ HSPOST_SWAP_C
+ );
+ }
+
+ // RESERVES POSTCONDITIONS
+
+ int256 amount0Delta = int256(amount0In) - int256(amount0Out);
+ int256 amount1Delta = int256(amount1In) - int256(amount1Out);
+
+ /// asset0 (eTST)
+ _checkAssetChanges(
+ amount0Delta,
+ defaultVarsBefore.holderETSTDebt,
+ defaultVarsAfter.holderETSTDebt,
+ defaultVarsBefore.holderETSTAssets,
+ defaultVarsAfter.holderETSTAssets,
+ "token0"
+ );
+
+ /// asset1 (eTST2)
+ _checkAssetChanges(
+ amount1Delta,
+ defaultVarsBefore.holderETST2Debt,
+ defaultVarsAfter.holderETST2Debt,
+ defaultVarsBefore.holderETST2Assets,
+ defaultVarsAfter.holderETST2Assets,
+ "token1"
+ );
+
+ // DEBT POSTCONDITIONS
+
+ assertLe(defaultVarsAfter.holderETSTDebt, eulerSwap.reserve0(), HSPOST_DEBT_A);
+ assertLe(defaultVarsAfter.holderETST2Debt, eulerSwap.reserve1(), HSPOST_DEBT_A);
+ assertLe(defaultVarsAfter.holderETSTDebt, eulerSwap.reserve1(), HSPOST_DEBT_A);
+ assertLe(defaultVarsAfter.holderETST2Debt, eulerSwap.reserve0(), HSPOST_DEBT_A);
+ }
+
+ function _checkAssetChanges(
+ int256 amountDelta,
+ uint256 beforeDebt,
+ uint256 afterDebt,
+ uint256 beforeAssets,
+ uint256 afterAssets,
+ string memory tokenId
+ ) internal {
+ if (amountDelta > 0) {
+ // Positive delta means repaying debt first, then possibly increasing assets
+ if (uint256(amountDelta) < beforeDebt) {
+ // Just reduce debt
+ assertEq(
+ afterDebt, beforeDebt - uint256(amountDelta), string.concat(HSPOST_RESERVES_A, " for ", tokenId)
+ );
+ } else {
+ // Debt is fully repaid
+ assertEq(afterDebt, 0, string.concat(HSPOST_RESERVES_B, " for ", tokenId));
+
+ // If there's excess after repaying debt, it should increase assets
+ uint256 excess = uint256(amountDelta) - beforeDebt;
+ if (excess > 0) {
+ assertEq(afterAssets, beforeAssets + excess, string.concat(HSPOST_RESERVES_C, " for ", tokenId));
+ }
+ }
+ } else {
+ // Negative delta means using assets first, then borrowing
+ if (uint256(-amountDelta) < beforeAssets) {
+ // Just reduce assets
+ assertEq(
+ afterAssets,
+ beforeAssets - uint256(-amountDelta),
+ string.concat(HSPOST_RESERVES_D, " for ", tokenId)
+ );
+ } else {
+ // Assets are depleted
+ assertEq(afterAssets, 0, string.concat(HSPOST_RESERVES_E, " for ", tokenId));
+
+ // Any deficit beyond available assets increases debt
+ uint256 deficit = uint256(-amountDelta) - beforeAssets;
+ assertEq(afterDebt - beforeDebt, deficit, string.concat(HSPOST_RESERVES_F, " for ", tokenId));
+ }
+ }
+ }
+}
diff --git a/test/enigma-dark-invariants/base/BaseHooks.t.sol b/test/enigma-dark-invariants/base/BaseHooks.t.sol
new file mode 100644
index 0000000..5514f06
--- /dev/null
+++ b/test/enigma-dark-invariants/base/BaseHooks.t.sol
@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Contracts
+import {ProtocolAssertions} from "./ProtocolAssertions.t.sol";
+
+// Test Contracts
+import {SpecAggregator} from "../SpecAggregator.t.sol";
+
+/// @title BaseHooks
+/// @notice Contains common logic for all hooks
+/// @dev inherits all suite assertions since per-action assertions are implemented in the handlers
+/// @dev inherits SpecAggregator
+contract BaseHooks is ProtocolAssertions, SpecAggregator {}
diff --git a/test/enigma-dark-invariants/base/BaseStorage.t.sol b/test/enigma-dark-invariants/base/BaseStorage.t.sol
new file mode 100644
index 0000000..3bd9781
--- /dev/null
+++ b/test/enigma-dark-invariants/base/BaseStorage.t.sol
@@ -0,0 +1,108 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Libraries
+
+// Contracts
+import {EthereumVaultConnector} from "ethereum-vault-connector/EthereumVaultConnector.sol";
+import {GenericFactory} from "evk/GenericFactory/GenericFactory.sol";
+import {ProtocolConfig} from "evk/ProtocolConfig/ProtocolConfig.sol";
+import {EulerSwap} from "src/EulerSwap.sol";
+import {EulerSwapPeriphery} from "src/EulerSwapPeriphery.sol";
+import {EulerSwapFactory} from "src/EulerSwapFactory.sol";
+
+// Interfaces
+import {IEVault} from "evk/EVault/IEVault.sol";
+
+// Mock Contracts
+import {TestERC20} from "test/enigma-dark-invariants/utils/mocks/TestERC20.sol";
+import {MockPriceOracle} from "../utils/mocks/MockPriceOracle.sol";
+
+// Utils
+import {Actor} from "../utils/Actor.sol";
+
+/// @notice BaseStorage contract for all test contracts, works in tandem with BaseTest
+abstract contract BaseStorage {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // CONSTANTS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ uint256 constant MAX_TOKEN_AMOUNT = 1e29;
+
+ uint256 constant ONE_DAY = 1 days;
+ uint256 constant ONE_MONTH = ONE_YEAR / 12;
+ uint256 constant ONE_YEAR = 365 days;
+
+ uint256 internal constant NUMBER_OF_ACTORS = 3;
+ uint256 internal constant INITIAL_ETH_BALANCE = 1e26;
+ uint256 internal constant INITIAL_COLL_BALANCE = 1e21;
+
+ address internal constant unitOfAccount = address(1);
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTORS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Stores the actor during a handler call
+ Actor internal actor;
+
+ /// @notice Mapping of fuzzer user addresses to actors
+ mapping(address => Actor) internal actors;
+
+ /// @notice Array of all actor addresses
+ address[] internal actorAddresses;
+
+ /// @notice The address that is targeted when executing an action
+ address internal targetActor;
+
+ /// @notice The account that owns the euler-swap liqudity
+ address internal holder;
+
+ address internal feeRecipient;
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // SUITE STORAGE //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Generic factory
+ GenericFactory factory;
+
+ /// @notice System vaults
+ IEVault eTST;
+ IEVault eTST2;
+
+ /// @notice Mock assets
+ TestERC20 assetTST;
+ TestERC20 assetTST2;
+
+ /// @notice EulerSwap contracts
+ EulerSwap eulerSwap;
+ EulerSwapPeriphery periphery;
+ EulerSwapFactory eulerSwapfactory;
+
+ /// @notice Extra contracts
+ MockPriceOracle oracle;
+ ProtocolConfig protocolConfig;
+ address balanceTracker;
+ address sequenceRegistry;
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // EXTRA VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Array of base assets for the suite
+ address[] internal baseAssets;
+
+ /// @notice Array of vaults for the suite
+ address[] internal vaults;
+
+ /// @notice Evc contract
+ EthereumVaultConnector evc;
+
+ /// @notice Permit2 contract
+ address permit2;
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STRUCTS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+}
diff --git a/test/enigma-dark-invariants/base/BaseTest.t.sol b/test/enigma-dark-invariants/base/BaseTest.t.sol
new file mode 100644
index 0000000..71076c3
--- /dev/null
+++ b/test/enigma-dark-invariants/base/BaseTest.t.sol
@@ -0,0 +1,283 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IERC20} from "openzeppelin-contracts/interfaces/IERC20.sol";
+import {IEulerSwap} from "src/interfaces/IEulerSwap.sol";
+
+// Libraries
+import {Vm} from "forge-std/Base.sol";
+import {StdUtils} from "forge-std/StdUtils.sol";
+import {Math} from "openzeppelin-contracts/utils/math/Math.sol";
+
+// Utils
+import {Actor} from "../utils/Actor.sol";
+import {PropertiesConstants} from "../utils/PropertiesConstants.sol";
+import {StdAsserts} from "../utils/StdAsserts.sol";
+import {CoverageChecker} from "../utils/CoverageChecker.sol";
+
+// Contracts
+import {EulerSwap} from "src/EulerSwap.sol";
+
+// Base
+import {BaseStorage} from "./BaseStorage.t.sol";
+
+import "forge-std/console.sol";
+
+/// @notice Base contract for all test contracts extends BaseStorage
+/// @dev Provides setup modifier and cheat code setup
+/// @dev inherits Storage, Testing constants assertions and utils needed for testing
+abstract contract BaseTest is BaseStorage, PropertiesConstants, StdAsserts, StdUtils, CoverageChecker {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTOR PROXY MECHANISM //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @dev Actor proxy mechanism
+ modifier setup() virtual {
+ actor = actors[msg.sender];
+ targetActor = address(actor);
+ _;
+ actor = Actor(payable(address(0)));
+ targetActor = address(0);
+ }
+
+ /// @dev Skim euler swap assets
+ modifier skimAll() virtual {
+ _skimAll(eulerSwap, true);
+ _;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STRUCTS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // CHEAT CODE SETUP //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @dev Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D.
+ address internal constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));
+
+ /// @dev Virtual machine instance
+ Vm internal constant vm = Vm(VM_ADDRESS);
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function _setTargetActor(address user) internal {
+ targetActor = user;
+ }
+
+ /// @notice Get a random address
+ function _makeAddr(string memory name) internal pure returns (address addr) {
+ uint256 privateKey = uint256(keccak256(abi.encodePacked(name)));
+ addr = vm.addr(privateKey);
+ }
+
+ /// @notice Helper function to deploy a contract from bytecode
+ function deployFromBytecode(bytes memory bytecode) internal returns (address child) {
+ assembly {
+ child := create(0, add(bytecode, 0x20), mload(bytecode))
+ }
+ }
+
+ /// @notice Helper function to approve an amount of tokens to a spender, a proxy Actor
+ function _approve(address token, Actor actor_, address spender, uint256 amount) internal {
+ bool success;
+ bytes memory returnData;
+ (success, returnData) = actor_.proxy(token, abi.encodeWithSelector(0x095ea7b3, spender, amount));
+ require(success, string(returnData));
+ }
+
+ /// @notice Helper function to safely approve an amount of tokens to a spender
+
+ function _approve(address token, address owner, address spender, uint256 amount) internal {
+ vm.prank(owner);
+ _safeApprove(token, spender, 0);
+ vm.prank(owner);
+ _safeApprove(token, spender, amount);
+ }
+
+ /// @notice Helper function to safely approve an amount of tokens to a spender
+ /// @dev This function is used to revert on failed approvals
+ function _safeApprove(address token, address spender, uint256 amount) internal {
+ (bool success, bytes memory retdata) =
+ token.call(abi.encodeWithSelector(IERC20.approve.selector, spender, amount));
+ assert(success);
+ if (retdata.length > 0) assert(abi.decode(retdata, (bool)));
+ }
+
+ function _transferByActor(address token, address to, uint256 amount) internal {
+ bool success;
+ bytes memory returnData;
+ (success, returnData) = actor.proxy(token, abi.encodeWithSelector(IERC20.transfer.selector, to, amount));
+ require(success, string(returnData));
+ }
+
+ function _setupActorApprovals(address[] memory tokens, address[] memory contracts_) internal {
+ for (uint256 i; i < actorAddresses.length; i++) {
+ for (uint256 j; j < tokens.length; j++) {
+ for (uint256 k; k < contracts_.length; k++) {
+ _approve(tokens[j], actorAddresses[i], contracts_[k], type(uint256).max);
+ }
+ }
+ }
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // EULER-SWAP SPECIFIC HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function _skimAll(EulerSwap ml, bool order) internal {
+ if (order) {
+ _runSkimAll(ml, true);
+ _runSkimAll(ml, false);
+ } else {
+ _runSkimAll(ml, false);
+ _runSkimAll(ml, true);
+ }
+ }
+
+ function _runSkimAll(EulerSwap ml, bool dir) internal returns (uint256) {
+ uint256 skimmed = 0;
+ uint256 val = 1;
+
+ // Phase 1: Keep doubling skim amount until it fails
+
+ while (true) {
+ (uint256 amount0, uint256 amount1) = dir ? (val, uint256(0)) : (uint256(0), val);
+
+ try ml.swap(amount0, amount1, address(0xDEAD), "") {
+ skimmed += val;
+ val *= 2;
+ } catch {
+ break;
+ }
+ }
+
+ // Phase 2: Keep halving skim amount until 1 wei skim fails
+
+ while (true) {
+ if (val > 1) val /= 2;
+
+ (uint256 amount0, uint256 amount1) = dir ? (val, uint256(0)) : (uint256(0), val);
+
+ try ml.swap(amount0, amount1, address(0xDEAD), "") {
+ skimmed += val;
+ } catch {
+ if (val == 1) break;
+ }
+ }
+
+ return skimmed;
+ }
+
+ function _getHolderNAV() internal view returns (int256) {
+ uint256 balance0 = eTST.convertToAssets(eTST.balanceOf(holder));
+ uint256 debt0 = eTST.debtOf(holder);
+ uint256 balance1 = eTST2.convertToAssets(eTST2.balanceOf(holder));
+ uint256 debt1 = eTST2.debtOf(holder);
+
+ uint256 balValue = oracle.getQuote(balance0, address(assetTST), unitOfAccount)
+ + oracle.getQuote(balance1, address(assetTST2), unitOfAccount);
+ uint256 debtValue = oracle.getQuote(debt0, address(assetTST), unitOfAccount)
+ + oracle.getQuote(debt1, address(assetTST2), unitOfAccount);
+
+ return int256(balValue) - int256(debtValue);
+ }
+
+ function _createEulerSwap(
+ uint112 debtLimitA,
+ uint112 debtLimitB,
+ uint256 fee,
+ uint256 px,
+ uint256 py,
+ uint256 cx,
+ uint256 cy
+ ) internal returns (bool) {
+ EulerSwap.Params memory params = _getEulerSwapParams(debtLimitA, debtLimitB, fee);
+
+ IEulerSwap.CurveParams memory curveParams =
+ IEulerSwap.CurveParams({priceX: px, priceY: py, concentrationX: cx, concentrationY: cy});
+
+ try new EulerSwap(params, curveParams) returns (EulerSwap _eulerSwap) {
+ eulerSwap = _eulerSwap;
+ vm.prank(holder);
+ evc.setAccountOperator(holder, address(eulerSwap), true);
+ return true;
+ } catch (bytes memory reason) {
+ console.logBytes(reason);
+ return false;
+ }
+ }
+
+ function _getEulerSwapParams(uint112 reserve0, uint112 reserve1, uint256 fee)
+ internal
+ view
+ returns (EulerSwap.Params memory)
+ {
+ (address vault0, address vault1) = (address(eTST), address(eTST2));
+
+ return IEulerSwap.Params({
+ vault0: vault0,
+ vault1: vault1,
+ eulerAccount: holder,
+ equilibriumReserve0: reserve0,
+ equilibriumReserve1: reserve1,
+ currReserve0: reserve0,
+ currReserve1: reserve1,
+ fee: fee
+ });
+ }
+
+ /// @notice Helper function to generate points that lie on the Euler curve
+ /// @param x The x coordinate to generate a corresponding y value for
+ /// @param priceX Price ratio for asset X
+ /// @param priceY Price ratio for asset Y
+ /// @param x0 Equilibrium reserve for x
+ /// @param y0 Equilibrium reserve for y
+ /// @param c Concentration parameter
+ /// @return y The corresponding y coordinate that lies on the curve
+ function _generatePointOnCurve(uint256 x, uint256 priceX, uint256 priceY, uint256 x0, uint256 y0, uint256 c)
+ internal
+ pure
+ returns (uint256 y)
+ {
+ // If x is above equilibrium, we're in the upper region
+ if (x >= x0) {
+ return y0; // In upper region, any y >= y0 is valid
+ }
+ // If x is below equilibrium, calculate required y using curve function
+ unchecked {
+ uint256 v = Math.mulDiv(priceX * (x0 - x), c * x + (1e18 - c) * x0, x * 1e18, Math.Rounding.Ceil);
+ require(v <= type(uint248).max, "Overflow");
+ y = y0 + (v + (priceY - 1)) / priceY;
+ }
+ }
+
+ /// @notice Helper function to generate balanced initial reserves that satisfy the curve
+ /// @param targetReserve0 Approximate target for reserve0
+ /// @param targetReserve1 Approximate target for reserve1
+ /// @param curveParams Curve parameters to use
+ /// @return reserve0 Valid reserve0 that lies on curve
+ /// @return reserve1 Valid reserve1 that lies on curve
+ function _generateBalancedReserves(
+ uint112 targetReserve0,
+ uint112 targetReserve1,
+ IEulerSwap.CurveParams memory curveParams
+ ) internal pure returns (uint112 reserve0, uint112 reserve1) {
+ // Start with target values as equilibrium points
+ uint256 x0 = targetReserve0;
+ uint256 y0 = targetReserve1;
+
+ // Generate a point slightly below equilibrium
+ uint256 x = (x0 * 95) / 100; // 95% of equilibrium
+ uint256 y = _generatePointOnCurve(x, curveParams.priceX, curveParams.priceY, x0, y0, curveParams.concentrationX);
+
+ // Ensure values fit within uint112
+ require(x <= type(uint112).max && y <= type(uint112).max, "Reserves too large");
+
+ return (uint112(x), uint112(y));
+ }
+}
diff --git a/test/enigma-dark-invariants/base/ProtocolAssertions.t.sol b/test/enigma-dark-invariants/base/ProtocolAssertions.t.sol
new file mode 100644
index 0000000..355bdfe
--- /dev/null
+++ b/test/enigma-dark-invariants/base/ProtocolAssertions.t.sol
@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Base
+import {BaseTest} from "./BaseTest.t.sol";
+import {StdAsserts} from "../utils/StdAsserts.sol";
+
+/// @title ProtocolAssertions
+/// @notice Helper contract for protocol specific assertions
+contract ProtocolAssertions is StdAsserts, BaseTest {}
diff --git a/test/enigma-dark-invariants/docs/internal-docs.md b/test/enigma-dark-invariants/docs/internal-docs.md
new file mode 100644
index 0000000..5a022a1
--- /dev/null
+++ b/test/enigma-dark-invariants/docs/internal-docs.md
@@ -0,0 +1,292 @@
+# Internal Documentation for the Euler Earn Enigma Dark Invariant Testing Suite
+
+## Table of Contents
+
+1. [Running the Suite](#running-the-suite)
+
+ - Prerequisites
+ - Starting the Suite
+ - Configurations
+
+2. [Property Formats](#property-formats)
+
+ - Invariants
+ - Postconditions
+ - Global Postconditions (GPOST)
+ - Handler-Specific Postconditions (HSPOST)
+
+3. [Handlers: Adding Support for New Functions](#handlers-adding-support-for-new-functions)
+
+ - Overview
+ - Adding New Functions
+ - Testing New Functions
+
+4. [Debugging Broken Properties](#debugging-broken-properties)
+ - Logging & Output
+ - Crytic to Foundry Test Helper
+ - Steps to Reproduce an Echidna Error Inside the Foundry Wrapper
+
+## Running the Suite
+
+- **Prerequisites**:
+
+ - Ensure that all protocol dependencies have been installed:
+
+ ```sh
+ cp .env.example .env
+
+ forge install
+ ```
+
+ - Make sure the latest version of **Echidna** is installed. If it is not installed, you can follow the guide [HERE](https://github.com/crytic/echidna?tab=readme-ov-file#installation) to install it.
+
+
+
+- **Starting the Suite**: The suite is able to check the invariants and postconditions of the Euler Earn protocol. For that it uses two different modes, property mode and assertion mode respectively.
+
+ - **Property Mode**: Checks protocol invariants. Run with:
+ ```sh
+ make echidna
+ ```
+ - **Assertion Mode**: Checks protocol postconditions. Run with:
+
+ ```sh
+ make echidna-assert
+ ```
+
+ - **Extra**: Run the suites without checking for properties, only increasing corpus size and coverage. Run with:
+ ```sh
+ make echidna-explore
+ ```
+
+
+
+- **Configurations**: The suite configuration can be found in the [echidna_config.yaml](../_config/echidna_config.yaml) file. This file contains the configuration for the Echidna testing tool, the following are the most important parameters of the configuration:
+
+ - **seqLen**: Defines the number of calls in each test sequence.
+ - **maxDepth**: Sets the total number of test sequences to execute.
+ - **coverage**: Enables coverage tracking, stored in the directory specified by `corpusDir`.
+ - **corpusDir**: Directory for saving coverage data. In this suite, coverage is saved in `tests/invariants/_corpus/echidna/default/_data/corpus`.
+ - **workers**: Sets the number of parallel threads for Echidna, ideally close to the machine's CPU thread count for optimal performance.
+
+
+## Property Formats
+
+As mentioned on the public documentation this suite framework spins around to types of properties, **invariants** and **postconditions**. The following section will provide a detailed explanation of each type of property and how they are implemented.
+
+### Invariants
+
+- **Definition**: Invariants are properties that must hold true across all states of the system. These are checked when the tool runs under property-mode, making echidna call all public functions starting with `echidna_` and making sure the assertions in those do not fail. These checks happen in between every call inside test sequences.
+- **Example**: BASE_INVARIANT_A
+
+ - **Spec**: totalAssetsDeposited + interestLeft >= totalAllocated.
+ - **Implementation**: `BaseInvariants::assert_INV_ASSETS_A`
+
+ ```solidity
+ function assert_INV_ASSETS_A() internal {
+ (,, uint168 interestLeft) = eulerEulerEarnVault.getEulerEarnSavingRate();
+
+ uint256 totalAssetsDeposited = eulerEulerEarnVault.totalAssetsDeposited();
+
+ if (eulerEulerEarnVault.totalAssetsAllocatable() - totalAssetsDeposited - interestLeft == 0) {
+ assertGe(totalAssetsDeposited + interestLeft, eulerEulerEarnVault.totalAllocated(), INV_ASSETS_A);
+ }
+ }
+ ```
+
+ Every implementation of an invariant must be called inside its wrapper `echidna_**` function on the `Invariants.sol` file, as shown in the following code snippet:
+
+ ```solidity
+ function echidna_INV_ASSETS_INVARIANTS() public returns (bool) {
+ assert_INV_ASSETS_A();
+ assert_INV_ASSETS_D();
+
+ uint256 sumStrategiesAllocated;
+ for (uint256 i; i < strategies.length; i++) { /// <--- Looping through all strategies tokens,
+ IEulerEarn.Strategy memory strategy = eulerEulerEarnVault.getStrategy(strategies[i]);
+ if (strategy.status == IEulerEarn.StrategyStatus.Active) {
+ sumStrategiesAllocated += eulerEulerEarnVault.getStrategy(strategies[i]).allocated;
+ }
+ }
+
+ assert_INV_ASSETS_B(sumStrategiesAllocated);
+ return true;
+ }
+ ```
+
+- **Implementation Guide**:
+ - Define core properties of the protocol (e.g., balance constraints, liquidity checks, internal accounting accuracy).
+ - Keep assertions clear and straightforward. If looping through users, assets, or reserves, aim for simplicity—avoid excessive or complex logic to maintain efficiency and readability (check example above looping through the suite actors).
+ - Minimize redundancy by ensuring invariants don’t overlap too heavily with each other. However, certain degree of overlap can be beneficial for covering more scenarios, so consider strategic overlaps to maximize checks coverage.
+
+### Postconditions
+
+- **Definition**: Postconditions are properties that must hold true following specific actions or interactions within a test sequence. They help ensure that each action in the sequence produces a valid protocol state, focusing on targeted outcomes rather than overall system-wide conditions. Unlike invariants, which are checked consistently across states, postconditions are enforced at designated points. These points include the end of each handler call (for handler-specific postconditions) or at the end of the `_after` hook (for global postconditions), validating the expected results of specific actions.
+
+ As the public documentation states, these checks are performed in assertion-mode, where echidna report a failing alert after detecting a `Panic(1)` error coming from a failed `assert` statement.
+
+- **Categories**: These postconditions can fall into two categories, the global postconditions and the handler-specific postconditions. The global postconditions (GPOST) are checked at the end of each test sequence using the `_after` hook, while the handler-specific postconditions (HSPOST) are checked at the end of specific handler calls.
+
+- **Example GPOST**: GPOST_BASE_A
+
+ - **Spec**: lastHarvestTimestamp increases monotonically.
+ - **Implementation**: `DefaultBeforeAfterHooks::assert_GPOST_BASE_A`
+
+ ```solidity
+ function assert_GPOST_BASE_A() internal {
+ assertGe(defaultVarsAfter.lastHarvestTimestamp, defaultVarsBefore.lastHarvestTimestamp, GPOST_BASE_A);
+ }
+ ```
+
+ Every global postcondition must be called at the end of the `_after` hook in the `_checkPostConditions` function, as shown in the following code snippet:
+
+ ```solidity
+ function _checkPostConditions() internal {
+ // Implement post conditions here
+ ...
+
+ // BASE
+ assert_GPOST_BASE_A(); /// <--- Global postcondition execution
+
+ ...
+ }
+ ```
+
+- **Example HSPOST**: HSPOST_USER_A
+
+ - **Spec**: After a deposit or mint, the amount should be credited to the cash reserve.
+ - **Implementation**: At the end of the `deposit` handler, the postcondition is checked.
+
+ ```solidity
+ function deposit(uint8 i) external setup {
+ bool success;
+ bytes memory returnData;
+
+ ... /// <--- variable caching, actor-call, etc. summarized for brevity
+
+ if (success) {
+ _after();
+
+ // POST-CONDITIONS
+ /// @dev HSPOST_USER_A
+ assertEq(defaultVarsBefore.balance + assets, defaultVarsAfter.balance, HSPOST_USER_A);
+ }
+ }
+ ```
+
+- **Implementation Guide**:
+ - Identify key outcomes or state changes that should result from each action (e.g., balance updates, collateral adjustments, interest accruals).
+ - Aim to complement invariants with global postconditions, ensuring that properties that are not possible to be implemented as invariants are still covered.
+
+
+## Handlers: Adding Support for New Functions
+
+- **Overview**: As the public documentation states, handlers act as a kind of middleware layer between the tooling and the protocol. That is why when new features are added to the protocol or this one is upgraded, new handler functions must be either added or updated to support the new features. The following section will provide a detailed explanation of how to add support for new functions in handlers.
+- **Adding New Functions**: Let's take the example of an upgrade. The following steps show a guide through the process of adding support for these new functions in the handlers:
+
+ - **Identify the Handler**: Determine which handler contract will be responsible for the new functions.
+
+ - **Identify the parameters**: Determine which parameters are needed for the actions, which ones can be randomized, which ones should be clamped and which ones should be taken from a finite set like a helper storage array.
+
+ - **Identify if the action is permissioned or permissionless**: If the action is permissioned, using actors as proxy is not needed since the suite is setup as the owner so a direct call to the handler is enough. If the action is permissionless, an actor-proxied call must be used along with the `setup` actor selection modifier. The following code is how the `deposit` implementation would look like:
+
+ - Function should be called by an actor so the `setup` modifier and a proxied call to the protocol are used.
+ - The function should be called between the `_before` and `_after` hooks to ensure values are cached for postconditions to be checked properly.
+
+ ```solidity
+ function deposit(
+ uint256 assets,
+ uint8 i
+ ) external setup {
+ bool success; /// <--- Variables to store the success of the call and return data
+ bytes memory returnData;
+
+ address receiver = _getRandomActor(i); /// <--- Random receiver actor selection
+
+ _before(); /// <--- Before hook
+ (success, returnData) = actor.proxy(target, /// <--- Proxied call to the protocol
+ abi.encodeWithSelector(
+ IERC4626.deposit.selector,
+ assets,
+ receiver
+ ));
+
+ if (success) {
+ _after(); /// <--- After hook on success
+ ...
+ }
+
+ }
+ ```
+
+ - **Update Postconditions**: If the new functions introduce changes to the protocol state, update the postconditions to reflect these changes.
+
+
+- **Testing**: After adding the new handler functions and updating the postconditions, run the tooling to make sure the new logic is being covered and work correctly. You can check for html coverage reports inside `echidna/default/_data/corpus` directory.
+
+
+## Debugging Broken Properties
+
+- **Logging & Output**: While running, Echidna displays a terminal UI that reports the status of properties—either passing or failing—along with relevant call traces. When a property fails, some threads initiate a "shrinking" process to simplify the call trace, making debugging easier. The amount of shrinking effort can be adjusted in the `echidna_config.yaml` file using the `shrinkLimit` parameter.
+ After shrinking completes for a failing property, the suite can be stopped with `Ctrl+C`. Corpus and coverage data are saved automatically, and the dashboard's information is output to the command line, allowing to copy the minimized call trace for further debugging with Foundry wrapper tests.
+
+- **Crytic to foundry test helper**: `CryticToFoundry` file serves as a call trace reproducer where call traces from echidna output can be debugged easily. The following is an example of how to use the helper for a failing property:
+
+ ```solidity
+ function test_INV_ASSETS_INVARIANTS_1() public {
+ Tester.donateUnderlying(1 ether, 0);
+ Tester.simulateYieldAccrual(1 ether, 0);
+ Tester.addStrategy(1, 0);
+ Tester.toggleStrategyEmergencyStatus(0);
+ Tester.toggleStrategyEmergencyStatus(0);
+ _delay(2 weeks);
+ console.log(block.timestamp);
+ echidna_INV_ASSETS_INVARIANTS();
+ }
+ ```
+
+- **Steps to reproduce an Echidna error inside the Foundry wrapper**:
+ - Copy the call trace from the Echidna output.
+ - Initiate the `[echidna-trace-parser](https://github.com/Enigma-Dark/echidna-trace-parser)` tool.
+ - Paste the call trace into the tool.
+ - Hit enter to generate the Foundry wrapper test.
+ - Copy the generated test and paste it into the `CryticToFoundry` file.
+ - Run the test and debug the failing property using foundry verbose output `-vvvv`.
+
+## CI Setup
+
+- **Overview**: The suite is integrated into the CI pipeline of the protocol to ensure that the properties are checked consistently with every updates. Once the suite has been tuned to be fast and efficient, it can be integrated in the development cycle to catch bugs. Once optimized for speed and efficiency, the suite can be incorporated into the development lifecycle to identify bugs early. The following rules should be followed to configure the CI pipeline for effective integration of the suite:
+
+ 1. **Corpus Directory Management**:
+ After completing the invariant testing engagement, a `corpus` directory is generated with the coverage data and reproducers. This directory represents hundreds of CPU hours of refinement and is valuable to make the tool run efficiently. Since an attacker could use the contents of this directory to quickly identify attack vectors and vulnerable code it is excluded from the files pushed to the github repository. The `corpus` directory is independetly stored in a private repository, and the CI pipeline has permissions and is configured to pull from the private repository to get the `corpus` directory and run the suite with the coverage data.
+ 2. **Ongoing Fuzzing Campaigns**:
+ For every code update, new feature, or public release, the fuzzing campaign should execute for at least 24 hours, starting with the existing `corpus` directory. This process ensures the corpus remains up to date with recent changes and verifies the suite continues to validate critical properties.
+ 3. **Corpus Updates**:
+ After the fuzzing campaign, the updated corpus directory should be pushed back to the private repository, maintaining a continuously evolving corpus.
+
+ > Note: The CI pipeline for the public repository is configured to pull the corpus directory securely from the private repository, which requires proper permissions and secrets.
+
+- **Setup**: Follow these steps to set up CI pipeline permissions and integrate the fuzzing suite effectively:
+
+ 1. **Create a private repository**:
+ - Name the repository following this convention: `protocol-name-suite-corpus` (e.g., `euler-earn-suite-corpus`).
+ - This repository should be owned by the same organization as the public repository.
+ 2. **Initialize the corpus repository**:
+ - Navigate to the local `corpus` directory, initialize a git repository, add the remote origin and push the contents to the private repository.
+ 3. **Generate SSH Keys**:
+ - Create a new RSA key pair:
+ ```sh
+ ssh-keygen -t rsa -b 4096 -C "
+ ```
+ - Add the public key as a read-only deployment key in the private repository, using the variable name `DEPLOY_CORPUS_KEY`.
+ - Save the private key as a GitHub Actions secret in the public repository under the name `SSH_CORPUS_PRIVATE_KEY`.
+
+- **CI Job Overview**:
+ The `enigma-invariants.yml` job has been configured to pull the corpus directory from the private repository and run the suite efficiently with the coverage data. Additionally, a new configuration file, `echidna_config_ci.yaml`, has been derived from the suite's original `echidna_config.yaml`. This CI-specific configuration has been optimized to utilize the `corpus` directory and coverage data efficiently while reducing execution time.
+
+ The adjustments include a more moderate number of runs and sequence lengths to improve the suite's performance in the CI pipeline. Since the primary goal in this context is to validate against existing coverage, the suite can afford shorter execution durations and reduced sequence complexity.
+
+ - `testLimit` reduced to 50000
+ - `seqLen` reduced to 200
+ - `shrinkLimit` reduced to 1500
+ - `corpusDir` set to the `corpus` directory created when cloning the private repository.
diff --git a/test/enigma-dark-invariants/docs/invariant-suite-inheritance.png b/test/enigma-dark-invariants/docs/invariant-suite-inheritance.png
new file mode 100644
index 0000000..0fea1c3
Binary files /dev/null and b/test/enigma-dark-invariants/docs/invariant-suite-inheritance.png differ
diff --git a/test/enigma-dark-invariants/docs/invariant-suite-overview.png b/test/enigma-dark-invariants/docs/invariant-suite-overview.png
new file mode 100644
index 0000000..39af008
Binary files /dev/null and b/test/enigma-dark-invariants/docs/invariant-suite-overview.png differ
diff --git a/test/enigma-dark-invariants/docs/overview.md b/test/enigma-dark-invariants/docs/overview.md
new file mode 100644
index 0000000..3a84e8e
--- /dev/null
+++ b/test/enigma-dark-invariants/docs/overview.md
@@ -0,0 +1,165 @@
+This document aims to present a high-level view of the architecture of the Actor-Based Invariant Testing Suite developed for the Euler Earn protocol.
+
+# System overview
+
+
+
+
+
+The Invariant Testing Suite serves as middleware between the tooling and the Protocol. The system’s setup can be split into the following components:
+
+- **Tooling**: Tool or set of tools used to test the system, targeting the suite middleware in order to conduct fuzzing campaigns and check properties. In this case, the tooling used is Echidna, a property-based testing tool for Ethereum smart contracts.
+- **Test Suite**: Middleware that connects the tooling with the protocol, which orchestrates all interactions with it, including the actors, handlers, and properties. It is responsible for setting up the environment, running the tests, and reporting the results.
+- **Local Protocol Deployment**: Local testing deployment of the protocol, whose setup is primarily based on the existing deployment scripts of Euler Earn. The Test Suite contracts are designed to setup and interact with this deployment of the protocol.
+
+## Inheritance Hierarchy
+
+The Test Suite centers around the main `Tester` contract, which inherits from several other contracts, each designated with a specific function within the system. The inheritance hierarchy appears as follows:
+
+
+
+
+
+This illustrates the inheritance graph for the suite.
+
+# Test Suite Architecture
+
+The Test Suite follows a modular architecture designed to address the different types of properties and upgrade needs for complex protocols like Euler Earn. It is designed to be flexible and easy to integrate with new features, allowing for the reuse of existing components and the addition of new ones. The Test Suite is composed of the following components:
+
+- **Base**: Base contracts of the Test Suite, which include the Storage contract, the Setup contract, and a few more. The Storage contract is responsible for storing protocol deployment addresses and extra variables, while the Setup contract is responsible for setting up the environment for the tests.
+- **Actors**: Actors of the Test Suite, which represent the different entities interacting with the protocol. Each actor is a proxy-like contract that forwards specific actions from the handlers to the protocol.
+- **Handlers**: Contracts that contain external-facing functions for tooling to execute user actions via actors. They are designed to be modular and extensible, allowing for the addition of new functions and features (eg. liquid eModes).
+- **Hooks**: Responsible for caching protocol and user values before and after calls, as well as executing global postconditions. They are designed to be modular and extensible, allowing for the incorporation of additional postconditions and value caching as needed.
+- **Properties**: Contracts that define the specifications and implement the required checks to ensure properties hold in the system.
+
+## Base
+
+The base contracts of the Test Suite are responsible for setting up the environment for the tests, storing the protocol deployment addresses and extra variables and helper functions for handlers and hooks.
+
+It is composed by the following smart contracts:
+
+- **BaseHandler**: Base contract that contains helper functions for the handlers such as random selectors for assets, Atokens, DebtTokens, eMode categories and priceAggregators. It is inherited by all handler contracts.
+
+- **BaseHooks**: Base contract where common logic for the hooks is implemented. In the case of this suite, no helper functions are implemented in this contract it is just used to agregate parent contracts: ProtocolAssertions and SpecAggregator.
+
+- **BaseStorage**: Storage contract that stores protocol deployment addresses and extra variables. This contract is the root of the inheritance chain, serving as the main parent contract.
+
+- **BaseTest**: Test temmplate contract that contains general protocol helper functions and the `setup` actor selector modifier implementation. It is inherited by all test contracts.
+
+- **ProtocolAssertions**: Helper contract for protocol specific assertions which are reused along the codebase.
+
+## Actors
+
+Actors are smart contract entities that interact with the protocol as showcased in the diagram. These contracts act as a proxy between the handlers and the protocol, forwarding actions to the protocols acting as the "real" users. The tooling for this suite is configured to randomly use three callers `USER1`, `USER2` and `USER3` to interact with the handlers. The `setup` modifier in the `BaseTest` contract is used on every user handler to select the actor to be used in the proxied call to the protocol based on the caller of the handler function.
+
+Example: `setup` Modifier in Action
+
+```solidity
+function redeem(uint256 amount, uint8 i) external setup {
+ /// setup modifier selects the actor to be used in the proxied call
+ /// based on the caller of this handler function
+
+ bool success; /// success flag and returnData for the proxied call are declared at the beginning of the function
+ bytes memory returnData;
+
+ ...
+
+ address target = address(eulerEulerEarnVault);
+
+ _before();
+
+ /// actor.proxy is used to call the protocol, targetting the protocol with the required calldata
+ (success, returnData) = actor.proxy(
+ target,
+ abi.encodeWithSelector(
+ IERC4626.redeem.selector,
+ shares,
+ receiver,
+ address(actor)
+ )
+ );
+
+ if (success) { /// success flag is checked to ensure the call was successful in order to make further checks
+ _after();
+ ...
+ }
+}
+```
+
+The Actor contract is located under `utils/`.
+
+## Handlers
+
+The Handlers contain the main functions exposed to the tooling, allowing it to execute actions through actors. They have been divided in three different categories: `user`, `permissioned` and `simulators`. Each of them implementing different actions and functionalities of the protocol, from user actions to price movement simmulators.
+
+- **Modules**: Handlers that contain functions to execute user actions or permissioned actions in the protocol. These actions are executed by the actors or the Tester contract itself and are used to test the protocol's behavior under different scenarios. All the exposed user functions on these handler category use the `setup` mmodifier showed above. Includes `ERC20Handler`, `ERC4626Handler`, `EulerEarnVaultModuleHandler`, `FeeModuleHandler`, `StrategyModuleHandler` and `WithdrawalQueueModuleHandler`.
+
+- **Simulators**: Handlers that contain functions which simulate real world external changes like donation attacks, asset price movements or flashloans. Includes `DonationAttackHandler` and `NigativeYieldHandler`.
+
+## Hooks
+
+Hooks handle caching of protocol and user values and enforce postconditions across the suite. They allow for modular expansion to add new postconditions, or additional value caching as needed.
+
+- `DefaultBeforeAfterHooks`: Abstract contract that contains the `DefaultVars` struct and custom setter functions, which is essential for caching protocol and user values before and after function calls. It also implements the global postconditions (GPOST) to be invoked in the `HookAggregator::_checkPostConditions` function.
+- `HookAggregator`: This contract aggregates various hooks (only the default one in this case) and invokes the `_checkPostConditions` function to execute the global postconditions.
+
+Values are cached before and after nearly every handler call using `_after` and `_before` functions. The `DefaultVars` struct contains the following fields:
+
+```solidity
+ // Vault Accounting
+ uint256 totalSupply;
+ uint256 totalAssets;
+ uint256 totalAssetsAllocatable;
+ uint256 totalAssetsDeposited;
+ uint256 totalAllocated;
+ // External Accounting
+ uint256 balance;
+ uint256 exchangeRate;
+ uint256 toGulp;
+ // Interest
+ uint256 lastHarvestTimestamp;
+ uint40 lastInterestUpdate;
+ uint40 interestSmearingEnd;
+ uint168 interestLeft;
+ uint256 interestAccrued;
+ // Strategies data
+ mapping(address => Strategy) strategies;
+```
+
+Example: `_checkPostConditions` function, called at the end of the `_after` hook
+
+```solidity
+function _after() internal {
+ _defaultHooksAfter();
+
+ // POST-CONDITIONS
+ _checkPostConditions();
+
+ // RESET
+ targetStrategy = address(0);
+}
+
+/// @notice Postconditions for the handlers
+function _checkPostConditions() internal {
+ // BASE
+ assert_GPOST_BASE_A();
+ assert_GPOST_BASE_B();
+ assert_GPOST_BASE_C();
+ // INTEREST
+ assert_GPOST_INTEREST_A();
+ assert_GPOST_INTEREST_B();
+ // STRATEGY
+ assert_GPOST_STRATEGIES_A();
+ assert_GPOST_STRATEGIES_H();
+}
+```
+
+## Properties
+
+Inside this testing suite, properties are the most important component, everything else works as scaffolding, helpers and setup scripts to ensure the tooling is able to reach the most amount of edge cases possible. The properties are the actual checks that are being run, they are the ones that ensure the protocol is behaving as expected. The properties are divided in two categories: invariants and postconditions.
+
+- **Invariants**: Properties that should always hold true in the system. The tooling executes them in between every transaction to ensure the system is not in an invalid state. They are implemented in the `BaseInvariants` and `ERC4626Invariants` contract following the specs at `InvariantsSpec`, `ERC4626PropertiesSpec` and `NonRevertPropertiesSpec`.
+
+- **Postconditions**: Properties that should hold true after a specific action is executed. There are two types of postconditions: global postconditions (GPOST) and handler specific postconditions (HSPOST).
+ - **GPOST**: Postconditions that are executed after every handler call. They are implemented in the `HookAggregator` contract.
+ - **HSPOST**: Postconditions that are executed after specific handler calls, very similar to unit test assertions. They are usually implemented in the success block at the end of a handler function.
diff --git a/test/enigma-dark-invariants/handlers/euler/EVCHandler.t.sol b/test/enigma-dark-invariants/handlers/euler/EVCHandler.t.sol
new file mode 100644
index 0000000..e979f4f
--- /dev/null
+++ b/test/enigma-dark-invariants/handlers/euler/EVCHandler.t.sol
@@ -0,0 +1,160 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Libraries
+import {EthereumVaultConnector} from "ethereum-vault-connector/EthereumVaultConnector.sol";
+
+// Testing contracts
+import {Actor} from "../../utils/Actor.sol";
+import {BaseHandler, EnumerableSet} from "../../base/BaseHandler.t.sol";
+
+/// @title EVCHandler
+/// @notice Handler test contract for the EVC actions
+abstract contract EVCHandler is BaseHandler {
+ using EnumerableSet for EnumerableSet.AddressSet;
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // GHOST VARAIBLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function setAccountOperator(uint8 i, uint8 j, bool authorised) external setup {
+ bool success;
+ bytes memory returnData;
+
+ address account = _getRandomActor(i);
+
+ address operator = _getRandomActor(j);
+
+ _before();
+ (success, returnData) = actor.proxy(
+ address(evc),
+ abi.encodeWithSelector(EthereumVaultConnector.setAccountOperator.selector, account, operator, authorised)
+ );
+
+ if (success) {
+ _after();
+ } else {
+ revert("EVCHandler: setAccountOperator failed");
+ }
+ }
+
+ // COLLATERAL
+
+ function enableCollateral(uint8 i, uint8 j) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address account = _getRandomActor(i);
+
+ address vaultAddress = _getRandomVault(j);
+
+ _before();
+ (success, returnData) = actor.proxy(
+ address(evc),
+ abi.encodeWithSelector(EthereumVaultConnector.enableCollateral.selector, account, vaultAddress)
+ );
+
+ if (success) {
+ _after();
+ } else {
+ revert("EVCHandler: enableCollateral failed");
+ }
+ }
+
+ function disableCollateral(uint8 i, uint8 j) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address account = _getRandomActor(i);
+
+ address vaultAddress = _getRandomVault(j);
+
+ _before();
+ (success, returnData) = actor.proxy(
+ address(evc),
+ abi.encodeWithSelector(EthereumVaultConnector.disableCollateral.selector, account, vaultAddress)
+ );
+
+ if (success) {
+ _after();
+ } else {
+ revert("EVCHandler: disableCollateral failed");
+ }
+ }
+
+ function reorderCollaterals(uint8 i, uint8 index1, uint8 index2) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address account = _getRandomActor(i);
+
+ _before();
+ (success, returnData) = actor.proxy(
+ address(evc),
+ abi.encodeWithSelector(EthereumVaultConnector.reorderCollaterals.selector, account, index1, index2)
+ );
+
+ if (success) {
+ _after();
+ } else {
+ revert("EVCHandler: disableCollateral failed");
+ }
+ }
+
+ // CONTROLLER
+
+ function enableController(uint8 i, uint8 j) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address account = _getRandomActor(i);
+
+ address vault = _getRandomVault(j);
+
+ _before();
+ (success, returnData) = actor.proxy(
+ address(evc), abi.encodeWithSelector(EthereumVaultConnector.enableController.selector, account, vault)
+ );
+
+ if (success) {
+ _after();
+ } else {
+ revert("EVCHandler: enableController failed");
+ }
+ }
+
+ function disableControllerEVC(uint8 i) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address account = _getRandomActor(i);
+
+ _before();
+ (success, returnData) = actor.proxy(
+ address(evc), abi.encodeWithSelector(EthereumVaultConnector.disableController.selector, account)
+ );
+
+ if (success) {
+ _after();
+ } else {
+ revert("EVCHandler: disableControllerEVC failed");
+ }
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+}
diff --git a/test/enigma-dark-invariants/handlers/interfaces/IERC4626Handler.sol b/test/enigma-dark-invariants/handlers/interfaces/IERC4626Handler.sol
new file mode 100644
index 0000000..6b98f2f
--- /dev/null
+++ b/test/enigma-dark-invariants/handlers/interfaces/IERC4626Handler.sol
@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+interface IERC4626Handler {
+ function withdraw(uint256 assets, uint8 i) external;
+ function redeem(uint256 shares, uint8 i) external;
+}
diff --git a/test/enigma-dark-invariants/handlers/setup/EulerSwapSetupHandler.t.sol b/test/enigma-dark-invariants/handlers/setup/EulerSwapSetupHandler.t.sol
new file mode 100644
index 0000000..04e4321
--- /dev/null
+++ b/test/enigma-dark-invariants/handlers/setup/EulerSwapSetupHandler.t.sol
@@ -0,0 +1,100 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IEulerSwap} from "src/interfaces/IEulerSwap.sol";
+
+// Contracts
+import {EulerSwap} from "src/EulerSwap.sol";
+
+// Libraries
+import "forge-std/console.sol";
+
+// Test Contracts
+import {BaseHandler} from "../../base/BaseHandler.t.sol";
+
+/// @title EulerSwapSetupHandler
+/// @notice Handler test contract for a set of actions
+abstract contract EulerSwapSetupHandler is BaseHandler {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function setupEulerSwap(
+ uint8 leverage,
+ uint112 initialAmount0,
+ uint112 initialAmount1,
+ uint256 fee,
+ IEulerSwap.CurveParams memory curveParams
+ ) public eulerSwapNotDeployed {
+ /// --- CLAMPING PARAMETERS ---
+
+ // Clamp fee to a maximum of 1e18
+ fee = clampBetween(fee, 0, 1e18);
+
+ // Restrict leverage to a maximum of x10
+ leverage = uint8(clampBetween(leverage, MIN_LEVERAGE, MAX_LEVERAGE));
+
+ (initialAmount0, initialAmount1) = _generateBalancedReserves(initialAmount0, initialAmount1, curveParams);
+
+ // Ensure initial deposit amounts are at least 1000 tokens and within leverage limits
+ initialAmount0 = uint112(clampBetween(initialAmount0, 1000e18, type(uint112).max / leverage));
+ initialAmount1 = uint112(clampBetween(initialAmount1, 1000e18, type(uint112).max / leverage));
+
+ // Calculate maximum debt limits based on leverage
+ uint112 debtLimit0 = initialAmount0 * leverage;
+ uint112 debtLimit1 = initialAmount1 * leverage;
+
+ // Clamp price values within a reasonable range
+ curveParams.priceX = clampBetween(curveParams.priceX, 0.1e16, 1e36);
+ curveParams.priceY = clampBetween(curveParams.priceY, 0.1e16, 1e36);
+
+ // Clamp concentration between 0.1e18 and 1e18
+ curveParams.concentrationX = clampBetween(curveParams.concentrationX, 0.1e18, 1e18); // TODO Implement test variants with imbalanced initial pools, reserves don't match equilibrium values - this should verify curve behavior under asymmetric conditions
+ curveParams.concentrationY = clampBetween(curveParams.concentrationY, 0.1e18, 1e18);
+
+ // Check equilibriumReserves are on the curve
+
+ /// --- INITIAL DEPOSITS ---
+
+ // Deposit initial funds into vaults on behalf of the holder
+ vm.prank(holder);
+ eTST.deposit(initialAmount0, holder);
+
+ vm.prank(holder);
+ eTST2.deposit(initialAmount1, holder);
+
+ /// --- DEPLOY EULER SWAP CONTRACT ---
+
+ assertTrue(
+ _createEulerSwap(
+ debtLimit0,
+ debtLimit1,
+ fee,
+ curveParams.priceX,
+ curveParams.priceY,
+ curveParams.concentrationX,
+ curveParams.concentrationY
+ ),
+ "EulerSwapSetupHandler: failed to create EulerSwap"
+ );
+
+ assertTrue(eulerSwap.asset0() == address(assetTST), "EulerSwapSetupHandler: asset0 is not assetTST");
+ assertTrue(eulerSwap.asset1() == address(assetTST2), "EulerSwapSetupHandler: asset1 is not assetTST2");
+ /// --- SETUP ACTORS' TOKEN APPROVALS ---
+
+ // Configure actors' token approvals for the eulerSwap contract
+ address[] memory contracts = new address[](1);
+ contracts[0] = address(eulerSwap);
+
+ _setupActorApprovals(baseAssets, contracts);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // EULER-SWAP SPECIFIC HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+}
diff --git a/test/enigma-dark-invariants/handlers/simulators/DonationAttackHandler.t.sol b/test/enigma-dark-invariants/handlers/simulators/DonationAttackHandler.t.sol
new file mode 100644
index 0000000..e68f141
--- /dev/null
+++ b/test/enigma-dark-invariants/handlers/simulators/DonationAttackHandler.t.sol
@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import {IEVault} from "evk/EVault/IEVault.sol";
+
+// Libraries
+import "forge-std/console.sol";
+
+// Test Contracts
+import {Actor} from "../../utils/Actor.sol";
+import {TestERC20} from "../../utils/mocks/TestERC20.sol";
+import {BaseHandler} from "../../base/BaseHandler.t.sol";
+
+/// @title DonationAttackHandler
+/// @notice Handler test contract for a set of actions
+contract DonationAttackHandler is BaseHandler {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice This function transfers any amount of assets to a contract in the system simulating
+ /// a big range of donation attacks
+ function donateUnderlying(uint256 amount, uint8 i) external eulerSwapDeployed {
+ TestERC20 _token = TestERC20(_getRandomBaseAsset(i));
+
+ address target = address(eulerSwap);
+
+ _token.mint(address(this), amount);
+
+ _token.transfer(target, amount);
+ }
+
+ function donateUnderlyingToVault(uint256 amount, uint8 i) external {
+ address target = _getRandomVault(i);
+
+ TestERC20 _token = TestERC20(IEVault(_getRandomBaseAsset(i)).asset());
+
+ _token.mint(address(this), amount);
+
+ _token.transfer(target, amount);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // OWNER ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+}
diff --git a/test/enigma-dark-invariants/handlers/simulators/PriceOracleHandler.t.sol b/test/enigma-dark-invariants/handlers/simulators/PriceOracleHandler.t.sol
new file mode 100644
index 0000000..cc013ba
--- /dev/null
+++ b/test/enigma-dark-invariants/handlers/simulators/PriceOracleHandler.t.sol
@@ -0,0 +1,31 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+import {BaseHandler} from "../../base/BaseHandler.t.sol";
+
+/// @title PriceOracleHandler
+/// @notice Handler test contract for the PriceOracle actions
+abstract contract PriceOracleHandler is BaseHandler {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // GHOST VARAIBLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice This function simulates changes in asset price
+ function setPrice(uint8 i, uint256 price) external {
+ address baseAsset = _getRandomBaseAsset(i);
+
+ //oracle.setPrice(baseAsset, unitOfAccount, price); TODO implement subtile variations
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+}
diff --git a/test/enigma-dark-invariants/handlers/standard/ERC20Handler.t.sol b/test/enigma-dark-invariants/handlers/standard/ERC20Handler.t.sol
new file mode 100644
index 0000000..c155de1
--- /dev/null
+++ b/test/enigma-dark-invariants/handlers/standard/ERC20Handler.t.sol
@@ -0,0 +1,95 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+
+// Libraries
+import "forge-std/console.sol";
+
+// Test Contracts
+import {Actor} from "../../utils/Actor.sol";
+import {BaseHandler} from "../../base/BaseHandler.t.sol";
+
+/// @title ERC20Handler
+/// @notice Handler test contract for a set of actions
+abstract contract ERC20Handler is BaseHandler {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function approve(uint256 amount, uint8 i, uint8 j) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address spender = _getRandomActor(i);
+
+ // Get one of the vaults randomly
+ address target = _getRandomVault(j);
+
+ _before();
+ (success, returnData) = actor.proxy(target, abi.encodeWithSelector(IERC20.approve.selector, spender, amount));
+
+ if (success) {
+ _after();
+ } else {
+ revert("ERC20Handler: approve failed");
+ }
+ }
+
+ function transfer(uint256 amount, uint8 i, uint8 j) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address to = _getRandomActor(i);
+
+ // Get one of the vaults randomly
+ address target = _getRandomVault(j);
+
+ _before();
+ (success, returnData) = actor.proxy(target, abi.encodeWithSelector(IERC20.transfer.selector, to, amount));
+
+ if (success) {
+ _after();
+ } else {
+ revert("ERC20Handler: transfer failed");
+ }
+ }
+
+ function transferFrom(uint256 amount, uint8 i, uint8 j, uint8 k) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address from = _getRandomActor(i);
+ // Get one of the three actors randomly
+ address to = _getRandomActor(j);
+
+ // Get one of the vaults randomly
+ address target = _getRandomVault(k);
+
+ _before();
+ (success, returnData) =
+ actor.proxy(target, abi.encodeWithSelector(IERC20.transferFrom.selector, from, to, amount));
+
+ if (success) {
+ _after();
+ } else {
+ revert("ERC20Handler: transferFrom failed");
+ }
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // OWNER ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+}
diff --git a/test/enigma-dark-invariants/handlers/standard/ERC4626Handler.t.sol b/test/enigma-dark-invariants/handlers/standard/ERC4626Handler.t.sol
new file mode 100644
index 0000000..e989d99
--- /dev/null
+++ b/test/enigma-dark-invariants/handlers/standard/ERC4626Handler.t.sol
@@ -0,0 +1,122 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IERC20} from "openzeppelin-contracts/token/ERC20/IERC20.sol";
+import {IERC4626} from "openzeppelin-contracts/interfaces/IERC4626.sol";
+import {IEVault} from "evk/EVault/IEVault.sol";
+
+// Libraries
+import "forge-std/console.sol";
+
+// Test Contracts
+import {Actor} from "../../utils/Actor.sol";
+import {BaseHandler} from "../../base/BaseHandler.t.sol";
+
+/// @title ERC4626Handler
+/// @notice Handler test contract for a set of actions
+abstract contract ERC4626Handler is BaseHandler {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function deposit(uint256 assets, uint8 i, uint8 j) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address receiver = _getRandomActor(i);
+
+ // Get one of the vaults randomly
+ address target = _getRandomVault(j);
+
+ _before();
+ (success, returnData) = actor.proxy(target, abi.encodeWithSelector(IERC4626.deposit.selector, assets, receiver));
+
+ if (success) {
+ _after();
+ } else {
+ revert("ERC4626Handler: deposit failed");
+ }
+ }
+
+ function mint(uint256 shares, uint8 i, uint8 j) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address receiver = _getRandomActor(i);
+
+ // Get one of the vaults randomly
+ address target = _getRandomVault(j);
+
+ _before();
+ (success, returnData) = actor.proxy(target, abi.encodeWithSelector(IERC4626.mint.selector, shares, receiver));
+
+ if (success) {
+ _after();
+ } else {
+ revert("ERC4626Handler: mint failed");
+ }
+ }
+
+ function withdraw(uint256 assets, uint8 i, uint8 j) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address receiver = _getRandomActor(i);
+
+ // Get one of the vaults randomly
+ address target = _getRandomVault(j);
+
+ _before();
+ (success, returnData) =
+ actor.proxy(target, abi.encodeWithSelector(IERC4626.withdraw.selector, assets, receiver, address(actor)));
+
+ if (success) {
+ _after();
+ } else {
+ revert("ERC4626Handler: withdraw failed");
+ }
+ }
+
+ function redeem(uint256 shares, uint8 i, uint8 j) external setup {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ address receiver = _getRandomActor(i);
+
+ // Get one of the vaults randomly
+ address target = _getRandomVault(j);
+
+ _before();
+ (success, returnData) =
+ actor.proxy(target, abi.encodeWithSelector(IERC4626.redeem.selector, shares, receiver, address(actor)));
+
+ if (success) {
+ _after();
+ } else {
+ revert("ERC4626Handler: redeem failed");
+ }
+ }
+
+ function skim(uint8 i, uint8 j) external {
+ // Get one of the three actors randomly
+ address receiver = _getRandomActor(i);
+
+ // Get one of the vaults randomly
+ address target = _getRandomVault(j);
+
+ IEVault(target).skim(type(uint256).max, receiver);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+}
diff --git a/test/enigma-dark-invariants/handlers/swap/EulerSwapHandler.t.sol b/test/enigma-dark-invariants/handlers/swap/EulerSwapHandler.t.sol
new file mode 100644
index 0000000..8cb4011
--- /dev/null
+++ b/test/enigma-dark-invariants/handlers/swap/EulerSwapHandler.t.sol
@@ -0,0 +1,122 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import {IEulerSwap} from "src/interfaces/IEulerSwap.sol";
+
+// Libraries
+import "forge-std/console.sol";
+
+// Test Contracts
+import {Actor} from "../../utils/Actor.sol";
+import {BaseHandler} from "../../base/BaseHandler.t.sol";
+
+/// @title EulerSwapHandler
+/// @notice Handler test contract for a set of actions
+abstract contract EulerSwapHandler is BaseHandler {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ address roundtripSwapActor;
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function activate() public setup eulerSwapDeployed {
+ eulerSwap.activate();
+ }
+
+ function swap(uint256 amount0Out, uint256 amount1Out, uint256 amount0In, uint256 amount1In, uint8 i)
+ public
+ setup
+ eulerSwapDeployed
+ skimAll
+ {
+ bool success;
+ bytes memory returnData;
+
+ // Get one of the three actors randomly
+ receiver = roundtripSwapActor == address(0) ? _getRandomActor(i) : roundtripSwapActor;
+
+ address target = address(eulerSwap);
+
+ //if (amount0Out >= 2 ether && amount1In >= 10 ether) assert(false);
+
+ //require(amount0Out > 1 ether || amount1Out > 1 ether, "EulerSwapHandler: Invalid amount out");
+
+ if (amount0In > 0) {
+ _transferByActor(address(assetTST), address(eulerSwap), amount0In);
+ }
+
+ if (amount1In > 0) {
+ _transferByActor(address(assetTST2), address(eulerSwap), amount1In);
+ }
+
+ _before();
+ (success, returnData) =
+ actor.proxy(target, abi.encodeWithSelector(IEulerSwap.swap.selector, amount0Out, amount1Out, receiver, ""));
+
+ if (success) {
+ _after();
+
+ // POSTCONDITIONS
+ _eulerSwapPostconditions(amount0Out, amount1Out, amount0In, amount1In);
+ } else {
+ revert("EulerSwapHandler: swap failed");
+ }
+
+ delete receiver;
+ }
+
+ function roundtripSwap(uint256 amount, uint8 i) external setup eulerSwapDeployed {
+ uint256 amount0Out;
+ uint256 amount1Out;
+ uint256 amount0In;
+ uint256 amount1In;
+
+ IERC20 assetTSTIn = IERC20(_getRandomBaseAsset(i));
+ roundtripSwapActor = address(actor);
+
+ // SWAP 1
+
+ uint256 actorInBalanceBefore = assetTSTIn.balanceOf(roundtripSwapActor);
+
+ if (i % 2 == 0) {
+ // token0 -> token1 case
+ amount0In = amount;
+ amount1Out = periphery.quoteExactInput(address(eulerSwap), address(assetTST), address(assetTST2), amount0In);
+ } else {
+ // token1 -> token0 case
+ amount1In = amount;
+ amount0Out = periphery.quoteExactInput(address(eulerSwap), address(assetTST2), address(assetTST), amount1In);
+ }
+
+ swap(amount0Out, amount1Out, amount0In, amount1In, 0);
+
+ // SWAP 2
+
+ if (i % 2 == 0) {
+ // token0 -> token1 case
+ amount1In = amount1Out;
+ amount0Out = periphery.quoteExactInput(address(eulerSwap), address(assetTST2), address(assetTST), amount1In);
+ delete amount1Out; // @audit seems like input amounts are kinda delayed check uniswap v2
+ delete amount0In;
+ } else {
+ // token1 -> token0 case
+ amount0In = amount0Out;
+ amount1Out = periphery.quoteExactInput(address(eulerSwap), address(assetTST), address(assetTST2), amount0In);
+ delete amount0Out;
+ delete amount1In;
+ }
+
+ swap(amount0Out, amount1Out, amount0In, amount1In, 0);
+
+ uint256 actorInBalanceAfter = assetTSTIn.balanceOf(roundtripSwapActor);
+
+ /// @dev HSPOST_SWAP_B
+ assertLe(actorInBalanceAfter, actorInBalanceBefore, HSPOST_SWAP_B);
+ }
+}
diff --git a/test/enigma-dark-invariants/handlers/swap/EulerSwapPeripheryHandler.t.sol b/test/enigma-dark-invariants/handlers/swap/EulerSwapPeripheryHandler.t.sol
new file mode 100644
index 0000000..e51f145
--- /dev/null
+++ b/test/enigma-dark-invariants/handlers/swap/EulerSwapPeripheryHandler.t.sol
@@ -0,0 +1,164 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import {IEulerSwapPeriphery} from "src/interfaces/IEulerSwapPeriphery.sol";
+
+// Libraries
+import "forge-std/console.sol";
+
+// Test Contracts
+import {Actor} from "../../utils/Actor.sol";
+import {BaseHandler} from "../../base/BaseHandler.t.sol";
+
+/// @title EulerSwapPeripheryHandler
+/// @notice Handler test contract for a set of actions
+abstract contract EulerSwapPeripheryHandler is BaseHandler {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE VARIABLES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // ACTIONS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function swapExactIn(uint256 amountIn, uint256 amountOutMin, bool dir) public setup eulerSwapDeployed skimAll {
+ bool success;
+ receiver = address(actor);
+
+ (address tokenIn, address tokenOut) = _getAssetsByDir(dir);
+ (uint256 tokenInLimit, uint256 tokenOutLimit) = periphery.getLimits(address(eulerSwap), tokenIn, tokenOut);
+
+ address target = address(periphery);
+
+ _before();
+ (success,) = actor.proxy(
+ target,
+ abi.encodeWithSelector(
+ IEulerSwapPeriphery.swapExactIn.selector, address(eulerSwap), tokenIn, tokenOut, amountIn, amountOutMin
+ )
+ );
+
+ if (success) {
+ _after();
+
+ if (dir) {
+ _eulerSwapPostconditions(0, amountOutMin, amountIn, 0);
+ } else {
+ _eulerSwapPostconditions(amountOutMin, 0, 0, amountIn);
+ }
+
+ // HSPOST
+ assertLe(amountIn, tokenInLimit, HSPOST_SWAP_D);
+ assertLe(amountOutMin, tokenOutLimit, HSPOST_SWAP_D);
+ } else {
+ revert("EulerSwapPeripheryHandler: swapExactIn failed");
+ }
+
+ delete receiver;
+ }
+
+ function swapExactOut(uint256 amountOut, uint256 amountInMax, bool dir) public setup eulerSwapDeployed skimAll {
+ bool success;
+ receiver = address(actor);
+
+ (address tokenIn, address tokenOut) = _getAssetsByDir(dir);
+ (uint256 tokenInLimit, uint256 tokenOutLimit) = periphery.getLimits(address(eulerSwap), tokenIn, tokenOut);
+
+ address target = address(periphery);
+
+ _before();
+ (success,) = actor.proxy(
+ target,
+ abi.encodeWithSelector(
+ IEulerSwapPeriphery.swapExactOut.selector, address(eulerSwap), tokenIn, tokenOut, amountOut, amountInMax
+ )
+ );
+
+ if (success) {
+ _after();
+
+ if (dir) {
+ _eulerSwapPostconditions(0, amountOut, amountInMax, 0);
+ } else {
+ _eulerSwapPostconditions(amountOut, 0, 0, amountInMax);
+ }
+
+ // HSPOST
+ assertLe(amountOut, tokenOutLimit, HSPOST_SWAP_D);
+ assertLe(amountInMax, tokenInLimit, HSPOST_SWAP_D);
+ } else {
+ revert("EulerSwapPeripheryHandler: swapExactOut failed");
+ }
+
+ delete receiver;
+ }
+
+ function quoteExactInput(uint256 amountIn, bool dir) external setup eulerSwapDeployed {
+ bool success;
+
+ (address tokenIn, address tokenOut) = _getAssetsByDir(dir);
+
+ uint256 amountOutMin;
+
+ try periphery.quoteExactInput(address(eulerSwap), tokenIn, tokenOut, amountIn) returns (uint256 amountOutMin_) {
+ amountOutMin = amountOutMin_;
+
+ if (amountIn > IERC20(tokenIn).balanceOf(address(actor))) {
+ _mint(tokenIn, address(actor), amountIn);
+ }
+ } catch Error(string memory) {
+ // HSPOST
+ assertTrue(false, NR_QUOTE_A);
+ }
+
+ address target = address(periphery);
+
+ _before();
+ (success,) = actor.proxy(
+ target,
+ abi.encodeWithSelector(
+ IEulerSwapPeriphery.swapExactIn.selector, address(eulerSwap), tokenIn, tokenOut, amountIn, amountOutMin
+ )
+ );
+ _after();
+
+ // HSPOST
+ assertTrue(success, HSPOST_SWAP_E);
+ }
+
+ function quoteExactOutput(uint256 amountOut, bool dir) external setup eulerSwapDeployed {
+ bool success;
+
+ (address tokenIn, address tokenOut) = _getAssetsByDir(dir);
+
+ uint256 amountInMax;
+
+ try periphery.quoteExactOutput(address(eulerSwap), tokenIn, tokenOut, amountOut) returns (uint256 amountInMax_)
+ {
+ amountInMax = amountInMax_;
+
+ if (amountInMax > IERC20(tokenIn).balanceOf(address(actor))) {
+ _mint(tokenIn, address(actor), amountInMax);
+ }
+ } catch Error(string memory) {
+ // HSPOST
+ assertTrue(false, NR_QUOTE_B);
+ }
+
+ address target = address(periphery);
+
+ _before();
+ (success,) = actor.proxy(
+ target,
+ abi.encodeWithSelector(
+ IEulerSwapPeriphery.swapExactOut.selector, address(eulerSwap), tokenIn, tokenOut, amountOut, amountInMax
+ )
+ );
+ _after();
+
+ // HSPOST
+ assertTrue(success, HSPOST_SWAP_E);
+ }
+}
diff --git a/test/enigma-dark-invariants/helpers/extended/.gitkeep b/test/enigma-dark-invariants/helpers/extended/.gitkeep
new file mode 100644
index 0000000..e69de29
diff --git a/test/enigma-dark-invariants/hooks/DefaultBeforeAfterHooks.t.sol b/test/enigma-dark-invariants/hooks/DefaultBeforeAfterHooks.t.sol
new file mode 100644
index 0000000..0eac5cd
--- /dev/null
+++ b/test/enigma-dark-invariants/hooks/DefaultBeforeAfterHooks.t.sol
@@ -0,0 +1,103 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Libraries
+import "forge-std/console.sol";
+
+// Test Contracts
+import {BaseHooks} from "../base/BaseHooks.t.sol";
+
+// Interfaces
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import {IERC4626Handler} from "../handlers/interfaces/IERC4626Handler.sol";
+
+/// @title Default Before After Hooks
+/// @notice Helper contract for before and after hooks
+/// @dev This contract is inherited by handlers
+abstract contract DefaultBeforeAfterHooks is BaseHooks {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STRUCTS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ struct User {
+ uint256 assetTSTBalance;
+ uint256 assetTST2Balance;
+ }
+
+ struct DefaultVars {
+ // Holder
+ int256 holderNAV;
+ uint256 holderETSTAssets;
+ uint256 holderETST2Assets;
+ uint256 holderETSTDebt;
+ uint256 holderETST2Debt;
+ mapping(address => User) users;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HOOKS STORAGE //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ DefaultVars defaultVarsBefore;
+ DefaultVars defaultVarsAfter;
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // SETUP //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// @notice Default hooks setup
+ function _setUpDefaultHooks() internal {}
+
+ /// @notice Helper to initialize storage arrays of default vars
+ function _setUpDefaultVars(DefaultVars storage _dafaultVars) internal {}
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // HOOKS //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function _defaultHooksBefore() internal {
+ // Default values
+ _setDefaultValues(defaultVarsBefore);
+ // Health & user account data
+ _setUserValues(defaultVarsBefore);
+ }
+
+ function _defaultHooksAfter() internal {
+ // Default values
+ _setDefaultValues(defaultVarsAfter);
+ // Health & user account data
+ _setUserValues(defaultVarsAfter);
+ }
+
+ /*/////////////////////////////////////////////////////////////////////////////////////////////
+ // HELPERS //
+ /////////////////////////////////////////////////////////////////////////////////////////////*/
+
+ function _setDefaultValues(DefaultVars storage _defaultVars) internal {
+ // Holder
+ _defaultVars.holderNAV = _getHolderNAV();
+ _defaultVars.holderETSTAssets = eTST.convertToAssets(eTST.balanceOf(holder));
+ /// @dev adding eulerSwap balance to take donations into account
+ _defaultVars.holderETST2Assets = eTST2.convertToAssets(eTST2.balanceOf(holder));
+ _defaultVars.holderETSTDebt = eTST.debtOf(holder);
+ _defaultVars.holderETST2Debt = eTST2.debtOf(holder);
+ }
+
+ function _setUserValues(DefaultVars storage _defaultVars) internal {
+ for (uint256 i; i < actorAddresses.length; i++) {
+ address actorAddress_ = actorAddresses[i];
+ _setUserValuesPerActor(_defaultVars.users[actorAddress_], actorAddress_);
+ }
+ }
+
+ function _setUserValuesPerActor(User storage _user, address _actorAddress) internal {
+ _user.assetTSTBalance = assetTST.balanceOf(_actorAddress);
+ _user.assetTST2Balance = assetTST2.balanceOf(_actorAddress);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // POST CONDITIONS: BASE //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function assert_GPOST_BASE_A() internal {}
+}
diff --git a/test/enigma-dark-invariants/hooks/HookAggregator.t.sol b/test/enigma-dark-invariants/hooks/HookAggregator.t.sol
new file mode 100644
index 0000000..2f4df46
--- /dev/null
+++ b/test/enigma-dark-invariants/hooks/HookAggregator.t.sol
@@ -0,0 +1,55 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Hook Contracts
+import {DefaultBeforeAfterHooks} from "./DefaultBeforeAfterHooks.t.sol";
+
+/// @title HookAggregator
+/// @notice Helper contract to aggregate all before / after hook contracts, inherited on each handler
+abstract contract HookAggregator is DefaultBeforeAfterHooks {
+ /// @notice Initializer for the hooks
+ function _setUpHooks() internal {
+ _setUpDefaultHooks();
+ }
+
+ /*/////////////////////////////////////////////////////////////////////////////////////////////
+ // HOOKS //
+ /////////////////////////////////////////////////////////////////////////////////////////////*/
+
+ /// @notice Modular hook selector, per module
+ function _before() internal {
+ _defaultHooksBefore();
+ }
+
+ /// @notice Modular hook selector, per module
+ function _after() internal {
+ _defaultHooksAfter();
+
+ // POST-CONDITIONS
+ _checkPostConditions();
+ }
+
+ /*/////////////////////////////////////////////////////////////////////////////////////////////
+ // POSTCONDITION CHECKS //
+ /////////////////////////////////////////////////////////////////////////////////////////////*/
+
+ /// @notice Postconditions for the handlers
+ function _checkPostConditions() internal {
+ // Check general postconditions
+ _checkGeneralPostConditions();
+
+ // Check user postconditions
+ for (uint256 i; i < actorAddresses.length; i++) {
+ _checkUserPostConditions(actorAddresses[i]);
+ }
+ }
+
+ function _checkGeneralPostConditions() internal {
+ // Check general postconditions
+ }
+
+ /// @notice Postconditions for each user
+ function _checkUserPostConditions(address user) internal {
+ // Check user postconditions
+ }
+}
diff --git a/test/enigma-dark-invariants/invariants/BaseInvariants.t.sol b/test/enigma-dark-invariants/invariants/BaseInvariants.t.sol
new file mode 100644
index 0000000..a345675
--- /dev/null
+++ b/test/enigma-dark-invariants/invariants/BaseInvariants.t.sol
@@ -0,0 +1,82 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Libraries
+
+// Interfaces
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import {IEVault} from "evk/EVault/IEVault.sol";
+
+// Contracts
+import {HandlerAggregator} from "../HandlerAggregator.t.sol";
+
+import "forge-std/console.sol";
+
+/// @title BaseInvariants
+/// @notice Implements Invariants for the protocol
+/// @dev Inherits HandlerAggregator to check actions in assertion testing mode
+abstract contract BaseInvariants is HandlerAggregator {
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // CORE //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function assert_INV_CORE_A() internal {
+ assertFalse(eTST.debtOf(holder) != 0 && eTST2.debtOf(holder) != 0, INV_CORE_A);
+ }
+
+ function assert_INV_CORE_B() internal {
+ address[] memory controllers = evc.getControllers(holder);
+
+ address controller = controllers[0];
+
+ (uint256 collateralValue, uint256 liabilityValue) =
+ IEVault(controller).accountLiquidity(eulerSwap.eulerAccount(), false);
+
+ assertTrue(collateralValue > liabilityValue, INV_CORE_B);
+ }
+
+ function assert_INV_CORE_C() internal {
+ // The curve invariant must always hold
+ (uint112 reserve0, uint112 reserve1,) = eulerSwap.getReserves();
+ assertTrue(eulerSwap.verify(reserve0, reserve1), INV_CORE_C);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE MANAGEMENT //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ function assert_INV_STATE_A() internal {
+ (,, uint32 status) = eulerSwap.getReserves();
+
+ assertTrue(status == 0 || status == 1 || status == 2, INV_STATE_A);
+ }
+
+ function assert_INV_STATE_B() internal {
+ assertTrue(eulerSwap.asset0() < eulerSwap.asset1(), INV_STATE_B);
+ }
+
+ function assert_INV_STATE_C() internal {
+ // Controller should be properly enabled/disabled
+ bool controller0 = evc.isControllerEnabled(eulerSwap.eulerAccount(), address(eTST));
+ bool controller1 = evc.isControllerEnabled(eulerSwap.eulerAccount(), address(eTST2));
+
+ // If there's debt, controller should be enabled
+ assertTrue(
+ (eTST.debtOf(eulerSwap.eulerAccount()) == 0 || controller0)
+ && (eTST2.debtOf(eulerSwap.eulerAccount()) == 0 || controller1),
+ INV_STATE_C
+ );
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // DEBT LIMIT //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ function assert_INV_DL_A() internal {
+ // Total borrowed amount should never exceed leverage * initial reserves
+ uint256 totalDebt0 = eTST.debtOf(eulerSwap.eulerAccount());
+ uint256 totalDebt1 = eTST2.debtOf(eulerSwap.eulerAccount());
+
+ assertLe(totalDebt0, uint256(eulerSwap.equilibriumReserve0()) * MAX_LEVERAGE, INV_DL_A);
+ assertLe(totalDebt1, uint256(eulerSwap.equilibriumReserve1()) * MAX_LEVERAGE, INV_DL_A);
+ }
+}
diff --git a/test/enigma-dark-invariants/specs/InvariantsSpec.t.sol b/test/enigma-dark-invariants/specs/InvariantsSpec.t.sol
new file mode 100644
index 0000000..9e3286b
--- /dev/null
+++ b/test/enigma-dark-invariants/specs/InvariantsSpec.t.sol
@@ -0,0 +1,57 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+/// @title InvariantsSpec
+/// @notice Invariants specification for the protocol
+/// @dev Contains pseudo code and description for the invariant properties in the protocol
+abstract contract InvariantsSpec {
+ /*/////////////////////////////////////////////////////////////////////////////////////////////
+ // PROPERTY TYPES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// - INVARIANTS (INV):
+ /// - Properties that should always hold true in the system.
+ /// - Implemented in the /invariants folder.
+
+ /////////////////////////////////////////////////////////////////////////////////////////////*/
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // CORE //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ string constant INV_CORE_A = "INV_CORE_A: At most one of vault0 or vault1 has debt (unless the CDP is under water)";
+
+ string constant INV_CORE_B = "INV_CORE_B: Account should never be liquidatable";
+
+ string constant INV_CORE_C = "INV_CORE_C: The curve invariant must always hold";
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // STATE MANAGEMENT //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ string constant INV_STATE_A = "INV_STATE_A: Status should only transition in valid ways";
+
+ string constant INV_STATE_B = "INV_STATE_B: Asset addresses should maintain correct ordering";
+
+ string constant INV_STATE_C = "INV_STATE_C: If there's debt, controller should be enabled";
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // DEBT LIMIT //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ string constant INV_DL_A = "INV_DL_A: Leverage should not exceed debt limits";
+
+ string constant INV_DL_B = "INV_DL_B: Total borrowed amount should never exceed leverage * initial reserves"; // TODO
+
+ // TODO: Implement invariants based on ChainSecurity report formulas
+ // TODO: Implement invariants for LTV checks from ChainSecurity report -> no implemented, checked with liquidation invariant
+ // TODO: Implement invariants for liquidation checks from ChainSecurity report -> X
+ // TODO: Implement invariants for reserve desynchronization from ChainSecurity report -> NO
+ // TODO: Implement invariant to ensure debt never exceeds the debt limit -> X
+ // TODO: Implement invariants from the team call notes -> TODO
+ // TODO: Review the trust model of the protocol as outlined in the ChainSecurity report -> TODO
+ // TODO: Review the binary search implementation -> TODO
+ // TODO: Implement check for rounding error amplification (5.5) -> TODO
+ // TODO: Implement check to prevent Donation Attack resulting in DoS (5.1), ensuring the "quote" rule makes swap always succeed -> TODO
+ // TODO: Implement invariant for relation between f and f inverse -> TODO
+}
diff --git a/test/enigma-dark-invariants/specs/NonRevertPropertiesSpec.t.sol b/test/enigma-dark-invariants/specs/NonRevertPropertiesSpec.t.sol
new file mode 100644
index 0000000..781ad45
--- /dev/null
+++ b/test/enigma-dark-invariants/specs/NonRevertPropertiesSpec.t.sol
@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+/// @title NonRevertPropertiesSpec
+/// @notice Properties specification for the protocol
+/// @dev Contains pseudo code and description for the invariant properties in the protocol
+abstract contract NonRevertPropertiesSpec {
+ /*/////////////////////////////////////////////////////////////////////////////////////////////
+ // PROPERTY TYPES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// - NON REVERT (NR):
+ /// - Properties that assert a specific function should never revert, or only revert under
+ /// certain defined conditions.
+
+ /////////////////////////////////////////////////////////////////////////////////////////////*/
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // BASE //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ string constant NR_QUOTE_A = "NR_QUOTE_A: quoteExactInput should not revert";
+
+ string constant NR_QUOTE_B = "NR_QUOTE_B: quoteExactOutput should not revert";
+}
diff --git a/test/enigma-dark-invariants/specs/PostconditionsSpec.t.sol b/test/enigma-dark-invariants/specs/PostconditionsSpec.t.sol
new file mode 100644
index 0000000..68e70e5
--- /dev/null
+++ b/test/enigma-dark-invariants/specs/PostconditionsSpec.t.sol
@@ -0,0 +1,66 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+/// @title PostconditionsSpec
+/// @notice Postcoditions specification for the protocol
+/// @dev Contains pseudo code and description for the postcondition properties in the protocol
+abstract contract PostconditionsSpec {
+ /*/////////////////////////////////////////////////////////////////////////////////////////////
+ // PROPERTY TYPES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ /// - POSTCONDITIONS:
+ /// - Properties that should hold true after an action is executed.
+ /// - Implemented in the /hooks and /handlers folders.
+ /// - There are two types of POSTCONDITIONS:
+ /// - GLOBAL POSTCONDITIONS (GPOST):
+ /// - Properties that should always hold true after any action is executed.
+ /// - Checked in the `_checkPostConditions` function within the HookAggregator contract.
+ /// - HANDLER-SPECIFIC POSTCONDITIONS (HSPOST):
+ /// - Properties that should hold true after a specific action is executed in a specific context.
+ /// - Implemented within each handler function, under the HANDLER-SPECIFIC POSTCONDITIONS section.
+
+ /////////////////////////////////////////////////////////////////////////////////////////////*/
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // SWAP //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ string constant HSPOST_SWAP_A = "HSPOST_SWAP_A: Holder's NAV should increase monotonically";
+
+ string constant HSPOST_SWAP_B = "HSPOST_SWAP_B: Swapping back and forth does not lead to a profit";
+
+ string constant HSPOST_SWAP_C = "HSPOST_SWAP_C: User should receive the amount out specified after a swap";
+
+ string constant HSPOST_SWAP_D = "HSPOST_SWAP_D: Successful swaps are always inside the swap limits";
+
+ string constant HSPOST_SWAP_E = "HSPOST_SWAP_E: Swaps with quoted amounts should always be successful";
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // RESERVES //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ string constant HSPOST_RESERVES_A =
+ "HSPOST_RESERVES_A: When positive delta exists, debt must decrease by min(delta, previous_debt)";
+
+ string constant HSPOST_RESERVES_B =
+ "HSPOST_RESERVES_B: When positive delta is greater than previous debt, debt is fully repaid";
+
+ string constant HSPOST_RESERVES_C =
+ "HSPOST_RESERVES_C: When positive delta is greater than previous debt, the excess delta is added to assets";
+
+ string constant HSPOST_RESERVES_D =
+ "HSPOST_RESERVES_D: When negative delta exists, assets must decrease by min(delta, previous_assets)";
+
+ string constant HSPOST_RESERVES_E =
+ "HSPOST_RESERVES_E: When negative delta is greater than previous assets, assets are fully depleted";
+
+ string constant HSPOST_RESERVES_F =
+ "HSPOST_RESERVES_F: When negative delta is greater than previous assets, the deficit is added to debt";
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+ // DEBT //
+ ///////////////////////////////////////////////////////////////////////////////////////////////
+
+ string constant HSPOST_DEBT_A = "HSPOST_DEBT_A: Debt on an asset after a swap should never exceed the debt limit";
+}
diff --git a/test/enigma-dark-invariants/utils/Actor.sol b/test/enigma-dark-invariants/utils/Actor.sol
new file mode 100644
index 0000000..5b24cb8
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/Actor.sol
@@ -0,0 +1,60 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+// Interfaces
+import {IERC20} from "forge-std/interfaces/IERC20.sol";
+
+/// @notice Proxy contract for invariant suite actors to avoid aTester calling contracts
+contract Actor {
+ /// @notice list of tokens to approve
+ address[] internal tokens;
+ /// @notice list of contracts to approve tokens to
+ address[] internal contracts;
+
+ constructor(address[] memory _tokens, address[] memory _contracts) payable {
+ tokens = _tokens;
+ contracts = _contracts;
+ for (uint256 i = 0; i < tokens.length; i++) {
+ for (uint256 j = 0; j < contracts.length; j++) {
+ IERC20(tokens[i]).approve(contracts[j], type(uint256).max);
+ }
+ }
+ }
+
+ /// @notice Helper function to proxy a call to a target contract, used to avoid Tester calling contracts
+ function proxy(address _target, bytes memory _calldata) public returns (bool success, bytes memory returnData) {
+ (success, returnData) = address(_target).call(_calldata);
+
+ handleAssertionError(success, returnData);
+ }
+
+ /// @notice Helper function to proxy a call and value to a target contract, used to avoid Tester calling contracts
+ function proxy(address _target, bytes memory _calldata, uint256 value)
+ public
+ returns (bool success, bytes memory returnData)
+ {
+ (success, returnData) = address(_target).call{value: value}(_calldata);
+
+ handleAssertionError(success, returnData);
+ }
+
+ /// @notice Checks if a call failed due to an assertion error and propagates the error if found.
+ /// @param success Indicates whether the call was successful.
+ /// @param returnData The data returned from the call.
+ function handleAssertionError(bool success, bytes memory returnData) internal pure {
+ if (!success && returnData.length == 36) {
+ bytes4 selector;
+ uint256 code;
+ assembly {
+ selector := mload(add(returnData, 0x20))
+ code := mload(add(returnData, 0x24))
+ }
+
+ if (selector == bytes4(0x4e487b71) && code == 1) {
+ assert(false);
+ }
+ }
+ }
+
+ receive() external payable {}
+}
diff --git a/test/enigma-dark-invariants/utils/CoverageChecker.sol b/test/enigma-dark-invariants/utils/CoverageChecker.sol
new file mode 100644
index 0000000..0c46295
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/CoverageChecker.sol
@@ -0,0 +1,57 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+abstract contract CoverageChecker {
+ function _checkCoverage(uint256 coverage, uint256 low, uint256 high) internal pure returns (string memory) {
+ // Validate the range
+ require(high > low, "High must be greater than Low.");
+ require(coverage >= low && coverage <= high, "Coverage must be within the provided range.");
+
+ // Calculate the size of each threshold interval
+ uint256 range = high - low;
+ uint256 step = range / 20; // Divide the range into 20 thresholds
+
+ // Check which threshold the coverage falls into
+ if (coverage <= low + step) {
+ return "Threshold 1: Very Low Coverage";
+ } else if (coverage <= low + step * 2) {
+ return "Threshold 2: Critical Low Coverage";
+ } else if (coverage <= low + step * 3) {
+ return "Threshold 3: Low Coverage";
+ } else if (coverage <= low + step * 4) {
+ return "Threshold 4: Below Average Coverage";
+ } else if (coverage <= low + step * 5) {
+ return "Threshold 5: Near Average Coverage";
+ } else if (coverage <= low + step * 6) {
+ return "Threshold 6: Average Coverage";
+ } else if (coverage <= low + step * 7) {
+ return "Threshold 7: Slightly Above Average";
+ } else if (coverage <= low + step * 8) {
+ return "Threshold 8: Moderate Coverage";
+ } else if (coverage <= low + step * 9) {
+ return "Threshold 9: Good Coverage";
+ } else if (coverage <= low + step * 10) {
+ return "Threshold 10: Very Good Coverage";
+ } else if (coverage <= low + step * 11) {
+ return "Threshold 11: Excellent Coverage";
+ } else if (coverage <= low + step * 12) {
+ return "Threshold 12: Strong Coverage";
+ } else if (coverage <= low + step * 13) {
+ return "Threshold 13: High Coverage";
+ } else if (coverage <= low + step * 14) {
+ return "Threshold 14: Very High Coverage";
+ } else if (coverage <= low + step * 15) {
+ return "Threshold 15: Outstanding Coverage";
+ } else if (coverage <= low + step * 16) {
+ return "Threshold 16: Exceptional Coverage";
+ } else if (coverage <= low + step * 17) {
+ return "Threshold 17: Nearly Perfect Coverage";
+ } else if (coverage <= low + step * 18) {
+ return "Threshold 18: Almost Full Coverage";
+ } else if (coverage <= low + step * 19) {
+ return "Threshold 19: Near Maximum Coverage";
+ } else {
+ return "Threshold 20: Maximum Coverage Achieved!";
+ }
+ }
+}
diff --git a/test/enigma-dark-invariants/utils/Create2Factory.sol b/test/enigma-dark-invariants/utils/Create2Factory.sol
new file mode 100644
index 0000000..1d41779
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/Create2Factory.sol
@@ -0,0 +1,32 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract Create2Factory {
+ // Fallback function to handle the creation of a new contract
+ fallback() external payable {
+ // Copy calldata into memory, excluding the first 32 bytes
+ assembly {
+ calldatacopy(0, 32, sub(calldatasize(), 32))
+
+ // Create the new contract with CREATE2
+ let result := create2(callvalue(), 0, sub(calldatasize(), 32), calldataload(0))
+
+ // Check if contract creation was successful
+ if iszero(result) { revert(0, 0) }
+
+ // Return the address of the newly created contract
+ mstore(0, result)
+ return(12, 20)
+ }
+ }
+}
+
+contract FactoryDeployer {
+ function deployFactory() public returns (address child) {
+ bytes memory bytecode =
+ hex"604580600e600039806000f350fe7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe03601600081602082378035828234f58015156039578182fd5b8082525050506014600cf3";
+ assembly {
+ child := create(0, add(bytecode, 0x20), mload(bytecode))
+ }
+ }
+}
diff --git a/test/enigma-dark-invariants/utils/DeployPermit2.sol b/test/enigma-dark-invariants/utils/DeployPermit2.sol
new file mode 100644
index 0000000..3fe83dc
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/DeployPermit2.sol
@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.17;
+
+/// @notice helper to deploy permit2 from precompiled bytecode
+/// @dev useful if testing externally against permit2 and want to avoid
+/// recompiling entirely and requiring viaIR compilation
+library DeployPermit2 {
+ /// @notice deploy permit2
+ function deployPermit2() internal returns (address) {
+ bytes memory bytecode =
+ hex"60c0346100bb574660a052602081017f8cad95687ba82c2ce50e74f7b754645e5117c3a5bec8151c0726d5857980a86681527f9ac997416e8ff9d2ff6bebeb7149f65cdae5e32e2b90440b566bb3044041d36a60408301524660608301523060808301526080825260a082019180831060018060401b038411176100a557826040525190206080526123c090816100c1823960805181611b47015260a05181611b210152f35b634e487b7160e01b600052604160045260246000fd5b600080fdfe6040608081526004908136101561001557600080fd5b600090813560e01c80630d58b1db1461126c578063137c29fe146110755780632a2d80d114610db75780632b67b57014610bde57806330f28b7a14610ade5780633644e51514610a9d57806336c7851614610a285780633ff9dcb1146109a85780634fe02b441461093f57806365d9723c146107ac57806387517c451461067a578063927da105146105c3578063cc53287f146104a3578063edd9444b1461033a5763fe8ec1a7146100c657600080fd5b346103365760c07ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc3601126103365767ffffffffffffffff833581811161033257610114903690860161164b565b60243582811161032e5761012b903690870161161a565b6101336114e6565b9160843585811161032a5761014b9036908a016115c1565b98909560a43590811161032657610164913691016115c1565b969095815190610173826113ff565b606b82527f5065726d697442617463685769746e6573735472616e7366657246726f6d285460208301527f6f6b656e5065726d697373696f6e735b5d207065726d69747465642c61646472838301527f657373207370656e6465722c75696e74323536206e6f6e63652c75696e74323560608301527f3620646561646c696e652c000000000000000000000000000000000000000000608083015282519a8b9181610222602085018096611f93565b918237018a8152039961025b7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe09b8c8101835282611437565b5190209085515161026b81611ebb565b908a5b8181106102f95750506102f6999a6102ed9183516102a081610294602082018095611f66565b03848101835282611437565b519020602089810151858b015195519182019687526040820192909252336060820152608081019190915260a081019390935260643560c08401528260e081015b03908101835282611437565b51902093611cf7565b80f35b8061031161030b610321938c5161175e565b51612054565b61031b828661175e565b52611f0a565b61026e565b8880fd5b8780fd5b8480fd5b8380fd5b5080fd5b5091346103365760807ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc3601126103365767ffffffffffffffff9080358281116103325761038b903690830161164b565b60243583811161032e576103a2903690840161161a565b9390926103ad6114e6565b9160643590811161049f576103c4913691016115c1565b949093835151976103d489611ebb565b98885b81811061047d5750506102f697988151610425816103f9602082018095611f66565b037fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe08101835282611437565b5190206020860151828701519083519260208401947ffcf35f5ac6a2c28868dc44c302166470266239195f02b0ee408334829333b7668652840152336060840152608083015260a082015260a081526102ed8161141b565b808b61031b8261049461030b61049a968d5161175e565b9261175e565b6103d7565b8680fd5b5082346105bf57602090817ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc3601126103325780359067ffffffffffffffff821161032e576104f49136910161161a565b929091845b848110610504578580f35b8061051a610515600193888861196c565b61197c565b61052f84610529848a8a61196c565b0161197c565b3389528385528589209173ffffffffffffffffffffffffffffffffffffffff80911692838b528652868a20911690818a5285528589207fffffffffffffffffffffffff000000000000000000000000000000000000000081541690558551918252848201527f89b1add15eff56b3dfe299ad94e01f2b52fbcb80ae1a3baea6ae8c04cb2b98a4853392a2016104f9565b8280fd5b50346103365760607ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc36011261033657610676816105ff6114a0565b936106086114c3565b6106106114e6565b73ffffffffffffffffffffffffffffffffffffffff968716835260016020908152848420928816845291825283832090871683528152919020549251938316845260a083901c65ffffffffffff169084015260d09190911c604083015281906060820190565b0390f35b50346103365760807ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc360112610336576106b26114a0565b906106bb6114c3565b916106c46114e6565b65ffffffffffff926064358481169081810361032a5779ffffffffffff0000000000000000000000000000000000000000947fda9fa7c1b00402c17d0161b249b1ab8bbec047c5a52207b9c112deffd817036b94338a5260016020527fffffffffffff0000000000000000000000000000000000000000000000000000858b209873ffffffffffffffffffffffffffffffffffffffff809416998a8d5260205283878d209b169a8b8d52602052868c209486156000146107a457504216925b8454921697889360a01b16911617179055815193845260208401523392a480f35b905092610783565b5082346105bf5760607ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc3601126105bf576107e56114a0565b906107ee6114c3565b9265ffffffffffff604435818116939084810361032a57338852602091600183528489209673ffffffffffffffffffffffffffffffffffffffff80911697888b528452858a20981697888a5283528489205460d01c93848711156109175761ffff9085840316116108f05750907f55eb90d810e1700b35a8e7e25395ff7f2b2259abd7415ca2284dfb1c246418f393929133895260018252838920878a528252838920888a5282528389209079ffffffffffffffffffffffffffffffffffffffffffffffffffff7fffffffffffff000000000000000000000000000000000000000000000000000083549260d01b16911617905582519485528401523392a480f35b84517f24d35a26000000000000000000000000000000000000000000000000000000008152fd5b5084517f756688fe000000000000000000000000000000000000000000000000000000008152fd5b503461033657807ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc360112610336578060209273ffffffffffffffffffffffffffffffffffffffff61098f6114a0565b1681528084528181206024358252845220549051908152f35b5082346105bf57817ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc3601126105bf577f3704902f963766a4e561bbaab6e6cdc1b1dd12f6e9e99648da8843b3f46b918d90359160243533855284602052818520848652602052818520818154179055815193845260208401523392a280f35b8234610a9a5760807ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc360112610a9a57610a606114a0565b610a686114c3565b610a706114e6565b6064359173ffffffffffffffffffffffffffffffffffffffff8316830361032e576102f6936117a1565b80fd5b503461033657817ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc36011261033657602090610ad7611b1e565b9051908152f35b508290346105bf576101007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc3601126105bf57610b1a3661152a565b90807fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7c36011261033257610b4c611478565b9160e43567ffffffffffffffff8111610bda576102f694610b6f913691016115c1565b939092610b7c8351612054565b6020840151828501519083519260208401947f939c21a48a8dbe3a9a2404a1d46691e4d39f6583d6ec6b35714604c986d801068652840152336060840152608083015260a082015260a08152610bd18161141b565b51902091611c25565b8580fd5b509134610336576101007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc36011261033657610c186114a0565b7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffdc360160c08112610332576080855191610c51836113e3565b1261033257845190610c6282611398565b73ffffffffffffffffffffffffffffffffffffffff91602435838116810361049f578152604435838116810361049f57602082015265ffffffffffff606435818116810361032a5788830152608435908116810361049f576060820152815260a435938285168503610bda576020820194855260c4359087830182815260e43567ffffffffffffffff811161032657610cfe90369084016115c1565b929093804211610d88575050918591610d786102f6999a610d7e95610d238851611fbe565b90898c511690519083519260208401947ff3841cd1ff0085026a6327b620b67997ce40f282c88a8e905a7a5626e310f3d086528401526060830152608082015260808152610d70816113ff565b519020611bd9565b916120c7565b519251169161199d565b602492508a51917fcd21db4f000000000000000000000000000000000000000000000000000000008352820152fd5b5091346103365760607ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc93818536011261033257610df36114a0565b9260249081359267ffffffffffffffff9788851161032a578590853603011261049f578051978589018981108282111761104a578252848301358181116103265785019036602383011215610326578382013591610e50836115ef565b90610e5d85519283611437565b838252602093878584019160071b83010191368311611046578801905b828210610fe9575050508a526044610e93868801611509565b96838c01978852013594838b0191868352604435908111610fe557610ebb90369087016115c1565b959096804211610fba575050508998995151610ed681611ebb565b908b5b818110610f9757505092889492610d7892610f6497958351610f02816103f98682018095611f66565b5190209073ffffffffffffffffffffffffffffffffffffffff9a8b8b51169151928551948501957faf1b0d30d2cab0380e68f0689007e3254993c596f2fdd0aaa7f4d04f794408638752850152830152608082015260808152610d70816113ff565b51169082515192845b848110610f78578580f35b80610f918585610f8b600195875161175e565b5161199d565b01610f6d565b80610311610fac8e9f9e93610fb2945161175e565b51611fbe565b9b9a9b610ed9565b8551917fcd21db4f000000000000000000000000000000000000000000000000000000008352820152fd5b8a80fd5b6080823603126110465785608091885161100281611398565b61100b85611509565b8152611018838601611509565b838201526110278a8601611607565b8a8201528d611037818701611607565b90820152815201910190610e7a565b8c80fd5b84896041867f4e487b7100000000000000000000000000000000000000000000000000000000835252fd5b5082346105bf576101407ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc3601126105bf576110b03661152a565b91807fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7c360112610332576110e2611478565b67ffffffffffffffff93906101043585811161049f5761110590369086016115c1565b90936101243596871161032a57611125610bd1966102f6983691016115c1565b969095825190611134826113ff565b606482527f5065726d69745769746e6573735472616e7366657246726f6d28546f6b656e5060208301527f65726d697373696f6e73207065726d69747465642c6164647265737320737065848301527f6e6465722c75696e74323536206e6f6e63652c75696e7432353620646561646c60608301527f696e652c0000000000000000000000000000000000000000000000000000000060808301528351948591816111e3602085018096611f93565b918237018b8152039361121c7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe095868101835282611437565b5190209261122a8651612054565b6020878101518589015195519182019687526040820192909252336060820152608081019190915260a081019390935260e43560c08401528260e081016102e1565b5082346105bf576020807ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc36011261033257813567ffffffffffffffff92838211610bda5736602383011215610bda5781013592831161032e576024906007368386831b8401011161049f57865b8581106112e5578780f35b80821b83019060807fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffdc83360301126103265761139288876001946060835161132c81611398565b611368608461133c8d8601611509565b9485845261134c60448201611509565b809785015261135d60648201611509565b809885015201611509565b918291015273ffffffffffffffffffffffffffffffffffffffff80808093169516931691166117a1565b016112da565b6080810190811067ffffffffffffffff8211176113b457604052565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052604160045260246000fd5b6060810190811067ffffffffffffffff8211176113b457604052565b60a0810190811067ffffffffffffffff8211176113b457604052565b60c0810190811067ffffffffffffffff8211176113b457604052565b90601f7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0910116810190811067ffffffffffffffff8211176113b457604052565b60c4359073ffffffffffffffffffffffffffffffffffffffff8216820361149b57565b600080fd5b6004359073ffffffffffffffffffffffffffffffffffffffff8216820361149b57565b6024359073ffffffffffffffffffffffffffffffffffffffff8216820361149b57565b6044359073ffffffffffffffffffffffffffffffffffffffff8216820361149b57565b359073ffffffffffffffffffffffffffffffffffffffff8216820361149b57565b7ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc01906080821261149b576040805190611563826113e3565b8082941261149b57805181810181811067ffffffffffffffff8211176113b457825260043573ffffffffffffffffffffffffffffffffffffffff8116810361149b578152602435602082015282526044356020830152606435910152565b9181601f8401121561149b5782359167ffffffffffffffff831161149b576020838186019501011161149b57565b67ffffffffffffffff81116113b45760051b60200190565b359065ffffffffffff8216820361149b57565b9181601f8401121561149b5782359167ffffffffffffffff831161149b576020808501948460061b01011161149b57565b91909160608184031261149b576040805191611666836113e3565b8294813567ffffffffffffffff9081811161149b57830182601f8201121561149b578035611693816115ef565b926116a087519485611437565b818452602094858086019360061b8501019381851161149b579086899897969594939201925b8484106116e3575050505050855280820135908501520135910152565b90919293949596978483031261149b578851908982019082821085831117611730578a928992845261171487611509565b81528287013583820152815201930191908897969594936116c6565b602460007f4e487b710000000000000000000000000000000000000000000000000000000081526041600452fd5b80518210156117725760209160051b010190565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052603260045260246000fd5b92919273ffffffffffffffffffffffffffffffffffffffff604060008284168152600160205282828220961695868252602052818120338252602052209485549565ffffffffffff8760a01c16804211611884575082871696838803611812575b5050611810955016926118b5565b565b878484161160001461184f57602488604051907ff96fb0710000000000000000000000000000000000000000000000000000000082526004820152fd5b7fffffffffffffffffffffffff000000000000000000000000000000000000000084846118109a031691161790553880611802565b602490604051907fd81b2f2e0000000000000000000000000000000000000000000000000000000082526004820152fd5b9060006064926020958295604051947f23b872dd0000000000000000000000000000000000000000000000000000000086526004860152602485015260448401525af13d15601f3d116001600051141617161561190e57565b60646040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152601460248201527f5452414e534645525f46524f4d5f4641494c45440000000000000000000000006044820152fd5b91908110156117725760061b0190565b3573ffffffffffffffffffffffffffffffffffffffff8116810361149b5790565b9065ffffffffffff908160608401511673ffffffffffffffffffffffffffffffffffffffff908185511694826020820151169280866040809401511695169560009187835260016020528383208984526020528383209916988983526020528282209184835460d01c03611af5579185611ace94927fc6a377bfc4eb120024a8ac08eef205be16b817020812c73223e81d1bdb9708ec98979694508715600014611ad35779ffffffffffff00000000000000000000000000000000000000009042165b60a01b167fffffffffffff00000000000000000000000000000000000000000000000000006001860160d01b1617179055519384938491604091949373ffffffffffffffffffffffffffffffffffffffff606085019616845265ffffffffffff809216602085015216910152565b0390a4565b5079ffffffffffff000000000000000000000000000000000000000087611a60565b600484517f756688fe000000000000000000000000000000000000000000000000000000008152fd5b467f000000000000000000000000000000000000000000000000000000000000000003611b69577f000000000000000000000000000000000000000000000000000000000000000090565b60405160208101907f8cad95687ba82c2ce50e74f7b754645e5117c3a5bec8151c0726d5857980a86682527f9ac997416e8ff9d2ff6bebeb7149f65cdae5e32e2b90440b566bb3044041d36a604082015246606082015230608082015260808152611bd3816113ff565b51902090565b611be1611b1e565b906040519060208201927f190100000000000000000000000000000000000000000000000000000000000084526022830152604282015260428152611bd381611398565b9192909360a435936040840151804211611cc65750602084510151808611611c955750918591610d78611c6594611c60602088015186611e47565b611bd9565b73ffffffffffffffffffffffffffffffffffffffff809151511692608435918216820361149b57611810936118b5565b602490604051907f3728b83d0000000000000000000000000000000000000000000000000000000082526004820152fd5b602490604051907fcd21db4f0000000000000000000000000000000000000000000000000000000082526004820152fd5b959093958051519560409283830151804211611e175750848803611dee57611d2e918691610d7860209b611c608d88015186611e47565b60005b868110611d42575050505050505050565b611d4d81835161175e565b5188611d5a83878a61196c565b01359089810151808311611dbe575091818888886001968596611d84575b50505050505001611d31565b611db395611dad9273ffffffffffffffffffffffffffffffffffffffff6105159351169561196c565b916118b5565b803888888883611d78565b6024908651907f3728b83d0000000000000000000000000000000000000000000000000000000082526004820152fd5b600484517fff633a38000000000000000000000000000000000000000000000000000000008152fd5b6024908551907fcd21db4f0000000000000000000000000000000000000000000000000000000082526004820152fd5b9073ffffffffffffffffffffffffffffffffffffffff600160ff83161b9216600052600060205260406000209060081c6000526020526040600020818154188091551615611e9157565b60046040517f756688fe000000000000000000000000000000000000000000000000000000008152fd5b90611ec5826115ef565b611ed26040519182611437565b8281527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0611f0082946115ef565b0190602036910137565b7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff8114611f375760010190565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b805160208092019160005b828110611f7f575050505090565b835185529381019392810192600101611f71565b9081519160005b838110611fab575050016000815290565b8060208092840101518185015201611f9a565b60405160208101917f65626cad6cb96493bf6f5ebea28756c966f023ab9e8a83a7101849d5573b3678835273ffffffffffffffffffffffffffffffffffffffff8082511660408401526020820151166060830152606065ffffffffffff9182604082015116608085015201511660a082015260a0815260c0810181811067ffffffffffffffff8211176113b45760405251902090565b6040516020808201927f618358ac3db8dc274f0cd8829da7e234bd48cd73c4a740aede1adec9846d06a1845273ffffffffffffffffffffffffffffffffffffffff81511660408401520151606082015260608152611bd381611398565b919082604091031261149b576020823592013590565b6000843b61222e5750604182036121ac576120e4828201826120b1565b939092604010156117725760209360009360ff6040608095013560f81c5b60405194855216868401526040830152606082015282805260015afa156121a05773ffffffffffffffffffffffffffffffffffffffff806000511691821561217657160361214c57565b60046040517f815e1d64000000000000000000000000000000000000000000000000000000008152fd5b60046040517f8baa579f000000000000000000000000000000000000000000000000000000008152fd5b6040513d6000823e3d90fd5b60408203612204576121c0918101906120b1565b91601b7f7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff84169360ff1c019060ff8211611f375760209360009360ff608094612102565b60046040517f4be6321b000000000000000000000000000000000000000000000000000000008152fd5b929391601f928173ffffffffffffffffffffffffffffffffffffffff60646020957fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0604051988997889687947f1626ba7e000000000000000000000000000000000000000000000000000000009e8f8752600487015260406024870152816044870152868601378b85828601015201168101030192165afa9081156123a857829161232a575b507fffffffff000000000000000000000000000000000000000000000000000000009150160361230057565b60046040517fb0669cbc000000000000000000000000000000000000000000000000000000008152fd5b90506020813d82116123a0575b8161234460209383611437565b810103126103365751907fffffffff0000000000000000000000000000000000000000000000000000000082168203610a9a57507fffffffff0000000000000000000000000000000000000000000000000000000090386122d4565b3d9150612337565b6040513d84823e3d90fdfea164736f6c6343000811000a";
+
+ return deployFromBytecode(bytecode);
+ }
+
+ /// @notice helper function to deploy bytecode
+ function deployFromBytecode(bytes memory bytecode) internal returns (address child) {
+ assembly {
+ child := create(0, add(bytecode, 0x20), mload(bytecode))
+ }
+ }
+}
diff --git a/test/enigma-dark-invariants/utils/Pretty.sol b/test/enigma-dark-invariants/utils/Pretty.sol
new file mode 100644
index 0000000..27a6ba5
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/Pretty.sol
@@ -0,0 +1,142 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+///@notice https://github.com/one-hundred-proof/kyberswap-exploit/blob/main/lib/helpers/Pretty.sol
+library Strings {
+ function concat(string memory _base, string memory _value) internal pure returns (string memory) {
+ bytes memory _baseBytes = bytes(_base);
+ bytes memory _valueBytes = bytes(_value);
+
+ string memory _tmpValue = new string(_baseBytes.length + _valueBytes.length);
+ bytes memory _newValue = bytes(_tmpValue);
+
+ uint256 i;
+ uint256 j;
+
+ for (i = 0; i < _baseBytes.length; i++) {
+ _newValue[j++] = _baseBytes[i];
+ }
+
+ for (i = 0; i < _valueBytes.length; i++) {
+ _newValue[j++] = _valueBytes[i];
+ }
+
+ return string(_newValue);
+ }
+}
+
+library Pretty {
+ uint8 constant DEFAULT_DECIMALS = 18;
+
+ function toBitString(uint256 n) external pure returns (string memory) {
+ return uintToBitString(n, 256);
+ }
+
+ function toBitString(uint256 n, uint8 decimals) external pure returns (string memory) {
+ return uintToBitString(n, decimals);
+ }
+
+ function pretty(uint256 n) external pure returns (string memory) {
+ return n == type(uint256).max
+ ? "type(uint256).max"
+ : n == type(uint128).max ? "type(uint128).max" : _pretty(n, DEFAULT_DECIMALS);
+ }
+
+ function pretty(bool value) external pure returns (string memory) {
+ return value ? "true" : "false";
+ }
+
+ function pretty(uint256 n, uint8 decimals) external pure returns (string memory) {
+ return _pretty(n, decimals);
+ }
+
+ function pretty(int256 n) external pure returns (string memory) {
+ return _prettyInt(n, DEFAULT_DECIMALS);
+ }
+
+ function pretty(int256 n, uint8 decimals) external pure returns (string memory) {
+ return _prettyInt(n, decimals);
+ }
+
+ function _pretty(uint256 n, uint8 decimals) internal pure returns (string memory) {
+ bool pastDecimals = decimals == 0;
+ uint256 place = 0;
+ uint256 r; // remainder
+ string memory s = "";
+
+ while (n != 0) {
+ r = n % 10;
+ n /= 10;
+ place++;
+ s = Strings.concat(toDigit(r), s);
+ if (pastDecimals && place % 3 == 0 && n != 0) {
+ s = Strings.concat("_", s);
+ }
+ if (!pastDecimals && place == decimals) {
+ pastDecimals = true;
+ place = 0;
+ s = Strings.concat("_", s);
+ }
+ }
+ if (pastDecimals && place == 0) {
+ s = Strings.concat("0", s);
+ }
+ if (!pastDecimals) {
+ uint256 i;
+ uint256 upper = (decimals >= place ? decimals - place : 0);
+ for (i = 0; i < upper; ++i) {
+ s = Strings.concat("0", s);
+ }
+ s = Strings.concat("0_", s);
+ }
+ return s;
+ }
+
+ function _prettyInt(int256 n, uint8 decimals) internal pure returns (string memory) {
+ bool isNegative = n < 0;
+ string memory s = "";
+ if (isNegative) {
+ s = "-";
+ }
+ return Strings.concat(s, _pretty(uint256(isNegative ? -n : n), decimals));
+ }
+
+ function toDigit(uint256 n) internal pure returns (string memory) {
+ if (n == 0) {
+ return "0";
+ } else if (n == 1) {
+ return "1";
+ } else if (n == 2) {
+ return "2";
+ } else if (n == 3) {
+ return "3";
+ } else if (n == 4) {
+ return "4";
+ } else if (n == 5) {
+ return "5";
+ } else if (n == 6) {
+ return "6";
+ } else if (n == 7) {
+ return "7";
+ } else if (n == 8) {
+ return "8";
+ } else if (n == 9) {
+ return "9";
+ } else {
+ revert("Not in range 0 to 10");
+ }
+ }
+
+ function uintToBitString(uint256 n, uint16 bits) internal pure returns (string memory) {
+ string memory s = "";
+ for (uint256 i; i < bits; i++) {
+ if (n % 2 == 0) {
+ s = Strings.concat("0", s);
+ } else {
+ s = Strings.concat("1", s);
+ }
+ n = n / 2;
+ }
+ return s;
+ }
+}
diff --git a/test/enigma-dark-invariants/utils/PropertiesAsserts.sol b/test/enigma-dark-invariants/utils/PropertiesAsserts.sol
new file mode 100644
index 0000000..487bb10
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/PropertiesAsserts.sol
@@ -0,0 +1,432 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+/// @notice PropertiesAsserts is a library that provides assertions for properties of Solidity contracts.
+/// @dev Added more assertions to the original PropertiesAsserts library.
+abstract contract PropertiesAsserts {
+ event LogUint256(string, uint256);
+ event LogAddress(string, address);
+ event LogString(string);
+
+ event AssertFail(string);
+ event AssertEqFail(string);
+ event AssertNeqFail(string);
+ event AssertGeFail(string);
+ event AssertGtFail(string);
+ event AssertLeFail(string);
+ event AssertLtFail(string);
+
+ function assertWithMsg(bool b, string memory reason) internal {
+ if (!b) {
+ emit AssertFail(reason);
+ assert(false);
+ }
+ }
+
+ /// @notice asserts that a is equal to b.
+ function assertEq(uint256 a, uint256 b) internal pure {
+ if (a != b) {
+ assert(false);
+ }
+ }
+
+ function assertEq(int256 a, int256 b) internal pure {
+ if (a != b) {
+ assert(false);
+ }
+ }
+
+ //write the function below for address
+ function assertEq(address a, address b) internal pure {
+ if (a != b) {
+ assert(false);
+ }
+ }
+
+ // now with a reason parameter
+ function assertEq(address a, address b, string memory reason) internal {
+ if (a != b) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, "!=", bStr, ", reason: ", reason);
+ emit AssertEqFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice asserts that a is equal to b. Violations are logged using reason.
+ function assertEq(uint256 a, uint256 b, string memory reason) internal {
+ if (a != b) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, "!=", bStr, ", reason: ", reason);
+ emit AssertEqFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice int256 version of assertEq
+ function assertEq(int256 a, int256 b, string memory reason) internal {
+ if (a != b) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, "!=", bStr, ", reason: ", reason);
+ emit AssertEqFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice asserts that a is not equal to b. Violations are logged using reason.
+ function assertNeq(uint256 a, uint256 b, string memory reason) internal {
+ if (a == b) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, "==", bStr, ", reason: ", reason);
+ emit AssertNeqFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice int256 version of assertNeq
+ function assertNeq(int256 a, int256 b, string memory reason) internal {
+ if (a == b) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, "==", bStr, ", reason: ", reason);
+ emit AssertNeqFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice asserts that a is greater than or equal to b. Violations are logged using reason.
+ function assertGe(uint256 a, uint256 b, string memory reason) internal {
+ if (!(a >= b)) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, "<", bStr, " failed, reason: ", reason);
+ emit AssertGeFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice int256 version of assertGe
+ function assertGe(int256 a, int256 b, string memory reason) internal {
+ if (!(a >= b)) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, "<", bStr, " failed, reason: ", reason);
+ emit AssertGeFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice asserts that a is greater than b. Violations are logged using reason.
+ function assertGt(uint256 a, uint256 b, string memory reason) internal {
+ if (!(a > b)) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, "<=", bStr, " failed, reason: ", reason);
+ emit AssertGtFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice int256 version of assertGt
+ function assertGt(int256 a, int256 b, string memory reason) internal {
+ if (!(a > b)) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, "<=", bStr, " failed, reason: ", reason);
+ emit AssertGtFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice asserts that a is less than or equal to b. Violations are logged using reason.
+ function assertLe(uint256 a, uint256 b, string memory reason) internal {
+ if (!(a <= b)) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, ">", bStr, " failed, reason: ", reason);
+ emit AssertLeFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice int256 version of assertLe
+ function assertLe(int256 a, int256 b, string memory reason) internal {
+ if (!(a <= b)) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, ">", bStr, " failed, reason: ", reason);
+ emit AssertLeFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice asserts that a is less than b. Violations are logged using reason.
+ function assertLt(uint256 a, uint256 b, string memory reason) internal {
+ if (!(a < b)) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, ">=", bStr, " failed, reason: ", reason);
+ emit AssertLtFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice int256 version of assertLt
+ function assertLt(int256 a, int256 b, string memory reason) internal {
+ if (!(a < b)) {
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory bStr = PropertiesLibString.toString(b);
+ bytes memory assertMsg = abi.encodePacked("Invalid: ", aStr, ">=", bStr, " failed, reason: ", reason);
+ emit AssertLtFail(string(assertMsg));
+ assert(false);
+ }
+ }
+
+ /// @notice Clamps value to be between low and high, both inclusive
+ function clampBetween(uint256 value, uint256 low, uint256 high) internal returns (uint256) {
+ if (value < low || value > high) {
+ uint256 ans = low + (value % (high - low + 1));
+ string memory valueStr = PropertiesLibString.toString(value);
+ string memory ansStr = PropertiesLibString.toString(ans);
+ bytes memory message = abi.encodePacked("Clamping value ", valueStr, " to ", ansStr);
+ emit LogString(string(message));
+ return ans;
+ }
+ return value;
+ }
+
+ /// @notice int256 version of clampBetween
+ function clampBetween(int256 value, int256 low, int256 high) internal returns (int256) {
+ if (value < low || value > high) {
+ int256 range = high - low + 1;
+ int256 clamped = (value - low) % (range);
+ if (clamped < 0) clamped += range;
+ int256 ans = low + clamped;
+ string memory valueStr = PropertiesLibString.toString(value);
+ string memory ansStr = PropertiesLibString.toString(ans);
+ bytes memory message = abi.encodePacked("Clamping value ", valueStr, " to ", ansStr);
+ emit LogString(string(message));
+ return ans;
+ }
+ return value;
+ }
+
+ /// @notice Clamps value to be between low and high, exclusively (not including boundary points)
+ function clampBetweenExclusive(uint256 value, uint256 low, uint256 high) internal pure returns (uint256) {
+ /// @dev
+ require(high > low + 1, "Invalid range: must have at least one value between low and high");
+ if (value <= low || value >= high) {
+ return low + 1 + (value % (high - low - 1));
+ }
+ return value;
+ }
+
+ /// @notice int256 version of clampBetweenExclusive
+ function clampBetweenExclusive(int256 value, int256 low, int256 high) internal pure returns (int256) {
+ require(high > low + 1, "Invalid range: must have at least one value between low and high");
+ if (value <= low || value >= high) {
+ int256 range = high - low - 1;
+ int256 clamped = (value - (low + 1)) % range;
+ if (clamped < 0) clamped += range;
+ return low + 1 + clamped;
+ }
+ return value;
+ }
+
+ /// @notice clamps a to be less than b
+ function clampLt(uint256 a, uint256 b) internal returns (uint256) {
+ if (!(a < b)) {
+ assertNeq(b, 0, "clampLt cannot clamp value a to be less than zero. Check your inputs/assumptions.");
+ uint256 value = a % b;
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory valueStr = PropertiesLibString.toString(value);
+ bytes memory message = abi.encodePacked("Clamping value ", aStr, " to ", valueStr);
+ emit LogString(string(message));
+ return value;
+ }
+ return a;
+ }
+
+ /// @notice int256 version of clampLt
+ function clampLt(int256 a, int256 b) internal returns (int256) {
+ if (!(a < b)) {
+ int256 value = b - 1;
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory valueStr = PropertiesLibString.toString(value);
+ bytes memory message = abi.encodePacked("Clamping value ", aStr, " to ", valueStr);
+ emit LogString(string(message));
+ return value;
+ }
+ return a;
+ }
+
+ /// @notice clamps a to be less than or equal to b
+ function clampLe(uint256 a, uint256 b) internal returns (uint256) {
+ if (!(a <= b)) {
+ uint256 value = a % (b + 1);
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory valueStr = PropertiesLibString.toString(value);
+ bytes memory message = abi.encodePacked("Clamping value ", aStr, " to ", valueStr);
+ emit LogString(string(message));
+ return value;
+ }
+ return a;
+ }
+
+ /// @notice int256 version of clampLe
+ function clampLe(int256 a, int256 b) internal returns (int256) {
+ if (!(a <= b)) {
+ int256 value = b;
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory valueStr = PropertiesLibString.toString(value);
+ bytes memory message = abi.encodePacked("Clamping value ", aStr, " to ", valueStr);
+ emit LogString(string(message));
+ return value;
+ }
+ return a;
+ }
+
+ /// @notice clamps a to be greater than b
+ function clampGt(uint256 a, uint256 b) internal returns (uint256) {
+ if (!(a > b)) {
+ assertNeq(
+ b,
+ type(uint256).max,
+ "clampGt cannot clamp value a to be larger than uint256.max. Check your inputs/assumptions."
+ );
+ uint256 value = b + 1;
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory valueStr = PropertiesLibString.toString(value);
+ bytes memory message = abi.encodePacked("Clamping value ", aStr, " to ", valueStr);
+ emit LogString(string(message));
+ return value;
+ } else {
+ return a;
+ }
+ }
+
+ /// @notice int256 version of clampGt
+ function clampGt(int256 a, int256 b) internal returns (int256) {
+ if (!(a > b)) {
+ int256 value = b + 1;
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory valueStr = PropertiesLibString.toString(value);
+ bytes memory message = abi.encodePacked("Clamping value ", aStr, " to ", valueStr);
+ emit LogString(string(message));
+ return value;
+ } else {
+ return a;
+ }
+ }
+
+ /// @notice clamps a to be greater than or equal to b
+ function clampGe(uint256 a, uint256 b) internal returns (uint256) {
+ if (!(a > b)) {
+ uint256 value = b;
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory valueStr = PropertiesLibString.toString(value);
+ bytes memory message = abi.encodePacked("Clamping value ", aStr, " to ", valueStr);
+ emit LogString(string(message));
+ return value;
+ }
+ return a;
+ }
+
+ /// @notice int256 version of clampGe
+ function clampGe(int256 a, int256 b) internal returns (int256) {
+ if (!(a > b)) {
+ int256 value = b;
+ string memory aStr = PropertiesLibString.toString(a);
+ string memory valueStr = PropertiesLibString.toString(value);
+ bytes memory message = abi.encodePacked("Clamping value ", aStr, " to ", valueStr);
+ emit LogString(string(message));
+ return value;
+ }
+ return a;
+ }
+}
+
+/// @notice Efficient library for creating string representations of integers.
+/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/utils/LibString.sol)
+/// @author Modified from Solady (https://github.com/Vectorized/solady/blob/main/src/utils/LibString.sol)
+/// @dev Name of the library is modified to prevent collisions with contract-under-test uses of LibString
+library PropertiesLibString {
+ function toString(int256 value) internal pure returns (string memory str) {
+ uint256 absValue = value >= 0 ? uint256(value) : uint256(-value);
+ str = toString(absValue);
+
+ if (value < 0) {
+ str = string(abi.encodePacked("-", str));
+ }
+ }
+
+ function toString(uint256 value) internal pure returns (string memory str) {
+ /// @solidity memory-safe-assembly
+ assembly {
+ // The maximum value of a uint256 contains 78 digits (1 byte per digit), but we allocate 160 bytes
+ // to keep the free memory pointer word aligned. We'll need 1 word for the length, 1 word for the
+ // trailing zeros padding, and 3 other words for a max of 78 digits. In total: 5 * 32 = 160 bytes.
+ let newFreeMemoryPointer := add(mload(0x40), 160)
+
+ // Update the free memory pointer to avoid overriding our string.
+ mstore(0x40, newFreeMemoryPointer)
+
+ // Assign str to the end of the zone of newly allocated memory.
+ str := sub(newFreeMemoryPointer, 32)
+
+ // Clean the last word of memory it may not be overwritten.
+ mstore(str, 0)
+
+ // Cache the end of the memory to calculate the length later.
+ let end := str
+
+ // We write the string from rightmost digit to leftmost digit.
+ // The following is essentially a do-while loop that also handles the zero case.
+ // prettier-ignore
+ for { let temp := value } 1 {} {
+ // Move the pointer 1 byte to the left.
+ str := sub(str, 1)
+
+ // Write the character to the pointer.
+ // The ASCII index of the '0' character is 48.
+ mstore8(str, add(48, mod(temp, 10)))
+
+ // Keep dividing temp until zero.
+ temp := div(temp, 10)
+
+ // prettier-ignore
+ if iszero(temp) { break }
+ }
+
+ // Compute and cache the final total length of the string.
+ let length := sub(end, str)
+
+ // Move the pointer 32 bytes leftwards to make room for the length.
+ str := sub(str, 32)
+
+ // Store the string's length at the start of memory allocated for our string.
+ mstore(str, length)
+ }
+ }
+
+ function toString(address value) internal pure returns (string memory str) {
+ bytes memory s = new bytes(40);
+ for (uint256 i = 0; i < 20; i++) {
+ bytes1 b = bytes1(uint8(uint256(uint160(value)) / (2 ** (8 * (19 - i)))));
+ bytes1 hi = bytes1(uint8(b) / 16);
+ bytes1 lo = bytes1(uint8(b) - 16 * uint8(hi));
+ s[2 * i] = char(hi);
+ s[2 * i + 1] = char(lo);
+ }
+ return string(s);
+ }
+
+ function char(bytes1 b) internal pure returns (bytes1 c) {
+ if (uint8(b) < 10) return bytes1(uint8(b) + 0x30);
+ else return bytes1(uint8(b) + 0x57);
+ }
+}
diff --git a/test/enigma-dark-invariants/utils/PropertiesConstants.sol b/test/enigma-dark-invariants/utils/PropertiesConstants.sol
new file mode 100644
index 0000000..f986436
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/PropertiesConstants.sol
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+abstract contract PropertiesConstants {
+ // Constant echidna addresses
+ address constant USER1 = address(0x10000);
+ address constant USER2 = address(0x20000);
+ address constant USER3 = address(0x30000);
+ uint256 constant INITIAL_BALANCE = 1000e30;
+
+ // EulerSwap constants
+ uint256 constant MAX_LEVERAGE = 10;
+ uint256 constant MIN_LEVERAGE = 1;
+
+ // EVault constants
+ uint16 constant MAX_LIQUIDATION_DISCOUNT = 0.2e4;
+ uint16 constant LIQUIDATION_LTV = 0.9e4;
+ uint16 constant BORROW_LTV = 0.9e4;
+}
diff --git a/test/enigma-dark-invariants/utils/StdAsserts.sol b/test/enigma-dark-invariants/utils/StdAsserts.sol
new file mode 100644
index 0000000..e43d10e
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/StdAsserts.sol
@@ -0,0 +1,443 @@
+// SPDX-License-Identifier: MIT
+pragma solidity >=0.6.2 <0.9.0;
+
+import {PropertiesAsserts} from "./PropertiesAsserts.sol";
+import {stdMath} from "forge-std/StdMath.sol";
+
+/// @notice Standardized assertions for use in Invariant tests, inherits PropertiesAsserts
+/// @dev Adapted from forge to work with echidna & medusa
+abstract contract StdAsserts is PropertiesAsserts {
+ event log(string);
+ event logs(bytes);
+
+ event log_address(address);
+ event log_bytes32(bytes32);
+ event log_int(int256);
+ event log_uint(uint256);
+ event log_bytes(bytes);
+ event log_string(string);
+
+ event log_named_address(string key, address val);
+ event log_named_bytes32(string key, bytes32 val);
+ event log_named_decimal_int(string key, int256 val, uint256 decimals);
+ event log_named_decimal_uint(string key, uint256 val, uint256 decimals);
+ event log_named_int(string key, int256 val);
+ event log_named_uint(string key, uint256 val);
+ event log_named_bytes(string key, bytes val);
+ event log_named_string(string key, string val);
+ event log_array(uint256[] val);
+ event log_array(int256[] val);
+ event log_array(address[] val);
+ event log_named_array(string key, uint256[] val);
+ event log_named_array(string key, int256[] val);
+ event log_named_array(string key, address[] val);
+
+ function fail(string memory err) internal virtual {
+ emit log_named_string("Error", err);
+ fail();
+ }
+
+ function fail() internal virtual {
+ assert(false);
+ }
+
+ function assertTrue(bool condition) internal {
+ if (!condition) {
+ emit log("Error: Assertion Failed");
+ fail();
+ }
+ }
+
+ function assertTrue(bool condition, string memory err) internal {
+ if (!condition) {
+ emit log_named_string("Error", err);
+ assertTrue(condition);
+ }
+ }
+
+ function assertFalse(bool data) internal virtual {
+ assertTrue(!data);
+ }
+
+ function assertFalse(bool data, string memory err) internal virtual {
+ assertTrue(!data, err);
+ }
+
+ function checkEq0(bytes memory a, bytes memory b) internal pure returns (bool ok) {
+ ok = true;
+ if (a.length == b.length) {
+ for (uint256 i = 0; i < a.length; i++) {
+ if (a[i] != b[i]) {
+ ok = false;
+ }
+ }
+ } else {
+ ok = false;
+ }
+ }
+
+ function assertEq0(bytes memory a, bytes memory b) internal {
+ if (!checkEq0(a, b)) {
+ emit log("Error: a == b not satisfied [bytes]");
+ emit log_named_bytes(" Expected", a);
+ emit log_named_bytes(" Actual", b);
+ fail();
+ }
+ }
+
+ function assertEq0(bytes memory a, bytes memory b, string memory err) internal {
+ if (!checkEq0(a, b)) {
+ emit log_named_string("Error", err);
+ assertEq0(a, b);
+ }
+ }
+
+ function assertEq(bool a, bool b) internal virtual {
+ if (a != b) {
+ emit log("Error: a == b not satisfied [bool]");
+ emit log_named_string(" Left", a ? "true" : "false");
+ emit log_named_string(" Right", b ? "true" : "false");
+ fail();
+ }
+ }
+
+ function assertEq(bool a, bool b, string memory err) internal virtual {
+ if (a != b) {
+ emit log_named_string("Error", err);
+ assertEq(a, b);
+ }
+ }
+
+ function assertEq(bytes memory a, bytes memory b) internal virtual {
+ assertEq0(a, b);
+ }
+
+ function assertEq(bytes memory a, bytes memory b, string memory err) internal virtual {
+ assertEq0(a, b, err);
+ }
+
+ function assertEq(uint256[] memory a, uint256[] memory b) internal virtual {
+ if (keccak256(abi.encode(a)) != keccak256(abi.encode(b))) {
+ emit log("Error: a == b not satisfied [uint[]]");
+ emit log_named_array(" Left", a);
+ emit log_named_array(" Right", b);
+ fail();
+ }
+ }
+
+ function assertEq(int256[] memory a, int256[] memory b) internal virtual {
+ if (keccak256(abi.encode(a)) != keccak256(abi.encode(b))) {
+ emit log("Error: a == b not satisfied [int[]]");
+ emit log_named_array(" Left", a);
+ emit log_named_array(" Right", b);
+ fail();
+ }
+ }
+
+ function assertEq(address[] memory a, address[] memory b) internal virtual {
+ if (keccak256(abi.encode(a)) != keccak256(abi.encode(b))) {
+ emit log("Error: a == b not satisfied [address[]]");
+ emit log_named_array(" Left", a);
+ emit log_named_array(" Right", b);
+ fail();
+ }
+ }
+
+ function assertEq(uint256[] memory a, uint256[] memory b, string memory err) internal virtual {
+ if (keccak256(abi.encode(a)) != keccak256(abi.encode(b))) {
+ emit log_named_string("Error", err);
+ assertEq(a, b);
+ }
+ }
+
+ function assertEq(int256[] memory a, int256[] memory b, string memory err) internal virtual {
+ if (keccak256(abi.encode(a)) != keccak256(abi.encode(b))) {
+ emit log_named_string("Error", err);
+ assertEq(a, b);
+ }
+ }
+
+ function assertEq(address[] memory a, address[] memory b, string memory err) internal virtual {
+ if (keccak256(abi.encode(a)) != keccak256(abi.encode(b))) {
+ emit log_named_string("Error", err);
+ assertEq(a, b);
+ }
+ }
+
+ // Legacy helper
+ function assertEqUint(uint256 a, uint256 b) internal virtual {
+ assertEq(uint256(a), uint256(b));
+ }
+
+ function assertApproxEqAbs(uint256 a, uint256 b, uint256 maxDelta) internal virtual {
+ uint256 delta = stdMath.delta(a, b);
+
+ if (delta > maxDelta) {
+ emit log("Error: a ~= b not satisfied [uint]");
+ emit log_named_uint(" Left", a);
+ emit log_named_uint(" Right", b);
+ emit log_named_uint(" Max Delta", maxDelta);
+ emit log_named_uint(" Delta", delta);
+ fail();
+ }
+ }
+
+ function assertApproxEqAbs(uint256 a, uint256 b, uint256 maxDelta, string memory err) internal virtual {
+ uint256 delta = stdMath.delta(a, b);
+
+ if (delta > maxDelta) {
+ emit log_named_string("Error", err);
+ assertApproxEqAbs(a, b, maxDelta);
+ }
+ }
+
+ function assertApproxEqAbsDecimal(uint256 a, uint256 b, uint256 maxDelta, uint256 decimals) internal virtual {
+ uint256 delta = stdMath.delta(a, b);
+
+ if (delta > maxDelta) {
+ emit log("Error: a ~= b not satisfied [uint]");
+ emit log_named_decimal_uint(" Left", a, decimals);
+ emit log_named_decimal_uint(" Right", b, decimals);
+ emit log_named_decimal_uint(" Max Delta", maxDelta, decimals);
+ emit log_named_decimal_uint(" Delta", delta, decimals);
+ fail();
+ }
+ }
+
+ function assertApproxEqAbsDecimal(uint256 a, uint256 b, uint256 maxDelta, uint256 decimals, string memory err)
+ internal
+ virtual
+ {
+ uint256 delta = stdMath.delta(a, b);
+
+ if (delta > maxDelta) {
+ emit log_named_string("Error", err);
+ assertApproxEqAbsDecimal(a, b, maxDelta, decimals);
+ }
+ }
+
+ function assertApproxEqAbs(int256 a, int256 b, uint256 maxDelta) internal virtual {
+ uint256 delta = stdMath.delta(a, b);
+
+ if (delta > maxDelta) {
+ emit log("Error: a ~= b not satisfied [int]");
+ emit log_named_int(" Left", a);
+ emit log_named_int(" Right", b);
+ emit log_named_uint(" Max Delta", maxDelta);
+ emit log_named_uint(" Delta", delta);
+ fail();
+ }
+ }
+
+ function assertApproxEqAbs(int256 a, int256 b, uint256 maxDelta, string memory err) internal virtual {
+ uint256 delta = stdMath.delta(a, b);
+
+ if (delta > maxDelta) {
+ emit log_named_string("Error", err);
+ assertApproxEqAbs(a, b, maxDelta);
+ }
+ }
+
+ function assertApproxEqAbsDecimal(int256 a, int256 b, uint256 maxDelta, uint256 decimals) internal virtual {
+ uint256 delta = stdMath.delta(a, b);
+
+ if (delta > maxDelta) {
+ emit log("Error: a ~= b not satisfied [int]");
+ emit log_named_decimal_int(" Left", a, decimals);
+ emit log_named_decimal_int(" Right", b, decimals);
+ emit log_named_decimal_uint(" Max Delta", maxDelta, decimals);
+ emit log_named_decimal_uint(" Delta", delta, decimals);
+ fail();
+ }
+ }
+
+ function assertApproxEqAbsDecimal(int256 a, int256 b, uint256 maxDelta, uint256 decimals, string memory err)
+ internal
+ virtual
+ {
+ uint256 delta = stdMath.delta(a, b);
+
+ if (delta > maxDelta) {
+ emit log_named_string("Error", err);
+ assertApproxEqAbsDecimal(a, b, maxDelta, decimals);
+ }
+ }
+
+ function assertApproxEqRel(
+ uint256 a,
+ uint256 b,
+ uint256 maxPercentDelta // An 18 decimal fixed point number, where 1e18 == 100%
+ ) internal virtual {
+ if (b == 0) return assertEq(a, b); // If the left is 0, right must be too.
+
+ uint256 percentDelta = stdMath.percentDelta(a, b);
+
+ if (percentDelta > maxPercentDelta) {
+ emit log("Error: a ~= b not satisfied [uint]");
+ emit log_named_uint(" Left", a);
+ emit log_named_uint(" Right", b);
+ emit log_named_decimal_uint(" Max % Delta", maxPercentDelta * 100, 18);
+ emit log_named_decimal_uint(" % Delta", percentDelta * 100, 18);
+ fail();
+ }
+ }
+
+ function assertApproxEqRel(
+ uint256 a,
+ uint256 b,
+ uint256 maxPercentDelta, // An 18 decimal fixed point number, where 1e18 == 100%
+ string memory err
+ ) internal virtual {
+ if (b == 0) return assertEq(a, b, err); // If the left is 0, right must be too.
+
+ uint256 percentDelta = stdMath.percentDelta(a, b);
+
+ if (percentDelta > maxPercentDelta) {
+ emit log_named_string("Error", err);
+ assertApproxEqRel(a, b, maxPercentDelta);
+ }
+ }
+
+ function assertApproxEqRelDecimal(
+ uint256 a,
+ uint256 b,
+ uint256 maxPercentDelta, // An 18 decimal fixed point number, where 1e18 == 100%
+ uint256 decimals
+ ) internal virtual {
+ if (b == 0) return assertEq(a, b); // If the left is 0, right must be too.
+
+ uint256 percentDelta = stdMath.percentDelta(a, b);
+
+ if (percentDelta > maxPercentDelta) {
+ emit log("Error: a ~= b not satisfied [uint]");
+ emit log_named_decimal_uint(" Left", a, decimals);
+ emit log_named_decimal_uint(" Right", b, decimals);
+ emit log_named_decimal_uint(" Max % Delta", maxPercentDelta * 100, 18);
+ emit log_named_decimal_uint(" % Delta", percentDelta * 100, 18);
+ fail();
+ }
+ }
+
+ function assertApproxEqRelDecimal(
+ uint256 a,
+ uint256 b,
+ uint256 maxPercentDelta, // An 18 decimal fixed point number, where 1e18 == 100%
+ uint256 decimals,
+ string memory err
+ ) internal virtual {
+ if (b == 0) return assertEq(a, b, err); // If the left is 0, right must be too.
+
+ uint256 percentDelta = stdMath.percentDelta(a, b);
+
+ if (percentDelta > maxPercentDelta) {
+ emit log_named_string("Error", err);
+ assertApproxEqRelDecimal(a, b, maxPercentDelta, decimals);
+ }
+ }
+
+ function assertApproxEqRel(int256 a, int256 b, uint256 maxPercentDelta) internal virtual {
+ if (b == 0) return assertEq(a, b); // If the left is 0, right must be too.
+
+ uint256 percentDelta = stdMath.percentDelta(a, b);
+
+ if (percentDelta > maxPercentDelta) {
+ emit log("Error: a ~= b not satisfied [int]");
+ emit log_named_int(" Left", a);
+ emit log_named_int(" Right", b);
+ emit log_named_decimal_uint(" Max % Delta", maxPercentDelta * 100, 18);
+ emit log_named_decimal_uint(" % Delta", percentDelta * 100, 18);
+ fail();
+ }
+ }
+
+ function assertApproxEqRel(int256 a, int256 b, uint256 maxPercentDelta, string memory err) internal virtual {
+ if (b == 0) return assertEq(a, b, err); // If the left is 0, right must be too.
+
+ uint256 percentDelta = stdMath.percentDelta(a, b);
+
+ if (percentDelta > maxPercentDelta) {
+ emit log_named_string("Error", err);
+ assertApproxEqRel(a, b, maxPercentDelta);
+ }
+ }
+
+ function assertApproxEqRelDecimal(int256 a, int256 b, uint256 maxPercentDelta, uint256 decimals) internal virtual {
+ if (b == 0) return assertEq(a, b); // If the left is 0, right must be too.
+
+ uint256 percentDelta = stdMath.percentDelta(a, b);
+
+ if (percentDelta > maxPercentDelta) {
+ emit log("Error: a ~= b not satisfied [int]");
+ emit log_named_decimal_int(" Left", a, decimals);
+ emit log_named_decimal_int(" Right", b, decimals);
+ emit log_named_decimal_uint(" Max % Delta", maxPercentDelta * 100, 18);
+ emit log_named_decimal_uint(" % Delta", percentDelta * 100, 18);
+ fail();
+ }
+ }
+
+ function assertApproxEqRelDecimal(int256 a, int256 b, uint256 maxPercentDelta, uint256 decimals, string memory err)
+ internal
+ virtual
+ {
+ if (b == 0) return assertEq(a, b, err); // If the left is 0, right must be too.
+
+ uint256 percentDelta = stdMath.percentDelta(a, b);
+
+ if (percentDelta > maxPercentDelta) {
+ emit log_named_string("Error", err);
+ assertApproxEqRelDecimal(a, b, maxPercentDelta, decimals);
+ }
+ }
+
+ function assertEqCall(address target, bytes memory callDataA, bytes memory callDataB) internal virtual {
+ assertEqCall(target, callDataA, target, callDataB, true);
+ }
+
+ function assertEqCall(address targetA, bytes memory callDataA, address targetB, bytes memory callDataB)
+ internal
+ virtual
+ {
+ assertEqCall(targetA, callDataA, targetB, callDataB, true);
+ }
+
+ function assertEqCall(address target, bytes memory callDataA, bytes memory callDataB, bool strictRevertData)
+ internal
+ virtual
+ {
+ assertEqCall(target, callDataA, target, callDataB, strictRevertData);
+ }
+
+ function assertEqCall(
+ address targetA,
+ bytes memory callDataA,
+ address targetB,
+ bytes memory callDataB,
+ bool strictRevertData
+ ) internal virtual {
+ (bool successA, bytes memory returnDataA) = address(targetA).call(callDataA);
+ (bool successB, bytes memory returnDataB) = address(targetB).call(callDataB);
+
+ if (successA && successB) {
+ assertEq(returnDataA, returnDataB, "Call return data does not match");
+ }
+
+ if (!successA && !successB && strictRevertData) {
+ assertEq(returnDataA, returnDataB, "Call revert data does not match");
+ }
+
+ if (!successA && successB) {
+ emit log("Error: Calls were not equal");
+ emit log_named_bytes(" Left call revert data", returnDataA);
+ emit log_named_bytes(" Right call return data", returnDataB);
+ fail();
+ }
+
+ if (successA && !successB) {
+ emit log("Error: Calls were not equal");
+ emit log_named_bytes(" Left call return data", returnDataA);
+ emit log_named_bytes(" Right call revert data", returnDataB);
+ fail();
+ }
+ }
+}
diff --git a/test/enigma-dark-invariants/utils/mocks/MockPriceOracle.sol b/test/enigma-dark-invariants/utils/mocks/MockPriceOracle.sol
new file mode 100644
index 0000000..7920d50
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/mocks/MockPriceOracle.sol
@@ -0,0 +1,80 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+pragma solidity ^0.8.0;
+
+import "evk/EVault/IEVault.sol";
+
+contract MockPriceOracle {
+ error PO_BaseUnsupported();
+ error PO_QuoteUnsupported();
+ error PO_Overflow();
+ error PO_NoPath();
+
+ mapping(address base => mapping(address quote => uint256)) price;
+ mapping(address base => mapping(address quote => Prices)) prices;
+
+ struct Prices {
+ bool set;
+ uint256 bid;
+ uint256 ask;
+ }
+
+ function name() external pure returns (string memory) {
+ return "MockPriceOracle";
+ }
+
+ function getQuote(uint256 amount, address base, address quote) public view returns (uint256 out) {
+ return calculateQuote(base, amount, price[resolveUnderlying(base)][quote]);
+ }
+
+ function getQuotes(uint256 amount, address base, address quote)
+ external
+ view
+ returns (uint256 bidOut, uint256 askOut)
+ {
+ if (prices[resolveUnderlying(base)][quote].set) {
+ return (
+ calculateQuote(base, amount, prices[resolveUnderlying(base)][quote].bid),
+ calculateQuote(base, amount, prices[resolveUnderlying(base)][quote].ask)
+ );
+ }
+
+ bidOut = askOut = getQuote(amount, base, quote);
+ }
+
+ ///// Mock functions
+
+ function setPrice(address base, address quote, uint256 newPrice) external {
+ price[resolveUnderlying(base)][quote] = newPrice;
+ }
+
+ function setPrices(address base, address quote, uint256 newBid, uint256 newAsk) external {
+ prices[resolveUnderlying(base)][quote] = Prices({set: true, bid: newBid, ask: newAsk});
+ }
+
+ function calculateQuote(address base, uint256 amount, uint256 p) internal view returns (uint256) {
+ // While base is a vault (for the purpose of the mock, if it implements asset()), then call
+ // convertToAssets() to price its shares. This is similar to how EulerRouter implements
+ // "resolved" vaults.
+
+ while (base.code.length > 0) {
+ (bool success, bytes memory data) = base.staticcall(abi.encodeCall(IERC4626.asset, ()));
+ if (!success) break;
+
+ (address asset) = abi.decode(data, (address));
+ amount = IEVault(base).convertToAssets(amount);
+ base = asset;
+ }
+
+ return amount * p / 1e18;
+ }
+
+ function resolveUnderlying(address asset) internal view returns (address) {
+ if (asset.code.length > 0) {
+ (bool success, bytes memory data) = asset.staticcall(abi.encodeCall(IERC4626.asset, ()));
+ if (success) return abi.decode(data, (address));
+ }
+
+ return asset;
+ }
+}
diff --git a/test/enigma-dark-invariants/utils/mocks/TestERC20.sol b/test/enigma-dark-invariants/utils/mocks/TestERC20.sol
new file mode 100644
index 0000000..b1c54b8
--- /dev/null
+++ b/test/enigma-dark-invariants/utils/mocks/TestERC20.sol
@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+pragma solidity >=0.7.0 <0.9.0;
+
+import {MockERC20} from "forge-std/mocks/MockERC20.sol";
+
+contract TestERC20 is MockERC20 {
+ constructor(string memory name, string memory symbol, uint8 decimals) {
+ initialize(name, symbol, decimals);
+ }
+
+ function mint(address to, uint256 value) public virtual {
+ _mint(to, value);
+ }
+
+ function burn(address from, uint256 value) public virtual {
+ _burn(from, value);
+ }
+}