diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml new file mode 100644 index 0000000..ca46ec3 --- /dev/null +++ b/.github/workflows/certora-prover.yml @@ -0,0 +1,59 @@ +name: Certora Prover Submission Workflow +description: |- + This workflow submits Certora Prover jobs on the specified configurations. Once all + jobs are successfully submitted, it will add a pending commit status to the commit. + This status will be periodically updated with verification results of the jobs, along + with the verification summary comment on the pull request. + + For more information, please visit https://github.com/certora/certora-run-action. + +on: + pull_request: + branches: + - master + workflow_dispatch: + +jobs: + certora_run_submission: + runs-on: ubuntu-latest + permissions: + contents: read + statuses: write + pull-requests: write + id-token: write + steps: + - name: Checkout repository + uses: actions/checkout@v4 + with: + submodules: recursive + + # Run Certora munge script + - name: Certora munge + run: ./certora/scripts/patch.sh + + # Submit verification jobs to Certora Prover + - name: Submit verification jobs to Certora Prover + uses: Certora/certora-run-action@v2 + with: + # Add your configurations as lines, each line is separated. + # Specify additional options for each configuration by adding them after the configuration. + configurations: |- + certora/confs/Balances.conf + certora/confs/ConsistentState.conf + certora/confs/Enabled.conf + certora/confs/Immutability.conf + certora/confs/Liveness.conf + certora/confs/PendingValues.conf + certora/confs/Range.conf + certora/confs/Reentrancy.conf + certora/confs/Reverts.conf + certora/confs/Roles.conf + certora/confs/Timelock.conf + certora/confs/LostAssets.conf + solc-versions: 0.8.17 0.8.26 + cli-release: beta + job-name: "Verified Rules" + certora-key: ${{ secrets.CERTORAKEY }} + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + diff --git a/.gitignore b/.gitignore index c90e0f5..61e22f6 100644 --- a/.gitignore +++ b/.gitignore @@ -12,4 +12,7 @@ broadcast/ .env # System Files -.DS_Store \ No newline at end of file +.DS_Store + +# certora generated files +.certora_internal \ No newline at end of file diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 0000000..c269a0f --- /dev/null +++ b/certora/README.md @@ -0,0 +1,59 @@ +This folder contains the verification of EulerEarn using the Certora Prover. + +The verification was inspired by the previous verification projects for Metamorpho and SiloVault (see https://github.com/morpho-org/metamorpho/tree/main/certora) + +## Getting started + +The code is compiled using 2 versions of solidity, which must be installed to run the verification as: + +- `solc-0.8.17` for solidity compiler version 0.8.17 which is used for compiling Permit2 +- `solc-0.8.19` for solidity compiler version 0.8.26 which is used for compiling the rest of the solidity files. + +Follow Certora installation instructions: https://docs.certora.com/en/latest/docs/user-guide/install.html and the repository build installation for EulerEarn. + +## Folders and file structure + +The [`certora/specs`](specs) folder contains the following files: + +- [`ConsistentState.spec`](specs/ConsistentState.spec) checks various properties specifying what is the consistent state of EulerEarn, what are the reachable setting configurations (such as caps and fee). +- [`Balances.spec`](specs/Balances.spec) checks that tokens are not kept on the EulerEarn contract. Any deposit ends up in the underlying vaults and any withdrawal is forwarded to the user. +- [`Enabled.spec`](specs/Enabled.spec) checks properties about enabled flag of market, notably that it correctly tracks the fact that the market is in the withdraw queue. +- [`Immutability.spec`](specs/Immutability.spec) checks that EulerEarn is immutable. +- [`Liveness.spec`](specs/Liveness.spec) checks some liveness properties of EulerEarn, notably that some emergency procedures are always available. +- [`PendingValues.spec`](specs/PendingValues.spec) checks properties on the values that are still under timelock. Those properties are notably useful to prove that actual storage variables, when set to the pending value, use a consistent value. +- [`Range.spec`](specs/Range.spec) checks the bounds (if any) of storage variables. +- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that EulerEarn is reentrancy safe by making sure that there are no untrusted external calls. +- [`Reverts.spec`](specs/Reverts.spec) checks the revert conditions on entrypoints. +- [`Roles.spec`](specs/Roles.spec) checks the access control and authorization granted by the respective EulerEarn roles. In particular it checks the hierarchy of roles. +- [`Timelock.spec`](specs/Timelock.spec) verifies computations for periods during which we know the values are under timelock. + +The [`certora/specs/summaries`](specs/summaries) folder contains summaries for different functions that simplify the behavior of different functions, namely mathematical functions in [`Math.spec`], and dispatching summaries that allow the prover to recognize the appropriate function to resolve to when we have external calls to underlying vaults. + +The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file. + +The [`certora/harnesses`](harnesses) folder contains harness contracts that enable the verification of EulerEarn, by exposing internal functions and fields. + +The [`certora/mocks`](mocks) folder contains mock contracts that simplify the verification of EulerEarn, by fixing reference implementations for the underlying token and vaults. + +The [`certora/scripts`](mocks) folder contains a patch that applies a simple modification to the EulerEarn contract that introduces ghost variables that simplify verification, and the `PatchAndCertoraRun.sh` script that is used to run rules after the patch is applied. + +The [`certora/gambit`](gambit) folder contains mutation testing - modified versions of the EulerEarn contract that have been injected with bugs and configuration files to run different rules on EulerEarn and the mutations to show that these bugs can be found by the given rules. + +## Specification imports graph + +Most rules follow the same setup starting with `Range.spec`, with the exception of Roles, Reentrancy, Immutability, Balances, and MarketInteractions that require a different setup with non-standard summaries that have assertions or modifications to rule-specific flags. + +```mermaid +graph +Liveness --> Reverts +Reverts --> ConsistentState +ConsistentState --> Timelock +Timelock --> Enabled +Enabled --> PendingValues +PendingValues --> Range +Roles +Reentrancy +Immutability +Balances +LostAssets --> Range +``` diff --git a/certora/confs/Balances.conf b/certora/confs/Balances.conf new file mode 100644 index 0000000..646709a --- /dev/null +++ b/certora/confs/Balances.conf @@ -0,0 +1,60 @@ +{ + "verify": "EulerEarnHarness:certora/specs/Balances.spec", + "msg": "Euler Earn - Rules about Balances", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "rule_sanity": "none", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol", + "certora/harnesses/ERC20Helper.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26", + "ERC20Helper": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf new file mode 100644 index 0000000..f49e5f0 --- /dev/null +++ b/certora/confs/ConsistentState.conf @@ -0,0 +1,60 @@ +{ + "verify": "EulerEarnHarness:certora/specs/ConsistentState.spec", + "msg": "Euler Earn - Rules about Consistency of State", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "rule_sanity": "none", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol", + "certora/harnesses/ERC20Helper.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26", + "ERC20Helper": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Conversions.conf b/certora/confs/Conversions.conf new file mode 100644 index 0000000..939e254 --- /dev/null +++ b/certora/confs/Conversions.conf @@ -0,0 +1,72 @@ +{ + "build_cache" : true, + //"prover_version" : "master", + "verify": "EulerEarnHarness:certora/specs/ConversionRules.spec", + "msg": "conversion rules", + "rule": [ + "conversionOfZero", + "convertToAssetsWeakAdditivity", + "convertToSharesWeakAdditivity", + "conversionWeakMonotonicity", + "conversionWeakIntegrity", + ], + "rule_sanity": "none", + "loop_iter": "1", + "optimistic_loop": true, + "global_timeout": "7200", + "smt_timeout": "6000", + "parametric_contracts": "EulerEarnHarness", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol", + "certora/harnesses/ERC20Helper.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + "ERC20Helper": "solc-0.8.26", + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "optimistic_summary_recursion" : true, + "process": "emv", + "prover_args": [ + "-depth 20", + //"-verifyCache ", + //"-verifyTACDumps", + //"-testMode", + //"-checkRuleDigest", + //"-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/ERC4626.conf b/certora/confs/ERC4626.conf new file mode 100644 index 0000000..7830813 --- /dev/null +++ b/certora/confs/ERC4626.conf @@ -0,0 +1,74 @@ +{ + "build_cache" : true, + //"prover_version" : "master", + "verify": "EulerEarnHarness:certora/specs/EulerEarnERC4626.spec", + "msg": "ERC4626-style properties and helper properties", + "rule": [ + "totalSupplyIsSumOfBalances", + "noAssetsOnEuler", + "underlyingCannotChange", + "configBalanceAndTotalSupply", + "zeroDepositZeroShares", + "redeemingAllValidity", + "zeroAllowanceOnAssets", + "onlyContributionMethodsReduceAssets", + ], + "rule_sanity": "none", + "loop_iter": "1", + "optimistic_loop": true, + "global_timeout": "7200", + "smt_timeout": "6000", + "parametric_contracts": "EulerEarnHarness", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol", + "certora/harnesses/ERC20Helper.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + "ERC20Helper": "solc-0.8.26", + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "optimistic_summary_recursion" : true, + "process": "emv", + "prover_args": [ + //"-verifyCache ", + //"-verifyTACDumps", + //"-testMode", + //"-checkRuleDigest", + //"-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Enabled.conf b/certora/confs/Enabled.conf new file mode 100644 index 0000000..6e52803 --- /dev/null +++ b/certora/confs/Enabled.conf @@ -0,0 +1,58 @@ +{ + "verify": "EulerEarnHarness:certora/specs/Enabled.spec", + "msg": "Euler Earn - Rules about Enabled Markets", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "rule_sanity": "none", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf new file mode 100644 index 0000000..47244db --- /dev/null +++ b/certora/confs/Immutability.conf @@ -0,0 +1,57 @@ +{ + "verify": "EulerEarnHarness:certora/specs/Immutability.spec", + "msg": "Euler Earn - Rules about Immutability", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf new file mode 100644 index 0000000..52e3b9a --- /dev/null +++ b/certora/confs/Liveness.conf @@ -0,0 +1,55 @@ +{ + "verify": "EulerEarnHarness:certora/specs/Liveness.spec", + "msg": "Euler Earn - rules about Liveness", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "rule_sanity": "none", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol", + "certora/harnesses/ERC20Helper.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26", + "ERC20Helper": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/LostAssets.conf b/certora/confs/LostAssets.conf new file mode 100644 index 0000000..ae4474e --- /dev/null +++ b/certora/confs/LostAssets.conf @@ -0,0 +1,56 @@ + +{ + "verify": "EulerEarnHarness:certora/specs/LostAssets.spec", + "msg": "Euler Earn - Properties on Lost Assets", + "loop_iter": "1", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts" : "EulerEarnHarness", + "rule_sanity" : "none", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map" : { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-cvlFunctionRevert true", + "-solvers [z3:def{randomSeed=110},z3:def{randomSeed=111},z3:def{randomSeed=112},z3:def{randomSeed=113},z3:def{randomSeed=114},z3:def{randomSeed=115},z3:def{randomSeed=116},z3:def{randomSeed=117},z3:def{randomSeed=118},z3:def{randomSeed=119}]" + ], + "build_cache": true +} diff --git a/certora/confs/PendingValues.conf b/certora/confs/PendingValues.conf new file mode 100644 index 0000000..53a43f9 --- /dev/null +++ b/certora/confs/PendingValues.conf @@ -0,0 +1,58 @@ +{ + "verify": "EulerEarnHarness:certora/specs/PendingValues.spec", + "msg": "Euler Earn - Rules about Pending Values", + "rule_sanity": "none", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Range.conf b/certora/confs/Range.conf new file mode 100644 index 0000000..3e11585 --- /dev/null +++ b/certora/confs/Range.conf @@ -0,0 +1,58 @@ +{ + "verify": "EulerEarnHarness:certora/specs/Range.spec", + "msg": "Euler Earn - Rules about Ranges", + "loop_iter": "2", + "optimistic_loop": true, + "rule_sanity": "none", + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf new file mode 100644 index 0000000..7710ea8 --- /dev/null +++ b/certora/confs/Reentrancy.conf @@ -0,0 +1,58 @@ +{ + "verify": "EulerEarnHarness:certora/specs/Reentrancy.spec", + "msg": "Euler Earn - Rules about Reentrancy", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "rule_sanity": "none", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf new file mode 100644 index 0000000..2332693 --- /dev/null +++ b/certora/confs/Reverts.conf @@ -0,0 +1,55 @@ +{ + "verify": "EulerEarnHarness:certora/specs/Reverts.spec", + "msg": "Euler Earn - rules about Reverts", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "rule_sanity": "none", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol", + "certora/harnesses/ERC20Helper.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26", + "ERC20Helper": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Roles.conf b/certora/confs/Roles.conf new file mode 100644 index 0000000..6885e26 --- /dev/null +++ b/certora/confs/Roles.conf @@ -0,0 +1,57 @@ +{ + "verify": "EulerEarnHarness:certora/specs/Roles.spec", + "msg": "Euler Earn - Rules about Roles", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Solvency.conf b/certora/confs/Solvency.conf new file mode 100644 index 0000000..362c1e7 --- /dev/null +++ b/certora/confs/Solvency.conf @@ -0,0 +1,67 @@ +{ + "build_cache":true, + //"prover_version" : "master", + "verify": "EulerEarnHarness:certora/specs/EulerEarnERC4626.spec", + "msg": "Solvency for all methods other than withdraw/redeem/deposit/mint", + "rule": [ + "TotalAssetsMoreThanSupplyAndFees", + ], + "rule_sanity": "none", + "loop_iter": "1", + "optimistic_loop": true, + "global_timeout": "7200", + "smt_timeout": "6000", + "parametric_contracts": "EulerEarnHarness", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol", + "certora/harnesses/ERC20Helper.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + "ERC20Helper": "solc-0.8.26", + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "optimistic_summary_recursion" : true, + "process": "emv", + "prover_args": [ + //"-verifyCache ", + //"-verifyTACDumps", + //"-testMode", + //"-checkRuleDigest", + //"-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/SolvencyInternalWithdraw.conf b/certora/confs/SolvencyInternalWithdraw.conf new file mode 100644 index 0000000..ebfb66c --- /dev/null +++ b/certora/confs/SolvencyInternalWithdraw.conf @@ -0,0 +1,66 @@ +{ + //"build_cache":true, + "prover_version" : "master", + "verify": "EulerEarnHarness:certora/specs/SolvencyInternal.spec", + "msg": "Solvency in internal methods - run on master", + "multi_assert_check" : true, + "rule_sanity": "none", + "loop_iter": "1", + "optimistic_loop": true, + "global_timeout": "7200", + "smt_timeout": "6000", + "parametric_contracts": "EulerEarnHarness", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol", + "certora/harnesses/ERC20Helper.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + "ERC20Helper": "solc-0.8.26", + }, + + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "optimistic_summary_recursion" : true, + "process": "emv", + "prover_args": [ + //"-verifyCache ", + //"-verifyTACDumps", + //"-testMode", + //"-checkRuleDigest", + //"-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/Timelock.conf b/certora/confs/Timelock.conf new file mode 100644 index 0000000..f2ff555 --- /dev/null +++ b/certora/confs/Timelock.conf @@ -0,0 +1,60 @@ +{ + "verify": "EulerEarnHarness:certora/specs/Timelock.spec", + "msg": "Euler Earn - Rules about Timelocks", + "loop_iter": "2", + "optimistic_loop": true, + "global_timeout": "7200", + "parametric_contracts": "EulerEarnHarness", + "rule_sanity": "none", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol", + "certora/harnesses/ERC20Helper.sol" + ], + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "IRMLinearKink": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26", + "ERC20Helper": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "process": "emv", + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ] +} diff --git a/certora/confs/setup/sanity_EulerEarn.conf b/certora/confs/setup/sanity_EulerEarn.conf new file mode 100644 index 0000000..b7349f1 --- /dev/null +++ b/certora/confs/setup/sanity_EulerEarn.conf @@ -0,0 +1,58 @@ +{ + "assert_autofinder_success": true, + "contract_recursion_limit": "1", + "files": [ + "certora/harnesses/EulerEarnHarness.sol", + "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol", + "lib/euler-vault-kit/lib/permit2/src/Permit2.sol", + "src/EulerEarnFactory.sol", + "test/mocks/PerspectiveMock.sol", + "certora/mocks/VaultMock0.sol", + "certora/mocks/VaultMock1.sol", + "certora/mocks/Token0.sol" + ], + "global_timeout": "7200", + "loop_iter": "2", + "msg": "sanity_EulerEarn", + "optimistic_loop": true, + "packages": [ + "ethereum-vault-connector=lib/ethereum-vault-connector/src", + "euler-vault-kit=lib/euler-vault-kit/src", + "forge-std=lib/forge-std/src", + "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate" + ], + "process": "emv", + "link": [ + "EulerEarnHarness:evc=EthereumVaultConnector", + "EulerEarnHarness:permit2Address=Permit2", + "EulerEarnFactory:permit2Address=Permit2", + "EulerEarnFactory:perspective=PerspectiveMock", + "VaultMock0:_asset=Token0", + "VaultMock1:_asset=Token0", + "EulerEarnHarness:_asset=Token0" + ], + "prover_args": [ + "-verifyCache ", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-cvlFunctionRevert true" + ], + "compiler_map": { + "EulerEarnHarness": "solc-0.8.26", + "EthereumVaultConnector": "solc-0.8.26", + "Permit2": "solc-0.8.17", + "EulerEarnFactory": "solc-0.8.26", + "PerspectiveMock": "solc-0.8.26", + "VaultMock0": "solc-0.8.26", + "VaultMock1": "solc-0.8.26", + "Token0": "solc-0.8.26" + }, + "solc_optimize": "200", + "solc_via_ir": true, + "verify": "EulerEarnHarness:certora/specs/setup/sanity_EulerEarn.spec", + "parametric_contracts": [ + "EulerEarnHarness" + ] +} diff --git a/certora/harnesses/ERC20Helper.sol b/certora/harnesses/ERC20Helper.sol new file mode 100644 index 0000000..0f8e5e2 --- /dev/null +++ b/certora/harnesses/ERC20Helper.sol @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity 0.8.26; + +import {SafeERC20, IERC20} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/utils/SafeERC20.sol"; + +contract ERC20Helper { + using SafeERC20 for IERC20; + + function balanceOf(address token, address user) external view returns (uint256) { + return IERC20(token).balanceOf(user); + } + + function totalSupply(address token) external view returns (uint256) { + return IERC20(token).totalSupply(); + } + + function safeTransferFrom(address token, address from, address to, uint256 amount) external { + IERC20(token).safeTransferFrom(from, to, amount); + } + + function allowance(address token, address owner, address spender) external view returns (uint256) { + return IERC20(token).allowance(owner, spender); + } +} \ No newline at end of file diff --git a/certora/harnesses/EulerEarnHarness.sol b/certora/harnesses/EulerEarnHarness.sol new file mode 100644 index 0000000..4e2b98d --- /dev/null +++ b/certora/harnesses/EulerEarnHarness.sol @@ -0,0 +1,195 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity 0.8.26; + +import "../../src/EulerEarn.sol"; +import "../../src/libraries/ConstantsLib.sol"; + +contract EulerEarnHarness is EulerEarn { + using Math for uint256; + + constructor( + address owner, + address evc, + address permit2, + uint256 initialTimelock, + address _asset, + string memory __name, + string memory __symbol + ) EulerEarn(owner, evc, permit2, initialTimelock, _asset, __name, __symbol) {} + + function fees() public view returns (uint256) { + uint256 feeShares; + (feeShares, , ) = _accruedFeeAndAssets(); + return feeShares; + } + + function wad() public view returns (uint256) { + return WAD; + } + + function virtualAmount() public view returns (uint256) { + return ConstantsLib.VIRTUAL_AMOUNT; + } + + function accruedFeeAndAssets() external view returns (uint256, uint256, uint256) { + return _accruedFeeAndAssets(); + } + + function accruedFeeAndAssetsNotSummarized() + external + view + returns (uint256 feeShares, uint256 newTotalAssets, uint256 newLostAssets) + { + // The assets that the Earn vault has on the strategy vaults. + uint256 realTotalAssets; + for (uint256 i; i < withdrawQueue.length; ++i) { + IERC4626 id = withdrawQueue[i]; + realTotalAssets += _expectedSupplyAssets(id); + } + + uint256 lastTotalAssetsCached = lastTotalAssets; + if (realTotalAssets < lastTotalAssetsCached - lostAssets) { + // If the vault lost some assets (realTotalAssets decreased), lostAssets is increased. + newLostAssets = lastTotalAssetsCached - realTotalAssets; + } else { + // If it did not, lostAssets stays the same. + newLostAssets = lostAssets; + } + + newTotalAssets = realTotalAssets + newLostAssets; + uint256 totalInterest = newTotalAssets - lastTotalAssetsCached; + if (totalInterest != 0 && fee != 0) { + // It is acknowledged that `feeAssets` may be rounded down to 0 if `totalInterest * fee < WAD`. + uint256 feeAssets = totalInterest.mulDiv(fee, WAD); + // The fee assets is subtracted from the total assets in this calculation to compensate for the fact + // that total assets is already increased by the total interest (including the fee assets). + feeShares = + _convertToSharesWithTotals(feeAssets, totalSupply(), newTotalAssets - feeAssets, Math.Rounding.Floor); + } + } + + function expectedSupplyAssets(IERC4626 id) external view returns (uint256) { + return _expectedSupplyAssets(id); + } + + function realTotalAssets() public view returns (uint256) { + uint256 realTotalAssets; + for (uint256 i; i < withdrawQueue.length; ++i) { + IERC4626 id = withdrawQueue[i]; + realTotalAssets += _expectedSupplyAssets(id); + } + return realTotalAssets; + } + + function msgSender() public view returns (address) { + return _msgSender(); + } + + function pendingTimelock_() external view returns (PendingUint136 memory) { + return pendingTimelock; + } + + function pendingGuardian_() external view returns (PendingAddress memory) { + return pendingGuardian; + } + + function pendingCap_(IERC4626 id) external view returns (PendingUint136 memory) { + return pendingCap[id]; + } + + function minTimelock() external pure returns (uint256) { + return ConstantsLib.POST_INITIALIZATION_MIN_TIMELOCK; + } + + function maxTimelock() external pure returns (uint256) { + return ConstantsLib.MAX_TIMELOCK; + } + + function maxQueueLength() external pure returns (uint256) { + return ConstantsLib.MAX_QUEUE_LENGTH; + } + + function maxFee() external pure returns (uint256) { + return ConstantsLib.MAX_FEE; + } + + function config_(IERC4626 id) external view returns (MarketConfig memory) { + return config[id]; + } + + function supplyQGetAt(uint256 index) external view returns (IERC4626) + { + return supplyQueue[index]; + } + + function supplyQLength() external view returns (uint256) + { + return supplyQueue.length; + } + + function withdrawQGetAt(uint256 index) external view returns (IERC4626) + { + return withdrawQueue[index]; + } + + function withdrawQLength() external view returns (uint256) + { + return withdrawQueue.length; + } + + function nextGuardianUpdateTime() external view returns (uint256 nextTime) { + nextTime = block.timestamp + timelock; + + if (pendingTimelock.validAt != 0) { + nextTime = Math.min(nextTime, pendingTimelock.validAt + pendingTimelock.value); + } + + uint256 validAt = pendingGuardian.validAt; + if (validAt != 0) nextTime = Math.min(nextTime, validAt); + } + + function nextCapIncreaseTime(IERC4626 id) external view returns (uint256 nextTime) { + nextTime = block.timestamp + timelock; + + if (pendingTimelock.validAt != 0) { + nextTime = Math.min(nextTime, pendingTimelock.validAt + pendingTimelock.value); + } + + uint256 validAt = pendingCap[id].validAt; + if (validAt != 0) nextTime = Math.min(nextTime, validAt); + } + + function nextTimelockDecreaseTime() external view returns (uint256 nextTime) { + nextTime = block.timestamp + timelock; + + if (pendingTimelock.validAt != 0) nextTime = Math.min(nextTime, pendingTimelock.validAt); + } + + function nextRemovableTime(IERC4626 id) external view returns (uint256 nextTime) { + nextTime = block.timestamp + timelock; + + if (pendingTimelock.validAt != 0) { + nextTime = Math.min(nextTime, pendingTimelock.validAt + pendingTimelock.value); + } + + uint256 removableAt = config[id].removableAt; + if (removableAt != 0) nextTime = Math.min(nextTime, removableAt); + } + + function getVaultAsset(IERC4626 id) external view returns (address asset) { + return id.asset(); + } + + function reentrancyGuardEntered() external view returns (bool) { + return _reentrancyGuardEntered(); + } + + function msgSenderOnlyEVCAccountOwner() external returns (address) { + return _msgSenderOnlyEVCAccountOwner(); + } + + function isStrategyAllowedHarness(IERC4626 id) external returns (bool) { + return IEulerEarnFactory(creator).isStrategyAllowed(address(id)); + } + +} \ No newline at end of file diff --git a/certora/mocks/Token0.sol b/certora/mocks/Token0.sol new file mode 100644 index 0000000..bbe2679 --- /dev/null +++ b/certora/mocks/Token0.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: MIT +pragma solidity >=0.8.21; + +import {ERC20} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol"; + +contract Token0 is ERC20 { + constructor() ERC20("Token0", "TOK0") {} +} \ No newline at end of file diff --git a/certora/mocks/VaultMock0.sol b/certora/mocks/VaultMock0.sol new file mode 100644 index 0000000..604c182 --- /dev/null +++ b/certora/mocks/VaultMock0.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: MIT +pragma solidity >=0.8.21; + +import { + IERC20, + IERC4626, + ERC20, + ERC4626, + Math +} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/ERC4626.sol"; + +contract VaultMock0 is ERC4626 { + constructor(IERC20 asset) ERC4626(asset) ERC20("VaultMock0", "V0") {} + + function maxDeposit(address owner) public view virtual override returns (uint256) { + return type(uint256).max; + } + + function getTotalSupply(address vault) external view returns (uint256) { + return IERC20(vault).totalSupply(); + } + + function getConvertToShares(address vault, uint256 assets) external view returns (uint256) { + return IERC4626(vault).convertToShares(assets); + } + + function getConvertToAssets(address vault, uint256 shares) external view returns (uint256) { + return IERC4626(vault).convertToAssets(shares); + } + + function convertToAssets(uint256 shares, Math.Rounding rounding) external view returns (uint256) { + return _convertToAssets(shares, rounding); + } + + function convertToShares(uint256 assets, Math.Rounding rounding) external view returns (uint256) { + return _convertToAssets(assets, rounding); + } + +} \ No newline at end of file diff --git a/certora/mocks/VaultMock1.sol b/certora/mocks/VaultMock1.sol new file mode 100644 index 0000000..119de7c --- /dev/null +++ b/certora/mocks/VaultMock1.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: MIT +pragma solidity >=0.8.21; + +import { + IERC20, + IERC4626, + ERC20, + ERC4626, + Math +} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/ERC4626.sol"; + +contract VaultMock1 is ERC4626 { + constructor(IERC20 asset) ERC4626(asset) ERC20("VaultMock1", "V1") {} + + function maxDeposit(address owner) public view virtual override returns (uint256) { + return type(uint256).max; + } + + function getTotalSupply(address vault) external view returns (uint256) { + return IERC20(vault).totalSupply(); + } + + function getConvertToShares(address vault, uint256 assets) external view returns (uint256) { + return IERC4626(vault).convertToShares(assets); + } + + function getConvertToAssets(address vault, uint256 shares) external view returns (uint256) { + return IERC4626(vault).convertToAssets(shares); + } + + function convertToAssets(uint256 shares, Math.Rounding rounding) external view returns (uint256) { + return _convertToAssets(shares, rounding); + } + + function convertToShares(uint256 assets, Math.Rounding rounding) external view returns (uint256) { + return _convertToAssets(assets, rounding); + } +} \ No newline at end of file diff --git a/certora/scripts/EulerEarn.patch b/certora/scripts/EulerEarn.patch new file mode 100644 index 0000000..beef118 --- /dev/null +++ b/certora/scripts/EulerEarn.patch @@ -0,0 +1,106 @@ +diff --git a/src/EulerEarn.sol b/src/EulerEarn.sol +index 7b3634c..b54636f 100644 +--- a/src/EulerEarn.sol ++++ b/src/EulerEarn.sol +@@ -106,6 +106,18 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + /// @dev "Overrides" the ERC20's storage variable to be able to modify it. + string private _symbol; + ++ // ghost variables ++ // The index of the identifier of the last market withdrawn. ++ uint256 public lastIndexWithdraw; ++ // The rank of a market identifier in the withdraw queue, returns 0 if the corresponding market is not in the withdraw queue. ++ mapping(address => uint256) public withdrawRank; ++ // The last index at which a market identifier has been removed from the withdraw queue. ++ mapping(address => uint256) public deletedAt; ++ ++ // hooks for cvl assertions ++ function HOOK_after_accrueInterest() internal {} ++ function HOOK_after_withdrawStrategy(uint256) internal {} ++ + /* CONSTRUCTOR */ + + /// @dev Initializes the contract. +@@ -353,6 +365,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + seen[prevIndex] = true; + + newWithdrawQueue[i] = id; ++ ++ // HARNESS ++ withdrawRank[address(id)] = i + 1; + } + + for (uint256 i; i < currLength; ++i) { +@@ -370,6 +385,10 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + } + } + ++ // HARNESS ++ deletedAt[address(id)] = i; ++ delete withdrawRank[address(id)]; ++ + delete config[id]; + } + } +@@ -546,6 +565,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + /// @inheritdoc IERC4626 + function deposit(uint256 assets, address receiver) public override nonReentrant returns (uint256 shares) { + _accrueInterest(); ++ HOOK_after_accrueInterest(); + + shares = _convertToSharesWithTotals(assets, totalSupply(), lastTotalAssets, Math.Rounding.Floor); + +@@ -557,6 +577,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + /// @inheritdoc IERC4626 + function mint(uint256 shares, address receiver) public override nonReentrant returns (uint256 assets) { + _accrueInterest(); ++ HOOK_after_accrueInterest(); + + assets = _convertToAssetsWithTotals(shares, totalSupply(), lastTotalAssets, Math.Rounding.Ceil); + +@@ -571,6 +592,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + returns (uint256 shares) + { + _accrueInterest(); ++ HOOK_after_accrueInterest(); + + // Do not call expensive `maxWithdraw` and optimistically withdraw assets. + +@@ -587,6 +609,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + returns (uint256 assets) + { + _accrueInterest(); ++ HOOK_after_accrueInterest(); + + // Do not call expensive `maxRedeem` and optimistically redeem shares. + +@@ -715,8 +738,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + // This can lead to a small accrual of `lostAssets` at the next interaction. + // clamp at 0 so the error raised is the more informative NotEnoughLiquidity. + _updateLastTotalAssets(lastTotalAssets.zeroFloorSub(assets)); +- ++ uint256 assetsIn = assets; + _withdrawStrategy(assets); ++ HOOK_after_withdrawStrategy(assetsIn); + + super._withdraw(caller, receiver, owner, assets, shares); + } +@@ -767,6 +791,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + IERC20(asset()).forceApproveMaxWithPermit2(address(id), permit2); + + if (!marketConfig.enabled) { ++ // HARNESS ++ withdrawRank[address(id)] = withdrawQueue.length + 1; ++ + withdrawQueue.push(id); + + if (withdrawQueue.length > ConstantsLib.MAX_QUEUE_LENGTH) revert ErrorsLib.MaxQueueLengthExceeded(); +@@ -824,6 +851,8 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar + /// @dev Withdraws `assets` from the strategy vaults. + function _withdrawStrategy(uint256 assets) internal { + for (uint256 i; i < withdrawQueue.length; ++i) { ++ // HARNESS ++ lastIndexWithdraw = i; + IERC4626 id = withdrawQueue[i]; + + uint256 toWithdraw = diff --git a/certora/scripts/PatchAndCertoraRun.sh b/certora/scripts/PatchAndCertoraRun.sh new file mode 100755 index 0000000..6caaf89 --- /dev/null +++ b/certora/scripts/PatchAndCertoraRun.sh @@ -0,0 +1,24 @@ +#!/bin/bash + +# run from root directory certora/scripts/PatchAndCertoraRun + +set -e + +CONF_FILE=$1 + +if [ -z "$CONF_FILE" ]; then + echo "Error: No conf file provided." + echo "Usage: $0 " + exit 1 +fi + +# Run Munge.sh +git apply certora/scripts/EulerEarn.patch + +# Run certoraRun with the provided conf file +if ! certoraRun certora/confs/$CONF_FILE --server production; then + echo "certoraRun failed, continuing to Unmunge." +fi + +# Run Unmunge.sh +git apply -R certora/scripts/EulerEarn.patch \ No newline at end of file diff --git a/certora/scripts/patch.sh b/certora/scripts/patch.sh new file mode 100755 index 0000000..431e149 --- /dev/null +++ b/certora/scripts/patch.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# run from root directory certora/scripts/patch.sh + +set -e + +git apply certora/scripts/EulerEarn.patch + diff --git a/certora/specs/Balances.spec b/certora/specs/Balances.spec new file mode 100644 index 0000000..91046f2 --- /dev/null +++ b/certora/specs/Balances.spec @@ -0,0 +1,355 @@ +// Aggregating different rules about balances from MetamorhpoV1,V1.1 and SiloVault. + +import "summaries/Math.spec"; + +using VaultMock0 as v0; +using VaultMock1 as v1; +using EulerEarnHarness as EulerEarnHarness; +using ERC20Helper as ERC20Helper; + +methods { + // These summaries are defined in this file and include assertions - see below + function _.deposit(uint256 assets, address receiver) external => summaryDeposit(calledContract, assets, receiver) expect (uint256) ALL; + function _.withdraw(uint256 assets, address receiver, address spender) external => summaryWithdraw(calledContract, assets, receiver, spender) expect (uint256) ALL; + function _.redeem(uint256 shares, address receiver, address spender) external => summaryRedeem(calledContract, shares, receiver, spender) expect (uint256) ALL; + + // Redefining dispatchers because we can't import the dispatching for withdraw. + function _.totalSupply() external => DISPATCHER(true); + function _.isStrategyAllowed(address) external => DISPATCHER(true); + function _.permit2Address() external => DISPATCHER(true); + function _.transfer(address, uint256) external => DISPATCHER(true); + function _.transferFrom(address, address, uint256) external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.approve(address,address,uint160,uint48) external => DISPATCHER(true); + function _.previewRedeem(uint256 shares) external with (env e) => cvlDispatchPreviewRedeem(shares, calledContract, e) expect uint256; + function _.maxWithdraw(address owner) external with (env e) => cvlDispatchMaxWithdraw(owner, calledContract, e) expect uint256; + function _.asset() external with (env e) => cvlDispatchAsset(calledContract, e) expect address; + function _.maxDeposit(address owner) external with (env e) => cvlDispatchMaxDeposit(owner, calledContract, e) expect uint256; + function _.convertToAssets(uint256 shares) external with (env e) + => cvlDispatchConvertToAssets(shares,calledContract,e) expect uint256; + function _.convertToShares(uint256 shares) external with (env e) + => cvlDispatchConvertToShares(shares,calledContract,e) expect uint256; + + function ERC20Helper.allowance(address, address, address) external returns (uint256) envfree; + function ERC20Helper.totalSupply(address) external returns (uint256) envfree; + function ERC20Helper.safeTransferFrom(address,address,address,uint256) external envfree; + function ERC20Helper.balanceOf(address,address) external returns (uint256) envfree; + function asset() external returns (address) envfree; + function config_(address) external returns(EulerEarnHarness.MarketConfig) envfree; + function supplyQGetAt(uint256) external returns (address) envfree; + function supplyQLength() external returns (uint256) envfree; + function withdrawQGetAt(uint256) external returns (address) envfree; + function withdrawQLength() external returns (uint256) envfree; + function getVaultAsset(address) external returns address envfree; + function v0.getConvertToShares(address vault, uint256 assets) external returns(uint256) envfree; + function v0.getConvertToAssets(address vault, uint256 shares) external returns(uint256) envfree; +} + + +function summaryDeposit(address market, uint256 assets, address receiver) returns uint256 { + assert assets != 0; + assert receiver == currentContract; + require market != currentContract; + + require config_(market).cap > 0 => config_(market).enabled; + require config_(market).enabled => getVaultAsset(market) == asset(), "invariant proven in ConsistentState.spec"; + + ERC20Helper.safeTransferFrom(asset(), currentContract, market, assets); + return v0.getConvertToShares(market, assets); +} + +function summaryWithdraw(address market, uint256 assets, address receiver, address spender) returns uint256 { + assert receiver == currentContract; + assert spender == currentContract; + require market != currentContract; + + // Safe require because it is verified in MarketInteractions. + require config_(market).enabled; + require config_(market).enabled => getVaultAsset(market) == asset(), "invariant proven in ConsistentState.spec"; + + address asset = asset(); + + ERC20Helper.safeTransferFrom(asset, market, currentContract, assets); + + return v0.getConvertToShares(market, assets); +} + +function summaryRedeem(address market, uint256 shares, address receiver, address spender) returns uint256 { + assert receiver == currentContract; + assert spender == currentContract; + require market != currentContract; + + // Safe require because it is verified in MarketInteractions. + require config_(market).enabled; + require config_(market).enabled => getVaultAsset(market) == asset(), "invariant proven in ConsistentState.spec"; + + address asset = asset(); + uint256 assets = v0.getConvertToAssets(market, shares); + + ERC20Helper.safeTransferFrom(asset, market, currentContract, assets); + + return assets; +} + +// Check balances change on deposit. +rule depositTokenChange(env e, uint256 assets, address receiver) { + address asset = asset(); + + // Trick to require that all the following addresses are different. + require asset == 0x11; + require currentContract == 0x12; + require msgSender(e) == 0x13; + + //this together with loop_iter == 2 ensures that the markets don't call "deposit" on the Vault + require supplyQGetAt(0) != msgSender(e); + require supplyQGetAt(1) != msgSender(e); + + require ERC20Helper.balanceOf(asset, currentContract) + + ERC20Helper.balanceOf(asset, msgSender(e)) <= ERC20Helper.totalSupply(asset); + + uint256 balanceVaultBefore = ERC20Helper.balanceOf(asset, currentContract); + uint256 balanceSenderBefore = ERC20Helper.balanceOf(asset, msgSender(e)); + deposit(e, assets, receiver); + uint256 balanceVaultAfter = ERC20Helper.balanceOf(asset, currentContract); + uint256 balanceSenderAfter = ERC20Helper.balanceOf(asset, msgSender(e)); + + require balanceSenderBefore > balanceSenderAfter; + + assert balanceVaultAfter == balanceVaultBefore; + assert assert_uint256(balanceSenderBefore - balanceSenderAfter) == assets; + // add third assert that appeared in metamorpho. +} + +// Check balance changes on withdraw. +rule withdrawTokenChange(env e, uint256 assets, address receiver, address owner) { + address asset = asset(); + + // Trick to require that all the following addresses are different. + require asset == 0x11; + require currentContract == 0x12; + require receiver == 0x13; + + //this togehter with loop_iter == 2 ensures that the markets don't withdraw from the Vault + require withdrawQGetAt(0) != msgSender(e); + require withdrawQGetAt(1) != msgSender(e); + + //with loop_iter = 2 this shows whether the reveiver is among the markets in the WithdrawQ + //(the caller of withdraw may set any receiver address so shouldn't discard this option) + bool isReceiverAVault = receiver == withdrawQGetAt(0) || receiver == withdrawQGetAt(1); + + require ERC20Helper.balanceOf(asset, currentContract) + + ERC20Helper.balanceOf(asset, msgSender(e)) <= ERC20Helper.totalSupply(asset); + require ERC20Helper.balanceOf(asset, currentContract) + + ERC20Helper.balanceOf(asset, receiver) <= ERC20Helper.totalSupply(asset); + + uint256 balanceVaultBefore = ERC20Helper.balanceOf(asset, currentContract); + uint256 balanceReceiverBefore = ERC20Helper.balanceOf(asset, receiver); + withdraw(e, assets, receiver, owner); + uint256 balanceVaultAfter = ERC20Helper.balanceOf(asset, currentContract); + uint256 balanceReceiverAfter = ERC20Helper.balanceOf(asset, receiver); + + // no overflow happened. + // Another way to ensure this is to require sum_i{balanceOf(withdrawQ[i])} + balanceOf(receiver) <= totalSupply + require balanceReceiverAfter > balanceReceiverBefore; + + assert balanceVaultAfter == balanceVaultBefore; + + // the balance of receiver must change unless the receiver is one of the markets in the queue + assert !isReceiverAVault => assert_uint256(balanceReceiverAfter - balanceReceiverBefore) == assets; +} + +// Check that balances do not change on reallocate. +rule reallocateTokenChange(env e, EulerEarnHarness.MarketAllocation[] allocations) { + address asset = asset(); + + // Trick to require that all the following addresses are different. + require asset == 0x11; + require currentContract == 0x12; + require msgSender(e) == 0x13; + + // this together with loop_iter = 2 ensures that markets in the withdrawQ are not Allocators and not SiloVault + // based on enabledIsInWithdrawQueue + require config_(allocations[0].id).enabled => allocations[0].id != msgSender(e); + require config_(allocations[1].id).enabled => allocations[1].id != msgSender(e); + require config_(allocations[0].id).enabled => allocations[0].id != currentContract; + require config_(allocations[1].id).enabled => allocations[1].id != currentContract; + + uint256 balanceVaultBefore = ERC20Helper.balanceOf(asset, currentContract); + uint256 balanceSenderBefore = ERC20Helper.balanceOf(asset, msgSender(e)); + reallocate(e, allocations); + + uint256 balanceVaultAfter = ERC20Helper.balanceOf(asset, currentContract); + uint256 balanceSenderAfter = ERC20Helper.balanceOf(asset, msgSender(e)); + + assert balanceVaultAfter == balanceVaultBefore; + assert balanceSenderAfter == balanceSenderBefore; +} + +ghost mathint vaultBalanceIncrease; +ghost mathint vaultBalanceDecrease; + +// we just want to track the increases and decreases of SiloVault's balance +hook Sstore Token0._balances[KEY address user] uint256 newBalance (uint256 oldBalance) { + if (user == EulerEarnHarness) + { + if (newBalance > oldBalance) vaultBalanceIncrease = vaultBalanceIncrease + newBalance - oldBalance; + if (newBalance < oldBalance) vaultBalanceDecrease = vaultBalanceDecrease - newBalance + oldBalance; + } +} + +// Shows that SiloVault doesn't hoard the tokens, i.e., that it sends outs everything that it receives. +rule vaultBalanceNeutral(env e, method f) + filtered { f -> !f.isView } +{ + require msgSender(e) != EulerEarnHarness; + require msgSender(e) != v0; + address receiver; + require receiver != EulerEarnHarness; + address asset = asset(); + uint256 balance_pre = ERC20Helper.balanceOf(asset, EulerEarnHarness); + dispatchCall(e, f, receiver); + uint256 balance_post = ERC20Helper.balanceOf(asset, EulerEarnHarness); + + assert balance_pre == balance_post; +} + +// a manual dispatcher that allows to constrain the receiver +function dispatchCall(env e, method f, address receiver) +{ + if (f.selector == sig:withdraw(uint256, address, address).selector) + { + uint256 _assets; address _owner; + withdraw(e, _assets, receiver, _owner); + } + else if (f.selector == sig:redeem(uint256, address, address).selector) + { + uint256 _shares; address _owner; + redeem(e, _shares, receiver, _owner); + } + else if (f.selector == sig:deposit(uint256, address).selector) + { + uint256 _assets; + deposit(e, _assets, receiver); + } + else if (f.selector == sig:mint(uint256, address).selector) + { + uint256 _shares; + mint(e, _shares, receiver); + } + else + { + calldataarg args; + f(e, args); + } +} + +rule onlySpecicifiedMethodsCanDecreaseMarketBalance(env e, method f, address market) +{ + require msgSender(e) != currentContract; + address asset = asset(); + + // otherwise deposit overflows and decreases the balance + require ERC20Helper.balanceOf(asset, currentContract) + + ERC20Helper.balanceOf(asset, msgSender(e)) <= ERC20Helper.totalSupply(asset); + + uint balanceBefore = ERC20Helper.balanceOf(asset, currentContract); + calldataarg args; + f(e, args); + bool isAllowedToDecreaseBalance = + (f.selector == sig:withdraw(uint256, address, address).selector || + f.selector == sig:redeem(uint256, address, address).selector || + f.selector == sig:reallocate(EulerEarnHarness.MarketAllocation[]).selector); + uint balanceAfter = ERC20Helper.balanceOf(asset, currentContract); + assert balanceAfter < balanceBefore => isAllowedToDecreaseBalance; +} + + +function cvlDispatchPreviewRedeem(uint256 shares, address called, env e) returns uint256 { + if(called == v0) { + return v0.previewRedeem(e, shares); + } + if(called == v1) { + return v1.previewRedeem(e, shares); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchMaxWithdraw(address owner, address called, env e) returns uint256 { + if(called == v0) { + return v0.maxWithdraw(e, owner); + } + if(called == v1) { + return v1.maxWithdraw(e, owner); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + + + +function cvlDispatchWithdraw(uint256 assets, address receiver, address owner, address called, env e) returns uint256 { + if(called == v0) { + return v0.withdraw(e, assets, receiver, owner); + } + if(called == v1) { + return v1.withdraw(e, assets, receiver, owner); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchAsset(address called, env e) returns address { + if(called == v0) { + return v0.asset(e); + } + if(called == v1) { + return v1.asset(e); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchMaxDeposit(address owner, address called, env e) returns uint256 { + if(called == v0) { + return v0.maxDeposit(e, owner); + } + if(called == v1) { + return v1.maxDeposit(e, owner); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchDeposit(uint256 assets, address receiver, address called, env e) returns uint256 { + if(called == v0) { + return v0.deposit(e, assets, receiver); + } + if(called == v1) { + return v1.deposit(e, assets, receiver); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchConvertToAssets(uint256 shares, address called, env e) returns uint256 { + if(called == v0) { + return v0.convertToAssets(e, shares); + } + if(called == v1) { + return v1.convertToAssets(e, shares); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchConvertToShares(uint256 shares, address called, env e) returns uint256 { + if(called == v0) { + return v0.convertToShares(e, shares); + } + if(called == v1) { + return v1.convertToShares(e, shares); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} \ No newline at end of file diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec new file mode 100644 index 0000000..bc1cfef --- /dev/null +++ b/certora/specs/ConsistentState.spec @@ -0,0 +1,155 @@ +// Based on ConsistentStates.spec, TokenApproval.spec, lastUpdated.spec in SiloVault spec + +import "Timelock.spec"; + +methods { + function asset() external returns(address) envfree; + function feeRecipient() external returns address envfree; + function getVaultAsset(address) external returns address envfree; + function ERC20Helper.allowance(address, address, address) external returns (uint256) envfree; + function ERC20Helper.totalSupply(address) external returns (uint256) envfree; + function ERC20Helper.safeTransferFrom(address,address,address,uint256) external envfree; + function owner() external returns(address) envfree; + function curator() external returns(address) envfree; + function isAllocator(address target) external returns(bool) envfree; + function permit2Address() external returns address envfree; +} + +function hasCuratorRole(address user) returns bool { + return user == owner() || user == curator(); +} + +function hasAllocatorRole(address user) returns bool { + return user == owner() || user == curator() || isAllocator(user); +} + +function hasGuardianRole(address user) returns bool { + return user == owner() || user == guardian(); +} + +// Check that the fee cannot accrue to an unset fee recipient +// Verified +invariant noFeeToUnsetFeeRecipient() + feeRecipient() == 0 => fee() == 0; + +function hasSupplyCapIsEnabled(address market) returns bool { + EulerEarnHarness.MarketConfig config = config_(market); + + return config.cap > 0 => config.enabled; +} + +// Check that having a positive supply cap implies that the market is enabled. +// This invariant is useful to conclude that markets that are not enabled cannot be interacted with (notably for reallocate). +// Verified +invariant supplyCapIsEnabled(address market) + hasSupplyCapIsEnabled(market); + +function hasPendingSupplyCapHasConsistentAsset(address market) returns bool { + return pendingCap_(market).validAt > 0 => getVaultAsset(market) == asset(); +} + +// Check that there can only be pending caps on markets where the loan asset is the asset of the vault +// Verified +invariant pendingSupplyCapHasConsistentAsset(address market) + hasPendingSupplyCapHasConsistentAsset(market); + +function isEnabledHasConsistentAsset(address market) returns bool { + return config_(market).enabled => getVaultAsset(market) == asset(); +} + +// Check that having a positive cap implies that the loan asset is the asset of the vault. +// Verified +invariant enabledHasConsistentAsset(address market) + isEnabledHasConsistentAsset(market) +{ preserved acceptCap(address _market) with (env e) { + requireInvariant pendingSupplyCapHasConsistentAsset(market); + require e.block.timestamp > 0; + } +} + +function hasSupplyCapIsNotMarkedForRemoval(address market) returns bool { + EulerEarnHarness.MarketConfig config = config_(market); + + return config.cap > 0 => config.removableAt == 0; +} + +// title Check that a market with a positive cap cannot be marked for removal. +// Verified +invariant supplyCapIsNotMarkedForRemoval(address market) + hasSupplyCapIsNotMarkedForRemoval(market); + +function isNotEnabledIsNotMarkedForRemoval(address market) returns bool { + EulerEarnHarness.MarketConfig config = config_(market); + + return !config.enabled => config.removableAt == 0; +} + +// Check that a non-enabled market cannot be marked for removal. +// Verified +invariant notEnabledIsNotMarkedForRemoval(address market) + isNotEnabledIsNotMarkedForRemoval(market); + +// Check that a market with a pending cap cannot be marked for removal. +// Verified +invariant pendingCapIsNotMarkedForRemoval(address market) + pendingCap_(market).validAt > 0 => config_(market).removableAt == 0; + +// Check that any new market in the supply queue necessarily has a positive cap. +// Verified +rule newSupplyQueueEnsuresPositiveCap(env e, address[] newSupplyQueue) +{ + uint256 i; + + setSupplyQueue(e, newSupplyQueue); + + address market = supplyQueue(i); + + assert config_(market).cap > 0; +} + +//The following two rules are from TokenApproval.spec in Silo and caught bugs in Silo. + +// violated after fix. +invariant noCapThenNoApproval(address market) + config_(market).cap == 0 => ERC20Helper.allowance(asset(), currentContract, market) == 0 + { + preserved acceptCap(address id) with (env e) { + // not sure all of these assumptions are necessary but all are legitimate. + require market != permit2Address(); + require msgSender(e) != currentContract; + requireInvariant pendingCapIsUint136(id); + requireInvariant enabledHasPositiveRank(id); + requireInvariant supplyCapIsEnabled(id); + requireInvariant withdrawRankCorrect(id); + requireInvariant noBadPendingCap(id); + requireInvariant noCapThenNoApproval(id); + requireInvariant pendingCapIsUint136(market); + requireInvariant enabledHasPositiveRank(market); + requireInvariant supplyCapIsEnabled(market); + requireInvariant withdrawRankCorrect(market); + requireInvariant noBadPendingCap(market); + requireInvariant noCapThenNoApproval(market); + } + preserved with (env e) { + require msgSender(e) != currentContract; + requireInvariant pendingCapIsUint136(market); + requireInvariant noBadPendingCap(market); + requireInvariant supplyCapIsEnabled(market); + } + } + +// violated after fix. +invariant notInWithdrawQThenNoApproval(address market) + withdrawRank(market) == 0 => ERC20Helper.allowance(asset(), currentContract, market) == 0 + { + preserved with (env e) { + require market != permit2Address(); + require msgSender(e) != currentContract; + requireInvariant pendingCapIsUint136(market); + requireInvariant enabledHasPositiveRank(market); + requireInvariant supplyCapIsEnabled(market); + requireInvariant withdrawRankCorrect(market); + requireInvariant noBadPendingCap(market); + requireInvariant noCapThenNoApproval(market); + } +} \ No newline at end of file diff --git a/certora/specs/ConversionRules.spec b/certora/specs/ConversionRules.spec new file mode 100644 index 0000000..0f29198 --- /dev/null +++ b/certora/specs/ConversionRules.spec @@ -0,0 +1,147 @@ +//Based on generic ERC4626 specitication: https://github.com/Certora/Examples/blob/master/DEFI/ERC4626/certora/specs/ERC4626.spec + +import "./EulerEarnERC4626.spec"; + +methods { + function _._accruedFeeAndAssets() internal with (env e) => _accruedFeeAndAssetsWithCaching(e) expect (uint256,uint256,uint256); // If this summary is used you need to call initCacheToZero at the start of every rule/invariant + function expectedSupplyAssets(address) external returns uint256 envfree; +} + +//summarization with caching -- doesn't approximate anything -- sometimes easier for the prover + +ghost uint256 lastTotalAssetsCached; +ghost uint256 lostAssetsCached; +ghost uint96 feeCached; +ghost uint256 totalSupplyCached; +ghost address firstMarketCached; +ghost uint256 firstMarketExpectedSupplyAssetsCached; +ghost uint256 feeSharesCached; +ghost uint256 newTotalAssetsCached; +ghost uint256 newLostAssetsCached; + + +function initCacheToZero() { + feeSharesCached = 0; + newTotalAssetsCached = 0; + newLostAssetsCached = 0; +} + +function _accruedFeeAndAssetsWithCaching(env e) returns (uint256,uint256,uint256) { + uint256 lastTotalAssets = lastTotalAssets(); + uint256 lostAssets = lostAssets(); + uint96 fee = fee(); + uint256 totalSupply = totalSupply(); + address firstMarket = withdrawQGetAt(0); + uint256 firstMarketExpectedSupplyAssets = expectedSupplyAssets(firstMarket); + if (feeSharesCached == 0 && newTotalAssetsCached == 0 && newLostAssetsCached == 0) { + lastTotalAssetsCached = lastTotalAssets; + lostAssetsCached = lostAssets; + feeCached = fee; + totalSupplyCached = totalSupply; + firstMarketCached = firstMarket; + firstMarketExpectedSupplyAssetsCached = firstMarketExpectedSupplyAssets; + uint256 feeSharesRet; + uint256 newTotalAssetsRet; + uint256 newLostAssetsRet; + (feeSharesRet, newTotalAssetsRet, newLostAssetsRet) = accruedFeeAndAssetsNotSummarized(e); + feeSharesCached = feeSharesRet; + newTotalAssetsCached = newTotalAssetsRet; + newLostAssetsCached = newLostAssetsRet; + return (feeSharesRet, newTotalAssetsRet, newLostAssetsRet); + } + else { + if ( + lastTotalAssets == lastTotalAssetsCached && + lostAssets == lostAssetsCached && + fee == feeCached && + totalSupply == totalSupplyCached && + firstMarket == firstMarketCached && + firstMarketExpectedSupplyAssets == firstMarketExpectedSupplyAssetsCached + ) { + uint256 feeSharesRet = feeSharesCached; + uint256 newTotalAssetsRet = newTotalAssetsCached; + uint256 newLostAssetsRet = newLostAssetsCached; + return (feeSharesRet,newTotalAssetsRet,newLostAssetsRet); + } + else { + lastTotalAssetsCached = lastTotalAssets; + lostAssetsCached = lostAssets; + feeCached = fee; + totalSupplyCached = totalSupply; + firstMarketCached = firstMarket; + firstMarketExpectedSupplyAssetsCached = firstMarketExpectedSupplyAssets; + uint256 feeSharesRet; + uint256 newTotalAssetsRet; + uint256 newLostAssetsRet; + (feeSharesRet, newTotalAssetsRet, newLostAssetsRet) = accruedFeeAndAssetsNotSummarized(e); + feeSharesCached = feeSharesRet; + newTotalAssetsCached = newTotalAssetsRet; + newLostAssetsCached = newLostAssetsRet; + return (feeSharesRet, newTotalAssetsRet, newLostAssetsRet); + } + } +} + +// Verified +rule conversionOfZero { + initCacheToZero(); + uint256 convertZeroShares = convertToAssets(0); + uint256 convertZeroAssets = convertToShares(0); + + assert convertZeroShares == 0, + "converting zero shares must return zero assets"; + assert convertZeroAssets == 0, + "converting zero assets must return zero shares"; +} + +// Verified with caching summary (see above) or with CONSTANT summary +rule convertToAssetsWeakAdditivity() { + initCacheToZero(); + uint256 sharesA; uint256 sharesB; + uint256 assetsA = convertToAssets(sharesA); + uint256 assetsB = convertToAssets(sharesB); + uint256 sharesAplusB = require_uint256(sharesA + sharesB); + uint256 assetsAplusB = convertToAssets(sharesAplusB); + require sharesA + sharesB < max_uint128 + && assetsA + assetsB < max_uint256 + && assetsAplusB < max_uint256; + assert assetsA + assetsB <= assetsAplusB, + "converting sharesA and sharesB to assets then summing them must yield a smaller or equal result to summing them then converting"; +} + +// Verified with caching summary +rule convertToSharesWeakAdditivity() { + initCacheToZero(); + uint256 assetsA; uint256 assetsB; + uint256 sharesA = convertToShares(assetsA); + uint256 sharesB = convertToShares(assetsB); + uint256 assetsAplusB = require_uint256(assetsA+assetsB); + uint256 sharesAplusB = convertToShares(assetsAplusB); + require assetsA + assetsB < max_uint128 + && sharesA + sharesB < max_uint256 + && sharesAplusB < max_uint256; + assert sharesA + sharesB <= sharesAplusB, + "converting assetsA and assetsB to shares then summing them must yield a smaller or equal result to summing them then converting"; +} + +// Verified +rule conversionWeakMonotonicity { + initCacheToZero(); + uint256 smallerShares; uint256 largerShares; + uint256 smallerAssets; uint256 largerAssets; + + assert smallerShares < largerShares => convertToAssets(smallerShares) <= convertToAssets(largerShares), + "converting more shares must yield equal or greater assets"; + assert smallerAssets < largerAssets => convertToShares(smallerAssets) <= convertToShares(largerAssets), + "converting more assets must yield equal or greater shares"; +} + +// Verified +rule conversionWeakIntegrity() { + initCacheToZero(); + uint256 sharesOrAssets; + assert convertToShares(convertToAssets(sharesOrAssets)) <= sharesOrAssets, + "converting shares to assets then back to shares must return shares less than or equal to the original amount"; + assert convertToAssets(convertToShares(sharesOrAssets)) <= sharesOrAssets, + "converting assets to shares then back to assets must return assets less than or equal to the original amount"; +} diff --git a/certora/specs/ERC20/specs/ERC20Params.spec b/certora/specs/ERC20/specs/ERC20Params.spec new file mode 100644 index 0000000..316f299 --- /dev/null +++ b/certora/specs/ERC20/specs/ERC20Params.spec @@ -0,0 +1,8 @@ +/// Maximum total supply +definition MAX_SUPPLY() returns mathint = max_uint128; +/// Native token address +definition NATIVE() returns address = 0; +/// The default precision (18 decimals) +definition DEFAULT_PRECISION() returns uint256 = 10^18; +/// A second option for precision (27 decimals) +definition SECONDARY_PRECISION() returns uint256 = 10^27; \ No newline at end of file diff --git a/certora/specs/ERC20/specs/ERC20Rebasing.spec b/certora/specs/ERC20/specs/ERC20Rebasing.spec new file mode 100644 index 0000000..934fa26 --- /dev/null +++ b/certora/specs/ERC20/specs/ERC20Rebasing.spec @@ -0,0 +1,201 @@ +import "./ERC20Storage.spec"; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Summarizations +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +function totalSupplyCVL(address token, uint256 timestamp) returns uint256 +{ + require token != NATIVE(); + if(isRebasing(token)) { + uint256 index = indexByToken[token][timestamp]; + uint256 amount = supplyByToken[token]; + return rawTokensToBalance(token, amount, index); + } else { + return supplyByToken[token]; + } +} + +function transferCVL(address token, uint256 timestamp, address from, address to, uint256 amount) returns bool +{ + require sumOfPairLessEqualThanSupply(token, from, to); + if(isRebasing(token)) { + return transferCVLRebasing(token, timestamp, from, to, amount); + } else { + return transferCVLStandard(token, from, to, amount); + } +} + +function transferFromCVL(address token, uint256 timestamp, address spender, address from, address to, uint256 amount) returns bool +{ + require sumOfPairLessEqualThanSupply(token, from, to); + if(isRebasing(token)) { + return transferFromCVLRebasing(token, timestamp, spender, from, to, amount); + } else { + return transferFromCVLStandard(token, spender, from, to, amount); + } +} + +function balanceOfCVL(address token, uint256 timestamp, address account) returns uint256 { + /// The share balance of any user cannot surpass than the total supply. + require balanceByToken[token][account] <= supplyByToken[token]; + require token != NATIVE(); + if(isRebasing(token)) { + uint256 index = indexByToken[token][timestamp]; + uint256 amount = balanceByToken[token][account]; + return rawTokensToBalance(token, amount, index); + } else { + return balanceByToken[token][account]; + } +} + +function approveCVL(address token, address account, address spender, uint256 amount) returns bool { + allowanceByToken[token][account][spender] = amount; + return true; +} + +function allowanceCVL(address token, address account, address spender) returns uint256 { + require token != NATIVE(); + return allowanceByToken[token][account][spender]; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Definitions +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Returns | x - y | <= tol. +definition equalUpTo(mathint x, mathint y, mathint tol) returns bool = x > y ? x - y <= tol : y - x <= tol; + +/// Returns the approximate condition for preservation of balance after a single transfer operation. +/// diff - the change in balance +/// amount - the expected change (rounding-error-free) +/// index - the token index at time of the transfer +/// precision - the token precision. +/// Relative error bound +/// |diff - amount| <= 2*index / precision; +definition balanceTolerance(mathint diff, mathint amount, mathint index, mathint precision) returns bool = + equalUpTo(diff * precision, amount * precision, 2*index); /// @dev Can we do better? + + +/// The tolerance for balance change in transfer operation +function amountsAllowedError(address token, uint256 timestamp, mathint amount_pre, mathint amount_post, mathint delta) returns bool +{ + return isRebasing(token) ? + balanceTolerance(amount_post - amount_pre, delta, indexByToken[token][timestamp], tokenIndexPrecision(token)) + : amount_post - amount_pre == delta; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rebasing tokens ghosts +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Returns the rebasing token index per each timestamp. +ghost mapping(address /* token */ => mapping(uint256 /* timestamp */ => uint256)) indexByToken; + +/// Returns the precision of the index (10^decimals) [STATIC] +/// For instance: +/// WAD = 10^18 +/// RAY = 10^27 +persistent ghost tokenIndexPrecision(address /* token */) returns uint256 +{ + /// The precision is never zero! + axiom forall address token. tokenIndexPrecision(token) != 0; + /// One can choose here the possible options for the precision: + axiom forall address token. + tokenIndexPrecision(token) == DEFAULT_PRECISION() + || + tokenIndexPrecision(token) == SECONDARY_PRECISION(); +} + +/// Returns the raw tokens given the balance and index. We assume rawTokens() rounds up. +/// Mocks rawTokens(balance) = ceil(balance * precision / index) +persistent ghost balanceToRawTokens(address,uint256,uint256) returns uint256 +{ + axiom forall address token. forall uint256 balance. forall uint256 index. + balance * tokenIndexPrecision(token) <= balanceToRawTokens(token, balance, index) * index + && + balance * tokenIndexPrecision(token) - balanceToRawTokens(token, balance, index) * index + index > 0; + + axiom forall address token. forall uint256 balance1. forall uint256 balance2. forall uint256 index. + balance1 < balance2 => balanceToRawTokens(token, balance1, index) <= balanceToRawTokens(token, balance2, index); + + axiom forall address token. forall uint256 index1. forall uint256 index2. forall uint256 balance. + index1 < index2 => balanceToRawTokens(token, balance, index1) >= balanceToRawTokens(token, balance, index2); +} + +/// Returns the balanceOf() given the amount and index. We assume balanceOf() rounds down. +/// Mocks balanceOf(user) = floor(raw_balance[user] * index / precision) +persistent ghost rawTokensToBalance(address,uint256,uint256) returns uint256 +{ + axiom forall address token. forall uint256 amount. forall uint256 index. + rawTokensToBalance(token, amount, index) <= MAX_SUPPLY(); + + axiom forall address token. forall uint256 amount. forall uint256 index. + amount * index - rawTokensToBalance(token, amount, index) * tokenIndexPrecision(token) < tokenIndexPrecision(token) + && + amount * index >= rawTokensToBalance(token, amount, index) * tokenIndexPrecision(token); + + axiom forall address token. forall uint256 amount1. forall uint256 amount2. forall uint256 index. + amount1 < amount2 => rawTokensToBalance(token, amount1, index) <= rawTokensToBalance(token, amount2, index); + + axiom forall address token. forall uint256 index1. forall uint256 index2. forall uint256 amount. + index1 < index2 => rawTokensToBalance(token, amount, index1) <= rawTokensToBalance(token, amount, index2); + + /// Round-trip axiom + axiom forall address token. forall uint256 amount. forall uint256 index. + (balanceToRawTokens(token, rawTokensToBalance(token, amount, index), index) - amount) * index < index && + (balanceToRawTokens(token, rawTokensToBalance(token, amount, index), index) - amount) * index + tokenIndexPrecision(token) > 0; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function implementations +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +function transferFromCVLRebasing(address token, uint256 timestamp, address spender, address from, address to, uint256 amount) returns bool { + require allowanceByToken[token][from][spender] >= amount; + require spender != from => allowanceByToken[token][from][spender] >= amount; + + bool success = transferCVLRebasing(token, timestamp, from, to, amount); + if(success && from != spender) { + allowanceByToken[token][from][spender] = assert_uint256(allowanceByToken[token][from][spender] - amount); + } + return success; +} + +function transferCVLRebasing(address token, uint256 timestamp, address from, address to, uint256 amount) returns bool { + uint256 index = indexByToken[token][timestamp]; + + mathint balanceFrom = rawTokensToBalance(token, balanceByToken[token][from], index) - amount; + if(balanceFrom < 0) return false; + balanceByToken[token][from] = balanceToRawTokens(token, assert_uint256(balanceFrom), index); + mathint balanceTo = rawTokensToBalance(token, balanceByToken[token][to], index) + amount; + balanceByToken[token][to] = balanceToRawTokens(token, require_uint256(balanceTo), index); + + return true; +} + +function transferFromCVLStandard(address token, address spender, address from, address to, uint256 amount) returns bool { + require spender != from => allowanceByToken[token][from][spender] >= amount; + //if (allowanceByToken[token][from][spender] < amount) return false; + bool success = transferCVLStandard(token, from, to, amount); + if(success && spender != from) { + allowanceByToken[token][from][spender] = assert_uint256(allowanceByToken[token][from][spender] - amount); + } + return success; +} + +function transferCVLStandard(address token, address from, address to, uint256 amount) returns bool { + require balanceByToken[token][from] >= amount; + //if(balanceByToken[token][from] < amount) return false; + balanceByToken[token][from] = assert_uint256(balanceByToken[token][from] - amount); + balanceByToken[token][to] = require_uint256(balanceByToken[token][to] + amount); // We neglect overflows. + return true; +} \ No newline at end of file diff --git a/certora/specs/ERC20/specs/ERC20Revert.spec b/certora/specs/ERC20/specs/ERC20Revert.spec new file mode 100644 index 0000000..b0f3ed7 --- /dev/null +++ b/certora/specs/ERC20/specs/ERC20Revert.spec @@ -0,0 +1,104 @@ +import "./ERC20Storage.spec"; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Summarizations +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +function totalSupplyCVL(address token, uint256 timestamp) returns uint256 +{ + require token != NATIVE(); + return supplyByToken[token]; +} + +function transferCVL(address token, uint256 timestamp, address from, address to, uint256 amount) returns bool +{ + require sumOfPairLessEqualThanSupply(token, from, to); + return transferCVLStandard(token, from, to, amount); +} + +function transferFromCVL(address token, uint256 timestamp, address spender, address from, address to, uint256 amount) returns bool +{ + require sumOfPairLessEqualThanSupply(token, from, to); + return transferFromCVLStandard(token, spender, from, to, amount); +} + +function approveCVL(address token, address account, address spender, uint256 amount) returns bool { + if(!approveSuccess(token, account, spender)) { + revert("Invalid accounts"); + } + allowanceByToken[token][account][spender] = amount; + return true; +} + +function balanceOfCVL(address token, uint256 timestamp, address account) returns uint256 { + if(!_validToken(token)) { + revert("Invalid token"); + } + require balanceByToken[token][account] <= supplyByToken[token]; + return balanceByToken[token][account]; +} + +function allowanceCVL(address token, address account, address spender) returns uint256 { + require token != NATIVE(); + return allowanceByToken[token][account][spender]; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function implementations +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +function transferFromCVLStandard(address token, address spender, address from, address to, uint256 amount) returns bool { + if(!hasAllowance(token, spender, from, amount)) { + revert("Insufficient allowance"); + } + //require spender != from => allowanceByToken[token][from][spender] >= amount; + //if (allowanceByToken[token][from][spender] < amount) return false; + if(spender != from) { + allowanceByToken[token][from][spender] = assert_uint256(allowanceByToken[token][from][spender] - amount); + } + bool success = transferCVLStandard(token, from, to, amount); + + return success; +} + +function transferCVLStandard(address token, address from, address to, uint256 amount) returns bool { + if(!transferSuccess(token, from, to, amount)) { + revert("Invalid transfer"); + } + balanceByToken[token][from] = assert_uint256(balanceByToken[token][from] - amount); + balanceByToken[token][to] = assert_uint256(balanceByToken[token][to] + amount); // We neglect overflows. + return true; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function success conditions +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +function transferFromSuccess(address token, address spender, address from, address to, uint256 amount) returns bool { + return transferSuccess(token, from, to, amount) && hasAllowance(token, spender, from, amount); +} + +function hasAllowance(address token, address spender, address from, uint256 amount) returns bool { + return from != spender => allowanceByToken[token][from][spender] >= amount; +} + +function transferSuccess(address token, address from, address to, uint256 amount) returns bool { + return balanceByToken[token][from] >= amount && + balanceByToken[token][to] + amount <= max_uint256 && + from !=0 && to != 0 && + _validToken(token); +} + +function approveSuccess(address token, address owner, address spender) returns bool { + return owner != 0 && spender != 0 && _validToken(token); +} + +function _validToken(address token) returns bool { + return token != NATIVE(); +} \ No newline at end of file diff --git a/certora/specs/ERC20/specs/ERC20Standard.spec b/certora/specs/ERC20/specs/ERC20Standard.spec new file mode 100644 index 0000000..7d77d33 --- /dev/null +++ b/certora/specs/ERC20/specs/ERC20Standard.spec @@ -0,0 +1,66 @@ +import "./ERC20Storage.spec"; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Summarizations +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +function totalSupplyCVL(address token, uint256 timestamp) returns uint256 +{ + require token != NATIVE(); + return supplyByToken[token]; +} + +function transferCVL(address token, uint256 timestamp, address from, address to, uint256 amount) returns bool +{ + require sumOfPairLessEqualThanSupply(token, from, to); + return transferCVLStandard(token, from, to, amount); +} + +function transferFromCVL(address token, uint256 timestamp, address spender, address from, address to, uint256 amount) returns bool +{ + require sumOfPairLessEqualThanSupply(token, from, to); + return transferFromCVLStandard(token, spender, from, to, amount); +} + +function balanceOfCVL(address token, uint256 timestamp, address account) returns uint256 { + /// The balance of any user cannot surpass than the total supply. + require balanceByToken[token][account] <= supplyByToken[token]; + require token != NATIVE(); + return balanceByToken[token][account]; +} + +function approveCVL(address token, address account, address spender, uint256 amount) returns bool { + allowanceByToken[token][account][spender] = amount; + return true; +} + +function allowanceCVL(address token, address account, address spender) returns uint256 { + require token != NATIVE(); + return allowanceByToken[token][account][spender]; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function implementations +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +function transferFromCVLStandard(address token, address spender, address from, address to, uint256 amount) returns bool { + require spender != from => allowanceByToken[token][from][spender] >= amount; + //if (allowanceByToken[token][from][spender] < amount) return false; + bool success = transferCVLStandard(token, from, to, amount); + if(success && spender != from) { + allowanceByToken[token][from][spender] = assert_uint256(allowanceByToken[token][from][spender] - amount); + } + return success; +} + +function transferCVLStandard(address token, address from, address to, uint256 amount) returns bool { + require balanceByToken[token][from] >= amount; + //if(balanceByToken[token][from] < amount) return false; + balanceByToken[token][from] = assert_uint256(balanceByToken[token][from] - amount); + balanceByToken[token][to] = require_uint256(balanceByToken[token][to] + amount); // We neglect overflows. + return true; +} \ No newline at end of file diff --git a/certora/specs/ERC20/specs/ERC20Storage.spec b/certora/specs/ERC20/specs/ERC20Storage.spec new file mode 100644 index 0000000..27be600 --- /dev/null +++ b/certora/specs/ERC20/specs/ERC20Storage.spec @@ -0,0 +1,20 @@ +import "./ERC20Params.spec"; + +/// Bare storage of ERC20 tokens +ghost mapping(address /* token */ => uint256) supplyByToken { + axiom forall address token. supplyByToken[token] <= MAX_SUPPLY(); +} +ghost mapping(address /* token */ => mapping(address /* account */ => uint256)) balanceByToken; +ghost mapping(address /* token */ => mapping(address /* account */ => mapping(address /* spender */ => uint256))) allowanceByToken; + +/// Returns the decimals of a token [STATIC] +persistent ghost decimalsCVL(address /* token */) returns uint8; //modified to match + +/// Returns whether a token is rebasing or not. [STATIC] +persistent ghost isRebasing(address /* token */) returns bool; + +function sumOfPairLessEqualThanSupply(address token, address user1, address user2) returns bool { + return balanceByToken[token][user1] <= supplyByToken[token] && + (user1 != user2 => + balanceByToken[token][user1] + balanceByToken[token][user2] <= supplyByToken[token]); +} \ No newline at end of file diff --git a/certora/specs/ERC20/specs/summary_rebasing.spec b/certora/specs/ERC20/specs/summary_rebasing.spec new file mode 100644 index 0000000..971aee9 --- /dev/null +++ b/certora/specs/ERC20/specs/summary_rebasing.spec @@ -0,0 +1,24 @@ +import "./ERC20Rebasing.spec"; + +methods { + function _.transfer(address to, uint256 amount) external with (env e) + => transferCVL(calledContract, e.block.timestamp, e.msg.sender, to, amount) expect bool; + + function _.transferFrom(address from, address to, uint256 amount) external with (env e) + => transferFromCVL(calledContract, e.block.timestamp, e.msg.sender, from, to, amount) expect bool; + + function _.balanceOf(address account) external with (env e) => + balanceOfCVL(calledContract, e.block.timestamp, account) expect uint256; + + function _.allowance(address account, address spender) external => + allowanceCVL(calledContract, account, spender) expect uint256; + + function _.decimals() external => + decimalsCVL(calledContract) expect uint256; + + function _.totalSupply() external with (env e) => + totalSupplyCVL(calledContract, e.block.timestamp) expect uint256; + + function _.approve(address spender, uint amount) external with (env e) => + approveCVL(calledContract, e.msg.sender, spender, amount) expect bool; +} \ No newline at end of file diff --git a/certora/specs/ERC20/specs/summary_standard.spec b/certora/specs/ERC20/specs/summary_standard.spec new file mode 100644 index 0000000..15d2684 --- /dev/null +++ b/certora/specs/ERC20/specs/summary_standard.spec @@ -0,0 +1,24 @@ +import "./ERC20Standard.spec"; + +methods { + function _.transfer(address to, uint256 amount) external with (env e) + => transferCVL(calledContract, e.block.timestamp, e.msg.sender, to, amount) expect bool; + + function _.transferFrom(address from, address to, uint256 amount) external with (env e) + => transferFromCVL(calledContract, e.block.timestamp, e.msg.sender, from, to, amount) expect bool; + + function _.balanceOf(address account) external with (env e) => + balanceOfCVL(calledContract, e.block.timestamp, account) expect uint256; + + function _.allowance(address account, address spender) external => + allowanceCVL(calledContract, account, spender) expect uint256; + + function _.decimals() external => + decimalsCVL(calledContract) expect uint256; + + function _.totalSupply() external with (env e) => + totalSupplyCVL(calledContract, e.block.timestamp) expect uint256; + + function _.approve(address spender, uint amount) external with (env e) => + approveCVL(calledContract, e.msg.sender, spender, amount) expect bool; +} \ No newline at end of file diff --git a/certora/specs/ERC20/specs/summary_standard_reverting.spec b/certora/specs/ERC20/specs/summary_standard_reverting.spec new file mode 100644 index 0000000..4830453 --- /dev/null +++ b/certora/specs/ERC20/specs/summary_standard_reverting.spec @@ -0,0 +1,24 @@ +import "./ERC20Revert.spec"; + +methods { + function _.transfer(address to, uint256 amount) external with (env e) + => transferCVL(calledContract, e.block.timestamp, e.msg.sender, to, amount) expect bool; + + function _.transferFrom(address from, address to, uint256 amount) external with (env e) + => transferFromCVL(calledContract, e.block.timestamp, e.msg.sender, from, to, amount) expect bool; + + function _.balanceOf(address account) external with (env e) => + balanceOfCVL(calledContract, e.block.timestamp, account) expect uint256; + + function _.allowance(address account, address spender) external => + allowanceCVL(calledContract, account, spender) expect uint256; + + function _.decimals() external => + decimalsCVL(calledContract) expect uint256; + + function _.totalSupply() external with (env e) => + totalSupplyCVL(calledContract, e.block.timestamp) expect uint256; + + function _.approve(address spender, uint amount) external with (env e) => + approveCVL(calledContract, e.msg.sender, spender, amount) expect bool; +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/IERC20.sol b/certora/specs/ERC20/verification/IERC20.sol new file mode 100644 index 0000000..090cc22 --- /dev/null +++ b/certora/specs/ERC20/verification/IERC20.sol @@ -0,0 +1,79 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v5.0.0) (token/ERC20/IERC20.sol) + +pragma solidity ^0.8.0; + +/** + * @dev Interface of the ERC20 standard as defined in the EIP. + */ +interface IERC20 { + /** + * @dev Emitted when `value` tokens are moved from one account (`from`) to + * another (`to`). + * + * Note that `value` may be zero. + */ + event Transfer(address indexed from, address indexed to, uint256 value); + + /** + * @dev Emitted when the allowance of a `spender` for an `owner` is set by + * a call to {approve}. `value` is the new allowance. + */ + event Approval(address indexed owner, address indexed spender, uint256 value); + + /** + * @dev Returns the value of tokens in existence. + */ + function totalSupply() external view returns (uint256); + + /** + * @dev Returns the value of tokens owned by `account`. + */ + function balanceOf(address account) external view returns (uint256); + + /** + * @dev Moves a `value` amount of tokens from the caller's account to `to`. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transfer(address to, uint256 value) external returns (bool); + + /** + * @dev Returns the remaining number of tokens that `spender` will be + * allowed to spend on behalf of `owner` through {transferFrom}. This is + * zero by default. + * + * This value changes when {approve} or {transferFrom} are called. + */ + function allowance(address owner, address spender) external view returns (uint256); + + /** + * @dev Sets a `value` amount of tokens as the allowance of `spender` over the + * caller's tokens. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * IMPORTANT: Beware that changing an allowance with this method brings the risk + * that someone may use both the old and the new allowance by unfortunate + * transaction ordering. One possible solution to mitigate this race + * condition is to first reduce the spender's allowance to 0 and set the + * desired value afterwards: + * https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729 + * + * Emits an {Approval} event. + */ + function approve(address spender, uint256 value) external returns (bool); + + /** + * @dev Moves a `value` amount of tokens from `from` to `to` using the + * allowance mechanism. `value` is then deducted from the caller's + * allowance. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transferFrom(address from, address to, uint256 value) external returns (bool); +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/RevertConditions.spec b/certora/specs/ERC20/verification/RevertConditions.spec new file mode 100644 index 0000000..8091994 --- /dev/null +++ b/certora/specs/ERC20/verification/RevertConditions.spec @@ -0,0 +1,22 @@ +import "../specs/summary_standard_reverting.spec"; + +using Test as Test; + +rule reverting_ERC20_summary(address token) { + env e; + address account = e.msg.sender; + require e.msg.value == 0; + + uint256 balance_pre = Test.balanceByToken(e, token, Test); + address recipient; require recipient != Test; + uint256 amount; + bool success = transferSuccess(token, Test, recipient, amount); + Test.transferByToken@withrevert(e, token, recipient, amount); + bool transfer_reverted = lastReverted; + uint256 balance_post = Test.balanceByToken(e, token, Test); + + assert !transfer_reverted => balance_post == balance_pre - amount; + assert !transfer_reverted => success; + assert transfer_reverted => balance_post == balance_pre; + satisfy transfer_reverted; +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/RulesRebasing.spec b/certora/specs/ERC20/verification/RulesRebasing.spec new file mode 100644 index 0000000..9bcfdb8 --- /dev/null +++ b/certora/specs/ERC20/verification/RulesRebasing.spec @@ -0,0 +1,105 @@ +import "../specs/ERC20Rebasing.spec"; + +rule transferIntegrity(address token, address from, address to) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_pre = balanceOfCVL(token, timestamp, to); + bool success = transferCVL(token, timestamp, from, to, amount); + require success; + uint256 balance_sender_post = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_post = balanceOfCVL(token, timestamp, to); + + if(from != to) { + assert amountsAllowedError(token, timestamp, balance_sender_pre, balance_sender_post, -amount); + assert amountsAllowedError(token, timestamp, balance_receiver_pre, balance_receiver_post, amount); + } else { + assert amountsAllowedError(token, timestamp, balance_receiver_pre, balance_receiver_post, 0); + } +} + +rule transferThirdParty(address token, address from, address to, address other) { + uint256 timestamp; + uint256 amount; + + uint256 balance_other_pre = balanceOfCVL(token, timestamp, other); + bool success = transferCVL(token, timestamp, from, to, amount); + require success; + uint256 balance_other_post = balanceOfCVL(token, timestamp, other); + + assert other != from && other != to => balance_other_pre == balance_other_post; +} + +rule transferPreservesTotalSupply(address token, address from, address to) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_pre = balanceOfCVL(token, timestamp, to); + uint256 supply_pre = totalSupplyCVL(token, timestamp); + bool success = transferCVL(token, timestamp, from, to, amount); + require success; + uint256 balance_sender_post = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_post = balanceOfCVL(token, timestamp, to); + uint256 supply_post = totalSupplyCVL(token, timestamp); + + assert amountsAllowedError(token, timestamp, balance_sender_pre + balance_receiver_pre, balance_sender_post + balance_receiver_post, 0); + assert supply_pre == supply_post; +} + +rule transferFromIntegrity(address token, address from, address to, address spender) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_pre = balanceOfCVL(token, timestamp, to); + uint256 allowance_spender_pre = allowanceCVL(token, from, spender); + bool success = transferFromCVL(token, timestamp, spender, from, to, amount); + require success; + uint256 balance_sender_post = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_post = balanceOfCVL(token, timestamp, to); + uint256 allowance_spender_post = allowanceCVL(token, from, spender); + + if(from != to) { + assert amountsAllowedError(token, timestamp, balance_sender_pre, balance_sender_post, -amount); + assert amountsAllowedError(token, timestamp, balance_receiver_pre, balance_receiver_post, amount); + } else { + assert amountsAllowedError(token, timestamp, balance_receiver_pre, balance_receiver_post, 0); + } + + if(spender == from) { + assert allowance_spender_pre == allowance_spender_post; + } else { + assert allowance_spender_post == allowance_spender_pre - amount; + } +} + +rule transferFromThirdParty(address token, address from, address to, address spender, address other) { + uint256 timestamp; + uint256 amount; + + uint256 balance_other_pre = balanceOfCVL(token, timestamp, other); + bool success = transferFromCVL(token, timestamp, spender, from, to, amount); + require success; + uint256 balance_other_post = balanceOfCVL(token, timestamp, other); + + assert other != from && other != to => balance_other_pre == balance_other_post; +} + +rule transferFromPreservesTotalSupply(address token, address from, address to, address spender) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_pre = balanceOfCVL(token, timestamp, to); + uint256 supply_pre = totalSupplyCVL(token, timestamp); + bool success = transferFromCVL(token, timestamp, spender, from, to, amount); + require success; + uint256 balance_sender_post = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_post = balanceOfCVL(token, timestamp, to); + uint256 supply_post = totalSupplyCVL(token, timestamp); + + assert amountsAllowedError(token, timestamp, balance_sender_pre + balance_receiver_pre, balance_sender_post + balance_receiver_post, 0); + assert supply_pre == supply_post; +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/RulesReverting.spec b/certora/specs/ERC20/verification/RulesReverting.spec new file mode 100644 index 0000000..3494f0e --- /dev/null +++ b/certora/specs/ERC20/verification/RulesReverting.spec @@ -0,0 +1,29 @@ +import "../specs/ERC20Revert.spec"; + +/// @TODO Add more revert conditions. +rule transferRevertsForInsufficientBalance(address token, address from, address to) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + require amount > balance_sender_pre; + bool success = transferCVL@withrevert(token, timestamp, from, to, amount); + bool reverted = lastReverted; + + assert reverted; + satisfy reverted; +} + +/// @TODO Add more revert conditions. +rule transferFromRevertsForInsufficientBalance(address token, address from, address to, address spender) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + require amount > balance_sender_pre; + bool success = transferFromCVL@withrevert(token, timestamp, spender, from, to, amount); + bool reverted = lastReverted; + + assert reverted; + satisfy reverted; +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/RulesStandard.spec b/certora/specs/ERC20/verification/RulesStandard.spec new file mode 100644 index 0000000..0462540 --- /dev/null +++ b/certora/specs/ERC20/verification/RulesStandard.spec @@ -0,0 +1,109 @@ +import "../specs/ERC20Standard.spec"; + +rule transferIntegrity(address token, address from, address to) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_pre = balanceOfCVL(token, timestamp, to); + bool success = transferCVL(token, timestamp, from, to, amount); + require success; + uint256 balance_sender_post = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_post = balanceOfCVL(token, timestamp, to); + + if(from != to) { + assert balance_sender_pre - balance_sender_post == amount; + assert balance_receiver_post - balance_receiver_pre == amount; + } else { + assert balance_receiver_post == balance_receiver_pre; + } +} + +rule transferThirdParty(address token, address from, address to, address other) { + uint256 timestamp; + uint256 amount; + + uint256 balance_other_pre = balanceOfCVL(token, timestamp, other); + bool success = transferCVL(token, timestamp, from, to, amount); + require success; + uint256 balance_other_post = balanceOfCVL(token, timestamp, other); + + assert other != from && other != to => balance_other_pre == balance_other_post; +} + +rule transferPreservesTotalSupply(address token, address from, address to) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_pre = balanceOfCVL(token, timestamp, to); + uint256 supply_pre = totalSupplyCVL(token, timestamp); + bool success = transferCVL(token, timestamp, from, to, amount); + require success; + uint256 balance_sender_post = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_post = balanceOfCVL(token, timestamp, to); + uint256 supply_post = totalSupplyCVL(token, timestamp); + + assert from == to + ? balance_sender_post <= supply_post + : balance_sender_post + balance_receiver_post <= supply_post; + assert supply_pre == supply_post; +} + +rule transferFromIntegrity(address token, address from, address to, address spender) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_pre = balanceOfCVL(token, timestamp, to); + uint256 allowance_spender_pre = allowanceCVL(token, from, spender); + bool success = transferFromCVL(token, timestamp, spender, from, to, amount); + require success; + uint256 balance_sender_post = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_post = balanceOfCVL(token, timestamp, to); + uint256 allowance_spender_post = allowanceCVL(token, from, spender); + + if(from != to) { + assert balance_sender_pre - balance_sender_post == amount; + assert balance_receiver_post - balance_receiver_pre == amount; + } else { + assert balance_receiver_post == balance_receiver_pre; + } + + if(spender == from) { + assert allowance_spender_pre == allowance_spender_post; + } else { + assert allowance_spender_post == allowance_spender_pre - amount; + } +} + +rule transferFromThirdParty(address token, address from, address to, address spender, address other) { + uint256 timestamp; + uint256 amount; + + uint256 balance_other_pre = balanceOfCVL(token, timestamp, other); + bool success = transferFromCVL(token, timestamp, spender, from, to, amount); + require success; + uint256 balance_other_post = balanceOfCVL(token, timestamp, other); + + assert other != from && other != to => balance_other_pre == balance_other_post; +} + +rule transferFromPreservesTotalSupply(address token, address from, address to, address spender) { + uint256 timestamp; + uint256 amount; + + uint256 balance_sender_pre = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_pre = balanceOfCVL(token, timestamp, to); + uint256 supply_pre = totalSupplyCVL(token, timestamp); + bool success = transferFromCVL(token, timestamp, spender, from, to, amount); + require success; + uint256 balance_sender_post = balanceOfCVL(token, timestamp, from); + uint256 balance_receiver_post = balanceOfCVL(token, timestamp, to); + uint256 supply_post = totalSupplyCVL(token, timestamp); + + assert from == to + ? balance_sender_post <= supply_post + : balance_sender_post + balance_receiver_post <= supply_post; + assert supply_pre == supply_post; +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/Test.sol b/certora/specs/ERC20/verification/Test.sol new file mode 100644 index 0000000..dddcba9 --- /dev/null +++ b/certora/specs/ERC20/verification/Test.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v5.0.0) (token/ERC20/IERC20.sol) + +pragma solidity ^0.8.0; + +import { IERC20 } from "./IERC20.sol"; + +library Math { + enum Rounding { + Floor, // Toward negative infinity + Ceil, // Toward positive infinity + Trunc, // Toward zero + Expand // Away from zero + } +} + +contract Test { + + function supplyByToken(address token) external view returns (uint256) { + return IERC20(token).totalSupply(); + } + + function balanceByToken(address token, address account) external view returns (uint256) { + return IERC20(token).balanceOf(account); + } + + function transferByToken(address token, address recipient, uint256 amount) external returns (bool) { + return IERC20(token).transfer(recipient, amount); + } + + function transferFromByToken(address token, address from, address recipient, uint256 amount) external returns (bool) { + return IERC20(token).transferFrom(from, recipient, amount); + } + + function approveByToken(address token, address spender, uint256 value) external returns (bool) { + return IERC20(token).approve(spender, value); + } +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/test_revert_summary.conf b/certora/specs/ERC20/verification/test_revert_summary.conf new file mode 100644 index 0000000..eb92b05 --- /dev/null +++ b/certora/specs/ERC20/verification/test_revert_summary.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "ERC20/verification/Test.sol", + ], + "verify": "Test:ERC20/verification/RevertConditions.spec", + "prover_args":[ + "-cvlFunctionRevert true", + ], + "process": "emv", + "smt_timeout": "1800", + "server": "prover", + "solc": "solc8.20", + "msg":"CVL Standard Reverting ERC20 test" +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/verify_rebasing.conf b/certora/specs/ERC20/verification/verify_rebasing.conf new file mode 100644 index 0000000..2dd343d --- /dev/null +++ b/certora/specs/ERC20/verification/verify_rebasing.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "ERC20/verification/Test.sol", + ], + "verify": "Test:ERC20/verification/RulesRebasing.spec", + "process": "emv", + "smt_timeout": "1800", + "server": "prover", + "solc": "solc8.20", + "msg":"CVL Rebasing ERC20 test" +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/verify_revert.conf b/certora/specs/ERC20/verification/verify_revert.conf new file mode 100644 index 0000000..0c1d2ec --- /dev/null +++ b/certora/specs/ERC20/verification/verify_revert.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "ERC20/verification/Test.sol", + ], + "verify": "Test:ERC20/verification/RulesReverting.spec", + "prover_args":[ + "-cvlFunctionRevert true", + ], + "process": "emv", + "smt_timeout": "1800", + "server": "prover", + "solc": "solc8.20", + "msg":"CVL Standard Reverting ERC20 test" +} \ No newline at end of file diff --git a/certora/specs/ERC20/verification/verify_standard.conf b/certora/specs/ERC20/verification/verify_standard.conf new file mode 100644 index 0000000..fde52a9 --- /dev/null +++ b/certora/specs/ERC20/verification/verify_standard.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "ERC20/verification/Test.sol", + ], + "verify": "Test:ERC20/verification/RulesStandard.spec", + "process": "emv", + "smt_timeout": "1800", + "server": "prover", + "solc": "solc8.20", + "msg":"CVL Standard ERC20 test" +} \ No newline at end of file diff --git a/certora/specs/ERC4626/specs/ERC4626.spec b/certora/specs/ERC4626/specs/ERC4626.spec new file mode 100644 index 0000000..f818d57 --- /dev/null +++ b/certora/specs/ERC4626/specs/ERC4626.spec @@ -0,0 +1,193 @@ +import "ERC4626Storage.spec"; +import "../../ERC20/specs/ERC20Storage.spec"; +import "../../ERC20/specs/ERC20Standard.spec"; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Shares <-> Assets Conversion Formulas +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Mathmatical ghost function for pro-rata converter of the form: +/// result = mulDiv(assets, total shares + offset, total assets + offset). +persistent ghost proRataConverter( + mathint /*assets*/, + mathint /*total shares + offset*/, + mathint /*total assets + offset*/ +) returns uint256 +{ + /// Rounding error bounds + axiom forall mathint assets. forall mathint totalShares. forall mathint totalAssets. + proRataConverter(assets,totalShares,totalAssets) * totalAssets + <= assets * totalShares + && + (proRataConverter(assets,totalShares,totalAssets) + 1) * totalAssets + > assets * totalShares; + + /// Monotonoticity + axiom forall mathint assets1. forall mathint assets2. forall mathint totalShares. forall mathint totalAssets. + assets1 < assets2 => proRataConverter(assets1,totalShares,totalAssets) <= proRataConverter(assets2,totalShares,totalAssets); + + axiom forall mathint assets. forall mathint totalShares1. forall mathint totalShares2. forall mathint totalAssets. + totalShares1 < totalShares2 => proRataConverter(assets,totalShares1,totalAssets) <= proRataConverter(assets,totalShares2,totalAssets); + + axiom forall mathint assets. forall mathint totalAssets1. forall mathint totalAssets2. forall mathint totalShares. + totalAssets1 < totalAssets2 => proRataConverter(assets,totalShares,totalAssets2) <= proRataConverter(assets,totalShares,totalAssets1); +} + +function convertToAssetsCVL(address token, uint256 shares, Math.Rounding rounding) returns uint256 +{ + uint256 assets = proRataConverter( + shares, + ERC4626TotalAssets[token] + ASSETS_OFFSET(), + supplyByToken[token] + SHARES_OFFSET() + ); + bool noRemainder = assets * (supplyByToken[token] + SHARES_OFFSET()) == shares * (ERC4626TotalAssets[token] + ASSETS_OFFSET()); + if(rounding == Math.Rounding.Floor) { + return assets; + } else if(rounding == Math.Rounding.Ceil) { + return noRemainder ? assets : require_uint256(assets+1); + } else { + assert false; + } + return 0; +} + +function convertToSharesCVL(address token, uint256 assets, Math.Rounding rounding) returns uint256 +{ + uint256 shares = proRataConverter( + assets, + supplyByToken[token] + SHARES_OFFSET(), + ERC4626TotalAssets[token] + ASSETS_OFFSET() + ); + bool noRemainder = assets * (supplyByToken[token] + SHARES_OFFSET()) == shares * (ERC4626TotalAssets[token] + ASSETS_OFFSET()); + if(rounding == Math.Rounding.Floor) { + return shares; + } else if(rounding == Math.Rounding.Ceil) { + return noRemainder ? shares : require_uint256(shares+1); + } else { + assert false; + } + return 0; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function implementations +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +function depositCVL(address token, uint256 timestamp, address sender, uint256 assets, address receiver) returns uint256 +{ + /// Assumption: the share token is non-rebasing. + require !isRebasing(token); + /// The share balance of any user cannot surpass the total supply. + require sumOfPairLessEqualThanSupply(token, sender, receiver); + /// Calculate amount of minted shares + uint256 shares = previewDepositCVL(token, assets); + + if(!depositSuccess(token, sender, receiver, assets, shares)) { + revert("Deposit is invalid"); + } + + address underlying = ERC4626Asset(token); + /// Deposit tokens from sender to vault. + /// @dev notice: + /* + The following call only invokes the standard CVL implementation of the IERC20 interface. + Any ERC20 contracts present in the scene will not be invoked here, thus missed behavior could be + possible, where the underlying token is a contract in the scene. + Consider adding a switch-case block to allow for special tokens + e.g. if(underlying == Contract) Contract.transferFrom(e, ...) + */ + bool success = transferFromCVL(underlying, timestamp, token, sender, token, assets); + require success; + + /// Mint shares and increase assets + supplyByToken[token] = assert_uint256(supplyByToken[token] + shares); + ERC4626TotalAssets[token] = assert_uint256(ERC4626TotalAssets[token] + assets); + balanceByToken[token][receiver] = assert_uint256(balanceByToken[token][receiver] + shares); + + return shares; +} + +function withdrawCVL(address token, uint256 timestamp, address sender, uint256 assets, address receiver, address owner) returns uint256 +{ + /// Assumption: the share token is non-rebasing. + require !isRebasing(token); + /// The share balance of any user cannot surpass the total supply. + require sumOfPairLessEqualThanSupply(token, owner, receiver); + uint256 shares = previewWithdrawCVL(token, assets); + + if(!withdrawSuccess(token, sender, owner, receiver, assets, shares)) { + revert("Withdraw is invalid"); + } + + /// Spend allowance + if(owner != sender) { + allowanceByToken[token][owner][sender] = assert_uint256(allowanceByToken[token][owner][sender] - shares); + } + /// Burn and decrease assets + supplyByToken[token] = assert_uint256(supplyByToken[token] - shares); + ERC4626TotalAssets[token] = assert_uint256(ERC4626TotalAssets[token] - assets); + balanceByToken[token][owner] = assert_uint256(balanceByToken[token][owner] - shares); + + address underlying = ERC4626Asset(token); + /// Send tokens to recipient. + /// @dev notice: + /* + The following call only invokes the standard CVL implementation of the IERC20 interface. + Any ERC20 contracts present in the scene will not be invoked here, thus missed behavior could be + possible, where the underlying token is a contract in the scene. + Consider adding a switch-case block to allow for special tokens + e.g. if(underlying == Contract) Contract.transfer(e, ...) + */ + bool success = transferCVL(underlying, timestamp, token, receiver, assets); + require success; + + return shares; +} + +function maxWithdrawCVL(address token, address account) returns uint256 { + return convertToAssetsCVL(token, balanceByToken[token][account], Math.Rounding.Floor); +} + +function previewRedeemCVL(address token, uint256 shares) returns uint256 { + return convertToAssetsCVL(token, shares, Math.Rounding.Floor); +} + +function previewDepositCVL(address token, uint256 assets) returns uint256 { + return convertToSharesCVL(token, assets, Math.Rounding.Floor); +} + +function previewMintCVL(address token, uint256 shares) returns uint256 { + return convertToAssetsCVL(token, shares, Math.Rounding.Ceil); +} + +function previewWithdrawCVL(address token, uint256 assets) returns uint256 { + return convertToSharesCVL(token, assets, Math.Rounding.Ceil); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function success conditions +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +function depositSuccess(address token, address sender, address receiver, uint256 assets, uint256 shares) returns bool { + return assets <= maxDepositCVL(token, receiver) && + ERC4626TotalAssets[token] + assets <= max_uint256 && + supplyByToken[token] + shares <= max_uint256; +} + +function withdrawSuccess(address token, address spender, address owner, address receiver, uint256 assets, uint256 shares) returns bool { + return hasAllowanceERC20(token, spender, owner, shares) && + assets <= maxWithdrawCVL(token, receiver) && + supplyByToken[token] >= shares && + ERC4626TotalAssets[token] >= assets && + balanceByToken[token][owner] >= shares; +} + +function hasAllowanceERC20(address token, address spender, address from, uint256 amount) returns bool { + return from != spender => allowanceByToken[token][from][spender] >= amount; +} \ No newline at end of file diff --git a/certora/specs/ERC4626/specs/ERC4626Params.spec b/certora/specs/ERC4626/specs/ERC4626Params.spec new file mode 100644 index 0000000..9696ed9 --- /dev/null +++ b/certora/specs/ERC4626/specs/ERC4626Params.spec @@ -0,0 +1,7 @@ +/// Maximum total assets per underlying token +definition MAX_ASSETS() returns uint256 = max_uint160; + +/// Offsets for the shares <-> assets conversion. Based on OZ ERC4626 implementation. +/// Currently global constants, with possibility to extend those to contract-specific values. +definition SHARES_OFFSET() returns uint256 = 1; +definition ASSETS_OFFSET() returns uint256 = 1; \ No newline at end of file diff --git a/certora/specs/ERC4626/specs/ERC4626Storage.spec b/certora/specs/ERC4626/specs/ERC4626Storage.spec new file mode 100644 index 0000000..56ea1ca --- /dev/null +++ b/certora/specs/ERC4626/specs/ERC4626Storage.spec @@ -0,0 +1,14 @@ +import "ERC4626Params.spec"; + +/// The total amount of assets deposited in the vault ( = totalAssets()) +ghost mapping(address /*ERC4626 token*/ => uint256) ERC4626TotalAssets { + axiom forall address token. ERC4626TotalAssets[token] <= MAX_ASSETS(); +} + +/// Returns the underlying asset of each ERC4626 token contract [STATIC]. +persistent ghost ERC4626Asset(address /*ERC4626 token*/) returns address { + axiom forall address token. (ERC4626Asset(token) != token || token == 0); +} + +/// Returns the max deposit amount per each ERC4626 token contract for any account. +persistent ghost maxDepositCVL(address /*ERC4626 token*/, address /*account*/) returns uint256; \ No newline at end of file diff --git a/certora/specs/ERC4626/specs/summary.spec b/certora/specs/ERC4626/specs/summary.spec new file mode 100644 index 0000000..514f492 --- /dev/null +++ b/certora/specs/ERC4626/specs/summary.spec @@ -0,0 +1,33 @@ +import "./ERC4626.spec"; + +methods { + function _.convertToAssets(uint256 shares, Math.Rounding rounding) internal => + convertToAssetsCVL(calledContract, shares, rounding) expect uint256; + + function _.convertToShares(uint256 assets, Math.Rounding rounding) internal => + convertToSharesCVL(calledContract, assets, rounding) expect uint256; + + function _.previewRedeem(uint256 shares) external => + previewRedeemCVL(calledContract, shares) expect uint256; + + function _.previewMint(uint256 shares) external => + previewMintCVL(calledContract, shares) expect uint256; + + function _.previewWithdraw(uint256 assets) external => + previewWithdrawCVL(calledContract, assets) expect uint256; + + function _.asset() external => + ERC4626Asset(calledContract) expect address; + + function _.maxDeposit(address account) external => + maxDepositCVL(calledContract, account) expect uint256; + + function _.maxWithdraw(address account) external => + maxWithdrawCVL(calledContract, account) expect uint256; + + function _.deposit(uint256 assets, address receiver) external with (env e) => + depositCVL(calledContract, e.block.timestamp, e.msg.sender, assets, receiver) expect uint256; + + function _.withdraw(uint256 assets, address receiver, address owner) external with (env e) => + withdrawCVL(calledContract, e.block.timestamp, e.msg.sender, assets, receiver, owner) expect uint256; +} \ No newline at end of file diff --git a/certora/specs/ERC4626/verification/Rules.spec b/certora/specs/ERC4626/verification/Rules.spec new file mode 100644 index 0000000..2f6fed4 --- /dev/null +++ b/certora/specs/ERC4626/verification/Rules.spec @@ -0,0 +1,56 @@ +import "../specs/ERC4626.spec"; +import "../../ERC20/specs/summary_standard.spec"; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ deposit() rules +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule depositTokenTransferIntegrity(address token, uint256 assets) { + uint256 timestamp; + address sender; + address receiver; + address underlying = ERC4626Asset(token); + + uint256 balanceShare_receiver_pre = balanceOfCVL(token, timestamp, receiver); + uint256 balanceToken_vault_pre = balanceOfCVL(underlying, timestamp, token); + uint256 shares = depositCVL(token, timestamp, sender, assets, receiver); + uint256 balanceShare_receiver_post = balanceOfCVL(token, timestamp, receiver); + uint256 balanceToken_vault_post = balanceOfCVL(underlying, timestamp, token); + + assert balanceShare_receiver_post - balanceShare_receiver_pre == shares; + assert sender != token => balanceToken_vault_post - balanceToken_vault_pre == assets; + satisfy balanceShare_receiver_post != balanceShare_receiver_pre; +} + +rule depositSharesMatchPreviewDeposit(address token, uint256 assets) { + uint256 timestamp; + address sender; + address receiver; + + uint256 shares_preview = previewDepositCVL(token, assets); + uint256 shares_real = depositCVL(token, _, _, assets, _); + + assert shares_preview == shares_real; + satisfy shares_preview > 0; +} + +rule depositIsSubAdditive(address token, uint256 assets1, uint256 assets2) { + uint256 shares1 = previewDepositCVL(token, assets1); + uint256 shares2 = previewDepositCVL(token, assets2); + uint256 shares_sum = previewDepositCVL(token, require_uint256(assets1+assets2)); + + assert shares1 + shares2 <= shares_sum; + satisfy shares_sum > 0; +} + +rule depositWithdrawRoundTripNoProfit(address token, uint256 assets) { + address depositor; + uint256 timestamp; + uint256 sharesIn = depositCVL(token, timestamp, depositor, assets, depositor); + uint256 sharesOut = withdrawCVL(token, timestamp, depositor, assets, depositor, depositor); + + assert sharesOut >= sharesIn; + satisfy assets > 0 && sharesOut == sharesIn; +} \ No newline at end of file diff --git a/certora/specs/ERC4626/verification/verify.conf b/certora/specs/ERC4626/verification/verify.conf new file mode 100644 index 0000000..f1eb4a7 --- /dev/null +++ b/certora/specs/ERC4626/verification/verify.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "ERC20/verification/Test.sol", + ], + "prover_args":[ + "-cvlFunctionRevert true", + ], + "verify": "Test:ERC4626/verification/Rules.spec", + "process": "emv", + "smt_timeout": "1800", + "server": "prover", + "solc": "solc8.20", + "msg":"CVL ERC4626 test" +} \ No newline at end of file diff --git a/certora/specs/Enabled.spec b/certora/specs/Enabled.spec new file mode 100644 index 0000000..3da4514 --- /dev/null +++ b/certora/specs/Enabled.spec @@ -0,0 +1,137 @@ +// Based on Enabled.spec and DistinctIdentifiers.spec in SiloVault spec + +import "PendingValues.spec"; + +methods +{ + function withdrawQueue(uint256) external returns(address) envfree; + function supplyQueue(uint256) external returns(address) envfree; + function supplyQGetAt(uint256) external returns (address) envfree; + function supplyQLength() external returns (uint256) envfree; + function withdrawQGetAt(uint256) external returns (address) envfree; + function withdrawQLength() external returns (uint256) envfree; + // these functions are ghost functions that come from the harness and simplify the verification + function withdrawRank(address) external returns(uint256) envfree; + function deletedAt(address) external returns(uint256) envfree; +} + +function isInWithdrawQueueIsEnabled(uint256 i) returns bool { + if(i >= withdrawQueueLength()) return true; + + address market = withdrawQueue(i); + + return config_(market).enabled; +} + +// Verified +invariant distinctIdentifiers(uint256 i, uint256 j) + i != j => withdrawQueue(i) != withdrawQueue(j) +{ + preserved updateWithdrawQueue(uint256[] indexes) with (env e) { + requireInvariant distinctIdentifiers(indexes[i], indexes[j]); + } +} + +// Verified +invariant inWithdrawQueueIsEnabled(uint256 i) + isInWithdrawQueueIsEnabled(i) +filtered { + f -> f.selector != sig:updateWithdrawQueue(uint256[]).selector +} + +// Verified +rule inWithdrawQueueIsEnabledPreservedUpdateWithdrawQueue(env e, uint256 i, uint256[] indexes) { + uint256 j; + require isInWithdrawQueueIsEnabled(indexes[i]); + + requireInvariant distinctIdentifiers(indexes[i], j); + + updateWithdrawQueue(e, indexes); + + address market = withdrawQueue(i); + // Safe require because j is not otherwise constrained. + // The ghost variable deletedAt is useful to make sure that markets are not permuted and deleted at the same time in updateWithdrawQueue. + require j == deletedAt(market); + + assert isInWithdrawQueueIsEnabled(i); +} + +function isWithdrawRankCorrect(address market) returns bool { + uint256 rank = withdrawRank(market); + + if (rank == 0) return true; + + return withdrawQueue(assert_uint256(rank - 1)) == market; +} + +// Verified +invariant withdrawRankCorrect(address market) + isWithdrawRankCorrect(market); + +// Verified +invariant enabledHasPositiveRank(address market) + config_(market).enabled => withdrawRank(market) > 0; + +// Verified +rule enabledIsInWithdrawQueue(address market) { + require config_(market).enabled; + + requireInvariant enabledHasPositiveRank(market); + requireInvariant withdrawRankCorrect(market); + + uint256 witness = assert_uint256(withdrawRank(market) - 1); + assert withdrawQueue(witness) == market; +} + +// Verified +invariant nonZeroCapHasPositiveRank(address market) + config_(market).cap > 0 => withdrawRank(market) > 0 + { + preserved { + requireInvariant enabledHasPositiveRank(market); + } +} + +function setSupplyQueueInputIsValid(address[] newSupplyQueue) returns bool +{ + uint256 i; + require i < newSupplyQueue.length; + uint184 someCap = config_(newSupplyQueue[i]).cap; + bool result; + require result == false => someCap == 0; + return result; +} + +// Verified + rule setSupplyQueueRevertsOnInvalidInput(env e, address[] newSupplyQueue) +{ + setSupplyQueue@withrevert(e, newSupplyQueue); + bool reverted = lastReverted; + assert !setSupplyQueueInputIsValid(newSupplyQueue) => reverted; +} + +// Verified +invariant addedToSupplyQThenIsInWithdrawQ(uint256 supplyQIndex) + supplyQIndex < supplyQLength() => withdrawRank(supplyQGetAt(supplyQIndex)) > 0 + filtered { f -> f.selector != sig:updateWithdrawQueue(uint256[]).selector /* the method allowed to break this */ } + { + preserved setSupplyQueue(address[] newSupplyQueue) with (env e) { + requireInvariant nonZeroCapHasPositiveRank(newSupplyQueue[supplyQIndex]); + require setSupplyQueueInputIsValid(newSupplyQueue); //safe assumption. See setSupplyQueueRevertsOnInvalidInput + } + preserved { + requireInvariant nonZeroCapHasPositiveRank(supplyQGetAt(supplyQIndex)); + } +} + + +// Verified +rule enabledIsInWithdrawalQueue(address market) { + require config_(market).enabled; + + requireInvariant enabledHasPositiveRank(market); + requireInvariant withdrawRankCorrect(market); + + uint256 witness = assert_uint256(withdrawRank(market) - 1); + assert withdrawQueue(witness) == market; +} diff --git a/certora/specs/EulerEarnERC4626.spec b/certora/specs/EulerEarnERC4626.spec new file mode 100644 index 0000000..a35494e --- /dev/null +++ b/certora/specs/EulerEarnERC4626.spec @@ -0,0 +1,231 @@ +//Based on generic ERC4626 specification: https://github.com/Certora/Examples/blob/master/DEFI/ERC4626/certora/specs/ERC4626.spec + +import "setup/dispatchingWithoutVaultSummaries.spec"; +import "summaries/Math.spec"; +using Token0 as Token0; +using ERC20Helper as ERC20Helper; +using EthereumVaultConnector as EVC; + +methods { + function _._msgSender() internal with (env e) => e.msg.sender expect address; //ignoring EVC compatibility + + function SafeERC20.safeTransfer(address token,address to,uint256 value) internal with (env e) + => tokenTransferFromToCVL(e,token,calledContract,to,value); + function EulerEarn.HOOK_after_accrueInterest() internal => CVL_after_accrueInterest(); + + function EVC.getAccountOwner(address) external returns address envfree; + function config_(address) external returns EulerEarnHarness.MarketConfig envfree; + function virtualAmount() external returns uint256 envfree; + function permit2Address() external returns address envfree; + function feeRecipient() external returns address envfree; + function withdrawQGetAt(uint256) external returns address envfree; + function name() external returns string envfree; + function symbol() external returns string envfree; + function decimals() external returns uint8 envfree; + function asset() external returns address envfree; + function fees() external returns uint256 envfree; + function lostAssets() external returns uint256 envfree; + function lastTotalAssets() external returns uint256 envfree; + function realTotalAssets() external returns uint256 envfree; + function fee() external returns uint96 envfree; + function wad() external returns uint256 envfree; + function withdrawQueueLength() external returns uint256 envfree; + function ERC20Helper.totalSupply(address) external returns uint256 envfree; + function totalSupply() external returns uint256 envfree; + function balanceOf(address) external returns uint256 envfree; + function reentrancyGuardEntered() external returns bool envfree; + + function approve(address,uint256) external returns bool; + function deposit(uint256,address) external; + function mint(uint256,address) external; + function withdraw(uint256,address,address) external; + function redeem(uint256,address,address) external; + function totalAssets() external returns uint256 envfree; + function convertToShares(uint256) external returns uint256 envfree; + function convertToAssets(uint256) external returns uint256 envfree; + function previewDeposit(uint256) external returns uint256 envfree; + function previewMint(uint256) external returns uint256 envfree; + function previewWithdraw(uint256) external returns uint256 envfree; + function previewRedeem(uint256) external returns uint256 envfree; + function maxDeposit(address) external returns uint256 envfree; + function maxMint(address) external returns uint256 envfree; + function maxWithdraw(address) external returns uint256 envfree; + function maxRedeem(address) external returns uint256 envfree; + function maxFee() external returns uint256 envfree; + function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external; + function DOMAIN_SEPARATOR() external returns bytes32; + function Token0.balanceOf(address) external returns uint256 envfree; + function Token0.allowance(address, address) external returns uint256 envfree; + function Token0.transferFrom(address,address,uint256) external returns bool; + function allowance(address,address) external returns uint256 envfree; +} + +function tokenTransferFromToCVL(env e,address token,address from, address to, uint256 value) { + if (token == Token0) { + Token0._transfer(e,from, to, value); + return; + } + require false, "this should only be called on Token0"; +} + +function safeAssumptions(env e) { + require currentContract != asset(); // Although this is not disallowed, we assume the contract's underlying asset is not the contract itself + requireInvariant totalSupplyIsSumOfBalances(); + require msgSender(e) != currentContract; // This is proved by rule noDynamicCalls + require require_uint256(fee()) <= maxFee(); + requireInvariant configBalanceAndTotalSupply(withdrawQGetAt(0)); + requireInvariant noAssetsOnEuler(); + + uint256 fees; + uint256 totalAssets; + uint256 lostAssets; + uint256 totalSupply = totalSupply(); + (fees,totalAssets,lostAssets) = _accruedFeeAndAssets(e); + require totalAssets >= fees + totalSupply, "proven in TotalAssetsMoreThanSupplyAndFees - in different cases"; + require totalAssets <= 2^128, "reasonable value for totalAssets"; + require totalSupply <= 2^128, "reasonable value for totalSupply"; + require lostAssets <= 2^128, "reasonable value for lostAssets"; +} + +ghost mathint sumOfBalances { + init_state axiom sumOfBalances == 0; +} + +hook Sstore _balances[KEY address addy] uint256 newValue (uint256 oldValue) { + sumOfBalances = sumOfBalances + newValue - oldValue; +} + +hook Sload uint256 val _balances[KEY address addy] { + require sumOfBalances >= val; +} + +// Verified +invariant totalSupplyIsSumOfBalances() + totalSupply() == sumOfBalances; + + +// Verified +invariant noAssetsOnEuler() + Token0.balanceOf(currentContract) == 0 + { + preserved withdraw(uint256 assets, address receiver, address owner) with (env e) { + require receiver != currentContract; + require owner != currentContract; + safeAssumptions(e); + } + preserved redeem(uint256 assets, address receiver, address owner) with (env e) { + require receiver != currentContract; + require owner != currentContract; + safeAssumptions(e); + } + preserved with (env e) { + safeAssumptions(e); + } + } + +/// solvency properties. + +function CVL_after_accrueInterest() { + assert totalAssets() >= totalSupply() + fees(); +} + +invariant TotalAssetsMoreThanSupplyAndFees() + totalAssets() >= totalSupply() + fees() + //filter out withdraw, redeem, deposit, mint - those are proven in a different rule - solvency in Internal Withdraw + filtered { + f -> (f.selector != sig:withdraw(uint256,address,address).selector && + f.selector != sig:redeem(uint256,address,address).selector && + f.selector != sig:deposit(uint256,address).selector && + f.selector != sig:mint(uint256,address).selector) + } + { + preserved updateWithdrawQueue(uint256[] indexes) with (env e) { + safeAssumptions(e); + require withdrawQueueLength() == 1; + require indexes.length != 0; + } + preserved with (env e) { + safeAssumptions(e); + require withdrawQueueLength() == 1; + } + } + +// Verified +rule underlyingCannotChange() +{ + address originalAsset = asset(); + + method f; env e; calldataarg args; + f(e, args); + + address newAsset = asset(); + + assert originalAsset == newAsset, + "the underlying asset of a contract must not change"; +} + +// Verified -- not standard ERC4626 but specific to us, this is simple because config_(market).balance should equal market.balanceOf(currentContract) +invariant configBalanceAndTotalSupply(address market) + config_(market).balance <= ERC20Helper.totalSupply(market) + { + preserved with(env e) { + require msgSender(e) != currentContract; + safeAssumptions(e); + } + } + + +// Verified on most recent verison (was violated before) https://prover.certora.com/output/5771024/75bb49eac8b34219bb9e177fcc25773a/ +rule zeroDepositZeroShares(uint assets, address receiver){ + env e; + + uint shares = deposit(e,assets, receiver); + + assert shares == 0 <=> assets == 0; +} + + +// Verified https://prover.certora.com/output/5771024/9d68a0e5a30c454f9f0ca25cd10230f6/ +rule redeemingAllValidity() { + address owner; + address feeRecipient = feeRecipient(); + require owner != feeRecipient; + + uint256 shares; require shares == balanceOf(owner); + + env e; safeAssumptions(e); + redeem(e, shares, _, owner); + uint256 ownerBalanceAfter = balanceOf(owner); + assert ownerBalanceAfter == 0; +} + +// Verified https://prover.certora.com/output/5771024/fdeec6302e9b429bb0b725f3d9fd22fe +invariant zeroAllowanceOnAssets(address user) + // no alloownaces from current contract. + Token0.allowance(currentContract, user) == 0 && currentContract.allowance(currentContract, user) == 0 { + preserved with(env e) { + require msgSender(e) != currentContract; + safeAssumptions(e); + require user != permit2Address(), "allownaces for permit2 behave differently."; + } + } + +// Verified +rule onlyContributionMethodsReduceAssets(method f) { + address user; require user != currentContract; + uint256 userBalanceOfBefore = Token0.balanceOf(user); + + env e; + calldataarg args; + safeAssumptions(e); + + f(e, args); + + uint256 userBalanceOfAfter = Token0.balanceOf(user); + + assert userBalanceOfBefore > userBalanceOfAfter => + (f.selector == sig:deposit(uint256,address).selector || + f.selector == sig:mint(uint256,address).selector || + f.contract == asset() || f.contract == currentContract), + "a user's assets must not go down except on calls to contribution methods or calls directly to the asset."; +} \ No newline at end of file diff --git a/certora/specs/Immutability.spec b/certora/specs/Immutability.spec new file mode 100644 index 0000000..2481b15 --- /dev/null +++ b/certora/specs/Immutability.spec @@ -0,0 +1,19 @@ +// Based on Immutability.spec in SiloVault spec + +persistent ghost bool delegateCall; + +hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + delegateCall = true; +} + +// Check that the contract is truly immutable. +rule noDelegateCalls(method f, env e, calldataarg data) + filtered { + f -> (f.contract == currentContract) + } +{ + // Set up the initial state. + require !delegateCall; + f(e,data); + assert !delegateCall; +} \ No newline at end of file diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec new file mode 100644 index 0000000..2ba3ced --- /dev/null +++ b/certora/specs/Liveness.spec @@ -0,0 +1,82 @@ +// Based on Liveness.spec in SiloVault spec + +import "Reverts.spec"; + +// Check that having the allocator role allows to pause supply on the vault. +// Verified +rule canPauseSupply() { + // require !lock(); + + env e1; address[] newSupplyQueue; + + address evc = EVC(); + require e1.msg.sender != evc && hasAllocatorRole(e1.msg.sender); + require e1.msg.value == 0; + require newSupplyQueue.length == 0; + + setSupplyQueue@withrevert(e1, newSupplyQueue); + assert !lastReverted; + + storage pausedSupply = lastStorage; + + env e2; uint256 assets2; address receiver2; + require assets2 != 0; + deposit@withrevert(e2, assets2, receiver2) at pausedSupply; + assert lastReverted; + + env e3; uint256 shares3; address receiver3; + uint256 assets3 = mint@withrevert(e3, shares3, receiver3) at pausedSupply; + require assets3 != 0; + assert lastReverted; +} + +// Checks that currator is able to remove (disable) any market +// Verified +rule canForceRemoveMarket(address market) { + requireInvariant supplyCapIsEnabled(market); + requireInvariant enabledHasConsistentAsset(market); + // Safe require because this holds as an invariant. + // require hasPositiveSupplyCapIsUpdated(market); + + EulerEarnHarness.MarketConfig config = config_(market); + require config.cap > 0; + require config.removableAt == 0; + // Assume that the withdraw queue is [X, market]; + require withdrawQueue(1) == market; + require withdrawQueueLength() == 2; + + require !reentrancyGuardEntered(), "call is not during reentrancy"; + + env e1; env e2; env e3; + require hasCuratorRole(e1.msg.sender); + require e2.msg.sender == e1.msg.sender; + require e3.msg.sender == e1.msg.sender; + address evc = EVC(); + require e1.msg.sender != evc; + + require e1.msg.value == 0; + revokePendingCap@withrevert(e1, market); + assert !lastReverted; + + require e2.msg.value == 0; + submitCap@withrevert(e2, market, 0); + assert !lastReverted; + + require e3.msg.value == 0; + requireInvariant timelockInRange(); + // Safe require as it corresponds to some time very far into the future. + require e3.block.timestamp < 2^63; + submitMarketRemoval@withrevert(e3, market); + assert !lastReverted; + + env e4; uint256[] newWithdrawQueue; + require newWithdrawQueue.length == 1; + require newWithdrawQueue[0] == 0; + require e4.msg.value == 0; + require hasAllocatorRole(e4.msg.sender); + require to_mathint(e4.block.timestamp) >= e3.block.timestamp + timelock(); + updateWithdrawQueue@withrevert(e4, newWithdrawQueue); + assert !lastReverted; + + assert !config_(market).enabled; +} \ No newline at end of file diff --git a/certora/specs/LostAssets.spec b/certora/specs/LostAssets.spec new file mode 100644 index 0000000..05a1b57 --- /dev/null +++ b/certora/specs/LostAssets.spec @@ -0,0 +1,150 @@ +//Based on rules from metamorpho v1.1 - https://github.com/morpho-org/metamorpho-v1.1/blob/main/certora/specs/LostAssetsNoLink.spec + +import "Range.spec"; + +methods { + function name() external returns string envfree; + function symbol() external returns string envfree; + function decimals() external returns uint8 envfree; + function asset() external returns address envfree; + function fees() external returns uint256 envfree; + function lostAssets() external returns uint256 envfree; + function lastTotalAssets() external returns uint256 envfree; + function realTotalAssets() external returns uint256 envfree; + function fee() external returns uint96 envfree; + function wad() external returns uint256 envfree; + function virtualAmount() external returns uint256 envfree; + + function totalSupply() external returns uint256 envfree; + function balanceOf(address) external returns uint256 envfree; + + function approve(address,uint256) external returns bool; + function deposit(uint256,address) external; + function mint(uint256,address) external; + function withdraw(uint256,address,address) external; + function redeem(uint256,address,address) external; + + function totalAssets() external returns uint256 envfree; + function convertToShares(uint256) external returns uint256 envfree; + function convertToAssets(uint256) external returns uint256 envfree; + function previewDeposit(uint256) external returns uint256 envfree; + function previewMint(uint256) external returns uint256 envfree; + function previewWithdraw(uint256) external returns uint256 envfree; + function previewRedeem(uint256) external returns uint256 envfree; + + function maxDeposit(address) external returns uint256 envfree; + function maxMint(address) external returns uint256 envfree; + function maxWithdraw(address) external returns uint256 envfree; + function maxRedeem(address) external returns uint256 envfree; + + function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external; + function DOMAIN_SEPARATOR() external returns bytes32; + + function Token0.balanceOf(address) external returns uint256 envfree; + function Token0.allowance(address, address) external returns uint256 envfree; + function Token0.transferFrom(address,address,uint256) external returns bool; + + function allowance(address,address) external returns uint256 envfree; +} + + +// Check that the lost assets always increase. +rule lostAssetsIncreases(method f, env e, calldataarg args) + filtered { f -> !f.isView } +{ + uint256 lostAssetsBefore = lostAssets(); + + f(e, args); + + uint256 lostAssetsAfter = lostAssets(); + + assert lostAssetsBefore <= lostAssetsAfter; +} + +// Check that the last total assets are smaller than the total assets. +rule lastTotalAssetsSmallerThanTotalAssets() { + assert lastTotalAssets() <= totalAssets(); +} + +// Check that the last total assets increase except on withdrawal and redeem. +rule lastTotalAssetsIncreases(method f, env e, calldataarg args) +filtered { + f -> f.selector != sig:withdraw(uint256, address, address).selector && + f.selector != sig:redeem(uint256, address, address).selector && + f.selector != sig:updateWithdrawQueue(uint256[]).selector && + !f.isView +} +{ + uint256 lastTotalAssetsBefore = lastTotalAssets(); + + f(e, args); + + uint256 lastTotalAssetsAfter = lastTotalAssets(); + + assert lastTotalAssetsBefore <= lastTotalAssetsAfter; +} + +// Check that the last total assets decreases on withdraw. +rule lastTotalAssetsDecreasesCorrectlyOnWithdraw(env e, uint256 assets, address receiver, address owner) { + uint256 lastTotalAssetsBefore = lastTotalAssets(); + + withdraw(e, assets, receiver, owner); + + uint256 lastTotalAssetsAfter = lastTotalAssets(); + + assert to_mathint(lastTotalAssetsAfter) >= lastTotalAssetsBefore - assets; +} + +// Check that the last total assets decreases on redeem. +rule lastTotalAssetsDecreasesCorrectlyOnRedeem(env e, uint256 shares, address receiver, address owner) { + uint256 lastTotalAssetsBefore = lastTotalAssets(); + + uint256 assets = redeem(e, shares, receiver, owner); + + uint256 lastTotalAssetsAfter = lastTotalAssets(); + + assert to_mathint(lastTotalAssetsAfter) >= lastTotalAssetsBefore - assets; +} + +persistent ghost mathint sumBalances { + init_state axiom sumBalances == 0; +} + +hook Sload uint256 balance _balances[KEY address addr] { + require sumBalances >= to_mathint(balance); +} + +hook Sstore _balances[KEY address user] uint256 newBalance (uint256 oldBalance) { + sumBalances = sumBalances + newBalance - oldBalance; +} + +// Check that the total supply is the sum of the balances. +strong invariant totalIsSumBalances() + to_mathint(totalSupply()) == sumBalances; + +// Check that the share price does not decrease lower than the one at the last interaction. +rule sharePriceIncreases(method f, env e, calldataarg args) + filtered { f -> !f.isView } +{ + requireInvariant totalIsSumBalances(); + require assert_uint256(fee()) == 0; + + // We query them in a state in which the vault is sync. + uint256 lastTotalAssetsBefore = lastTotalAssets(); + uint256 totalSupplyBefore = totalSupply(); + require totalSupplyBefore > 0; + + f(e, args); + + uint256 totalAssetsAfter = lastTotalAssets(); + uint256 totalSupplyAfter = totalSupply(); + require totalSupplyAfter > 0; + + // there is no decimals_offset here + // uint256 decimalsOffset = assert_uint256(DECIMALS_OFFSET()); + // require decimalsOffset == 18; + // instead we have virtual amount + uint256 virtualAmount = virtualAmount(); + + assert (lastTotalAssetsBefore + virtualAmount) * (totalSupplyAfter + virtualAmount) <= (totalAssetsAfter + virtualAmount) * (totalSupplyBefore + virtualAmount); +} \ No newline at end of file diff --git a/certora/specs/PendingValues.spec b/certora/specs/PendingValues.spec new file mode 100644 index 0000000..51c9369 --- /dev/null +++ b/certora/specs/PendingValues.spec @@ -0,0 +1,71 @@ +// Based on PendingValues.spec in SiloVault spec + +import "Range.spec"; + +methods { + function pendingGuardian_() external returns(EulerEarnHarness.PendingAddress) envfree; + function guardian() external returns(address) envfree; + function pendingTimelock_() external returns(EulerEarnHarness.PendingUint136) envfree; + function config_(address) external returns(EulerEarnHarness.MarketConfig) envfree; +} + +// Pending Values have two fields: value - the value to be set, and validAt - the minimal timestamp when it can be set. +// When the value valid and set we reset the pending value to 0 -- this is what is verified here. + +// Verified +invariant noBadPendingTimelock() + pendingTimelock_().validAt == 0 <=> pendingTimelock_().value == 0 +{ + preserved with (env e) { + requireInvariant timelockInRange(); + require e.block.timestamp < 2^63, "reasonable timestamp"; + } +} + +// Verified +invariant smallerPendingTimelock() + (assert_uint256(pendingTimelock_().value) < timelock()) || timelock() == 0 +{ + preserved { + requireInvariant pendingTimelockInRange(); + requireInvariant timelockInRange(); + } +} + +// Verified +invariant noBadPendingCap(address market) + pendingCap_(market).validAt == 0 <=> pendingCap_(market).value == 0 +{ + preserved with (env e) { + requireInvariant timelockInRange(); + require e.block.timestamp < 2^63, "reasonable timestamp"; + require e.block.timestamp > 0, "reasonable timestamp"; + } +} + +function isGreaterPendingCap(address market) returns bool { + uint192 pendingCapValue = pendingCap_(market).value; + uint192 currentCapValue = config_(market).cap; + + return pendingCapValue != 0 => assert_uint256(pendingCapValue) > assert_uint256(currentCapValue); +} + +// Verified +invariant greaterPendingCap(address market) + isGreaterPendingCap(market); + +// Verified +invariant noBadPendingGuardian() + // Notice that address(0) is a valid value for a new guardian. + pendingGuardian_().validAt == 0 => pendingGuardian_().value == 0 +{ + preserved with (env e) { + requireInvariant timelockInRange(); + require e.block.timestamp < 2^63, "reasonable timestamp"; + require e.block.timestamp > 0, "reasonable timestamp"; + } +} + +// Verified +invariant differentPendingGuardian() + pendingGuardian_().value != 0 => pendingGuardian_().value != guardian(); \ No newline at end of file diff --git a/certora/specs/Range.spec b/certora/specs/Range.spec new file mode 100644 index 0000000..4560cc9 --- /dev/null +++ b/certora/specs/Range.spec @@ -0,0 +1,48 @@ +// Based on Range.spec in SiloVault spec + +import "setup/dispatching_EulerEarn.spec"; +import "summaries/Math.spec"; + +methods { + function timelock() external returns(uint256) envfree; + function supplyQueueLength() external returns(uint256) envfree; + function withdrawQueueLength() external returns(uint256) envfree; + function fee() external returns(uint96) envfree; + function pendingTimelock_() external returns(EulerEarnHarness.PendingUint136) envfree; + function minTimelock() external returns(uint256) envfree; + function maxTimelock() external returns(uint256) envfree; + function maxQueueLength() external returns(uint256) envfree; + function maxFee() external returns(uint256) envfree; + function pendingCap_(address) external returns(EulerEarnHarness.PendingUint136) envfree; +} + +//Verified +invariant pendingTimelockInRange() + pendingTimelock_().validAt != 0 => + assert_uint256(pendingTimelock_().value) <= maxTimelock() && + assert_uint256(pendingTimelock_().value) >= minTimelock(); + +//Verified -- in Euler timelock can be initiated at 0 like in metamorpho v1.1 (and unlike Silo) +invariant timelockInRange() + (timelock() <= maxTimelock() && timelock() >= minTimelock()) || timelock() == 0 + { + preserved { + requireInvariant pendingTimelockInRange(); + } + } + +//Verified +invariant pendingCapIsUint136(address market) + to_mathint(pendingCap_(market).value) < 2^136; + +//Verified +invariant feeInRange() + assert_uint256(fee()) <= maxFee(); + +//Verified +invariant supplyQueueLengthInRange() + supplyQueueLength() <= maxQueueLength(); + +//Verified +invariant withdrawQueueLengthInRange() + withdrawQueueLength() <= maxQueueLength(); \ No newline at end of file diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec new file mode 100644 index 0000000..16bc1df --- /dev/null +++ b/certora/specs/Reentrancy.spec @@ -0,0 +1,105 @@ +// Based on Reentrancy.spec in SiloVault spec + +import "summaries/Math.spec"; + +using EulerEarnHarness as EulerEarnHarness; + +methods { + // because these rules only depend on the call structure we heavily summarize + // by making all action just nondeterministic returns + // for functions that perform trusted external calls we additionally call + // ignoreExternalCall() that sets the guard ignoreCall to true, avoiding the next hooked ext. call. + function _.deposit(uint256, address) external => uintTrustedExternalCall() expect (uint256); + function _.withdraw(uint256, address, address) external => uintTrustedExternalCall() expect (uint256); + function _.redeem(uint256, address, address) external => uintTrustedExternalCall() expect (uint256); + function _.approve(address, uint256) external => boolTrustedExternalCall() expect (bool); + function _.approve(address, address, uint160, uint48) external => boolTrustedExternalCall() expect (bool); + function _.transfer(address, uint256) external => boolTrustedExternalCall() expect bool; + function _.transferFrom(address, address, uint256) external => boolTrustedExternalCall() expect bool; + function SafeERC20Permit2Lib.forceApproveMaxWithPermit2(address,address,address) internal => voidTrustedExternalCall(); + function SafeERC20Permit2Lib.revokeApprovalWithPermit2(address,address,address) internal => voidTrustedExternalCall(); + function SafeERC20Permit2Lib.safeTransferFromWithPermit2(address, address, address, uint256, address) internal => voidTrustedExternalCall(); + function SafeERC20.safeTransfer(address,address,uint256) internal => voidTrustedExternalCall(); + function SafeERC20.safeTransferFrom(address,address,address,uint256) internal => voidTrustedExternalCall(); + + function _.balanceOf(address) external => uintNoCall() expect uint256; + function _.previewRedeem(uint256) external => uintNoCall() expect uint256; + function _.convertToAssets(uint256) external => uintNoCall() expect (uint256); + function _.asset() external => addressNoCall() expect address; + function _.permit2Address() external => addressNoCall() expect address; + function _.isStrategyAllowed(address) external => boolNoCall() expect bool; + function _.maxWithdraw(address) external => uintNoCall() expect uint; + function _.maxDeposit(address) external => uintNoCall() expect uint; +} + +persistent ghost bool ignoredCall; +persistent ghost bool hasCall; + +hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + if (ignoredCall) { + // Ignore calls to tokens and Morpho markets as they are trusted (they have gone through a timelock). + ignoredCall = false; + } else { + hasCall = true; + } +} + + +function ignoreExternalCall() { + ignoredCall = true; +} + +function uintTrustedExternalCall() returns uint256 { + ignoreExternalCall(); + uint256 value; + return value; +} + +function uintNoCall() returns uint256 { + uint256 value; + return value; +} + +function boolTrustedExternalCall() returns bool { + ignoreExternalCall(); + bool value; + return value; +} + +function boolNoCall() returns bool { + bool value; + return value; +} + +function addressTrustedExternalCall() returns address { + ignoreExternalCall(); + address value; + return value; +} + +function addressNoCall() returns address { + address value; + return value; +} + +function voidTrustedExternalCall() { + ignoreExternalCall(); + return; +} + +function voidNoCall() { + return; +} + + +// Check that there are no untrusted external calls, ensuring notably reentrancy safety. +rule reentrancySafe(method f, env e, calldataarg data) + filtered { + f -> (f.contract == currentContract) + } +{ + // Set up the initial state. + require !ignoredCall && !hasCall; + f(e,data); + assert !hasCall; +} \ No newline at end of file diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec new file mode 100644 index 0000000..9aafa69 --- /dev/null +++ b/certora/specs/Reverts.spec @@ -0,0 +1,381 @@ +// Based on Reverts.spec in SiloVault spec + +import "ConsistentState.spec"; + +methods { + function msgSender() external returns address; + function reentrancyGuardEntered() external returns bool envfree; + function msgSenderOnlyEVCAccountOwner() external returns address; + function isStrategyAllowedHarness(address) external returns bool envfree; + function EVC() external returns address envfree; +} + +function msgSenderOnlyEVCAccountOwnerReverted(env e) returns bool { + msgSenderOnlyEVCAccountOwner@withrevert(e); + return lastReverted; +} + +function msgSenderReverted(env e) returns bool { + msgSender@withrevert(e); + return lastReverted; +} + + +//Check that vault can't have reentrancy lock on after interaction +// Verified +rule reentrancyLockFalseAfterInteraction (method f, env e, calldataarg args) + filtered { + f -> (f.contract == currentContract) + } +{ + require !reentrancyGuardEntered(); + f(e, args); + assert !reentrancyGuardEntered(); +} + + +//Check all the revert conditions of the setCurator function. +// Verified +rule setCuratorRevertCondition(env e, address newCurator) { + address msgSender = msgSender(e); + address owner = owner(); + address oldCurator = curator(); + + setCurator@withrevert(e, newCurator); + + assert lastReverted <=> + e.msg.value != 0 || + msgSender != owner || + newCurator == oldCurator; +} + + +//Check all the revert conditions of the setIsAllocator function. +// Verified +rule setIsAllocatorRevertCondition(env e, address newAllocator, bool newIsAllocator) { + address msgSender = msgSender(e); + address owner = owner(); + bool wasAllocator = isAllocator(newAllocator); + + setIsAllocator@withrevert(e, newAllocator, newIsAllocator); + + assert lastReverted <=> + e.msg.value != 0 || + msgSender != owner || + newIsAllocator == wasAllocator; +} + + +//Check the input validation conditions under which the setFee function reverts. +// This function can also revert if interest accrual reverts. +// Verified +rule setFeeInputValidation(env e, uint256 newFee) { + address msgSender = msgSender(e); + address owner = owner(); + uint96 oldFee = fee(); + address feeRecipient = feeRecipient(); + + setFee@withrevert(e, newFee); + + assert e.msg.value != 0 || + msgSender != owner || + newFee == assert_uint256(oldFee) || + (newFee != 0 && feeRecipient == 0) + => lastReverted; +} + + +//Check the input validation conditions under which the setFeeRecipient function reverts. +// This function can also revert if interest accrual reverts. +// Verified +rule setFeeRecipientInputValidation(env e, address newFeeRecipient) { + address msgSender = msgSender(e); + address owner = owner(); + uint96 fee = fee(); + address oldFeeRecipient = feeRecipient(); + + setFeeRecipient@withrevert(e, newFeeRecipient); + + assert e.msg.value != 0 || + msgSender != owner || + newFeeRecipient == oldFeeRecipient || + (fee != 0 && newFeeRecipient == 0) + => lastReverted; +} + + +//Check all the revert conditions of the submitGuardian function. +// Verified +rule submitGuardianRevertCondition(env e, address newGuardian) { + address msgSender = msgSender(e); + address owner = owner(); + address oldGuardian = guardian(); + uint64 pendingGuardianValidAt = pendingGuardian_().validAt; + + requireInvariant timelockInRange(); + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + submitGuardian@withrevert(e, newGuardian); + + assert lastReverted <=> + e.msg.value != 0 || + msgSender != owner || + newGuardian == oldGuardian || + pendingGuardianValidAt != 0; +} + + +//Check all the revert conditions of the submitCap function. +// Verified +rule submitCapRevertCondition(env e, address market, uint256 newSupplyCap) { + address msgSender = msgSender(e); + bool hasCuratorRole = hasCuratorRole(msgSender); + bool msgSenderOnlyEVCAccountOwnerReverted = msgSenderOnlyEVCAccountOwnerReverted(e); + address asset = asset(); + uint256 pendingCapValidAt = pendingCap_(market).validAt; + EulerEarnHarness.MarketConfig config = config_(market); + bool strategyAllowed = isStrategyAllowedHarness(market); + bool reentrancyEntered = reentrancyGuardEntered(); + + requireInvariant timelockInRange(); + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + requireInvariant supplyCapIsEnabled(market); + + submitCap@withrevert(e, market, newSupplyCap); + + assert lastReverted <=> + e.msg.value != 0 || + !hasCuratorRole || + getVaultAsset(market) != asset || + pendingCapValidAt != 0 || + config.removableAt != 0 || + newSupplyCap == assert_uint256(config.cap) || + (newSupplyCap == 2^184-1 && config.cap == 2^136-1 ) || //new revert condition due to their most recent fix. + (newSupplyCap >= 2^136 && newSupplyCap != 2^184-1) || + msgSenderOnlyEVCAccountOwnerReverted || + reentrancyEntered || + !strategyAllowed; +} + + +//Check all the revert conditions of the submitMarketRemoval function. +// Verified + +rule submitMarketRemovalRevertCondition(env e, address market) { + address msgSender = msgSender(e); + bool hasCuratorRole = hasCuratorRole(msgSender); + uint256 pendingCapValidAt = pendingCap_(market).validAt; + EulerEarnHarness.MarketConfig config = config_(market); + bool msgSenderOnlyEVCAccountOwnerReverted = msgSenderOnlyEVCAccountOwnerReverted(e); + + requireInvariant timelockInRange(); + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + submitMarketRemoval@withrevert(e, market); + + assert lastReverted <=> + e.msg.value != 0 || + !hasCuratorRole || + pendingCapValidAt != 0 || + config.cap != 0 || + !config.enabled || + config.removableAt != 0 || + msgSenderOnlyEVCAccountOwnerReverted; +} + + +//Check the input validation conditions under which the setSupplyQueue function reverts. +// There are no other condition under which this function reverts, but it cannot be expressed easily because of the encoding of the universal quantifier chosen. +// Verified + +rule setSupplyQueueInputValidation(env e, address[] newSupplyQueue) { + address msgSender = msgSender(e); + bool hasAllocatorRole = hasAllocatorRole(msgSender); + uint256 maxQueueLength = maxQueueLength(); + uint256 i; + require i < newSupplyQueue.length; + uint184 anyCap = config_(newSupplyQueue[i]).cap; + bool msgSenderOnlyEVCAccountOwnerReverted = msgSenderOnlyEVCAccountOwnerReverted(e); + + setSupplyQueue@withrevert(e, newSupplyQueue); + + assert e.msg.value != 0 || + !hasAllocatorRole || + newSupplyQueue.length > maxQueueLength || + anyCap == 0 || + msgSenderOnlyEVCAccountOwnerReverted + => lastReverted; +} + + +//Check the input validation conditions under which the updateWithdrawQueue function reverts. +// This function can also revert if a market is removed when it shouldn't: +// - a removed market should have 0 supply cap +// - a removed market should not have a pending cap +// - a removed market should either have no supply or (be marked for forced removal and that timestamp has elapsed) +// Verified + +rule updateWithdrawQueueInputValidation(env e, uint256[] indexes) { + address msgSender = msgSender(e); + bool hasAllocatorRole = hasAllocatorRole(msgSender); + uint256 i; + require i < indexes.length; + uint256 j; + require j < indexes.length; + uint256 anyIndex = indexes[i]; + uint256 oldLength = withdrawQueueLength(); + uint256 anyOtherIndex = indexes[j]; + bool msgSenderOnlyEVCAccountOwnerReverted = msgSenderOnlyEVCAccountOwnerReverted(e); + + updateWithdrawQueue@withrevert(e, indexes); + + assert e.msg.value != 0 || + !hasAllocatorRole || + anyIndex > oldLength || + (i != j && anyOtherIndex == anyIndex) || + msgSenderOnlyEVCAccountOwnerReverted + => lastReverted; +} + + +//Check the input validation conditions under which the reallocate function reverts. +// This function can also revert for non enabled markets and if the total withdrawn differs from the total supplied. +// Verified + +rule reallocateInputValidation(env e, EulerEarnHarness.MarketAllocation[] allocations) { + address msgSender = msgSender(e); + bool hasAllocatorRole = hasAllocatorRole(msgSender); + bool msgSenderOnlyEVCAccountOwnerReverted = msgSenderOnlyEVCAccountOwnerReverted(e); + + reallocate@withrevert(e, allocations); + + assert e.msg.value != 0 || + !hasAllocatorRole || + msgSenderOnlyEVCAccountOwnerReverted + => lastReverted; +} + + +//Check all the revert conditions of the revokePendingTimelock function. +// Verified + +rule revokePendingTimelockRevertCondition(env e) { + address msgSender = msgSender(e); + bool hasGuardianRole = hasGuardianRole(msgSender); + bool msgSenderOnlyEVCAccountOwnerReverted = msgSenderOnlyEVCAccountOwnerReverted(e); + + revokePendingTimelock@withrevert(e); + + assert lastReverted <=> + e.msg.value != 0 || + !hasGuardianRole || + msgSenderOnlyEVCAccountOwnerReverted; +} + + +//Check all the revert conditions of the revokePendingGuardian function. +// Verified + +rule revokePendingGuardianRevertCondition(env e) { + address msgSender = msgSender(e); + bool hasGuardianRole = hasGuardianRole(msgSender); + bool msgSenderOnlyEVCAccountOwnerReverted = msgSenderOnlyEVCAccountOwnerReverted(e); + + revokePendingGuardian@withrevert(e); + + assert lastReverted <=> + e.msg.value != 0 || + !hasGuardianRole || + msgSenderOnlyEVCAccountOwnerReverted; +} + + +//Check all the revert conditions of the revokePendingCap function. +// Verified + +rule revokePendingCapRevertCondition(env e, address market) { + address msgSender = msgSender(e); + bool hasGuardianRole = hasGuardianRole(msgSender); + bool hasCuratorRole = hasCuratorRole(msgSender); + bool msgSenderOnlyEVCAccountOwnerReverted = msgSenderOnlyEVCAccountOwnerReverted(e); + + revokePendingCap@withrevert(e, market); + + assert lastReverted <=> + e.msg.value != 0 || + !(hasGuardianRole || hasCuratorRole) || + msgSenderOnlyEVCAccountOwnerReverted; +} + + +//Check all the revert conditions of the revokePendingMarketRemoval function. +// Verified + +rule revokePendingMarketRemovalRevertCondition(env e, address market) { + address msgSender = msgSender(e); + bool hasGuardianRole = hasGuardianRole(msgSender); + bool hasCuratorRole = hasCuratorRole(msgSender); + bool msgSenderOnlyEVCAccountOwnerReverted = msgSenderOnlyEVCAccountOwnerReverted(e); + + revokePendingMarketRemoval@withrevert(e, market); + + assert lastReverted <=> + e.msg.value != 0 || + !(hasGuardianRole || hasCuratorRole) || + msgSenderOnlyEVCAccountOwnerReverted; +} + + +//Check all the revert conditions of the acceptTimelock function. +// Verified + +rule acceptTimelockRevertCondition(env e) { + uint256 pendingTimelockValidAt = pendingTimelock_().validAt; + bool msgSenderReverted = msgSenderReverted(e); + + acceptTimelock@withrevert(e); + + assert lastReverted <=> + e.msg.value != 0 || + pendingTimelockValidAt == 0 || + pendingTimelockValidAt > e.block.timestamp || + msgSenderReverted; +} + + +//Check all the revert conditions of the acceptGuardian function. +// Verified + +rule acceptGuardianRevertCondition(env e) { + uint256 pendingGuardianValidAt = pendingGuardian_().validAt; + bool msgSenderReverted = msgSenderReverted(e); + + acceptGuardian@withrevert(e); + + assert lastReverted <=> + e.msg.value != 0 || + pendingGuardianValidAt == 0 || + pendingGuardianValidAt > e.block.timestamp || + msgSenderReverted; +} + + +//Check the input validation conditions under which the acceptCap function reverts. +// This function can also revert if interest accrual reverts or if it would lead to growing the withdraw queue past the max length. +// Verified + +rule acceptCapInputValidation(env e, address market) { + uint256 pendingCapValidAt = pendingCap_(market).validAt; + bool msgSenderReverted = msgSenderReverted(e); + + acceptCap@withrevert(e, market); + + assert e.msg.value != 0 || + pendingCapValidAt == 0 || + pendingCapValidAt > e.block.timestamp || + msgSenderReverted + => lastReverted; +} diff --git a/certora/specs/Roles.spec b/certora/specs/Roles.spec new file mode 100644 index 0000000..6ce2c78 --- /dev/null +++ b/certora/specs/Roles.spec @@ -0,0 +1,139 @@ +// Based on Roles.spec in SiloVault spec + + +methods { + // Only verify the admin functions, not the main entrypoints. + function deposit(uint256, address) external returns(uint256) => NONDET DELETE; + function mint(uint256, address) external returns(uint256) => NONDET DELETE; + function withdraw(uint256, address, address) external returns(uint256) => NONDET DELETE; + function redeem(uint256, address, address) external returns(uint256) => NONDET DELETE; + function transferFrom(address, address, uint256) external returns(bool) => NONDET DELETE; + + function EVC() external returns address envfree; + function owner() external returns(address) envfree; + function pendingOwner() external returns(address) envfree; + function curator() external returns(address) envfree; + function guardian() external returns(address) envfree; + function isAllocator(address target) external returns(bool) envfree; + + function _.deposit(uint256, address) external => CONSTANT; + function _.mint(uint256, address) external => CONSTANT; + function _.withdraw(uint256, address, address) external => CONSTANT; + function _.redeem(uint256, address, address) external => CONSTANT; + function _.convertToAssets(uint256) external => CONSTANT; + function _.approve(address, uint256) external => CONSTANT; + function _.approve(address, address, uint160, uint48) external => CONSTANT; + + function _.previewRedeem(uint256) external => CONSTANT; + function _.transferFrom(address, address, uint256) external => CONSTANT; + function _.asset() external => CONSTANT; + + function allowance(address, address) internal returns(uint256) => CONSTANT; + function ERC20._transfer(address, address, uint256) internal => CONSTANT; + + function _.isStrategyAllowed(address) external => DISPATCHER(true); + function _.permit2Address() external => DISPATCHER(true); + + function _.balanceOf(address) external => CONSTANT; + function SafeERC20.safeTransfer(address, address, uint256) internal => CONSTANT; +} + +// Check that the owner has more power than the guardian. +// Verified +rule ownerIsGuardian(method f, calldataarg args) + filtered { + f -> (!f.isView && f.contract == currentContract) + } +{ + storage initial = lastStorage; + + env e1; env e2; + require e1.block.timestamp == e2.block.timestamp; + require e1.msg.value == e2.msg.value; + + address evc = EVC(); + require e1.msg.sender != 0; + require e2.msg.sender != 0; + + require e1.msg.sender != evc; + require e2.msg.sender != evc; + + require e1.msg.sender == guardian(); + require e1.msg.sender != owner(); + require e1.msg.sender != pendingOwner(); + f@withrevert(e1, args) at initial; + bool revertedGuardian = lastReverted; + + require e2.msg.sender == owner(); + f@withrevert(e2, args) at initial; + bool revertedOwner = lastReverted; + + assert revertedOwner => revertedGuardian; +} + +// Check that the owner has more power than the curator. +// Verified +rule ownerIsCurator(method f, calldataarg args) + filtered { + f -> (!f.isView && f.contract == currentContract) + } +{ + storage initial = lastStorage; + + env e1; env e2; + require e1.block.timestamp == e2.block.timestamp; + require e1.msg.value == e2.msg.value; + + address evc = EVC(); + require e1.msg.sender != 0; + require e2.msg.sender != 0; + + require e1.msg.sender != evc; + require e2.msg.sender != evc; + + require e1.msg.sender == curator(); + require e1.msg.sender != owner(); + require e1.msg.sender != pendingOwner(); + f@withrevert(e1, args) at initial; + bool revertedCurator = lastReverted; + + require e2.msg.sender == owner(); + f@withrevert(e2, args) at initial; + bool revertedOwner = lastReverted; + + assert revertedOwner => revertedCurator; +} + +// Check that the curator has more power than allocators. +// Verified +rule curatorIsAllocator(method f, calldataarg args) + filtered { + f -> (!f.isView && f.contract == currentContract) + } +{ + storage initial = lastStorage; + + env e1; env e2; + require e1.block.timestamp == e2.block.timestamp; + require e1.msg.value == e2.msg.value; + + address evc = EVC(); + require e1.msg.sender != 0; + require e2.msg.sender != 0; + + require e1.msg.sender != evc; + require e2.msg.sender != evc; + + require isAllocator(e1.msg.sender); + require e1.msg.sender != owner(); + require e1.msg.sender != guardian(); + require e1.msg.sender != pendingOwner(); + f@withrevert(e1, args) at initial; + bool revertedAllocator = lastReverted; + + require e2.msg.sender == curator(); + f@withrevert(e2, args) at initial; + bool revertedCurator = lastReverted; + + assert revertedCurator => revertedAllocator; +} \ No newline at end of file diff --git a/certora/specs/SolvencyInternal.spec b/certora/specs/SolvencyInternal.spec new file mode 100644 index 0000000..dbda42e --- /dev/null +++ b/certora/specs/SolvencyInternal.spec @@ -0,0 +1,132 @@ +import "./EulerEarnERC4626.spec"; + +ghost uint256 totalSupplyGhost; +ghost uint256 assetsInGhost; +ghost uint256 totalAssetsAfterWithdrawStrategy; + +methods { + function EulerEarn.HOOK_after_withdrawStrategy(uint256 assets) internal => CVL_after_withdrawStrategy(assets); +} + +// Hook summaries that serve as lemmas for the solvencyInInternalWithdraw rule +// this is only useful if run with multi_assert_check = true +function CVL_after_withdrawStrategy(uint256 assetsIn) { + // There is some bug with the summaries (see ticket -- so I am using asstsInGhost instead of assetsIn input) + + // not sure about these still -- need to think + assert totalSupply() == totalSupplyGhost, + "total supply does not change"; //verified + assert Token0.balanceOf(currentContract) == assetsInGhost, + "after withdraw stategy the assets are moved to Euler"; // verified + uint256 totalAssetsNow = totalAssets(); + assert totalAssetsNow + Token0.balanceOf(currentContract) >= totalSupply(), + "The sum of assets moved to Euler + totalAssets in vaults >= totalSupply"; //verified + totalAssetsAfterWithdrawStrategy = totalAssetsNow; +} + +// Verified https://prover.certora.com/output/5771024/455e0433202940aebcd4aa94b939561e/ +rule propertiesAfterAccrue() { + require totalAssets() >= totalSupply() + fees(); + env e; + _accrueInterest(e); + assert fees() == 0; + assert totalAssets() >= totalSupply() + fees(); +} + +// verified https://prover.certora.com/output/5771024/d1f58762c7934808b936bd1a41fb15d9/ (most revent proof with less approximations) +rule solvencyInInternalWithdraw() { + // simulating the internal _withdraw in a call from the external withdraw + env e; + address caller; + address receiver; + address owner; + uint256 assets; + uint256 shares; + safeAssumptions(e); + + require withdrawQueueLength() == 1; + address withdrawQueueFirstVault = withdrawQGetAt(0); + + require caller != withdrawQueueFirstVault; + require receiver != withdrawQueueFirstVault; + require owner != withdrawQueueFirstVault; + require receiver != currentContract; + require caller != currentContract; + require owner != currentContract; + require currentContract != withdrawQueueFirstVault; + + uint256 totalAssetsPre; + uint256 feesPre; + uint256 lostAssetsPre; + uint256 totalSupplyPre = totalSupply(); + (feesPre,totalAssetsPre,lostAssetsPre) = _accruedFeeAndAssets(e); // 6 non-linear ops + require totalSupplyGhost == totalSupplyPre; + require assetsInGhost == assets; + + uint256 lastTotalAssetsPre = lastTotalAssets(); + require totalAssetsPre >= totalSupplyPre + feesPre, "solvent before"; + require lastTotalAssetsPre == totalAssetsPre, "_withdraw is called after _accrueInterest"; + assert feesPre == 0; // verified + + bool assetSharesRelationInWithdraw = ( shares == _convertToSharesWithTotals(e,assets, totalSupplyPre, lastTotalAssetsPre, Math.Rounding.Ceil) ); // 2 non-linear ops + bool assetSharesRelationInRedeem = ( assets == _convertToAssetsWithTotals(e,shares, totalSupplyPre, lastTotalAssetsPre, Math.Rounding.Floor)); // 2 non-linear ops + require assetSharesRelationInWithdraw || assetSharesRelationInRedeem, + "internal withdraw is called either in the external withdraw or the external redeem"; + + assert shares <= assets; // verified + + _withdraw(e,caller,receiver,owner,assets,shares); // 22 non-linear ops -> cvlDispatchMaxWithdraw - 4, cvlDispatchPreviewRedeem - 4, CVL_after_withdrawStrategy - 6 + + uint256 totalAssetsPost; + uint256 feesPost; + uint256 lostAssetsPost; + uint256 totalSupplyPost = totalSupply(); + (feesPost,totalAssetsPost,lostAssetsPost) = _accruedFeeAndAssets(e); // 6 non-linear ops + uint256 lastTotalAssetsPost = lastTotalAssets(); + + assert totalAssetsPost == totalAssetsAfterWithdrawStrategy; + assert totalSupplyPost == assert_uint256(totalSupplyPre - shares); + assert Token0.balanceOf(currentContract) == 0; + assert lastTotalAssetsPost == assert_uint256(lastTotalAssetsPre - assets); + uint256 totalInterest = assert_uint256(totalAssetsPost-lastTotalAssetsPost); + uint256 feeAssets = cvlMulDiv(totalInterest,fee(), wad()); + assert feeAssets <= totalInterest; + assert assert_uint256(totalAssetsPost-feeAssets) >= totalSupplyPost; + assert require_uint256(assert_uint256(totalAssetsPost-feeAssets)+virtualAmount()) >= require_uint256(totalSupplyPost+virtualAmount()); + assert feesPost <= feeAssets; + assert feesPost <= totalInterest; + assert totalAssetsPost >= totalSupplyPost + feesPost, "solvent after"; +} + + +rule solvencyInInternalDeposit() { + // simulating the internal _deposit in a call from the external deposit + env e; + address caller; + address receiver; + uint256 assets; + uint256 shares; + safeAssumptions(e); + + uint256 totalAssetsPre; + uint256 feesPre; + uint256 lostAssetsPre; + uint256 totalSupplyPre = totalSupply(); + (feesPre,totalAssetsPre,lostAssetsPre) = _accruedFeeAndAssets(e); + + uint256 lastTotalAssetsPre = lastTotalAssets(); + require totalAssetsPre >= totalSupplyPre + feesPre, "solvent before"; + require lastTotalAssetsPre == totalAssetsPre, "_deposit is called after _accrueInterest"; + + require shares == _convertToSharesWithTotals(e,assets, totalSupplyPre, lastTotalAssetsPre, Math.Rounding.Floor); + + _deposit(e,caller,receiver,assets,shares); + + uint256 totalAssetsPost; + uint256 feesPost; + uint256 lostAssetsPost; + uint256 totalSupplyPost = totalSupply(); + (feesPost,totalAssetsPost,lostAssetsPost) = _accruedFeeAndAssets(e); + + assert totalAssetsPost >= totalSupplyPost + feesPost, "solvent after"; +} diff --git a/certora/specs/Timelock.spec b/certora/specs/Timelock.spec new file mode 100644 index 0000000..adde181 --- /dev/null +++ b/certora/specs/Timelock.spec @@ -0,0 +1,203 @@ +// Based on Timelock.spec in SiloVault spec + +import "Enabled.spec"; +using ERC20Helper as ERC20Helper; + +methods { + function ERC20Helper.balanceOf(address token, address user) external returns (uint256) envfree; +} + +persistent ghost uint256 lastTimestamp; + +hook TIMESTAMP uint newTimestamp { + // Safe require because timestamps are guaranteed to be increasing. + require newTimestamp >= lastTimestamp; + // Safe require as it corresponds to some time very far into the future. + require newTimestamp < 2^63; + lastTimestamp = newTimestamp; +} + +// Verified +// Show that nextGuardianUpdateTime does not revert. +rule nextGuardianUpdateTimeDoesNotRevert() { + // The environment e yields the current time. + env e; + require e.msg.value == 0; + + requireInvariant timelockInRange(); + requireInvariant pendingTimelockInRange(); + + nextGuardianUpdateTime@withrevert(e); + + assert !lastReverted; +} + +// Verified +// Show that nextGuardianUpdateTime is increasing with time and that no change of guardian can happen before it. +rule guardianUpdateTime(env e_next, method f, calldataarg args) { + // The environment e yields the current time. + env e; + + requireInvariant timelockInRange(); + + uint256 nextTime = nextGuardianUpdateTime(e); + address prevGuardian = guardian(); + + // Assume that the guardian is already set. + require prevGuardian != 0; + uint256 nextGuardianUpdateTimeBeforeInteraction = nextGuardianUpdateTime(e); + // Increasing nextGuardianUpdateTime with no interaction; + assert nextGuardianUpdateTimeBeforeInteraction >= nextTime; + + f(e_next, args); + + if (e_next.block.timestamp < nextTime) { + // Check that guardian cannot change. + assert guardian() == prevGuardian; + // Increasing nextGuardianUpdateTime with an interaction; + assert nextGuardianUpdateTime(e_next) >= nextGuardianUpdateTimeBeforeInteraction; + } + assert true; +} + +// Verified +// Show that nextCapIncreaseTime does not revert. +rule nextCapIncreaseTimeDoesNotRevert(address id) { + // The environment e yields the current time. + env e; + require e.msg.value == 0; + + requireInvariant timelockInRange(); + requireInvariant pendingTimelockInRange(); + + nextCapIncreaseTime@withrevert(e, id); + + assert !lastReverted; +} + +// Verified +// Show that nextCapIncreaseTime is increasing with time and that no increase of cap can happen before it. +rule capIncreaseTime(env e_next, method f, calldataarg args) { + // The environment e yields the current time. + env e; + + address id; + + requireInvariant timelockInRange(); + + uint256 nextTime = nextCapIncreaseTime(e, id); + uint184 prevCap = config_(id).cap; + + uint256 nextCapIncreaseTimeBeforeInteraction = nextCapIncreaseTime(e_next, id); + // Increasing nextCapIncreaseTime with no interaction; + assert nextCapIncreaseTimeBeforeInteraction >= nextTime; + + f(e_next, args); + + if (e_next.block.timestamp < nextTime) { + // Check that the cap cannot increase. + assert config_(id).cap <= prevCap; + // Increasing nextCapIncreaseTime with an interaction; + assert nextCapIncreaseTime(e_next, id) >= nextCapIncreaseTimeBeforeInteraction; + } + assert true; +} + +// Verified +// Show that nextTimelockDecreaseTime does not revert. +rule nextTimelockDecreaseTimeDoesNotRevert() { + // The environment e yields the current time. + env e; + require e.msg.value == 0; + + requireInvariant timelockInRange(); + requireInvariant pendingTimelockInRange(); + + nextTimelockDecreaseTime@withrevert(e); + + assert !lastReverted; +} + +// Verified +// Show that nextTimelockDecreaseTime is increasing with time and that no decrease of timelock can happen before it. +rule timelockDecreaseTime(env e_next, method f, calldataarg args) { + // The environment e yields the current time. + env e; + requireInvariant timelockInRange(); + + uint256 nextTime = nextTimelockDecreaseTime(e); + uint256 prevTimelock = timelock(); + + uint256 nextTimelockDecreaseTimeBeforeInteraction = nextTimelockDecreaseTime(e_next); + // Increasing nextTimelockDecreaseTime with no interaction; + assert nextTimelockDecreaseTimeBeforeInteraction >= nextTime; + + f(e_next, args); + + if (e_next.block.timestamp < nextTime) { + // Check that timelock cannot decrease. + assert timelock() >= prevTimelock; + // Increasing nextTimelockDecreaseTime with an interaction; + assert nextTimelockDecreaseTime(e_next) >= nextTimelockDecreaseTimeBeforeInteraction; + } + assert true; +} + +// Verified +// Show that nextRemovableTime does not revert. +rule nextRemovableTimeDoesNotRevert(address id) { + // The environment e yields the current time. + env e; + require e.msg.value == 0; + + requireInvariant timelockInRange(); + requireInvariant pendingTimelockInRange(); + + nextRemovableTime@withrevert(e, id); + + assert !lastReverted; +} + +// Verified +// Show that nextRemovableTime is increasing with time and that no removal can happen before it. +rule removableTime(env e_next, method f, calldataarg args) { + // The environment e yields the current time. + env e; + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + address id; + + requireInvariant timelockInRange(); + + uint256 nextTime = nextRemovableTime(e, id); + + // Assume that the market is enabled. + require config_(id).enabled; + uint256 nextRemovableTimeBeforeInteraction = nextRemovableTime(e_next, id); + // Increasing nextRemovableTime with no interaction; + assert nextRemovableTimeBeforeInteraction >= nextTime; + + f(e_next, args); + + if (e_next.block.timestamp < nextTime) { + // Check that no forced removal happened. + // assert ERC20Helper.balanceOf(id,currentContract) => config_(id).enabled; + assert config_(id).balance > 0 => config_(id).enabled; //CHANGED DUE TO FIX + // Increasing nextRemovableTime with an interaction; + assert nextRemovableTime(e_next, id) >= nextRemovableTimeBeforeInteraction; + } + assert true; +} + +// Verified +rule timelockCantGoToZero(env e, method f, calldataarg args) { + requireInvariant pendingTimelockInRange(); + + uint256 timelockBefore = timelock(); + + f(e, args); + uint256 timelockAfter = timelock(); + + assert timelockAfter == 0 => timelockBefore == 0; +} diff --git a/certora/specs/setup/dispatchingWithoutVaultSummaries.spec b/certora/specs/setup/dispatchingWithoutVaultSummaries.spec new file mode 100644 index 0000000..e0e3ead --- /dev/null +++ b/certora/specs/setup/dispatchingWithoutVaultSummaries.spec @@ -0,0 +1,112 @@ +// import "./vaults_summaries_EulerEarn.spec"; +using VaultMock0 as v0; +using VaultMock1 as v1; + +methods { +function _.approve(address,uint256) external => DISPATCHER(true); +function _.approve(address,address,uint160,uint48) external => DISPATCHER(true); +function _.transferFrom(address,address,uint256) external => DISPATCHER(true); +function _.redeem(uint256,address,address) external => DISPATCHER(true); +function _.allowance(address,address) external => DISPATCHER(true); +function _.transfer(address,uint256) external => DISPATCHER(true); +function _.balanceOf(address) external => DISPATCHER(true); +function _.isStrategyAllowed(address) external => DISPATCHER(true); +function _.permit2Address() external => DISPATCHER(true); +function _.getCurrentOnBehalfOfAccount(address) external => DISPATCHER(true); + +// ERC4626 methods that are implemented in EulerEarn, but we mean to dispatch to the vaults when they're called within it +function _.previewRedeem(uint256 shares) external with (env e) => cvlDispatchPreviewRedeem(shares, calledContract, e) expect uint256; +function _.maxWithdraw(address owner) external with (env e) => cvlDispatchMaxWithdraw(owner, calledContract, e) expect uint256; +function _.withdraw(uint256 assets, address receiver, address owner) external with (env e) + => cvlDispatchWithdraw(assets, receiver, owner, calledContract, e) expect uint256; +function _.asset() external with (env e) => cvlDispatchAsset(calledContract, e) expect address; +function _.maxDeposit(address owner) external with (env e) => cvlDispatchMaxDeposit(owner, calledContract, e) expect uint256; +function _.deposit(uint256 assets, address receiver) external with (env e) + => cvlDispatchDeposit(assets, receiver, calledContract, e) expect uint256; +function _.totalSupply() external with (env e) => cvlDispathTotalSupply(calledContract,e) expect uint256; + +function _.checkVaultStatus() external => NONDET; +function _.checkAccountStatus(address, address[]) external => NONDET; + +// might want to summarize this to something more deterministic if the asset decimals are relevant to the rules +function _._tryGetAssetDecimals(address) internal => NONDET; +} + +function cvlDispatchPreviewRedeem(uint256 shares, address called, env e) returns uint256 { + if(called == v0) { + return v0.previewRedeem(e, shares); + } + if(called == v1) { + return v1.previewRedeem(e, shares); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchMaxWithdraw(address owner, address called, env e) returns uint256 { + if(called == v0) { + return v0.maxWithdraw(e, owner); + } + if(called == v1) { + return v1.maxWithdraw(e, owner); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + + + +function cvlDispatchWithdraw(uint256 assets, address receiver, address owner, address called, env e) returns uint256 { + if(called == v0) { + return v0.withdraw(e, assets, receiver, owner); + } + if(called == v1) { + return v1.withdraw(e, assets, receiver, owner); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchAsset(address called, env e) returns address { + if(called == v0) { + return v0.asset(e); + } + if(called == v1) { + return v1.asset(e); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchMaxDeposit(address owner, address called, env e) returns uint256 { + if(called == v0) { + return v0.maxDeposit(e, owner); + } + if(called == v1) { + return v1.maxDeposit(e, owner); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchDeposit(uint256 assets, address receiver, address called, env e) returns uint256 { + if(called == v0) { + return v0.deposit(e, assets, receiver); + } + if(called == v1) { + return v1.deposit(e, assets, receiver); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispathTotalSupply(address called, env e) returns uint256 { + if(called == v0) { + return v0.totalSupply(e); + } + if(called == v1) { + return v1.totalSupply(e); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} \ No newline at end of file diff --git a/certora/specs/setup/dispatching_EulerEarn.spec b/certora/specs/setup/dispatching_EulerEarn.spec new file mode 100644 index 0000000..4e94e3a --- /dev/null +++ b/certora/specs/setup/dispatching_EulerEarn.spec @@ -0,0 +1,110 @@ +import "./vaults_summaries_EulerEarn.spec"; + +methods { +function _.approve(address,uint256) external => DISPATCHER(true); +function _.approve(address,address,uint160,uint48) external => DISPATCHER(true); +function _.transferFrom(address,address,uint256) external => DISPATCHER(true); +function _.redeem(uint256,address,address) external => DISPATCHER(true); +function _.allowance(address,address) external => DISPATCHER(true); +function _.transfer(address,uint256) external => DISPATCHER(true); +function _.balanceOf(address) external => DISPATCHER(true); +function _.isStrategyAllowed(address) external => DISPATCHER(true); +function _.permit2Address() external => DISPATCHER(true); +function _.getCurrentOnBehalfOfAccount(address) external => DISPATCHER(true); + +// ERC4626 methods that are implemented in EulerEarn, but we mean to dispatch to the vaults when they're called within it +function _.previewRedeem(uint256 shares) external with (env e) => cvlDispatchPreviewRedeem(shares, calledContract, e) expect uint256; +function _.maxWithdraw(address owner) external with (env e) => cvlDispatchMaxWithdraw(owner, calledContract, e) expect uint256; +function _.withdraw(uint256 assets, address receiver, address owner) external with (env e) + => cvlDispatchWithdraw(assets, receiver, owner, calledContract, e) expect uint256; +function _.asset() external with (env e) => cvlDispatchAsset(calledContract, e) expect address; +function _.maxDeposit(address owner) external with (env e) => cvlDispatchMaxDeposit(owner, calledContract, e) expect uint256; +function _.deposit(uint256 assets, address receiver) external with (env e) + => cvlDispatchDeposit(assets, receiver, calledContract, e) expect uint256; +function _.totalSupply() external with (env e) => cvlDispathTotalSupply(calledContract,e) expect uint256; + +function _.checkVaultStatus() external => NONDET; +function _.checkAccountStatus(address, address[]) external => NONDET; + +// might want to summarize this to something more deterministic if the asset decimals are relevant to the rules +function _._tryGetAssetDecimals(address) internal => NONDET; +} + +function cvlDispatchPreviewRedeem(uint256 shares, address called, env e) returns uint256 { + if(called == v0) { + return v0.previewRedeem(e, shares); + } + if(called == v1) { + return v1.previewRedeem(e, shares); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchMaxWithdraw(address owner, address called, env e) returns uint256 { + if(called == v0) { + return v0.maxWithdraw(e, owner); + } + if(called == v1) { + return v1.maxWithdraw(e, owner); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + + + +function cvlDispatchWithdraw(uint256 assets, address receiver, address owner, address called, env e) returns uint256 { + if(called == v0) { + return v0.withdraw(e, assets, receiver, owner); + } + if(called == v1) { + return v1.withdraw(e, assets, receiver, owner); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchAsset(address called, env e) returns address { + if(called == v0) { + return v0.asset(e); + } + if(called == v1) { + return v1.asset(e); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchMaxDeposit(address owner, address called, env e) returns uint256 { + if(called == v0) { + return v0.maxDeposit(e, owner); + } + if(called == v1) { + return v1.maxDeposit(e, owner); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispatchDeposit(uint256 assets, address receiver, address called, env e) returns uint256 { + if(called == v0) { + return v0.deposit(e, assets, receiver); + } + if(called == v1) { + return v1.deposit(e, assets, receiver); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} + +function cvlDispathTotalSupply(address called, env e) returns uint256 { + if(called == v0) { + return v0.totalSupply(e); + } + if(called == v1) { + return v1.totalSupply(e); + } + require false, "We assume external calls to ERC4626 methods are always on one of the vaults"; + return 0; +} \ No newline at end of file diff --git a/certora/specs/setup/sanity_EulerEarn.spec b/certora/specs/setup/sanity_EulerEarn.spec new file mode 100644 index 0000000..5e88277 --- /dev/null +++ b/certora/specs/setup/sanity_EulerEarn.spec @@ -0,0 +1,8 @@ +import "dispatching_EulerEarn.spec"; + +methods { +} + +use builtin rule sanity filtered { f -> f.contract == currentContract +&& f.selector != sig:multicall(bytes[]).selector +} diff --git a/certora/specs/setup/vaults_summaries_EulerEarn.spec b/certora/specs/setup/vaults_summaries_EulerEarn.spec new file mode 100644 index 0000000..7ec898e --- /dev/null +++ b/certora/specs/setup/vaults_summaries_EulerEarn.spec @@ -0,0 +1,71 @@ +import "../ERC4626/specs/ERC4626.spec"; +using VaultMock0 as v0; +using VaultMock1 as v1; + +methods { + function v0.convertToAssets(uint256 shares, Math.Rounding rounding) external returns (uint256) => + convertToAssetsCVL(calledContract, shares, rounding); + + function v0.convertToShares(uint256 assets, Math.Rounding rounding) external returns (uint256) => + convertToSharesCVL(calledContract, assets, rounding); + + function v0.previewRedeem(uint256 shares) internal returns (uint256) => + previewRedeemCVL(calledContract, shares); + + function v0.previewMint(uint256 shares) internal returns (uint256) => + previewMintCVL(calledContract, shares); + + function v0.previewWithdraw(uint256 assets) internal returns (uint256) => + previewWithdrawCVL(calledContract, assets); + + function v0.asset() internal returns (address) => + ERC4626Asset(calledContract); + + function v0.maxDeposit(address owner) internal returns (uint256) => + maxDepositCVL(calledContract, owner); + + function v0.maxWithdraw(address owner) internal returns (uint256) => + maxWithdrawCVL(calledContract, owner); + + function v0.deposit(uint256 assets, address receiver) internal returns (uint256) with (env e) => + depositCVL(calledContract, e.block.timestamp, e.msg.sender, assets, receiver); + + function v0.withdraw(uint256 assets, address receiver, address owner) internal returns (uint256) with (env e) => + withdrawCVL(calledContract, e.block.timestamp, e.msg.sender, assets, receiver, owner); + + function v0.decimals() internal returns (uint8) => + decimalsCVL(calledContract); + + function v1.convertToAssets(uint256 shares, Math.Rounding rounding) external returns (uint256) => + convertToAssetsCVL(calledContract, shares, rounding); + + function v1.convertToShares(uint256 assets, Math.Rounding rounding) external returns (uint256) => + convertToSharesCVL(calledContract, assets, rounding); + + function v1.previewRedeem(uint256 shares) internal returns (uint256) => + previewRedeemCVL(calledContract, shares); + + function v1.previewMint(uint256 shares) internal returns (uint256) => + previewMintCVL(calledContract, shares); + + function v1.previewWithdraw(uint256 assets) internal returns (uint256) => + previewWithdrawCVL(calledContract, assets); + + function v1.asset() internal returns (address) => + ERC4626Asset(calledContract); + + function v1.maxDeposit(address owner) internal returns (uint256) => + maxDepositCVL(calledContract, owner); + + function v1.maxWithdraw(address owner) internal returns (uint256) => + maxWithdrawCVL(calledContract, owner); + + function v1.deposit(uint256 assets, address receiver) internal returns (uint256) with (env e) => + depositCVL(calledContract, e.block.timestamp, e.msg.sender, assets, receiver); + + function v1.withdraw(uint256 assets, address receiver, address owner) internal returns (uint256) with (env e) => + withdrawCVL(calledContract, e.block.timestamp, e.msg.sender, assets, receiver, owner); + + function v1.decimals() internal returns (uint8) => + decimalsCVL(calledContract); +} \ No newline at end of file diff --git a/certora/specs/summaries/Math.spec b/certora/specs/summaries/Math.spec new file mode 100644 index 0000000..5b21fb6 --- /dev/null +++ b/certora/specs/summaries/Math.spec @@ -0,0 +1,61 @@ +methods { + function _.mulDiv(uint256 x, uint256 y, uint256 denominator) internal => cvlMulDiv(x, y, denominator) expect uint256; + function _.mulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) internal => cvlMulDivWithRounding(x, y, denominator, rounding) expect uint256; + function _.sqrt(uint256 a) internal => cvlSqrt(a) expect uint256; + function _.average(uint256 a, uint256 b) internal => cvlAverage(a, b) expect uint256; + function _.ternary(bool condition, uint256 a, uint256 b) internal => cvlTernary(condition, a, b) expect uint256; + function _.zeroFloorSub(uint256 x, uint256 y) internal => cvlZeroFloorSub(x, y) expect (uint256); + function _.exactlyOneZero(uint256 x, uint256 y) internal => cvlExactlyOneZero(x,y) expect bool; + function _.min(uint256 x, uint256 y) internal => cvlMin(x,y) expect uint256; +} + +function cvlExactlyOneZero(uint256 x, uint256 y) returns bool { + return (x == 0 && y != 0) || (x != 0 && y == 0); +} + +function cvlMin(uint256 x, uint256 y) returns uint256 { + return x < y ? x : y; +} + +function cvlZeroFloorSub(uint256 x, uint256 y) returns uint256 { + if (x > y) return require_uint256(x - y); + else return 0; +} + +function cvlMulDiv(uint256 x, uint256 y, uint256 denominator) returns uint256 { + require denominator > 0; + mathint res = x * y / denominator; + return require_uint256(res); +} + +function cvlMulDivWithRounding(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256 +{ + require denominator > 0; + if (rounding == Math.Rounding.Ceil) { + return require_uint256((x * y + denominator - 1) / denominator); + } + if (rounding == Math.Rounding.Floor) { + return require_uint256((x * y) / denominator); + } + else { + assert false; //add other branches if different rounding type is used + return 0; + } +} + +function cvlSqrt(uint256 a) returns uint256 { + mathint a_mathint = to_mathint(a); + uint256 sqrt_a; + require + sqrt_a * sqrt_a <= a_mathint && + (sqrt_a + 1) * (sqrt_a + 1) > a_mathint; + return sqrt_a; +} + +function cvlAverage(uint256 a, uint256 b) returns uint256 { + return require_uint256((a + b) / 2); +} + +function cvlTernary(bool condition, uint256 a, uint256 b) returns uint256 { + return condition ? a : b; +} \ No newline at end of file