Merge pull request #14 from euler-xyz/main

License

.github/workflows/certora.yml

@@ -0,0 +1,106 @@
+# 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: {}
+  workflow_dispatch: {}
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    steps:
+      # check out the current version
+      - uses: actions/checkout@v4
+        with:
+            token: ${{ secrets.GITHUB_TOKEN }}
+            submodules: recursive
+
+      # 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: |
+          pip install solc-select
+          solc-select install 0.8.20
+          solc-select use 0.8.20
+        # It is also possible to download the solc binaries directly
+        # 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
+        # ln -s /usr/local/bin/solc8.0 /usr/local/bin/solc
+
+      # 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
+      #
+      # 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')";
+            ./formal-verification/run.sh ${{ 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/<contents of the command>
+          #
+          # 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'}
+          #- {name: generalRulesOnERC20, command: 'generalRules_ERC20'}
+          #- {name: generalRulesOnVAULT, command: 'generalRules_VAULT'}
+          - {name: RulesForFeeFlowController, command: 'default'}
+

formal-verification/certora/harnesses/FeeFlowControllerHarness.sol

@@ -42,19 +42,27 @@ contract FeeFlowControllerHarness is FeeFlowController {
     }
 
     function getInitPrice() external view returns (uint256) {
-        return slot1.initPrice;
+        return slot0.initPrice;
     }
 
     function getStartTime() external view returns (uint256) {
-        return slot1.startTime;
+        return slot0.startTime;
+    }
+
+    function getEpochId() external view returns (uint256) {
+        return slot0.epochId;
     }
 
     // address immutable public paymentReceiver;
     function getPaymentReceiver() external view returns (address) {
         return paymentReceiver;
     }
-    // uint256 immutable public epochPeriod;
+
+    function getPaymentToken() external view returns (address) {
+        return address(paymentToken);
+    }
 
+    // uint256 immutable public epochPeriod;
     function getEpochPeriod() external view returns (uint256) {
         return epochPeriod;
     }

formal-verification/certora/specs/FeeFlowController.spec

@@ -67,9 +67,10 @@ function initialStateAssertions(env e) {
 	assert e.block.timestamp >= startTime, "e.block.timestamp >= startTime";
 }
 
-function requirementsForBuyExecution(env e, address[] assets, address assetsReceiver, uint256 deadline, uint256 maxPaymentTokenAmount) {
+function requirementsForSuccessfulBuyExecution(env e, address[] assets, address assetsReceiver,uint256 epochId, uint256 deadline, uint256 maxPaymentTokenAmount) {
 	reentrancyMock(); // this sets the lock to the correct initial value
 	uint256 initPriceStart = getInitPrice();
+	require(epochId == getEpochId());
 	require(maxPaymentTokenAmount > initPriceStart);
 	require(e.block.timestamp <= deadline);
 	uint256 paymentAmount = getPrice(e);
@@ -100,6 +101,10 @@ persistent ghost bool reentrancy_happened {
     init_state axiom !reentrancy_happened;
 }
 
+persistent ghost bool reverted {
+	init_state axiom !reverted;
+}
+
 hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, 
           uint retOffset, uint retLength) uint rc {
     if (addr == currentContract) {
@@ -108,13 +113,17 @@ hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength,
     }
 }
 
+hook REVERT(uint offset, uint size) {
+	reverted = true;
+}
 
 // Invariants
 // NOTE: we are executing optimistic dispatches for the ERC20 tokens
-invariant invariant_no_reentrant_calls() !reentrancy_happened;
+invariant invariant_no_reentrant_calls() !reentrancy_happened || reentrancy_happened && reverted;
 invariant invariant_init_price_must_be_in_range() getInitPrice() >= getMinInitPrice() && getInitPrice() <= getABS_MAX_INIT_PRICE();
 invariant invariant_price_must_be_below_max_init_price(env e) getPrice(e) <= getInitPrice();
 
+
 // Rules
 rule reachability(method f)
 {
@@ -124,7 +133,7 @@ rule reachability(method f)
 	satisfy true, "a non-reverting path through this method was found";
 }
 
-rule check_initailStateAssertionsAfterBuy() {
+rule check_constructorAssumptionsSatisfiedAfterBuy() {
 	env e;
 	constructorAssumptions(e);
 	calldataarg args;
@@ -135,19 +144,19 @@ rule check_initailStateAssertionsAfterBuy() {
 rule check_buyNeverRevertsUnexpectedly() {
 	env e;
 	constructorAssumptions(e);
-	address[] assets; address assetsReceiver; uint256 deadline; uint256 maxPaymentTokenAmount;
-	requirementsForBuyExecution(e, assets, assetsReceiver, deadline, maxPaymentTokenAmount);
-	buy@withrevert(e, assets, assetsReceiver, deadline, maxPaymentTokenAmount);
+	address[] assets; address assetsReceiver; uint256 epochId; uint256 deadline; uint256 maxPaymentTokenAmount;
+	requirementsForSuccessfulBuyExecution(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
+	buy@withrevert(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
 	assert !lastReverted, "buy never reverts with arithmetic exceptions or internal solidity reverts";
 }
 
 rule check_buyNextInitPriceAtLeastBuyPriceTimesMultiplier() {
 	env e;
 	constructorAssumptions(e);
 	calldataarg args;
-	address[] assets; address assetsReceiver; uint256 deadline; uint256 maxPaymentTokenAmount;
-	requirementsForBuyExecution(e, assets, assetsReceiver, deadline, maxPaymentTokenAmount);
-	mathint paymentAmount = buy@withrevert(e, assets, assetsReceiver, deadline, maxPaymentTokenAmount);
+	address[] assets; address assetsReceiver; uint256 epochId; uint256 deadline; uint256 maxPaymentTokenAmount;
+	requirementsForSuccessfulBuyExecution(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
+	mathint paymentAmount = buy@withrevert(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
 
 	mathint priceMultiplier = getPriceMultiplier();
 	mathint PRICE_MULTIPLIER_SCALE = getPRICE_MULTIPLIER_SCALE();
@@ -166,3 +175,108 @@ rule check_buyNextInitPriceAtLeastBuyPriceTimesMultiplier() {
 		}
 	}
 }
+
+// Balance of fee flow controller of a bought asset is always 0 after buy
+rule check_feeFlowControllerTokenBalanceOfAfterBuy() {
+	env e;
+	constructorAssumptions(e);
+	address[] assets; address assetsReceiver; uint256 epochId; uint256 deadline; uint256 maxPaymentTokenAmount;
+
+	require(assets.length == 1); // making 1 transfer for simplicity and since we have no loops in CVL
+	require(assetsReceiver != feeFlowController); // make sure the receiver is not feeFlowController
+
+	buy(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
+	uint256 feeControllerTokenBalance = feeFlowController.getTokenBalanceOf(e, assets[0], feeFlowController);
+	assert feeControllerTokenBalance == 0, "feeFlowController.getTokenBalanceOf(assets[0], feeFlowController) == 0";
+}
+
+// Balance of asset receiver is incremented by balance of fee flow controller after buy
+rule check_balanceOfAssetsReceiverIsIncrementedByFeeFlowControllerTokenBalanceOfAfterBuy() {
+	env e;
+	constructorAssumptions(e);
+	address[] assets; address assetsReceiver; uint256 epochId; uint256 deadline; uint256 maxPaymentTokenAmount;
+
+	require(assets.length == 1); // making 1 transfer for simplicity and since we have no loops in CVL
+
+	require(assetsReceiver != feeFlowController); // make sure the receiver is not feeFlowController
+	require(assets[0] != getPaymentToken()); // make sure the asset is not the payment token
+
+	uint256 assetReceiverTokenBalance = feeFlowController.getTokenBalanceOf(e, assets[0], assetsReceiver);
+	uint256 feeControllerTokenBalance = feeFlowController.getTokenBalanceOf(e, assets[0], feeFlowController);
+	uint256 assetReceiverTokenBalanceAfterPredicted = require_uint256(feeControllerTokenBalance + assetReceiverTokenBalance);
+
+	buy(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
+
+	assert feeFlowController.getTokenBalanceOf(e, assets[0], assetsReceiver) == assetReceiverTokenBalanceAfterPredicted, "feeFlowController.getTokenBalanceOf(assets[0], assetsReceiver) == assetReceiverTokenBalanceAfter";
+}
+
+// Balance of buyer is reduced by payment amount, and never by more than max payment amount
+rule check_balanceOfBuyerIsReducedByPaymentAmount() {
+	env e;
+	constructorAssumptions(e);
+	address[] assets; address assetsReceiver; uint256 epochId; uint256 deadline; uint256 maxPaymentTokenAmount;
+
+	require(assets.length == 1); // making 1 transfer for simplicity and since we have no loops in CVL
+
+	require(assetsReceiver != feeFlowController); // make sure the receiver is not feeFlowController
+	require(assets[0] != getPaymentToken()); // make sure the asset is not the payment toke
+	require(getPaymentReceiver() != e.msg.sender); // make sure the payment receiver is not the buyer
+
+	uint256 paymentAmount = getPrice(e);
+	uint256 balanceBefore = feeFlowController.getPaymentTokenBalanceOf(e, e.msg.sender);
+	buy(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
+	uint256 balanceAfter = feeFlowController.getPaymentTokenBalanceOf(e, e.msg.sender);
+	assert to_mathint(balanceAfter) == (balanceBefore - paymentAmount), "msg.sender (PaymentToken) => balanceAfter == (balanceBefore - paymentAmount)";
+}
+
+// Balance of payment receiver is increased by payment amount
+rule check_balanceOfPaymentReceiverIsIncreasedByPaymentAmount() {
+	env e;
+	constructorAssumptions(e);
+	address[] assets; address assetsReceiver; uint256 epochId; uint256 deadline; uint256 maxPaymentTokenAmount;
+
+	require(assets.length == 1); // making 1 transfer for simplicity and since we have no loops in CVL
+
+	require(assetsReceiver != feeFlowController); // make sure the receiver is not feeFlowController
+	require(assets[0] != getPaymentToken()); // make sure the asset is not the payment token
+	require(getPaymentReceiver() != e.msg.sender); // make sure the payment receiver is not the buyer
+
+	uint256 paymentAmount = getPrice(e);
+	address paymentReceiver = getPaymentReceiver();
+
+	uint256 balanceBefore = feeFlowController.getPaymentTokenBalanceOf(e, paymentReceiver);
+	buy(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
+	uint256 balanceAfter = feeFlowController.getPaymentTokenBalanceOf(e, paymentReceiver);
+	assert to_mathint(balanceAfter) == (balanceBefore + paymentAmount), "paymentReceiver (PaymentToken) => balanceAfter == (balanceBefore + paymentAmount)";
+}
+
+// Payment amount returned on buy is never higher than maximum payout
+rule check_paymentAmountReturnedOnBuyIsNeverHigherThanMaximumPayout() {
+	env e;
+	constructorAssumptions(e);
+	address[] assets; address assetsReceiver; uint256 epochId; uint256 deadline; uint256 maxPaymentTokenAmount;
+
+	require(assets.length == 1); // making 1 transfer for simplicity and since we have no loops in CVL
+
+	require(assetsReceiver != feeFlowController); // make sure the receiver is not feeFlowController
+	require(assets[0] != getPaymentToken()); // make sure the asset is not the payment token
+	require(getPaymentReceiver() != e.msg.sender); // make sure the payment receiver is not the buyer
+
+	uint256 paymentAmount = getPrice(e);
+	uint256 balanceBefore = feeFlowController.getPaymentTokenBalanceOf(e, assetsReceiver);
+	buy(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
+	uint256 balanceAfter = feeFlowController.getPaymentTokenBalanceOf(e, assetsReceiver);
+	assert paymentAmount <= maxPaymentTokenAmount, "paymentAmount <= maxPaymentTokenAmount";
+	assert to_mathint(balanceAfter) <= (balanceBefore + maxPaymentTokenAmount), "balanceAfter <= (balanceBefore + maxPaymentTokenAmount)";
+}
+
+// Epoch Id is always incremented by 1 after buy (and becomes 0 if it reaches max uint16)
+rule check_epochIdAlwaysIncrementedBy1AfterBuy() {
+	env e;
+	constructorAssumptions(e);
+	address[] assets; address assetsReceiver; uint256 epochId; uint256 deadline; uint256 maxPaymentTokenAmount;
+	uint256 epochIdBefore = getEpochId();
+	buy(e, assets, assetsReceiver, epochId, deadline, maxPaymentTokenAmount);
+	uint256 epochIdAfter = getEpochId();
+	assert (epochIdAfter == 0 && epochIdBefore == max_uint16) || epochIdAfter == assert_uint256(epochIdBefore + 1), "epochIdAfter == (epochIdBefore + 1) || (epochIdAfter == 0 && epochIdBefore == 65535)";
+}

formal-verification/certora/specs/methods/IFeeFlowController.spec

@@ -1,5 +1,5 @@
 methods {
-	function buy(address[] assets, address assetsReceiver, uint256 deadline, uint256 maxPaymentTokenAmount) external returns(uint256) => HAVOC_ECF; // nonReentrant summary
+	function buy(address[] assets, address assetsReceiver, uint256 epochId, uint256 deadline, uint256 maxPaymentTokenAmount) external returns(uint256) => HAVOC_ECF; // nonReentrant summary
     function getPrice() external returns(uint256);
     function paymentReceiver() external returns(address) envfree => CONSTANT;
     function reentrancyMock() external envfree;
@@ -12,7 +12,9 @@ methods {
 	function getMinInitPrice() external returns (uint256) envfree;
 	function getInitPrice() external returns (uint256) envfree;
     function getStartTime() external returns (uint256) envfree; 
+    function getEpochId() external returns (uint256) envfree;
     function getPaymentReceiver() external returns (address) envfree; 
+    function getPaymentToken() external returns (address) envfree;
     function getEpochPeriod() external returns (uint256) envfree; 
     function getPriceMultiplier() external returns (uint256) envfree; 
     // function getMsgSender() external returns (address) envfree;

formal-verification/run.sh

@@ -5,4 +5,11 @@ echo "Running make record"
 
 "$SCRIPT_DIR"/make-patch.sh
 
-certoraRun  "$SCRIPT_DIR"/certora/conf/default.conf
+# get any args passed to this script
+args=("$@")
+
+# if the arg is only one, then it is the file name
+FILE_NAME=$1
+# append all the rest of args 
+REST_OF_ARGS=${args[@]:1}
+certoraRun  "$SCRIPT_DIR"/certora/conf/"$FILE_NAME".conf $REST_OF_ARGS