diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000..1e7971d --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,107 @@ +# A workflow file for running Certora verification through github actions. +# Find results for each push in the "Actions" tab on the github website. +name: Certora verification + +on: + push: {} + pull_request: {} + workflow_dispatch: {} + +jobs: + verify: + runs-on: ubuntu-latest + steps: + # check out the current version + - uses: actions/checkout@v2 + + # install Certora dependencies and CLI + - name: Install python + uses: actions/setup-python@v2 + with: + python-version: '3.10' + # cache: 'pip' + - name: Install certora + run: pip3 install certora-cli + + # the following is only necessary if your project depends on contracts + # installed using yarn + # - name: Install yarn + # uses: actions/setup-node@v3 + # with: + # node-version: 16 + # cache: 'yarn' + # - name: Install dependencies + # run: yarn + + # Install the appropriate version of solc + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.0/solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.0 + chmod +x /usr/local/bin/solc8.0 + + wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.20 + chmod +x /usr/local/bin/solc8.20 + + # Do the actual verification. The `run` field could be simply + # + # certoraRun certora/conf/${{ matrix.params }} + # + # but we do a little extra work to get the commit messages into the + # `--msg` argument to `certoraRun` + # + # Here ${{ matrix.params }} gets replaced with each of the parameters + # listed in the `params` section below. + - name: Verify rule ${{ matrix.params.name }} + run: > + message="$(git log -n 1 --pretty=format:'CI ${{matrix.params.name}} %h .... %s')"; + cd lesson4_reading/erc4626/ && certoraRun \ + ${{ matrix.params.command }} \ + --msg "$(echo $message | sed 's/[^a-zA-Z0-9., _-]/ /g')" + env: + # For this to work, you must set your CERTORAKEY secret on the github + # website (settings > secrets > actions > new repository secret) + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + # The following two steps save the output json as a github artifact. + # This can be useful for automation that collects the output. + - name: Download output json + if: always() + run: > + outputLink=$(sed 's/zipOutput/output/g' .zip-output-url.txt | sed 's/?/\/output.json?/g'); + curl -L -b "certoraKey=$CERTORAKEY;" ${outputLink} --output output.json || true; + touch output.json; + + - name: Archive output json + if: always() + uses: actions/upload-artifact@v3 + with: + name: output for ${{ matrix.params.name }} + path: output.json + + strategy: + fail-fast: false + max-parallel: 4 + matrix: + params: + # each of these commands is passed to the "Verify rule" step above, + # which runs certoraRun on certora/conf/ + # + # Note that each of these lines will appear as a separate run on + # prover.certora.com + # + # It is often helpful to split up by rule or even by method for a + # parametric rule, although it is certainly possible to run everything + # at once by not passing the `--rule` or `--method` options + #- {name: transferSpec, command: 'ERC20.conf --rule transferSpec'} + #- {name: generalRulesOnERC20, command: 'generalRules_ERC20.conf --debug'} + #- {name: generalRulesOnVAULT, command: 'generalRules_VAULT.conf --debug'} + - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-FunctionalAccountingProps.conf'} + - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-MonotonicityInvariant.conf'} + - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-MustNotRevertProps.conf'} + - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-RedeemUsingApprovalProps.conf'} + - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-RoundingProps.conf'} + - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-SecurityProps.conf'} + + diff --git a/.gitignore b/.gitignore index 3c3c63f..688e55e 100644 --- a/.gitignore +++ b/.gitignore @@ -11,3 +11,5 @@ # vim .*.swp .*.swo + +emv-* diff --git a/lesson4_reading/erc4626/doIt.sh b/lesson4_reading/erc4626/doIt.sh new file mode 100755 index 0000000..5d3b8b1 --- /dev/null +++ b/lesson4_reading/erc4626/doIt.sh @@ -0,0 +1,10 @@ +echo -e "\n\n\n########### New execution ##########\n\n\n" >> results.out +echo -e "\n\n\n########### Started on $(date) ##########\n\n\n" >> results.out +git rev-parse HEAD >> results.out +git status --short >> results.out +for file in ./src/certora/conf-openzeppelin/*.conf +do + echo -e "\n\n\n" >> results.out + echo -e "Results for $file can be found at:" >> results.out + certoraRun "$file" >> results.out +done \ No newline at end of file diff --git a/lesson4_reading/erc4626/gitCertoraRun.sh b/lesson4_reading/erc4626/gitCertoraRun.sh new file mode 100755 index 0000000..a78b45f --- /dev/null +++ b/lesson4_reading/erc4626/gitCertoraRun.sh @@ -0,0 +1,13 @@ +certoraOutput=$(certoraRun "$@") + +echo "$certoraOutput" + +if [[ ${certoraOutput} != *"ERROR"* ]];then + + certoraURL=$(echo $certoraOutput | sed -n 's/.*\(https:\/\/prover.certora.com\/output\/\)/\1/p') + + git add -A + + git commit -m "Results for run: $certoraURL with arguments $@" + echo $certoraURL +fi \ No newline at end of file diff --git a/lesson4_reading/erc4626/results.out b/lesson4_reading/erc4626/results.out new file mode 100644 index 0000000..9505da1 --- /dev/null +++ b/lesson4_reading/erc4626/results.out @@ -0,0 +1,299 @@ +-e + + +########### New execution ########## + + + +-e + + +########### Started on Wed Sep 13 11:52:43 CEST 2023 ########## + + + +c811e4c9a971ccf4d2901e633b8b122b44a280d0 +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-FunctionalAccountingProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/589b802bed9447f99cece7c32e71a41a?anonymousKey=2262cba1db3ee5c1bf0b4173094f0e68397a569b +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-InflationAttack.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/6b07f818e8cb45c684dc26a641db900a?anonymousKey=a5bee64bcf1b9a84dd8a2edcd37cd827c451abb0 +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-MonotonicityInvariant.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/0a010c866c1e45a58c7e026bbc86fdcd?anonymousKey=754ccffdf7256cb161fe3020e4439c17aec40235 +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-MustNotRevertProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/fa11af735c9e405b9da26f577be17a27?anonymousKey=88b2dbbe94f5f8d83f22c09b4307e43a4e4ac3dc +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-OZ-Modular.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +ERROR: Failed to compile spec file in /Users/johannesspath/Documents/Git/tutorials-code/lesson4_reading/erc4626/.certora_internal/23_09_13_11_53_11_441 +CRITICAL: Found errors +CRITICAL: [main] ERROR ALWAYS - Error in spec file (ERC4626-MonotonicityInvariant.spec:8:5): External method declaration for ERC20Mock.totalAssets() returns (uint256) does not correspond to any known declaration. Did you mean to add optional? +CRITICAL: [main] ERROR ALWAYS - Error in spec file (ERC4626-MonotonicityInvariant.spec:9:5): External method declaration for ERC20Mock.previewMint(uint256) returns (uint256) does not correspond to any known declaration. Did you mean to add optional? +CRITICAL: [main] ERROR ALWAYS - Error in spec file (ERC4626-MonotonicityInvariant.spec:10:5): External method declaration for ERC20Mock.previewWithdraw(uint256) returns (uint256) does not correspond to any known declaration. Did you mean to add optional? +CRITICAL: [main] ERROR ALWAYS - Error in spec file (ERC4626-MonotonicityInvariant.spec:11:5): External method declaration for ERC20Mock.previewDeposit(uint256) returns (uint256) does not correspond to any known declaration. Did you mean to add optional? +CRITICAL: [main] ERROR ALWAYS - Error in spec file (ERC4626-MonotonicityInvariant.spec:12:5): External method declaration for ERC20Mock.previewRedeem(uint256) returns (uint256) does not correspond to any known declaration. Did you mean to add optional? +CRITICAL: Encountered an error running Certora Prover: +CVL specification syntax and type check failed +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-RedeemUsingApprovalProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +CRITICAL: Encountered an error running Certora Prover: +/Users/johannesspath/Documents/Git/CVT-Executables-Mac/solc8.0 had an error: +ParserError: Source file requires different compiler version (current compiler is 0.8.0+commit.c7dfd78e.Darwin.appleclang) - note that nightly builds are considered to be strictly less than the released version + --> /Users/johannesspath/Documents/Git/tutorials-code/lesson4_reading/erc4626/src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol:2:1: + | +2 | pragma solidity ^0.8.20; + | ^^^^^^^^^^^^^^^^^^^^^^^^ + + +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-RoundingProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/29948ba728864a2b93b3d6812aa10d2d?anonymousKey=375a4cae866ffca3428f7ab4cf7470b4ed9c24b7 +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-SecurityProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/e9377ba043224b559c83d3f52d1114f5?anonymousKey=a548d58ad295e43982dc7fc3ecc70020db8b3e40 +-e + + +########### New execution ########## + + + +-e + + +########### Started on Wed Sep 13 12:00:23 CEST 2023 ########## + + + +c811e4c9a971ccf4d2901e633b8b122b44a280d0 +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-FunctionalAccountingProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/f44d98f7305f435797b931b57396c735?anonymousKey=b3e9cebeb330d1e5959d36848201f73b19fb5c5c +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-InflationAttack.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/745442ce1b9442aca9a15f0e3cde02e0?anonymousKey=817ecf59c8c7d23f9f111156957d9311beed67d5 +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-MonotonicityInvariant.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/1e1631c22fea44e49dc7bd6cf1e4b5cf?anonymousKey=a21f4188243af37140fddc1c7dcb41ed3da3029d +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-MustNotRevertProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/5ef8c739d82a4442a4c03b17bcca8e90?anonymousKey=84b13caf75cbdab928207f495a29e1a7c9a9df03 +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-RedeemUsingApprovalProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/8a1bb2ec704d4327abfb6f91f5e4fab2?anonymousKey=6341584b2bad4b2f78933381a1fdd813a4ff9456 +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-RoundingProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/d84eb38292ff457fb97fb695fe2d8156?anonymousKey=6f5a93f867b930e40e2cb2ee515fc7f8bec9aa44 +-e + + + +-e Results for ./src/certora/conf-openzeppelin/certoraRun-SecurityProps.conf can be found at: +WARNING: Default package file package.json not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +WARNING: Default package file remappings.txt not found, external contract dependencies could be unresolved. Ignore if solc invocation was successful +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC20Mock.sol to expose internal function information... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol... +Compiling src/openzeppelin-9ef69c0/contracts/mocks/token/ERC4626Mock.sol to expose internal function information... + +Connecting to server... + +Job submitted to server + +Follow your job at https://prover.certora.com +Once the job is completed, the results will be available at https://prover.certora.com/output/53900/3d3ae3662478429eacd8eb58a203271a?anonymousKey=a6b78821c940f3c410ef8eaeee865dd347510705 diff --git a/lesson4_reading/erc4626/src/ERC4626.sol b/lesson4_reading/erc4626/src/ERC4626.sol new file mode 100644 index 0000000..cd62a31 --- /dev/null +++ b/lesson4_reading/erc4626/src/ERC4626.sol @@ -0,0 +1,180 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +import {ERC20} from "./tokens/ERC20.sol"; +import {SafeTransferLib} from "./libs/SafeTransferLib.sol"; +import {FixedPointMathLib} from "./libs/FixedPointMathLib.sol"; + +/// @notice Minimal ERC4626 tokenized Vault implementation. +/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/mixins/ERC4626.sol) +/// @dev This contract implements the `totalAssets()` function by simply +/// returning the contract's balance. +/// @notice This contract is open to an attack where the first depositor +/// can steal all the other users' funds. +/// This can be done by front-running the deposit transaction and +/// transferring enough tokens to zero the shares calculation. +contract ERC4626 is ERC20 { + using SafeTransferLib for ERC20; + using FixedPointMathLib for uint256; + + // EVENTS + + event Deposit(address indexed caller, address indexed owner, uint256 assets, uint256 shares); + + event Withdraw( + address indexed caller, + address indexed receiver, + address indexed owner, + uint256 assets, + uint256 shares + ); + + // IMMUTABLES + + ERC20 public immutable asset; + + constructor( + ERC20 _asset, + string memory _name, + string memory _symbol + ) ERC20(_name, _symbol, _asset.decimals()) { + asset = _asset; + } + + // DEPOSIT/WITHDRAWAL LOGIC + + function deposit(uint256 assets, address receiver) public virtual returns (uint256 shares) { + // Check for rounding error since we round down in previewDeposit. + require((shares = previewDeposit(assets)) != 0, "ZERO_SHARES"); + + // Need to transfer before minting or ERC777s could reenter. + asset.safeTransferFrom(msg.sender, address(this), assets); + + _mint(receiver, shares); + + emit Deposit(msg.sender, receiver, assets, shares); + + afterDeposit(assets, shares); + } + + function mint(uint256 shares, address receiver) public virtual returns (uint256 assets) { + assets = previewMint(shares); // No need to check for rounding error, previewMint rounds up. + + // Need to transfer before minting or ERC777s could reenter. + asset.safeTransferFrom(msg.sender, address(this), assets); + + _mint(receiver, shares); + + emit Deposit(msg.sender, receiver, assets, shares); + + afterDeposit(assets, shares); + } + + function withdraw( + uint256 assets, + address receiver, + address owner + ) public virtual returns (uint256 shares) { + shares = previewWithdraw(assets); // No need to check for rounding error, previewWithdraw rounds up. + + if (msg.sender != owner) { + uint256 allowed = allowance[owner][msg.sender]; // Saves gas for limited approvals. + + if (allowed != type(uint256).max) allowance[owner][msg.sender] = allowed - shares; + } + + beforeWithdraw(assets, shares); + + _burn(owner, shares); + + emit Withdraw(msg.sender, receiver, owner, assets, shares); + + asset.safeTransfer(receiver, assets); + } + + function redeem( + uint256 shares, + address receiver, + address owner + ) public virtual returns (uint256 assets) { + if (msg.sender != owner) { + uint256 allowed = allowance[owner][msg.sender]; // Saves gas for limited approvals. + + if (allowed != type(uint256).max) allowance[owner][msg.sender] = allowed - shares; + } + + // Check for rounding error since we round down in previewRedeem. + require((assets = previewRedeem(shares)) != 0, "ZERO_ASSETS"); + + beforeWithdraw(assets, shares); + + _burn(owner, shares); + + emit Withdraw(msg.sender, receiver, owner, assets, shares); + + asset.safeTransfer(receiver, assets); + } + + // ACCOUNTING LOGIC + + function totalAssets() public view returns (uint256) { + return asset.balanceOf(address(this)); + } + + function convertToShares(uint256 assets) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? assets : assets.mulDivDown(supply, totalAssets()); + } + + function convertToAssets(uint256 shares) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? shares : shares.mulDivDown(totalAssets(), supply); + } + + function previewDeposit(uint256 assets) public view virtual returns (uint256) { + return convertToShares(assets); + } + + function previewMint(uint256 shares) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? shares : shares.mulDivUp(totalAssets(), supply); + } + + function previewWithdraw(uint256 assets) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? assets : assets.mulDivUp(supply, totalAssets()); + } + + function previewRedeem(uint256 shares) public view virtual returns (uint256) { + return convertToAssets(shares); + } + + // DEPOSIT/WITHDRAWAL LIMIT LOGIC + + function maxDeposit(address) public view virtual returns (uint256) { + return type(uint256).max; + } + + function maxMint(address) public view virtual returns (uint256) { + return type(uint256).max; + } + + function maxWithdraw(address owner) public view virtual returns (uint256) { + return convertToAssets(balanceOf[owner]); + } + + function maxRedeem(address owner) public view virtual returns (uint256) { + return balanceOf[owner]; + } + + // INTERNAL HOOKS LOGIC + + function beforeWithdraw(uint256 assets, uint256 shares) internal virtual {} + + function afterDeposit(uint256 assets, uint256 shares) internal virtual {} + +} diff --git a/lesson4_reading/erc4626/src/ERC4626InflationAttack.sol b/lesson4_reading/erc4626/src/ERC4626InflationAttack.sol new file mode 100644 index 0000000..226e2e8 --- /dev/null +++ b/lesson4_reading/erc4626/src/ERC4626InflationAttack.sol @@ -0,0 +1,189 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +import {ERC20} from "./tokens/ERC20.sol"; +import {SafeTransferLib} from "./libs/SafeTransferLib.sol"; +import {FixedPointMathLib} from "./libs/FixedPointMathLib.sol"; + +/// @notice Minimal ERC4626 tokenized Vault implementation. +/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/mixins/ERC4626.sol) +/// @dev This contract implements the `totalAssets()` function by simply +/// returning the contract's balance. +/// @notice This contract is open to an attack where the first depositor +/// can steal all the other users' funds. +/// This can be done by front-running the deposit transaction and +/// transferring enough tokens to zero the shares calculation. +contract ERC4626InflationAttack is ERC20 { + using SafeTransferLib for ERC20; + using FixedPointMathLib for uint256; + + // EVENTS + + event Deposit(address indexed caller, address indexed owner, uint256 assets, uint256 shares); + + event Withdraw( + address indexed caller, + address indexed receiver, + address indexed owner, + uint256 assets, + uint256 shares + ); + + // IMMUTABLES + + ERC20 public immutable asset; + + constructor( + ERC20 _asset, + string memory _name, + string memory _symbol + ) ERC20(_name, _symbol, _asset.decimals()) { + asset = _asset; + } + + // DEPOSIT/WITHDRAWAL LOGIC + + function deposit(uint256 assets, address receiver) public virtual returns (uint256 shares) { + // Check for rounding error since we round down in previewDeposit. + //Commented out to make the contract vulnerable to inflation attack + + //Added minimal change required for the InflationAttack to work. + //require((shares = previewDeposit(assets)) != 0, "ZERO_SHARES"); + shares = previewDeposit(assets); + + // Need to transfer before minting or ERC777s could reenter. + asset.safeTransferFrom(msg.sender, address(this), assets); + + _mint(receiver, shares); + + emit Deposit(msg.sender, receiver, assets, shares); + + afterDeposit(assets, shares); + } + + function mint(uint256 shares, address receiver) public virtual returns (uint256 assets) { + assets = previewMint(shares); // No need to check for rounding error, previewMint rounds up. + + // Need to transfer before minting or ERC777s could reenter. + asset.safeTransferFrom(msg.sender, address(this), assets); + + _mint(receiver, shares); + + emit Deposit(msg.sender, receiver, assets, shares); + + afterDeposit(assets, shares); + } + + function withdraw( + uint256 assets, + address receiver, + address owner + ) public virtual returns (uint256 shares) { + shares = previewWithdraw(assets); // No need to check for rounding error, previewWithdraw rounds up. + + if (msg.sender != owner) { + uint256 allowed = allowance[owner][msg.sender]; // Saves gas for limited approvals. + + if (allowed != type(uint256).max) allowance[owner][msg.sender] = allowed - shares; + } + + beforeWithdraw(assets, shares); + + _burn(owner, shares); + + emit Withdraw(msg.sender, receiver, owner, assets, shares); + + asset.safeTransfer(receiver, assets); + } + + function redeem( + uint256 shares, + address receiver, + address owner + ) public virtual returns (uint256 assets) { + if (msg.sender != owner) { + uint256 allowed = allowance[owner][msg.sender]; // Saves gas for limited approvals. + + if (allowed != type(uint256).max) allowance[owner][msg.sender] = allowed - shares; + } + + // Check for rounding error since we round down in previewRedeem. + require((assets = previewRedeem(shares)) != 0, "ZERO_ASSETS"); + //Don't check for rounding errors to allow inflation attack. + + beforeWithdraw(assets, shares); + + _burn(owner, shares); + + emit Withdraw(msg.sender, receiver, owner, assets, shares); + + asset.safeTransfer(receiver, assets); + } + + // ACCOUNTING LOGIC + + function totalAssets() public view returns (uint256) { + return asset.balanceOf(address(this)); + } + + function convertToShares(uint256 assets) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? assets : assets.mulDivDown(supply, totalAssets()); + } + + function convertToAssets(uint256 shares) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? shares : shares.mulDivDown(totalAssets(), supply); + } + + function previewDeposit(uint256 assets) public view virtual returns (uint256) { + return convertToShares(assets); + } + + function previewMint(uint256 shares) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? shares : shares.mulDivUp(totalAssets(), supply); + } + + function previewWithdraw(uint256 assets) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? assets : assets.mulDivUp(supply, totalAssets()); + } + + function previewRedeem(uint256 shares) public view virtual returns (uint256) { + return convertToAssets(shares); + } + + // DEPOSIT/WITHDRAWAL LIMIT LOGIC + + function maxDeposit(address) public view virtual returns (uint256) { + return type(uint256).max; + } + + function maxMint(address) public view virtual returns (uint256) { + return type(uint256).max; + } + + function maxWithdraw(address owner) public view virtual returns (uint256) { + return convertToAssets(balanceOf[owner]); + } + + function maxRedeem(address owner) public view virtual returns (uint256) { + return balanceOf[owner]; + } + + // INTERNAL HOOKS LOGIC + + function beforeWithdraw(uint256 assets, uint256 shares) internal virtual {} + + function afterDeposit(uint256 assets, uint256 shares) internal virtual {} + + //Logic added for Certora Prover. TODO remove as cleanup of specs/ERC4626-FunctionalAccountingProps.spec. + function getUserBalance(address addr) external view returns (uint256) { + return address(addr).balance; + } +} diff --git a/lesson4_reading/erc4626/src/certora/conf/certoraRun-FunctionalAccountingProps.conf b/lesson4_reading/erc4626/src/certora/conf/certoraRun-FunctionalAccountingProps.conf new file mode 100644 index 0000000..e0552bb --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/conf/certoraRun-FunctionalAccountingProps.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "src/ERC4626.sol", + "src/tokens/ERC20.sol", + ], + "verify": "ERC4626:src/certora/specs/ERC4626-FunctionalAccountingProps.spec", + "link": ["ERC4626:asset=ERC20"], + "solc": "solc8.0", + "server": "production", + "send_only": true, + "rule_sanity": "basic", + "msg": "Verification of ERC4626", + "optimistic_loop": true, +} \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/certora/conf/certoraRun-InflationAttack.conf b/lesson4_reading/erc4626/src/certora/conf/certoraRun-InflationAttack.conf new file mode 100644 index 0000000..e3e9ae5 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/conf/certoraRun-InflationAttack.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "src/ERC4626InflationAttack.sol", + "src/tokens/ERC20.sol", + ], + "verify": "ERC4626InflationAttack:src/certora/specs/ERC4626-InflationAttack.spec", + "link": ["ERC4626InflationAttack:asset=ERC20"], + "solc": "solc8.0", + "server": "production", + "send_only": true, + "rule_sanity": "basic", + "msg": "Verification of ERC4626", + "optimistic_loop": true, +} \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/certora/conf/certoraRun-MonotonicityInvariant.conf b/lesson4_reading/erc4626/src/certora/conf/certoraRun-MonotonicityInvariant.conf new file mode 100644 index 0000000..387d479 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/conf/certoraRun-MonotonicityInvariant.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "src/ERC4626.sol", + "src/tokens/ERC20.sol", + ], + "verify": "ERC4626:src/certora/specs/ERC4626-MonotonicityInvariant.spec", + "link": ["ERC4626:asset=ERC20"], + "solc": "solc8.0", + "server": "production", + "send_only": true, + "rule_sanity": "basic", + "msg": "Verification of ERC4626", + "optimistic_loop": true, +} \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/certora/conf/certoraRun-MustNotRevertProps.conf b/lesson4_reading/erc4626/src/certora/conf/certoraRun-MustNotRevertProps.conf new file mode 100644 index 0000000..6a7ab1e --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/conf/certoraRun-MustNotRevertProps.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "src/ERC4626.sol", + "src/tokens/ERC20.sol", + ], + "verify": "ERC4626:src/certora/specs/ERC4626-MustNotRevertProps.spec", + "link": ["ERC4626:asset=ERC20"], + "solc": "solc8.0", + "server": "production", + "send_only": true, + "rule_sanity": "basic", + "msg": "Verification of ERC4626", + "optimistic_loop": true, +} \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/certora/conf/certoraRun-RedeemUsingApprovalProps.conf b/lesson4_reading/erc4626/src/certora/conf/certoraRun-RedeemUsingApprovalProps.conf new file mode 100644 index 0000000..7a156cf --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/conf/certoraRun-RedeemUsingApprovalProps.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "src/ERC4626.sol", + "src/tokens/ERC20.sol", + ], + "verify": "ERC4626:src/certora/specs/ERC4626-RedeemUsingApprovalProps.spec", + "link": ["ERC4626:asset=ERC20"], + "solc": "solc8.0", + "server": "production", + "send_only": true, + "rule_sanity": "basic", + "msg": "Verification of ERC4626", + "optimistic_loop": true, +} \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/certora/conf/certoraRun-RoundingProps.conf b/lesson4_reading/erc4626/src/certora/conf/certoraRun-RoundingProps.conf new file mode 100644 index 0000000..fb8be14 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/conf/certoraRun-RoundingProps.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "src/ERC4626.sol", + "src/tokens/ERC20.sol", + ], + "verify": "ERC4626:src/certora/specs/ERC4626-RoundingProps.spec", + "link": ["ERC4626:asset=ERC20"], + "solc": "solc8.0", + "server": "production", + "send_only": true, + "rule_sanity": "basic", + "msg": "Verification of ERC4626", + "optimistic_loop": true, +} \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/certora/conf/certoraRun-SecurityProps.conf b/lesson4_reading/erc4626/src/certora/conf/certoraRun-SecurityProps.conf new file mode 100644 index 0000000..418e7e8 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/conf/certoraRun-SecurityProps.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "src/ERC4626.sol", + "src/tokens/ERC20.sol", + ], + "verify": "ERC4626:src/certora/specs/ERC4626-SecurityProps.spec", + "link": ["ERC4626:asset=ERC20"], + "smt_timeout": "900", + "prover_args":[ + "-mediumTimeout 600" + ], + "solc": "solc8.0", + "multi_assert_check": true, + "server": "production", + "send_only": true, + "rule_sanity": "basic", + "msg": "Verification of ERC4626", + "optimistic_loop": true, +} \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/certora/specs/ERC4626-FunctionalAccountingProps.spec b/lesson4_reading/erc4626/src/certora/specs/ERC4626-FunctionalAccountingProps.spec new file mode 100644 index 0000000..2fcc3e4 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/specs/ERC4626-FunctionalAccountingProps.spec @@ -0,0 +1,131 @@ +import "./ERC4626-MonotonicityInvariant.spec"; + +//Had to change _ERC20 to __ERC20 as of import that already declares _ERC20. +using ERC20 as __ERC20; + +//This is counter-intuitive: why we need to import invariants that should be loaded when calling safeAssumptions()? +use invariant totalAssetsZeroImpliesTotalSupplyZero; +use invariant sumOfBalancesEqualsTotalSupplyERC4626; +use invariant sumOfBalancesEqualsTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC4626; +use invariant mirrorIsCorrectERC20; +use invariant mirrorIsCorrectERC4626; + +methods { + function __ERC20.balanceOf(address) external returns uint256 envfree; + + function balanceOf(address) external returns uint256 envfree; + function previewDeposit(uint256) external returns uint256 envfree; + function previewMint(uint256) external returns uint256 envfree; + function previewRedeem(uint256) external returns uint256 envfree; + function previewWithdraw(uint256) external returns uint256 envfree; + function totalSupply() external returns uint256 envfree; +} + +rule depositProperties(uint256 assets, address receiver, address owner){ + safeAssumptions(); + env e; + //Not an assumption, but just creating an alias for e.msg.sender. Tryout if uint256 owver = e.msg.sender is a better choice here? + require(e.msg.sender == owner); + + //The caller may not be the currentContract. Is that a fair assumption? + //Not sure if solidity allows a way to to fake e.msg.sender attribute. (Delegate call, reflection,...?) + require(owner != currentContract); + + + mathint ownerAssetsBefore = __ERC20.balanceOf(owner); + mathint receiverSharesBefore = balanceOf(receiver); + + mathint previewShares = previewDeposit(assets); + mathint shares = deposit(e, assets, receiver); + + mathint ownerAssetsAfter = __ERC20.balanceOf(owner); + mathint receiverSharesAfter = balanceOf(receiver); + + assert ownerAssetsAfter + assets == ownerAssetsBefore; + assert receiverSharesAfter - shares == receiverSharesBefore; + assert shares >= previewShares; +} + +rule mintProperties(uint256 shares, address receiver, address owner){ + safeAssumptions(); + env e; + require(e.msg.sender == owner); + + //The caller may not be the currentContract. Is that a fair assumption? + //Not sure if solidity allows a way to to fake e.msg.sender attribute. (Delegate call, reflection,...?) + require(owner != currentContract); + + + mathint ownerAssetsBefore = __ERC20.balanceOf(owner); + mathint receiverSharesBefore = balanceOf(receiver); + + mathint previewAssets = previewMint(shares); + mathint assets = mint(e, shares, receiver); + + + mathint ownerAssetsAfter = __ERC20.balanceOf(owner); + mathint receiverSharesAfter = balanceOf(receiver); + + assert ownerAssetsAfter + assets == ownerAssetsBefore; + assert receiverSharesAfter - shares == receiverSharesBefore; + assert assets <= previewAssets; +} + + + +rule withdrawProperties(uint256 assets, address receiver, address owner){ + safeAssumptions(); + env e; + + //The caller may not be the currentContract. Is that a fair assumption? + //Not sure if solidity allows a way to to fake e.msg.sender attribute. (Delegate call, reflection,...?) + require(e.msg.sender != currentContract); + + mathint ownerSharesBefore = balanceOf(owner); + mathint receiverAssetsBefore = __ERC20.balanceOf(receiver); + + mathint previewShares = previewWithdraw(assets); + mathint shares = withdraw(e, assets, receiver, owner); + + + mathint ownerSharesAfter = balanceOf(owner); + mathint receiverAssetsAfter = __ERC20.balanceOf(receiver); + + assert ownerSharesAfter + shares == ownerSharesBefore; + assert receiver != currentContract => receiverAssetsAfter - assets == receiverAssetsBefore; + + //Is this according to specifications or a bug? Couldn't find a clear answer to it. Probably yes, receiverAssets remain unchanged, at least don't increase. + assert receiver == currentContract => receiverAssetsAfter == receiverAssetsBefore; + + assert shares <= previewShares; +} + + +rule redeemProperties(uint256 shares, address receiver, address owner){ + safeAssumptions(); + env e; + + //The caller may not be the currentContract. Is that a fair assumption? + //Not sure if solidity allows a way to to fake e.msg.sender attribute. (Delegate call, reflection,...?) + require(e.msg.sender != currentContract); + + mathint ownerSharesBefore = balanceOf(owner); + mathint receiverAssetsBefore = __ERC20.balanceOf(receiver); + + mathint previewAssets = previewRedeem(shares); + mathint assets = redeem(e, shares, receiver, owner); + + + mathint ownerSharesAfter = balanceOf(owner); + mathint receiverAssetsAfter = __ERC20.balanceOf(receiver); + + assert ownerSharesAfter + shares == ownerSharesBefore; + assert receiver != currentContract => receiverAssetsAfter - assets == receiverAssetsBefore; + + //Is this according to specifications or a bug? Couldn't find a clear answer to it. Probably yes, receiverAssets remain unchanged, at least don't increase. + assert receiver == currentContract => receiverAssetsAfter == receiverAssetsBefore; + + assert assets >= previewAssets; +} diff --git a/lesson4_reading/erc4626/src/certora/specs/ERC4626-InflationAttack.spec b/lesson4_reading/erc4626/src/certora/specs/ERC4626-InflationAttack.spec new file mode 100644 index 0000000..bd021f3 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/specs/ERC4626-InflationAttack.spec @@ -0,0 +1,178 @@ + +import "./ERC4626-MonotonicityInvariant.spec"; + +//Had to change _ERC20 to ___ERC20 as of import that already declares __ERC20. +using ERC20 as __ERC20; + +//This is counter-intuitive: why we need to import invariants that should be loaded when calling safeAssumptions()? +use invariant totalAssetsZeroImpliesTotalSupplyZero; +use invariant sumOfBalancesEqualsTotalSupplyERC4626; +use invariant sumOfBalancesEqualsTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC4626; +use invariant mirrorIsCorrectERC20; +use invariant mirrorIsCorrectERC4626; + + +methods{ + function __ERC20.allowance(address,address) external returns uint256 envfree; + function __ERC20.balanceOf(address) external returns uint256 envfree; + function __ERC20.decimals() external returns uint8 envfree; + function __ERC20.totalSupply() external returns uint256 envfree; + + function balanceOf(address) external returns uint256 envfree; + function convertToAssets(uint256) external returns uint256 envfree; + function convertToShares(uint256) external returns uint256 envfree; + function decimals() external returns uint8 envfree; + function previewDeposit(uint256) external returns uint256 envfree; + function previewMint(uint256) external returns uint256 envfree; + function previewWithdraw(uint256) external returns uint256 envfree; + function totalAssets() external returns uint256 envfree; + function totalSupply() external returns uint256 envfree; +} + + + +rule simpleVersionOfInflationAttack(uint256 assets, address deposit_receiver, address redeem_receiver, address redeem_ownver) { + env e; + safeAssumptions(); + address attacker = e.msg.sender; + + require(balanceOf(attacker) == 0); + require(balanceOf(deposit_receiver) == 0); + require(balanceOf(redeem_receiver) == 0); + require(balanceOf(redeem_ownver) == 0); + + require(attacker != currentContract); + + uint256 shares = deposit(e, assets, deposit_receiver); + + //In the inflationAttack there are 2 steps that we don't model here! + + uint256 receivedAssets = redeem(e, shares, redeem_receiver, redeem_ownver); + assert(receivedAssets <= assets); +} + + + + +//Source: Medium Article by Shao https://tienshaoku.medium.com/eip-4626-inflation-sandwich-attack-deep-dive-and-how-to-solve-it-9e3e320cc3f1 +rule vulnerableToInflationAttack(address attacker, address victim, address deposit1_receiver, address deposit2_victim_receiver,address redeem_receiver,address redeem_ownver ){ + + + + //Doesn't work properly...Retry later. + /*requireInvariant sumOfBalancesEqualsTotalSupplyERC4626; + requireInvariant sumOfBalancesEqualsTotalSupplyERC20; + requireInvariant singleUserBalanceSmallerThanTotalSupplyERC4626; + requireInvariant singleUserBalanceSmallerThanTotalSupplyERC20;*/ + //Doesn't work + //require forall address x. balanceOf(x) <= totalSupply(); + //Doesn't work + //require forall address y. __ERC20.balanceOf(y) <= __ERC20.totalSupply(); + safeAssumptions(); + uint256 oneEther; + uint256 oneWei; + + require(oneWei > 0); + require(oneEther > 0); + + mathint assetsAttackerPreAttack = to_mathint(oneEther) + to_mathint(oneWei); + uint8 ERC4626decimals = decimals(); + uint8 ERC20decimals = __ERC20.decimals(); + + require(attacker != currentContract); + require(attacker != __ERC20); + require(attacker != 0); + require(victim != currentContract); + require(victim != __ERC20); + require(victim != 0); + require(victim != attacker); + + //Following the pattern "First Deposit" of the article. + require(totalSupply() == 0); + require(totalAssets() == 0); + + //Duplicated all requireInvariants + //Doesn't work either.... + require(balanceOf(attacker) == 0); + require(balanceOf(victim) == 0); + require(balanceOf(deposit1_receiver) == 0); + require(balanceOf(deposit2_victim_receiver) == 0); + require(balanceOf(redeem_receiver) == 0); + require(balanceOf(redeem_ownver) == 0); + + //These are fair assumptions on the addresses. + require(attacker == deposit1_receiver); + require(attacker == redeem_ownver); + require(attacker == redeem_receiver); + //It is important that deposit2_victim_receiver is not equal to attacker, as otherwise the deposit by the victim has to transfer assets to the attacker. + //This would mean the victim already trusts the attacker. Interstingly, we could find a CEX for this case. + require(deposit2_victim_receiver != attacker); + + require(balanceOf(attacker) + balanceOf(victim) + balanceOf(deposit1_receiver) +balanceOf(deposit2_victim_receiver) +balanceOf(redeem_receiver) + balanceOf(redeem_ownver) <= to_mathint(totalSupply())); + require(__ERC20.balanceOf(currentContract) + __ERC20.balanceOf(attacker) + __ERC20.balanceOf(victim) + __ERC20.balanceOf(deposit1_receiver) +__ERC20.balanceOf(deposit2_victim_receiver) +__ERC20.balanceOf(redeem_receiver) + __ERC20.balanceOf(redeem_ownver) <= to_mathint(__ERC20.totalSupply())); + + + uint256 before_step_1_totalSupply = totalSupply(); + uint256 before_step_1_totalAssets = totalAssets(); + + /** + * Step 1: the attacker front-runs the depositor and deposits 1 wei WETH and gets 1 share: since totalSupply is 0, shares = 1 * 10**18 / 10**18 = 1 + */ + env e1; + require(e1.msg.sender == attacker); + uint256 firstShares = deposit(e1, oneEther, deposit1_receiver); + + uint256 before_step_2_totalSupply = totalSupply(); + uint256 before_step_2_totalAssets = totalAssets(); + + env e2; + require(e2.msg.sender == attacker); + require(e2.block.timestamp > e1.block.timestamp); + + require(__ERC20.balanceOf(attacker) >= oneWei); + + /** + * Step 2: the attacker also transfers 1 * 1e18 weiWETH, making the totalAssets() WETH balance of the vault become 1e18 + 1 wei + */ + __ERC20.transferFrom(e2, attacker, currentContract, oneWei); + require(__ERC20.balanceOf(currentContract) > 0); + + uint256 before_step_3_totalSupply = totalSupply(); + uint256 before_step_3_totalAssets = totalAssets(); + + //assert before_step_3_totalSupply > 0; + + + /** + * Step 3: + * The spied-on depositor deposits 1e18 wei WETH. However, the depositor gets 0 shares: 1e18 * 1 (totalSupply) / (1e18 + 1) = 1e18 / (1e18 + 1) = 0. + * Since the depositor gets 0 shares, totalSupply() remains at 1 + */ + env e3; + require(e3.msg.sender == victim); + require(e3.block.timestamp > e2.block.timestamp); + uint256 previweAssets = previewDeposit(oneWei); + uint256 victimShares = deposit(e3, oneWei, deposit2_victim_receiver); + + /** + * Step 4: the attacker still has the 1 only share ever minted and thus the withdrawal of + * that 1 share takes away everything in the vault, including the depositor’s 1e18 weiWETH + */ + + uint256 before_step_4_totalSupply = totalSupply(); + uint256 before_step_4_totalAssets = totalAssets(); + uint256 random; + env e4; + require(e4.msg.sender == attacker); + require(e4.block.timestamp > e3.block.timestamp); + //TODO: can attacker actually withdraw `convertToAssets(before_step_4_totalSupply)` or only `assetsAttackerPreAttack` + mathint assetsAttackerPostAttack = redeem(e4, before_step_4_totalSupply, redeem_receiver, redeem_ownver); + + uint256 finalTotalAssets = totalAssets(); + uint256 finalTotalSupply = totalSupply(); + mathint assetsAttackerGained = assetsAttackerPostAttack - assetsAttackerPreAttack; + + assert assetsAttackerPreAttack >= assetsAttackerPostAttack, "The attacker gained assets."; +} diff --git a/lesson4_reading/erc4626/src/certora/specs/ERC4626-MonotonicityInvariant.spec b/lesson4_reading/erc4626/src/certora/specs/ERC4626-MonotonicityInvariant.spec new file mode 100644 index 0000000..40db33a --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/specs/ERC4626-MonotonicityInvariant.spec @@ -0,0 +1,146 @@ + +using ERC20 as _ERC20; + +methods { + function totalSupply() external returns uint256 envfree; + function balanceOf(address) external returns uint256 envfree; + function allowance(address, address) external returns uint256 envfree; + function totalAssets() external returns uint256 envfree; + function previewMint(uint256) external returns uint256 envfree; + function previewWithdraw(uint256) external returns uint256 envfree; + function previewDeposit(uint256) external returns uint256 envfree; + function previewRedeem(uint256) external returns uint256 envfree; + function _ERC20.totalSupply() external returns uint256 envfree; + function _ERC20.balanceOf(address) external returns uint256 envfree; +} + + +function safeAssumptions(){ + requireInvariant sumOfBalancesEqualsTotalSupplyERC4626; + requireInvariant sumOfBalancesEqualsTotalSupplyERC20; + requireInvariant singleUserBalanceSmallerThanTotalSupplyERC20; + requireInvariant singleUserBalanceSmallerThanTotalSupplyERC4626; +} + +function balaceMirrorsAreCorrect(address x) { + requireInvariant mirrorIsCorrectERC20(x); + requireInvariant mirrorIsCorrectERC4626(x); +} + +function safeAssumptionsERC20() { + requireInvariant sumOfBalancesEqualsTotalSupplyERC20; + requireInvariant singleUserBalanceSmallerThanTotalSupplyERC20; +} + +rule assetAndShareMonotonicy(){ + + safeAssumptions(); + uint256 totalAssetsBefore = totalAssets(); + uint256 totalSupplyBefore = totalSupply(); + + method f; + env e; + uint256 amount; + address receiver; + address owner; + if(f.selector == sig:mint(uint,address).selector){ + mint(e, amount, receiver); + } else if(f.selector == sig:withdraw(uint,address,address).selector){ + withdraw(e, amount, receiver, owner); + } else if(f.selector == sig:deposit(uint,address).selector){ + deposit(e, amount, receiver); + } else if(f.selector == sig:redeem(uint,address,address).selector){ + redeem(e, amount, receiver, owner); + } else { + calldataarg args; + f(e,args); + } + + uint256 totalAssetsAfter = totalAssets(); + uint256 totalSupplyAfter = totalSupply(); + + require(e.msg.sender != currentContract); + assert totalSupplyBefore < totalSupplyAfter <=> totalAssetsBefore < totalAssetsAfter , "Strong monotonicity doesn't hold."; + assert (receiver != currentContract) => (totalAssetsBefore <= totalAssetsAfter <=> totalSupplyBefore <= totalSupplyAfter), "Monotonicity doesn't hold."; +} + +/** +* This invariant does not hold for OpenZeppelin. There is a public function mint that allows to increase totalSupply without increasing totalAssets! +*/ +invariant totalAssetsZeroImpliesTotalSupplyZero() + totalAssets() == 0 => totalSupply() == 0 + { + + preserved { + requireInvariant sumOfBalancesEqualsTotalSupplyERC4626; + requireInvariant sumOfBalancesEqualsTotalSupplyERC20; + requireInvariant singleUserBalanceSmallerThanTotalSupplyERC4626; + requireInvariant singleUserBalanceSmallerThanTotalSupplyERC20; + } +} + +invariant sumOfBalancesEqualsTotalSupplyERC4626() + sumOfBalancesERC4626 == to_mathint(totalSupply()); + +ghost mathint sumOfBalancesERC4626 { + init_state axiom sumOfBalancesERC4626 == 0; +} + +hook Sstore currentContract.balanceOf[KEY address user] uint256 newValue (uint256 oldValue) STORAGE { + sumOfBalancesERC4626 = sumOfBalancesERC4626 + newValue - oldValue; + userBalanceERC4626 = newValue; + balanceOfMirroredERC4626[user] = newValue; +} +hook Sload uint256 value currentContract.balanceOf[KEY address user] STORAGE { + //This line makes the proof work. But is this actually safe to assume? With every load in the programm, we assume the invariant to hold. + require to_mathint(value) <= sumOfBalancesERC4626; + require value == balanceOfMirroredERC4626[user]; +} + +invariant sumOfBalancesEqualsTotalSupplyERC20() + sumOfBalancesERC20 == to_mathint(_ERC20.totalSupply()); + +ghost mathint sumOfBalancesERC20 { + init_state axiom sumOfBalancesERC20 == 0; +} + +hook Sstore _ERC20.balanceOf[KEY address user] uint256 newValue (uint256 oldValue) STORAGE { + sumOfBalancesERC20 = sumOfBalancesERC20 + newValue - oldValue; + userBalanceERC20 = newValue; + balanceOfMirroredERC20[user] = newValue; +} + +hook Sload uint256 value _ERC20.balanceOf[KEY address user] STORAGE { + //This line makes the proof work. But is this actually safe to assume? With every load in the programm, we assume the invariant to already hold. + require to_mathint(value) <= sumOfBalancesERC20; + require value == balanceOfMirroredERC20[user]; +} + +invariant singleUserBalanceSmallerThanTotalSupplyERC20() + userBalanceERC20 <= sumOfBalancesERC20; + +ghost mathint userBalanceERC20 { + init_state axiom userBalanceERC20 == 0; +} + +invariant singleUserBalanceSmallerThanTotalSupplyERC4626() + userBalanceERC4626 <= sumOfBalancesERC4626; + +ghost mathint userBalanceERC4626 { + init_state axiom userBalanceERC4626 == 0; +} + +ghost mapping(address => uint256) balanceOfMirroredERC4626 { + init_state axiom forall address a. (balanceOfMirroredERC4626[a] == 0); +} + +ghost mapping(address => uint256) balanceOfMirroredERC20 { + init_state axiom forall address a. (balanceOfMirroredERC20[a] == 0); +} + +invariant mirrorIsCorrectERC20(address x) + balanceOfMirroredERC20[x] == _ERC20.balanceOf(x); + + +invariant mirrorIsCorrectERC4626(address x) + balanceOfMirroredERC4626[x] == balanceOf(x); \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/certora/specs/ERC4626-MustNotRevertProps.spec b/lesson4_reading/erc4626/src/certora/specs/ERC4626-MustNotRevertProps.spec new file mode 100644 index 0000000..82111b2 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/specs/ERC4626-MustNotRevertProps.spec @@ -0,0 +1,85 @@ + + +import "./ERC4626-MonotonicityInvariant.spec"; + +//Had to change _ERC20 to ___ERC20 as of import that already declares __ERC20. +using ERC20 as __ERC20; + +//This is counter-intuitive: why we need to import invariants that should be loaded when calling safeAssumptions()? +use invariant totalAssetsZeroImpliesTotalSupplyZero; +use invariant sumOfBalancesEqualsTotalSupplyERC4626; +use invariant sumOfBalancesEqualsTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC4626; +use invariant mirrorIsCorrectERC20; +use invariant mirrorIsCorrectERC4626; + + + +methods{ + function balanceOf(address) external returns uint256 envfree; + function convertToAssets(uint256) external returns uint256 envfree; + function convertToShares(uint256) external returns uint256 envfree; + function maxDeposit(address) external returns uint256 envfree; + function maxMint(address) external returns uint256 envfree; + function maxRedeem(address) external returns uint256 envfree; + function maxWithdraw(address) external returns uint256 envfree; + function totalAssets() external returns uint256 envfree; + function totalSupply() external returns uint256 envfree; +} + + +definition nonReveritngFunction(method f) returns bool = + f.selector == sig:convertToAssets(uint256).selector + || f.selector == sig:convertToShares(uint256).selector + || f.selector == sig:totalAssets().selector + || f.selector == sig:asset().selector + || f.selector == sig:maxDeposit(address).selector + || f.selector == sig:maxMint(address).selector + || f.selector == sig:maxRedeem(address).selector + || f.selector == sig:maxWithdraw(address).selector; + + +rule mustNotRevertProps(method f) filtered {f -> nonReveritngFunction(f)}{ + env e; + require(e.msg.value == 0); + safeAssumptions(); + bool res = callMethodsWithParamenter(e, f); + assert res == false, "Method ${f} reverted."; +} + +function callMethodsWithParamenter(env e, method f) returns bool { + uint256 amount; + address addr; + if(f.selector == sig:convertToAssets(uint256).selector){ + /**OZ: + We'd need to ensure that totalAssets() + 1 does not overflow....totalSupply() + 10**__decimalsOffset() doesn't overflow and the mulDiv doesn't either + function _convertToAssets(uint256 shares, Math.Rounding rounding) internal view virtual returns (uint256) { + return shares.mulDiv(totalAssets() + 1, totalSupply() + 10 ** _decimalsOffset(), rounding); + } + */ + convertToAssets@withrevert(amount); + return lastReverted; + } else if(f.selector == sig:convertToShares(uint256).selector){ + convertToShares@withrevert(amount); + return lastReverted; + } else if(f.selector == sig:maxWithdraw(address).selector){ + maxWithdraw@withrevert(addr); + return lastReverted; + } else if(f.selector == sig:maxDeposit(address).selector){ + maxDeposit@withrevert(addr); + return lastReverted; + } else if(f.selector == sig:maxMint(address).selector){ + maxMint@withrevert(addr); + return lastReverted; + } else if(f.selector == sig:maxRedeem(address).selector){ + maxRedeem@withrevert(addr); + return lastReverted; + } else if(f.selector == sig:totalAssets().selector || f.selector == sig:asset().selector){ + calldataarg args; + f@withrevert(e, args); + return lastReverted; + } + //Should be unreachable. + return true; +} diff --git a/lesson4_reading/erc4626/src/certora/specs/ERC4626-RedeemUsingApprovalProps.spec b/lesson4_reading/erc4626/src/certora/specs/ERC4626-RedeemUsingApprovalProps.spec new file mode 100644 index 0000000..5a972a4 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/specs/ERC4626-RedeemUsingApprovalProps.spec @@ -0,0 +1,118 @@ +using ERC20 as _ERC20; + +methods { + function _ERC20.balanceOf(address) external returns uint256 envfree; + function allowance(address, address) external returns uint256 envfree; + function balanceOf(address) external returns uint256 envfree; + function previewWithdraw(uint256) external returns uint256 envfree; + function previewRedeem(uint256) external returns uint256 envfree; + function totalAssets() external returns uint256 envfree; +} + +/** +* Special case for when e.msg.sender == owner. +* 1. Third party `withdraw()` calls must update the msg.sender's allowance +* 2. withdraw() must allow proxies to withdraw tokens on behalf of the owner using share token approvals +* 3. Check that is doesn't revert. +*/ +rule ownerWithdrawal(uint256 assets, address receiver, address owner){ + env e; + require(e.msg.sender == owner); + + uint256 allowanceBefore = allowance(owner, e.msg.sender); + withdraw@withrevert(e, assets, receiver, owner); + uint256 allowanceAfter = allowance(owner, e.msg.sender); + assert allowanceAfter == allowanceBefore; + assert lastReverted == false; +} + + +//Third party `withdraw()` calls must update the msg.sender's allowance +//withdraw() must allow proxies to withdraw tokens on behalf of the owner using share token approvals +rule thirdPartyWithdrawal(uint256 assets, address receiver, address owner){ + env e; + require(e.msg.sender != owner); + + uint256 allowanceBefore = allowance(owner, e.msg.sender); + uint256 shares = previewWithdraw(assets); + + withdraw(e, assets, receiver, owner); + + uint256 allowanceAfter = allowance(owner, e.msg.sender); + assert allowanceAfter <= allowanceBefore; + assert shares <= allowanceBefore; +} + +//Third parties must not be able to withdraw() tokens on an owner's behalf without a token approval +rule thirdPartyWithdrawalRevertCase(uint256 assets, address receiver, address owner){ + env e; + uint256 allowanceBefore = allowance(owner, e.msg.sender); + uint256 shares = previewWithdraw(assets); + + require shares > allowanceBefore; + //If e.msg.sender is the owner, no allowance is required, see rule ownerWithdrawal + require e.msg.sender != owner; + + withdraw@withrevert(e, assets, receiver, owner); + + bool withdrawReverted = lastReverted; + + assert withdrawReverted, "withdraw does not revert when no allowance provided."; +} + + + +/** +* Special case for when e.msg.sender == owner. +* 1. Third party `redeem()` calls must update the msg.sender's allowance +* 2. redeem() must allow proxies to redeem shares on behalf of the owner using share token approvals +* 3. Check that is doesn't revert. +*/ +rule ownerRedeem(uint256 shares, address receiver, address owner){ + env e; + require(e.msg.sender == owner); + + uint256 allowanceBefore = allowance(owner, e.msg.sender); + redeem@withrevert(e, shares, receiver, owner); + uint256 allowanceAfter = allowance(owner, e.msg.sender); + assert allowanceAfter == allowanceBefore; + assert lastReverted == false; +} + + +//Third party `redeem()` calls must update the msg.sender's allowance +//redeem() must allow proxies to withdraw tokens on behalf of the owner using share token approvals +rule thirdPartyRedeem(uint256 shares, address receiver, address owner){ + env e; + require(e.msg.sender != owner); + + uint256 allowanceBefore = allowance(owner, e.msg.sender); + uint256 assets = previewRedeem(shares); + + redeem(e, shares, receiver, owner); + + uint256 allowanceAfter = allowance(owner, e.msg.sender); + assert allowanceAfter <= allowanceBefore; + assert shares <= allowanceBefore; +} + +//Third parties must not be able to redeem() tokens on an owner's behalf without a token approval +rule thirdPartyRedeemRevertCase(uint256 shares, address receiver, address owner){ + env e; + uint256 allowanceBefore = allowance(owner, e.msg.sender); + uint256 assets = previewRedeem(shares); + + require shares > allowanceBefore; + //If e.msg.sender is the owner, no allowance is required, see rule ownerWithdrawal + require e.msg.sender != owner; + + redeem@withrevert(e, shares, receiver, owner); + + bool redeemReverted = lastReverted; + + assert redeemReverted, "redeem does not revert when no allowance provided."; +} + + +invariant balanceOfERC20EqualToTotalAsset() + totalAssets() == _ERC20.balanceOf(currentContract); diff --git a/lesson4_reading/erc4626/src/certora/specs/ERC4626-RoundingProps.spec b/lesson4_reading/erc4626/src/certora/specs/ERC4626-RoundingProps.spec new file mode 100644 index 0000000..f50ab59 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/specs/ERC4626-RoundingProps.spec @@ -0,0 +1,173 @@ + +import "./ERC4626-MonotonicityInvariant.spec"; +//Had to change _ERC20 to ___ERC20 as of import that already declares __ERC20. +using ERC20 as __ERC20; +//This is counter-intuitive: why we need to import invariants that should be loaded when calling safeAssumptions()? +use invariant totalAssetsZeroImpliesTotalSupplyZero; +use invariant sumOfBalancesEqualsTotalSupplyERC4626; +use invariant sumOfBalancesEqualsTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC4626; +use invariant mirrorIsCorrectERC20; +use invariant mirrorIsCorrectERC4626; + +methods{ + function balanceOf(address) external returns uint256 envfree; + function __ERC20.balanceOf(address) external returns uint256 envfree; + function __ERC20.totalSupply() external returns uint256 envfree; + function decimals() external returns uint8 envfree; + function totalAssets() external returns uint256 envfree; + function totalSupply() external returns uint256 envfree; + function previewWithdraw(uint256 assets) external returns uint256 envfree; + function previewRedeem(uint256 shares) external returns uint256 envfree; +} + +function assumeBalanceEqualSumManualERC4626_4(address addr1,address addr2,address addr3, address addr4){ + mathint totalSupply = totalSupply(); + mathint balanceOfAddr1 = balanceOf(addr1); + mathint balanceOfAddr2 = balanceOf(addr2); + mathint balanceOfAddr3 = balanceOf(addr3); + mathint balanceOfAddr4 = balanceOf(addr4); + + //Case all different + require addr1 != addr2 && addr1 != addr3 && addr1 != addr4 && addr2 != addr3 && addr2 != addr4 && addr3 != addr4 => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr3 + balanceOfAddr4; + + //Case two are equal + require (addr1 == addr2 && addr1 != addr3 && addr1 != addr4 && addr3 != addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr3 + balanceOfAddr4; + require (addr1 == addr3 && addr1 != addr2 && addr1 != addr4 && addr2 != addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr4; + require (addr1 == addr4 && addr1 != addr2 && addr1 != addr3 && addr2 != addr3) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr3; + require (addr2 == addr3 && addr2 != addr1 && addr2 != addr4 && addr1 != addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr4; + require (addr2 == addr4 && addr2 != addr1 && addr2 != addr3 && addr1 != addr3) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr3; + require (addr3 == addr4 && addr3 != addr1 && addr3 != addr2 && addr1 != addr2) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr3; + + //Cases two are equal and the other two as well. + require (addr1 == addr2 && addr3 == addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr3; + require (addr1 == addr3 && addr2 == addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr2; + require (addr2 == addr3 && addr1 == addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr2; + + //Cases three are same + require (addr1 == addr2 && addr2 == addr3 && addr1 != addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr4; //4 differs + require (addr1 == addr2 && addr2 == addr4 && addr1 != addr3) => totalSupply == balanceOfAddr1 + balanceOfAddr3; //3 differs + require (addr1 == addr3 && addr3 == addr4 && addr1 != addr2) => totalSupply == balanceOfAddr1 + balanceOfAddr2; //2 differs + require (addr2 == addr3 && addr3 == addr4 && addr1 != addr2) => totalSupply == balanceOfAddr2 + balanceOfAddr1; //1 differs + + require addr1 == addr2 && addr2 == addr3 && addr3 == addr4 => totalSupply == balanceOfAddr1; +} + +function assumeBalanceEqualSumManualERC20_4(address addr1,address addr2,address addr3, address addr4){ + + mathint totalSupply = __ERC20.totalSupply(); + + if(addr1 != currentContract && addr2 != currentContract  && addr3 != currentContract && addr4 != currentContract){ + totalSupply = totalSupply - __ERC20.balanceOf(currentContract); + } + mathint balanceOfAddr1 = __ERC20.balanceOf(addr1); + mathint balanceOfAddr2 = __ERC20.balanceOf(addr2); + mathint balanceOfAddr3 = __ERC20.balanceOf(addr3); + mathint balanceOfAddr4 = __ERC20.balanceOf(addr4); + + //Case all different + require addr1 != addr2 && addr1 != addr3 && addr1 != addr4 && addr2 != addr3 && addr2 != addr4 && addr3 != addr4 => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr3 + balanceOfAddr4; + + //Case two are equal + require (addr1 == addr2 && addr1 != addr3 && addr1 != addr4 && addr3 != addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr3 + balanceOfAddr4; + require (addr1 == addr3 && addr1 != addr2 && addr1 != addr4 && addr2 != addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr4; + require (addr1 == addr4 && addr1 != addr2 && addr1 != addr3 && addr2 != addr3) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr3; + require (addr2 == addr3 && addr2 != addr1 && addr2 != addr4 && addr1 != addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr4; + require (addr2 == addr4 && addr2 != addr1 && addr2 != addr3 && addr1 != addr3) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr3; + require (addr3 == addr4 && addr3 != addr1 && addr3 != addr2 && addr1 != addr2) => totalSupply == balanceOfAddr1 + balanceOfAddr2 + balanceOfAddr3; + + //Cases two are equal and the other two as well. + require (addr1 == addr2 && addr3 == addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr3; + require (addr1 == addr3 && addr2 == addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr2; + require (addr2 == addr3 && addr1 == addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr2; + + //Cases three are same + require (addr1 == addr2 && addr2 == addr3 && addr1 != addr4) => totalSupply == balanceOfAddr1 + balanceOfAddr4; //4 differs + require (addr1 == addr2 && addr2 == addr4 && addr1 != addr3) => totalSupply == balanceOfAddr1 + balanceOfAddr3; //3 differs + require (addr1 == addr3 && addr3 == addr4 && addr1 != addr2) => totalSupply == balanceOfAddr1 + balanceOfAddr2; //2 differs + require (addr2 == addr3 && addr3 == addr4 && addr1 != addr2) => totalSupply == balanceOfAddr2 + balanceOfAddr1; //1 differs + + require addr1 == addr2 && addr2 == addr3 && addr3 == addr4 => totalSupply == balanceOfAddr1; +} + +rule inverseDepositRedeemInFavourForVault(uint256 assets, address deposit_receiver, address redeem_receiver, address redeem_owner){ + env e; + safeAssumptions(); + + assumeBalanceEqualSumManualERC20_4(deposit_receiver,redeem_receiver, redeem_owner, e.msg.sender); + assumeBalanceEqualSumManualERC4626_4(deposit_receiver,redeem_receiver, redeem_owner, e.msg.sender); + + uint256 shares = deposit(e, assets, deposit_receiver); + uint256 redeemedAssets = redeem(e, shares, redeem_receiver, redeem_owner); + + assert assets >= redeemedAssets, "User cannot gain assets using deposit / redeem combination."; +} + +rule inverseRedeemDepositInFavourForVault(uint256 shares, address deposit_receiver, address redeem_receiver, address redeem_owner){ + env e; + safeAssumptions(); + + assumeBalanceEqualSumManualERC20_4(deposit_receiver,redeem_receiver, redeem_owner, e.msg.sender); + assumeBalanceEqualSumManualERC4626_4(deposit_receiver,redeem_receiver, redeem_owner, e.msg.sender); + + uint256 redeemedAssets = redeem(e, shares, redeem_receiver, redeem_owner); + uint256 depositedShares = deposit(e, redeemedAssets, deposit_receiver); + + assert shares >= depositedShares, "User cannot gain shares using redeem / deposit combination."; +} + + +//TODO: Double check, is this property correct? +//Mint and withdraw are inverse from perspective of the implementation, at least one mint shares, the other burns shares +rule inverseMintWithdrawInFavourForVault(uint256 shares, address mint_receiver, address withdraw_receiver, address withdraw_owner){ + env e; + safeAssumptions(); + + assumeBalanceEqualSumManualERC20_4(mint_receiver,withdraw_receiver, withdraw_owner, e.msg.sender); + assumeBalanceEqualSumManualERC4626_4(mint_receiver,withdraw_receiver, withdraw_owner, e.msg.sender); + + uint256 assets = mint(e, shares, mint_receiver); + uint256 withdrawnShares = withdraw(e, assets, withdraw_receiver, withdraw_owner); + + assert shares >= withdrawnShares, "User cannot gain assets using mint / withdraw combination."; +} + +//TODO: Double check, is this property correct? +//Mint and withdraw are inverse from perspective of the implementation, at least one mint shares, the other burns shares +rule inverseWithdrawMintInFavourForVault(uint256 assets, address mint_receiver, address withdraw_receiver, address withdraw_owner){ + env e; + safeAssumptions(); + + assumeBalanceEqualSumManualERC20_4(mint_receiver,withdraw_receiver, withdraw_owner, e.msg.sender); + assumeBalanceEqualSumManualERC4626_4(mint_receiver,withdraw_receiver, withdraw_owner, e.msg.sender); + + uint256 withdrawnShares = withdraw(e, assets, withdraw_receiver, withdraw_owner); + uint256 mintedAssets = mint(e, withdrawnShares, mint_receiver); + + assert assets >= mintedAssets, "User cannot gain assets using withdraw / mint combination."; +} + + +//TODO: Not sure if this is even a valid property: The rule fails. +rule redeemInOneTransactionIsPreferable(address user, address receiver, uint256 s1, uint256 s2) { + env e; + + safeAssumptions(); + uint256 shares = require_uint256(s1 + s2); + + //The below requires have been added to find more intuitive counter examples. + require(e.msg.sender != currentContract); + require(e.msg.sender != user); + require(e.msg.sender != receiver); + require(user != receiver); + require(totalAssets() >= totalSupply()); + + storage init = lastStorage; + + mathint redeemed1a = redeem(e, s1, receiver, user); + mathint redeemed1b = redeem(e, s2, receiver, user); + mathint redeemed2 = redeem(e, shares, receiver, user) at init; + + assert(redeemed2 <= redeemed1a + redeemed1b); +} \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/certora/specs/ERC4626-SecurityProps.spec b/lesson4_reading/erc4626/src/certora/specs/ERC4626-SecurityProps.spec new file mode 100644 index 0000000..842e846 --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/specs/ERC4626-SecurityProps.spec @@ -0,0 +1,207 @@ +import "./ERC4626-MonotonicityInvariant.spec"; + +//Had to change _ERC20 to ___ERC20 as of import that already declares __ERC20. +using ERC20 as __ERC20; + +use invariant totalAssetsZeroImpliesTotalSupplyZero; +use invariant sumOfBalancesEqualsTotalSupplyERC4626; +use invariant sumOfBalancesEqualsTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC20; +use invariant singleUserBalanceSmallerThanTotalSupplyERC4626; +use invariant mirrorIsCorrectERC4626; +use invariant mirrorIsCorrectERC20; + + +methods { + function allowance(address, address) external returns uint256 envfree; + function totalAssets() external returns uint256 envfree; + function decimals() external returns uint8 envfree; + function __ERC20.decimals() external returns uint8 envfree; + function totalSupply() external returns uint256 envfree; +} + + +//deposit must increase totalSupply +rule depositMustIncreaseTotalSupply(uint256 assets, address user){ + safeAssumptions(); + + uint256 totalSupplyBefore = totalSupply(); + env e; + deposit(e, assets, user); + uint256 totalSupplyAfter = totalSupply(); + assert totalSupplyAfter >= totalSupplyBefore, "Total supply must increase when deposit is called."; +} + +//mint must increase totalAssets +rule mintMustIncreaseTotalAssets(uint256 shares, address user){ + safeAssumptions(); + + uint256 totalAssetsBefore = totalAssets(); + env e; + mint(e, shares, user); + uint256 totalAssetsAfter = totalAssets(); + assert totalAssetsAfter >= totalAssetsBefore, "Total assets must increase when mint is called."; +} + +//withdraw must decrease totalAssets +rule withdrawMustDecreaseTotalSupply(uint256 assets, address receiver, address owner){ + safeAssumptions(); + + uint256 totalSupplyBefore = totalSupply(); + env e; + + withdraw(e, assets, receiver, owner); + uint256 totalSupplyAfter = totalSupply(); + assert totalSupplyAfter <= totalSupplyBefore, "Total supply must decrease when withdraw is called."; +} + +//redeem must decrease totalAssets +rule redeemMustDecreaseTotalAssets(uint256 shares, address receiver, address owner){ + safeAssumptions(); + + uint256 totalAssetsBefore = totalAssets(); + env e; + redeem(e, shares, receiver, owner); + uint256 totalAssetsAfter = totalAssets(); + assert totalAssetsAfter <= totalAssetsBefore, "Total assets must decrease when redeem is called."; +} + +/** +Checks that a user gains assets in the following process +1. User mints X shares, (corresponding to Y assets) +2. Underlying vault increases total value +3. User redeemed X minted shares again and receives Z assets in return. + +This rule derives upper and lower limits to the newly gained assets Z. +*/ +rule increaseInUnderlyingVaultMustReflectToRedeemedShares_UpperAndLowerLimits(){ + env e; + uint256 mintedShares; + uint256 newAssets; + address user; + require(e.msg.sender == user); + require(newAssets > 0); + require(e.msg.sender != currentContract); + + safeAssumptions(); + + uint256 totalSupplyBefore = totalSupply(); + uint256 totalAssetsBefore = totalAssets(); + + //Otherwise, inequalities below do not hold as of division by zero. TODO: think of Upper Bound in case totalSupplyBefore = 0; + require mintedShares > 0; + require totalSupplyBefore > 0; + + //Mint some new shares + uint256 mintedAssets = mint(e, mintedShares, user); + + //underlying vault increases value, models a transfer from 0 to the currenctContract, essentially a call to "mint". + __ERC20.transferFrom(e, 0, currentContract, newAssets); + + uint256 totalSupplyAfter = totalSupply(); + uint256 totalAssetsAfter = totalAssets(); + + //Redeem mintedShares again + uint256 redeemedAssets = redeem(e, mintedShares, user, user); + + /** + Explanation of the assert below. + Inequalities baisc idea: (a/c <= b/d) => (a/c <= (a + b)/(c + d) <= b/d) + + Given.... totalAssetsBefore / totalSupplyBefore <= (mintedAssets + newAssets) / mintedShares ... implies ... totalAssetsBefore / totalSupplyBefore <= totalAssetsAfter / totalSupplyAfter <= (mintedAssets + newAssets) / mintedShares + Given.... totalAssetsBefore / totalSupplyBefore >= (mintedAssets + newAssets) / mintedShares ... implies ... totalAssetsBefore / totalSupplyBefore >= totalAssetsAfter / totalSupplyAfter >= (mintedAssets + newAssets) / mintedShares + + Now it should be redeemedAssets = floor(mintedShares * totalAssetsAfter / totalSupplyAfter) that can be relaxed to + Given.... totalAssetsBefore / totalSupplyBefore <= (mintedAssets + newAssets) / mintedShares ... implies ... mintedShares * totalAssetsBefore / totalSupplyBefore <= redeemedAssets <= (mintedAssets + newAssets) + Given.... totalAssetsBefore / totalSupplyBefore >= (mintedAssets + newAssets) / mintedShares ... implies ... mintedShares * totalAssetsBefore / totalSupplyBefore >= redeemedAssets >= (mintedAssets + newAssets) + + + Now it is mintedShares * totalAssetsAfter / totalSupplyAfter >= floor(mintedShares * totalAssetsAfter / totalSupplyAfter) [= redeemedAssets] > mintedShares * totalAssetsAfter / totalSupplyAfter - 1 + + Note in the formular below, one can replace tAA / tSA by (tAB + mA + nA) / (tSB + mS) + Let tAB := totalAssetBefore + Let tAA := totalAssetAfter + Let tSB := totalSupplyBefore + Let tSA := totalSupplyAfter + Let mS := mintedShares + Let mA := mintedAssets + Let nA := newAssets + Then it is + + (1) tAB / tSB <= (mA + nA) / mS => tAB / tSB <= tAA / tSA + (2): tAB / tSB <= (mA + nA) / mS => tAA / tSA <= (mA + nA) / mS + (3): tAB / tSB >= (mA + nA) / mS => tAB / tSB >= tAA / tSA + (4): tAB / tSB >= (mA + nA) / mS => tAA / tSA >= (mA + nA) / mS + we also know that (5) redeemedAssets <= mS * tAA / tSA and (6) mS * tAA / tSA - 1 < redeemedAssets + + Combining (1) and (6) it is + (7) tAB / tSB <= (mA + nA) / mS => tAB / tSB < (redeemedAssets + 1) / mS + Combining (2) and (5) it is + (8) tAB / tSB <= (mA + nA) / mS => redeemedAssets / mS <= (mA + nA) / mS + Combining (3) and (5) it is + (9) tAB / tSB >= (mA + nA) / mS => tAB / tSB >= redeemedAssets / mS + Combining (4) and (6) it is + (10) tAB / tSB >= (mA + nA) / mS => (redeemedAssets + 1) / mS > (mA + nA) / mS + */ + + //Sanity asserts to ensure the reasoning is correct + //assert to_mathint(totalAssetsAfter) == totalAssetsBefore + mintedAssets + newAssets; + //assert to_mathint(totalSupplyAfter) == totalSupplyBefore + mintedShares; + + //Implements (7) without division to avoid rounding. + assert totalAssetsBefore * mintedShares <= (mintedAssets + newAssets) * totalSupplyBefore => totalAssetsBefore * mintedShares < to_mathint(redeemedAssets + 1) * totalSupplyBefore, "Checking lower bound in case of increase of ratio"; //Causes timeout + //Implements (8) without division to avoid rounding. + assert totalAssetsBefore * mintedShares <= (mintedAssets + newAssets) * totalSupplyBefore => to_mathint(redeemedAssets) <= (mintedAssets + newAssets), "Checking upper bound in case of increase of ratio"; //Does not causes timeout with the correct config. https://prover.certora.com/output/53900/1c3ce153358048709a259f7ce383019c/?anonymousKey=ffd32ec358795cb4c1a1d006a98993335151ee23 + //Implements (9) without division to avoid rounding. + assert totalAssetsBefore * mintedShares >= (mintedAssets + newAssets) * totalSupplyBefore => totalAssetsBefore * mintedShares >= redeemedAssets * totalSupplyBefore , "Checking upper bound in case of decrease of ratio"; //Not a cause of the timeout, as identified by "multi_assert_check": true + //Implements (10) without division to avoid rounding. + assert totalAssetsBefore * mintedShares >= (mintedAssets + newAssets) * totalSupplyBefore => to_mathint(redeemedAssets + 1) > (mintedAssets + newAssets), "Checking lower bound in case of decrease of ratio"; //Not a cause of the timeout, as identified by "multi_assert_check": true +} + + +/** +Checks that a user gains assets in the following process +1. User mints X shares, (corresponding to Y assets) +2. Underlying vault increases total value +3. User redeemed X minted shares again. + +The received assets in step 3 must be larger than Y (in the assert there is an offset +1 as of rounding) as the vaults total assets increases. + + +property derived from table in https://github.com/transmissions11/solmate/blob/0384dbaaa4fcb5715738a9254a7c0a4cb62cf458/src/test/ERC4626.t.sol#L117 +*/ +rule increaseInUnderlyingVaultMustReflectInRedeemNoTimeout_LowerLimit(){ + env e; + uint256 mintedShares; + uint256 newAssets; + address user; + require(e.msg.sender == user); + require(e.msg.sender != currentContract); + require(newAssets > 0); + + safeAssumptions(); + + //Mint some new shares + uint256 mintedAssets = mint(e, mintedShares, user); + + //underlying vault increases value, models a transfer from 0 to the currenctContract, essentially a call to "mint". + __ERC20.transferFrom(e, 0, currentContract, newAssets); + + //Redeem mintedShares again + uint256 redeemedAssets = redeem(e, mintedShares, user, user); + + //Redeemed assets should have increased. TODO can we be more specific? + assert to_mathint(mintedAssets) <= redeemedAssets + 1, "Redeemed assets must increase."; +} + + +//`decimals()` should be larger than or equal to `asset.decimals()` +rule decimalsOfUnderlyingVaultShouldBeLarger(uint256 shares, address receiver, address owner){ + //TODO: Rule fails. The method call to decimals returns a HAVOC'd value. Still the solver should be able to reason that ERC4626.decimals == ERC20.decimals as of the call to the super constructor. Don't understand why. + safeAssumptions(); + + uint8 assetDecimals = __ERC20.decimals(); + uint8 decimals = decimals(); + + assert decimals >= assetDecimals, "Decimals of underlying ERC20 should be larger than ERC4626 decimals."; +} diff --git a/lesson4_reading/erc4626/src/certora/specs/Properties.md b/lesson4_reading/erc4626/src/certora/specs/Properties.md new file mode 100644 index 0000000..7573d9d --- /dev/null +++ b/lesson4_reading/erc4626/src/certora/specs/Properties.md @@ -0,0 +1,131 @@ +MustNotRevertProps +--- +* `convertToAssets()` must not revert for reasonable values +* `convertToShares()` must not revert for reasonable values + +> Comment Johannes: What's meant by reasonable values here? There are ways to make both revert, when `totalSupply * shares|assets` overflows. + +* `asset()` must not revert +* `totalAssets()` must not revert +* `maxDeposit()` must not revert +* `maxMint()` must not revert +* `maxRedeem()` must not revert +* `maxWithdraw()` must not revert + +> Comment Johannes: `maxWithdraw` reverts in an integer overflow case as it depends on `convertToAssets()`. If that spec is correct, it's a bug. + +FunctionalAccountingProps +--- +> Implementation see rule depositProperties +* `deposit()` must deduct assets from the owner +* `deposit()` must credit shares to the receiver +* `deposit()` must mint greater than or equal to the number of shares predicted by `previewDeposit()` +> Implementation see rule mintProperties +* `mint()` must deduct assets from the owner +* `mint()` must credit shares to the receiver +* `mint()` must consume less than or equal to the number of assets predicted by `previewMint()` +> Implementation see rule withdrawProperties +* `withdraw()` must deduct shares from the owner +* `withdraw()` must credit assets to the receiver +* `withdraw()` must deduct less than or equal to the number of shares predicted by `previewWithdraw()` +> Implementation see rule redeemProperties +* `redeem()` must deduct shares from the owner +* `redeem()` must credit assets to the receiver +* `redeem()` must credit greater than or equal to the number of assets predicted by `previewRedeem()` + +RedeemUsingApprovalProps +--- +> All properties with withdraw and redeem implemented. +* `withdraw()` must allow proxies to withdraw tokens on behalf of the owner using share token approvals +* `redeem()` must allow proxies to redeem shares on behalf of the owner using share token approvals +* Third party `withdraw()` calls must update the msg.sender's allowance +* Third party `redeem()` calls must update the msg.sender's allowance +* Third parties must not be able to `withdraw()` tokens on an owner's behalf without a token approval +* Third parties must not be able to `redeem()` shares on an owner's behalf without a token approval + +SenderIndependentProps +--- +> declaring methods env free checks this automatically for us. Otherwise one _could_ take two different env e1, env e2 and show that the return value of the function calls is equal for any environment. +* `maxDeposit()` must assume the receiver/sender has infinite assets +* `maxMint()` must assume the receiver/sender has infinite assets +* `previewMint()` must not account for msg.sender asset balance +* `previewDeposit()` must not account for msg.sender asset balance +* `previewWithdraw()` must not account for msg.sender share balance +* `previewRedeem()` must not account for msg.sender share balance + + + +RoundingProps +--- +> Show that storage doesn't change when using these function. (i.e. check that all view function are actually view) +* Shares may never be minted for free using: + * `previewDeposit()` + * `previewMint()` + * `convertToShares()` + +* Tokens may never be withdrawn for free using: + * `previewWithdraw()` + * `previewRedeem()` + * `convertToAssets()` + +> Solve a rule totalMonotonicty +* Shares may never be minted for free using: + * `deposit()` + * `mint()` + +* Tokens may never be withdrawn for free using: + * `withdraw()` + * `redeem()` + +SecurityProps +--- +* `decimals()` should be larger than or equal to `asset.decimals()` + +> Added specification in file `ERC4626-InflationAttack.spec`` +* Accounting system must not be vulnerable to share price inflation attacks + +> Johannes: Added 4 rules to show the below. +* `deposit/mint` must increase `totalSupply/totalAssets` +* `withdraw/redeem` must decrease `totalSupply/totalAssets` + + +* `previewDeposit()` must not account for vault specific/user/global limits +* `previewMint()` must not account for vault specific/user/global limits +* `previewWithdraw()` must not account for vault specific/user/global limits +* `previewRedeem()` must not account for vault specific/user/global limits + + +Properties that may not be testable +--- +* Note that any unfavorable discrepancy between `convertToShares` and `previewDeposit` SHOULD be considered slippage in share price or some other type of condition, meaning the depositor will lose assets by depositing. +* Whether a given method is inclusive of withdraw/deposit fees + + + + +Other Properties +------ +* `withdraw` and `redeem` are semantically equivalent when the inputs are converted using the respective `convert` method. +* `mint` and `deposit` are semantically equivalent when the inputs are converted using the respective `convert` method. +* Deposit increases the number of shares by mint. Shares minted should be proportional to the increase of the balance of the vault. + ``` + a: amount to deposit + B: Balance of vault before deposit + s: shares to mint + T: Total shares before minting + Then it holds: (a+B)/B = (s+T)/T => s = aT/B + ``` + Source https://www.youtube.com/watch?v=k7WNibJOBXE + +* When withdrawing, the shares burned must be proportional to the total balance of the vault + ``` + a: amount to withdraw + B: Balance of vault before deposit + s: shares to burn + T: Total shares before burning + Then it holds: (B-a)/B = (T-s)/T => s = aT/B + ``` + Source https://www.youtube.com/watch?v=k7WNibJOBXE +* ERC-4626 Inflation attack: Can we model a rule that "executes" the inflation attack? What happens if we change the analyzed contract to use standard division instead of `FixedPointMathLib.sol`? Does the rule detect it? + + Source https://tienshaoku.medium.com/eip-4626-inflation-sandwich-attack-deep-dive-and-how-to-solve-it-9e3e320cc3f1 \ No newline at end of file diff --git a/lesson4_reading/erc4626/src/libs/FixedPointMathLib.sol b/lesson4_reading/erc4626/src/libs/FixedPointMathLib.sol new file mode 100644 index 0000000..c989b75 --- /dev/null +++ b/lesson4_reading/erc4626/src/libs/FixedPointMathLib.sol @@ -0,0 +1,230 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +/// @notice Arithmetic library with operations for fixed-point numbers. +/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/utils/FixedPointMathLib.sol) +/// @author Inspired by USM (https://github.com/usmfum/USM/blob/master/contracts/WadMath.sol) +library FixedPointMathLib { + /*////////////////////////////////////////////////////////////// + SIMPLIFIED FIXED POINT OPERATIONS + //////////////////////////////////////////////////////////////*/ + + uint256 internal constant MAX_UINT256 = 2**256 - 1; + + uint256 internal constant WAD = 1e18; // The scalar of ETH and most ERC20s. + + function mulWadDown(uint256 x, uint256 y) internal pure returns (uint256) { + return mulDivDown(x, y, WAD); // Equivalent to (x * y) / WAD rounded down. + } + + function mulWadUp(uint256 x, uint256 y) internal pure returns (uint256) { + return mulDivUp(x, y, WAD); // Equivalent to (x * y) / WAD rounded up. + } + + function divWadDown(uint256 x, uint256 y) internal pure returns (uint256) { + return mulDivDown(x, WAD, y); // Equivalent to (x * WAD) / y rounded down. + } + + function divWadUp(uint256 x, uint256 y) internal pure returns (uint256) { + return mulDivUp(x, WAD, y); // Equivalent to (x * WAD) / y rounded up. + } + + /*////////////////////////////////////////////////////////////// + LOW LEVEL FIXED POINT OPERATIONS + //////////////////////////////////////////////////////////////*/ + + function mulDivDown( + uint256 x, + uint256 y, + uint256 denominator + ) internal pure returns (uint256 z) { + assembly { + // Store x * y in z for now. + z := mul(x, y) + + // Equivalent to require(denominator != 0 && (x == 0 || (x * y) / x == y)) + if iszero(and(iszero(iszero(denominator)), or(iszero(x), eq(div(z, x), y)))) { + revert(0, 0) + } + // Case above: 2*8 mod 10 = 16 mod 10 == 6 mod 10 = 2*3 mod 10. 8 != 3 => revert. + // Case below: 2 <= 10 / 8 which is false => revert + // Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y)) + /*if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT256, y)))))) { + revert(0, 0) + }*/ + + // Divide z by the denominator. + z := div(z, denominator) + } + } + + function mulDivUp( + uint256 x, + uint256 y, + uint256 denominator + ) internal pure returns (uint256 z) { + assembly { + // Store x * y in z for now. + z := mul(x, y) + + // Equivalent to require(denominator != 0 && (x == 0 || (x * y) / x == y)) + if iszero(and(iszero(iszero(denominator)), or(iszero(x), eq(div(z, x), y)))) { + revert(0, 0) + } + + // First, divide z - 1 by the denominator and add 1. + // We allow z - 1 to underflow if z is 0, because we multiply the + // end result by 0 if z is zero, ensuring we return 0 if z is zero. + z := mul(iszero(iszero(z)), add(div(sub(z, 1), denominator), 1)) + } + } + + function rpow( + uint256 x, + uint256 n, + uint256 scalar + ) internal pure returns (uint256 z) { + assembly { + switch x + case 0 { + switch n + case 0 { + // 0 ** 0 = 1 + z := scalar + } + default { + // 0 ** n = 0 + z := 0 + } + } + default { + switch mod(n, 2) + case 0 { + // If n is even, store scalar in z for now. + z := scalar + } + default { + // If n is odd, store x in z for now. + z := x + } + + // Shifting right by 1 is like dividing by 2. + let half := shr(1, scalar) + + for { + // Shift n right by 1 before looping to halve it. + n := shr(1, n) + } n { + // Shift n right by 1 each iteration to halve it. + n := shr(1, n) + } { + // Revert immediately if x ** 2 would overflow. + // Equivalent to iszero(eq(div(xx, x), x)) here. + if shr(128, x) { + revert(0, 0) + } + + // Store x squared. + let xx := mul(x, x) + + // Round to the nearest number. + let xxRound := add(xx, half) + + // Revert if xx + half overflowed. + if lt(xxRound, xx) { + revert(0, 0) + } + + // Set x to scaled xxRound. + x := div(xxRound, scalar) + + // If n is even: + if mod(n, 2) { + // Compute z * x. + let zx := mul(z, x) + + // If z * x overflowed: + if iszero(eq(div(zx, x), z)) { + // Revert if x is non-zero. + if iszero(iszero(x)) { + revert(0, 0) + } + } + + // Round to the nearest number. + let zxRound := add(zx, half) + + // Revert if zx + half overflowed. + if lt(zxRound, zx) { + revert(0, 0) + } + + // Return properly scaled zxRound. + z := div(zxRound, scalar) + } + } + } + } + } + + /*////////////////////////////////////////////////////////////// + GENERAL NUMBER UTILITIES + //////////////////////////////////////////////////////////////*/ + + function sqrt(uint256 x) internal pure returns (uint256 z) { + assembly { + // Start off with z at 1. + z := 1 + + // Used below to help find a nearby power of 2. + let y := x + + // Find the lowest power of 2 that is at least sqrt(x). + if iszero(lt(y, 0x100000000000000000000000000000000)) { + y := shr(128, y) // Like dividing by 2 ** 128. + z := shl(64, z) // Like multiplying by 2 ** 64. + } + if iszero(lt(y, 0x10000000000000000)) { + y := shr(64, y) // Like dividing by 2 ** 64. + z := shl(32, z) // Like multiplying by 2 ** 32. + } + if iszero(lt(y, 0x100000000)) { + y := shr(32, y) // Like dividing by 2 ** 32. + z := shl(16, z) // Like multiplying by 2 ** 16. + } + if iszero(lt(y, 0x10000)) { + y := shr(16, y) // Like dividing by 2 ** 16. + z := shl(8, z) // Like multiplying by 2 ** 8. + } + if iszero(lt(y, 0x100)) { + y := shr(8, y) // Like dividing by 2 ** 8. + z := shl(4, z) // Like multiplying by 2 ** 4. + } + if iszero(lt(y, 0x10)) { + y := shr(4, y) // Like dividing by 2 ** 4. + z := shl(2, z) // Like multiplying by 2 ** 2. + } + if iszero(lt(y, 0x8)) { + // Equivalent to 2 ** z. + z := shl(1, z) + } + + // Shifting right by 1 is like dividing by 2. + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + + // Compute a rounded down version of z. + let zRoundDown := div(x, z) + + // If zRoundDown is smaller, use it. + if lt(zRoundDown, z) { + z := zRoundDown + } + } + } +} diff --git a/lesson4_reading/erc4626/src/libs/SafeTransferLib.sol b/lesson4_reading/erc4626/src/libs/SafeTransferLib.sol new file mode 100644 index 0000000..d08d1b8 --- /dev/null +++ b/lesson4_reading/erc4626/src/libs/SafeTransferLib.sol @@ -0,0 +1,124 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +import {ERC20} from "../tokens/ERC20.sol"; + +/// @notice Safe ETH and ERC20 transfer library that gracefully handles missing return values. +/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/utils/SafeTransferLib.sol) +/// @dev Use with caution! Some functions in this library knowingly create dirty bits at the destination of the free memory pointer. +/// @dev Note that none of the functions in this library check that a token has code at all! That responsibility is delegated to the caller. +library SafeTransferLib { + /*////////////////////////////////////////////////////////////// + ETH OPERATIONS + //////////////////////////////////////////////////////////////*/ + + function safeTransferETH(address to, uint256 amount) internal { + bool success; + + assembly { + // Transfer the ETH and store if it succeeded or not. + success := call(gas(), to, amount, 0, 0, 0, 0) + } + + require(success, "ETH_TRANSFER_FAILED"); + } + + /*////////////////////////////////////////////////////////////// + ERC20 OPERATIONS + //////////////////////////////////////////////////////////////*/ + + function safeTransferFrom( + ERC20 token, + address from, + address to, + uint256 amount + ) internal { + bool success; + + assembly { + // Get a pointer to some free memory. + let freeMemoryPointer := mload(0x40) + + // Write the abi-encoded calldata into memory, beginning with the function selector. + mstore(freeMemoryPointer, 0x23b872dd00000000000000000000000000000000000000000000000000000000) + mstore(add(freeMemoryPointer, 4), from) // Append the "from" argument. + mstore(add(freeMemoryPointer, 36), to) // Append the "to" argument. + mstore(add(freeMemoryPointer, 68), amount) // Append the "amount" argument. + + success := and( + // Set success to whether the call reverted, if not we check it either + // returned exactly 1 (can't just be non-zero data), or had no return data. + or(and(eq(mload(0), 1), gt(returndatasize(), 31)), iszero(returndatasize())), + // We use 100 because the length of our calldata totals up like so: 4 + 32 * 3. + // We use 0 and 32 to copy up to 32 bytes of return data into the scratch space. + // Counterintuitively, this call must be positioned second to the or() call in the + // surrounding and() call or else returndatasize() will be zero during the computation. + call(gas(), token, 0, freeMemoryPointer, 100, 0, 32) + ) + } + + require(success, "TRANSFER_FROM_FAILED"); + } + + function safeTransfer( + ERC20 token, + address to, + uint256 amount + ) internal { + bool success; + + assembly { + // Get a pointer to some free memory. + let freeMemoryPointer := mload(0x40) + + // Write the abi-encoded calldata into memory, beginning with the function selector. + mstore(freeMemoryPointer, 0xa9059cbb00000000000000000000000000000000000000000000000000000000) + mstore(add(freeMemoryPointer, 4), to) // Append the "to" argument. + mstore(add(freeMemoryPointer, 36), amount) // Append the "amount" argument. + + success := and( + // Set success to whether the call reverted, if not we check it either + // returned exactly 1 (can't just be non-zero data), or had no return data. + or(and(eq(mload(0), 1), gt(returndatasize(), 31)), iszero(returndatasize())), + // We use 68 because the length of our calldata totals up like so: 4 + 32 * 2. + // We use 0 and 32 to copy up to 32 bytes of return data into the scratch space. + // Counterintuitively, this call must be positioned second to the or() call in the + // surrounding and() call or else returndatasize() will be zero during the computation. + call(gas(), token, 0, freeMemoryPointer, 68, 0, 32) + ) + } + + require(success, "TRANSFER_FAILED"); + } + + function safeApprove( + ERC20 token, + address to, + uint256 amount + ) internal { + bool success; + + assembly { + // Get a pointer to some free memory. + let freeMemoryPointer := mload(0x40) + + // Write the abi-encoded calldata into memory, beginning with the function selector. + mstore(freeMemoryPointer, 0x095ea7b300000000000000000000000000000000000000000000000000000000) + mstore(add(freeMemoryPointer, 4), to) // Append the "to" argument. + mstore(add(freeMemoryPointer, 36), amount) // Append the "amount" argument. + + success := and( + // Set success to whether the call reverted, if not we check it either + // returned exactly 1 (can't just be non-zero data), or had no return data. + or(and(eq(mload(0), 1), gt(returndatasize(), 31)), iszero(returndatasize())), + // We use 68 because the length of our calldata totals up like so: 4 + 32 * 2. + // We use 0 and 32 to copy up to 32 bytes of return data into the scratch space. + // Counterintuitively, this call must be positioned second to the or() call in the + // surrounding and() call or else returndatasize() will be zero during the computation. + call(gas(), token, 0, freeMemoryPointer, 68, 0, 32) + ) + } + + require(success, "APPROVE_FAILED"); + } +} diff --git a/lesson4_reading/erc4626/src/tokens/ERC20.sol b/lesson4_reading/erc4626/src/tokens/ERC20.sol new file mode 100644 index 0000000..99217dd --- /dev/null +++ b/lesson4_reading/erc4626/src/tokens/ERC20.sol @@ -0,0 +1,116 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +/// @notice Modern and gas efficient ERC20 implementation. +/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol) +/// @author Modified from Uniswap +/// (https://github.com/Uniswap/uniswap-v2-core/blob/master/contracts/UniswapV2ERC20.sol) +/// @dev Do not manually set balances without updating totalSupply, as the sum of all +/// user balances must not exceed it. +contract ERC20 { + // EVENTS + + event Transfer(address indexed from, address indexed to, uint256 amount); + + event Approval(address indexed owner, address indexed spender, uint256 amount); + + // METADATA STORAGE + + string public name; + + string public symbol; + + uint8 public immutable decimals; + + // ERC20 STORAGE + + uint256 public totalSupply; + + mapping(address => uint256) public balanceOf; + + mapping(address => mapping(address => uint256)) public allowance; + + // CONSTRUCTOR + + constructor( + string memory _name, + string memory _symbol, + uint8 _decimals + ) { + name = _name; + symbol = _symbol; + decimals = _decimals; + } + + // ERC20 LOGIC + + function approve(address spender, uint256 amount) public virtual returns (bool) { + allowance[msg.sender][spender] = amount; + + emit Approval(msg.sender, spender, amount); + + return true; + } + + function transfer(address to, uint256 amount) public virtual returns (bool) { + balanceOf[msg.sender] -= amount; + + // Cannot overflow because the sum of all user + // balances can't exceed the max uint256 value. + unchecked { + balanceOf[to] += amount; + } + + emit Transfer(msg.sender, to, amount); + + return true; + } + + function transferFrom( + address from, + address to, + uint256 amount + ) public virtual returns (bool) { + uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals. + + if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount; + + balanceOf[from] -= amount; + + // Cannot overflow because the sum of all user + // balances can't exceed the max uint256 value. + unchecked { + balanceOf[to] += amount; + } + + emit Transfer(from, to, amount); + + return true; + } + + // INTERNAL MINT/BURN LOGIC + + function _mint(address to, uint256 amount) internal virtual { + totalSupply += amount; + + // Cannot overflow because the sum of all user + // balances can't exceed the max uint256 value. + unchecked { + balanceOf[to] += amount; + } + + emit Transfer(address(0), to, amount); + } + + function _burn(address from, uint256 amount) internal virtual { + balanceOf[from] -= amount; + + // Cannot underflow because a user's balance + // will never be larger than the total supply. + unchecked { + totalSupply -= amount; + } + + emit Transfer(from, address(0), amount); + } +}