chore: Added certora CI workflow

liquid-collective · Oct 21, 2024 · 358cc59 · 358cc59
1 parent 53d70ab
commit 358cc59
Show file tree

Hide file tree

Showing 56 changed files with 6,818 additions and 0 deletions.
diff --git a/.github/workflows/Certora.yaml b/.github/workflows/Certora.yaml
@@ -0,0 +1,55 @@
+name: Certora verification
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+      - name: Install forge dependencies
+        run: forge install
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with:
+          python-version: '3.10'
+          cache: 'pip'
+
+      - name: Install certora
+        run: pip3 install certora-cli
+
+      - name: Install solc
+        run: |
+          pip install solc-select
+          solc-select install 0.8.20
+          solc-select use 0.8.20
+
+      - name: Verify conf ${{ matrix.params.name }}
+        run: >
+          message="$(git log -n 1 --pretty=format:'CI ${{matrix.params.name}} %h .... %s')";
+          certoraRun \
+            certora/confs_for_CI/${{ matrix.params.command }} \
+            --msg "$(echo $message | sed 's/[^a-zA-Z0-9., _-]/ /g')"
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        params: 
+          - {name: AllowlistV1, command: 'AllowlistV1.conf'} 
+          - {name: OperatorRegistryV1_1, command: 'OperatorRegistryV1_1.conf'} 
+          - {name: OperatorRegistryV1_2_2loops, command: 'OperatorRegistryV1_2_2loops.conf'} 
+          - {name: OperatorRegistryV1_2_4loops_v1, command: 'OperatorRegistryV1_2_4loops_v1.conf'} 
+          - {name: OperatorRegistryV1_2_4loops_v2, command: 'OperatorRegistryV1_2_4loops_v2.conf'} 
+          - {name: OperatorRegistryV1_3, command: 'OperatorRegistryV1_3.conf'} 
+          - {name: RedeemManagerV1, command: 'RedeemManagerV1.conf'} 
+          - {name: RiverV1, command: 'RiverV1.conf'} 
+          - {name: SharesManagerV1, command: 'SharesManagerV1.conf'} 
diff --git a/.gitignore b/.gitignore
@@ -26,3 +26,20 @@ deployments/tenderly
 .DS_Store
 .idea
 lcov.info
+
+
+# certora
+certora/munged*
+certora/diagrams*
+.certora*
+.certora*.json
+**.last_conf*
+certora-logs
+.certora_internal*
+certora_debug_log.txt
+resource_errors.json
+.zip-output-url.txt
+timeoutsToInvestigate/*
+emv-**/*
+
+runRiver.sh
diff --git a/certora/Makefile b/certora/Makefile
@@ -0,0 +1,59 @@
+default: help
+
+PATCH         = applyHarness.patch
+MUNGED_DIR    = ./munged
+CONTRACTS_DIR = ../contracts/src
+file1_origin = ../contracts/src/RedeemManager.1.sol
+file1_munged = ./munged/RedeemManager.1.sol
+file1_copy = ./munged/RedeemManager_origin.1.sol
+file2_origin = ../contracts/src/River.1.sol
+file2_munged = ./munged/River.1.sol
+file2_copy = ./munged/River_origin.1.sol
+file3_origin = ../contracts/src/components/SharesManager.1.sol
+file3_munged = ./munged/SharesManager.1.sol
+file3_copy = ./munged/SharesManager_origin.1.sol
+file4_origin = ../contracts/src/components/OracleManager.1.sol
+file4_munged = ./munged/OracleManager.1.sol
+file4_copy = ./munged/OracleManager_origin.1.sol
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(file1_munged) and $(file1_origin)"
+
+munge:
+	mkdir -p $(MUNGED_DIR)
+	cp $(file1_origin) $(file1_munged)
+	cp $(file1_origin) $(file1_copy)
+	cp $(file2_origin) $(file2_munged)
+	cp $(file2_origin) $(file2_copy)
+	cp $(file3_origin) $(file3_munged)
+	cp $(file3_origin) $(file3_copy)
+	cp $(file4_origin) $(file4_munged)
+	cp $(file4_origin) $(file4_copy)
+	patch -d $(MUNGED_DIR) < $(PATCH)
+	mv $(file1_munged) $(file1_origin)
+	mv $(file2_munged) $(file2_origin)
+	mv $(file3_munged) $(file3_origin)
+	mv $(file4_munged) $(file4_origin)
+
+record:
+	diff -uN $(file1_origin) $(file1_munged) | sed 's+\$(file1_origin)/++g' | sed 's+$(file1_munged)++g' > $(PATCH)
+	diff -uN $(file2_origin) $(file2_munged) | sed 's+\$(file2_origin)/++g' | sed 's+$(file2_munged)++g' >> $(PATCH)
+	diff -uN $(file3_origin) $(file3_munged) | sed 's+\$(file3_origin)/++g' | sed 's+$(file3_munged)++g' >> $(PATCH)
+	diff -uN $(file4_origin) $(file4_munged) | sed 's+\$(file4_origin)/++g' | sed 's+$(file4_munged)++g' >> $(PATCH)
+
+revert:
+	cp $(file1_origin) $(file1_munged)
+	mv $(file1_copy) $(file1_origin)
+	cp $(file2_origin) $(file2_munged)
+	mv $(file2_copy) $(file2_origin)
+	cp $(file3_origin) $(file3_munged)
+	mv $(file3_copy) $(file3_origin)
+	cp $(file4_origin) $(file4_munged)
+	mv $(file4_copy) $(file4_origin)
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
@@ -0,0 +1,140 @@
+--- ../contracts/src/RedeemManager.1.sol	2024-01-29 15:39:54.964002324 +0200
++++ 	2024-01-29 15:48:14.633945763 +0200
+@@ -26,11 +26,11 @@
+     int64 internal constant RESOLVE_FULLY_CLAIMED = -3;
+
+     /// @notice Status value returned when fully claiming a redeem request
+-    uint8 internal constant CLAIM_FULLY_CLAIMED = 0;
++    uint8 public constant CLAIM_FULLY_CLAIMED = 0;
+     /// @notice Status value returned when partially claiming a redeem request
+-    uint8 internal constant CLAIM_PARTIALLY_CLAIMED = 1;
++    uint8 public constant CLAIM_PARTIALLY_CLAIMED = 1;
+     /// @notice Status value returned when a redeem request is already claimed and skipped during a claim
+-    uint8 internal constant CLAIM_SKIPPED = 2;
++    uint8 public constant CLAIM_SKIPPED = 2;
+
+     modifier onlyRiver() {
+         if (msg.sender != RiverAddress.get()) {
+@@ -369,12 +369,14 @@
+                 LibUint256.min(_params.redeemRequest.amount, withdrawalEventEndPosition - _params.redeemRequest.height);
+             // we can now compute the equivalent eth amount based on the withdrawal event details
+             vars.ethAmount =
+-                (vars.matchingAmount * _params.withdrawalEvent.withdrawnEth) / _params.withdrawalEvent.amount;
++            //    (vars.matchingAmount * _params.withdrawalEvent.withdrawnEth) / _params.withdrawalEvent.amount;
++            math.mulDiv(vars.matchingAmount, _params.withdrawalEvent.withdrawnEth, _params.withdrawalEvent.amount);
+
+             // as each request has a maximum withdrawable amount, we verify that the eth amount is not exceeding this amount, pro rata
+             // the amount that is matched
+             uint256 maxRedeemableEthAmount =
+-                (vars.matchingAmount * _params.redeemRequest.maxRedeemableEth) / _params.redeemRequest.amount;
++            //    (vars.matchingAmount * _params.redeemRequest.maxRedeemableEth) / _params.redeemRequest.amount;
++            math.mulDiv(vars.matchingAmount, _params.redeemRequest.maxRedeemableEth, _params.redeemRequest.amount);
+
+             if (maxRedeemableEthAmount < vars.ethAmount) {
+                 vars.exceedingEthAmount = vars.ethAmount - maxRedeemableEthAmount;
+@@ -529,3 +531,9 @@
+         RedeemDemand.set(_newValue);
+     }
+ }
++
++library math {
++    function mulDiv(uint256 x, uint256 y, uint256 z) internal pure returns (uint256) {
++        return (x * y) / z;
++    }
++}
+--- ../contracts/src/River.1.sol	2024-01-29 15:39:54.964002324 +0200
++++ 	2024-01-29 15:48:14.633945763 +0200
+@@ -369,9 +369,11 @@
+         }
+         uint256 newTotalBalance = _assetBalance();
+         uint256 globalFee = GlobalFee.get();
+-        uint256 numerator = _amount * oldTotalSupply * globalFee;
++        //uint256 numerator = _amount * oldTotalSupply * globalFee;
++        //uint256 denominator = (newTotalBalance * LibBasisPoints.BASIS_POINTS_MAX) - (_amount * globalFee);
++        //uint256 sharesToMint = denominator == 0 ? 0 : (numerator / denominator);
+         uint256 denominator = (newTotalBalance * LibBasisPoints.BASIS_POINTS_MAX) - (_amount * globalFee);
+-        uint256 sharesToMint = denominator == 0 ? 0 : (numerator / denominator);
++        uint256 sharesToMint = denominator == 0 ? 0 : math.mulDiv(_amount * oldTotalSupply, globalFee, denominator);
+
+         if (sharesToMint > 0) {
+             address collector = CollectorAddress.get();
+@@ -589,12 +591,15 @@
+         // this value is computed by subtracting the current balance to deposit from the underlying asset balance
+         uint256 currentMaxDailyCommittableAmount = LibUint256.max(
+             dcl.minDailyNetCommittableAmount,
+-            (uint256(dcl.maxDailyRelativeCommittableAmount) * (underlyingAssetBalance - currentBalanceToDeposit))
+-                / LibBasisPoints.BASIS_POINTS_MAX
++            //(uint256(dcl.maxDailyRelativeCommittableAmount) * (underlyingAssetBalance - currentBalanceToDeposit))
++            //    / LibBasisPoints.BASIS_POINTS_MAX
++            math.mulDiv(uint256(dcl.maxDailyRelativeCommittableAmount), 
++                underlyingAssetBalance - currentBalanceToDeposit, LibBasisPoints.BASIS_POINTS_MAX)
+         );
+         // we adapt the value for the reporting period by using the asset balance as upper bound
+         uint256 currentMaxCommittableAmount =
+-            LibUint256.min((currentMaxDailyCommittableAmount * _period) / 1 days, currentBalanceToDeposit);
++            //LibUint256.min((currentMaxDailyCommittableAmount * _period) / 1 days, currentBalanceToDeposit);
++            LibUint256.min(math.mulDiv(currentMaxDailyCommittableAmount, _period, 1 days), currentBalanceToDeposit);
+         // we only commit multiples of 32 ETH
+         currentMaxCommittableAmount = (currentMaxCommittableAmount / DEPOSIT_SIZE) * DEPOSIT_SIZE;
+
+--- ../contracts/src/components/SharesManager.1.sol	2024-01-29 15:39:54.974002324 +0200
++++ 	2024-01-29 15:48:14.643945761 +0200
+@@ -202,7 +202,8 @@
+             return 0;
+         }
+
+-        return ((_shares * _assetBalance())) / _totalSharesValue;
++        //return ((_shares * _assetBalance())) / _totalSharesValue;
++        return math.mulDiv(_shares, _assetBalance(), _totalSharesValue);
+     }
+
+     /// @notice Internal utility to retrieve the shares count for a given underlying asset amount
+@@ -215,7 +216,8 @@
+             return 0;
+         }
+
+-        return (_balance * _totalSharesValue) / _assetBalance();
++        //return (_balance * _totalSharesValue) / _assetBalance();
++        return  math.mulDiv(_balance, _totalSharesValue, _assetBalance());
+     }
+
+     /// @notice Internal utility to mint shares for the specified user
+@@ -230,7 +232,8 @@
+             sharesToMint = _underlyingAssetValue;
+             _mintRawShares(_owner, _underlyingAssetValue);
+         } else {
+-            sharesToMint = (_underlyingAssetValue * _totalSupply()) / oldTotalAssetBalance;
++            //sharesToMint = (_underlyingAssetValue * _totalSupply()) / oldTotalAssetBalance;
++            sharesToMint = math.mulDiv(_underlyingAssetValue, _totalSupply(), oldTotalAssetBalance);
+             _mintRawShares(_owner, sharesToMint);
+         }
+     }
+@@ -267,3 +270,10 @@
+         emit SetTotalSupply(newTotalSupply);
+     }
+ }
++
++library math {
++    function mulDiv(uint256 x, uint256 y, uint256 z) internal pure returns (uint256) {
++        return (x * y) / z;
++    }
++}
++
+--- ../contracts/src/components/OracleManager.1.sol	2024-01-29 15:39:54.974002324 +0200
++++ 	2024-01-29 15:48:14.643945761 +0200
+@@ -256,7 +256,7 @@
+     }
+
+     /// @inheritdoc IOracleManagerV1
+-    function setConsensusLayerData(IOracleManagerV1.ConsensusLayerReport calldata _report) external {
++    function setConsensusLayerData(IOracleManagerV1.ConsensusLayerReport calldata _report) external virtual {
+         // only the oracle is allowed to call this endpoint
+         if (msg.sender != OracleAddress.get()) {
+             revert LibErrors.Unauthorized(msg.sender);
+@@ -494,4 +494,4 @@
+     {
+         return (_epochNow - _epochPast) * (_cls.secondsPerSlot * _cls.slotsPerEpoch);
+     }
+-}
++}
+\ No newline at end of file
diff --git a/certora/conf/AllowlistV1.conf b/certora/conf/AllowlistV1.conf
@@ -0,0 +1,25 @@
+{
+  "files": [
+    // "certora/harness/RiverV1Harness.sol",
+    "contracts/src/Allowlist.1.sol:AllowlistV1",
+    // "contracts/src/CoverageFund.1.sol:CoverageFundV1",
+    // "contracts/src/ELFeeRecipient.1.sol:ELFeeRecipientV1",
+    // "contracts/src/OperatorsRegistry.1.sol:OperatorsRegistryV1",
+    // "certora/harness/RedeemManagerV1Harness.sol",
+    // "contracts/src/Withdraw.1.sol:WithdrawV1",
+  ],
+  "verify": "AllowlistV1:certora/specs/AllowlistV1.spec",
+  "link" : [],
+  "rule_sanity": "basic",
+  "loop_iter": "5",
+  "optimistic_loop": true,
+  "packages": ["openzeppelin-contracts=lib/openzeppelin-contracts"],
+  "optimistic_hashing": true,
+  "solc": "solc8.20",
+  "prover_args": ["-cache none"],
+  "optimistic_summary_recursion": true,
+  "summary_recursion_limit" : "1",
+  // "parametric_contracts": ["AllowlistV1"],
+  "msg": "AllowlistV1",
+  //"rule": ["method_reachability"],
+}
diff --git a/certora/conf/ConsensusLayerDepositManagerV1.conf b/certora/conf/ConsensusLayerDepositManagerV1.conf
@@ -0,0 +1,31 @@
+{
+  "files": [
+    "certora/harness/RiverV1Harness.sol",
+    "certora/munged/contracts/src/Allowlist.1.sol:AllowlistV1",
+    "certora/munged/contracts/src/CoverageFund.1.sol:CoverageFundV1",
+    "certora/munged/contracts/src/ELFeeRecipient.1.sol:ELFeeRecipientV1",
+    "certora/munged/contracts/src/OperatorsRegistry.1.sol:OperatorsRegistryV1",
+    "certora/harness/RedeemManagerV1Harness.sol",
+    "certora/munged/contracts/src/Withdraw.1.sol:WithdrawV1",
+    // "certora/munged/contracts/src/mock/DepositContractMock.sol", // This is needed only when working with the Ethereum network outside.
+  ],
+  "verify": "RiverV1Harness:certora/specs/ConsensusLayerDepositManagerV1.spec",
+  "link" : [],
+  "rule_sanity": "basic",
+  "loop_iter": "2", // Lets use smaller numbers, like 1,2 or 3. Later try 5.
+  "optimistic_loop": true,
+  "packages": ["openzeppelin-contracts=lib/openzeppelin-contracts"],
+  "optimistic_hashing": true,
+  "solc": "solc8.20",
+  "global_timeout": "7198",
+  "prover_args": [
+    " -contractRecursionLimit 1", // River.resolveRedeemRequests(uint32[]) calls RedeemManager.resolveRedeemRequests(uint32[]) 
+    " -optimisticFallback true", // does not take to much additional time
+    "-depth 11"
+    ],
+  "optimistic_summary_recursion": true,
+  "summary_recursion_limit" : "1",
+  "parametric_contracts": ["RiverV1Harness"],
+  "msg": "ConsensusLayerDepositManagerV1",
+  "rule": ["method_reachability"],
+}
diff --git a/certora/conf/CoverageFundV1.conf b/certora/conf/CoverageFundV1.conf
@@ -0,0 +1,23 @@
+{
+  "files": [
+    "certora/munged/contracts/src/CoverageFund.1.sol:CoverageFundV1",
+  ],
+  "verify": "CoverageFundV1:certora/specs/CoverageFundV1.spec",
+  "link" : [],
+  "rule_sanity": "basic",
+  "loop_iter": "2", // Lets use smaller numbers, like 1,2 or 3. Later try 5.
+  "optimistic_loop": true,
+  "packages": ["openzeppelin-contracts=lib/openzeppelin-contracts"],
+  "optimistic_hashing": true,
+  "solc": "solc8.20",
+  "global_timeout": "7198",
+  "prover_args": [
+    " -contractRecursionLimit 1", // River.resolveRedeemRequests(uint32[]) calls RedeemManager.resolveRedeemRequests(uint32[]) 
+    " -optimisticFallback true", // does not take to much additional time
+    "-depth 11"
+    ],
+  "optimistic_summary_recursion": true,
+  "summary_recursion_limit" : "1",
+  "msg": "CoverageFundV1",
+  "rule": ["method_reachability"],
+}
diff --git a/certora/conf/Firewall.conf b/certora/conf/Firewall.conf
@@ -0,0 +1,23 @@
+{
+  "files": [
+    "certora/munged/contracts/src/Firewall.sol",
+  ],
+  "verify": "Firewall:certora/specs/Firewall.spec",
+  "link" : [],
+  "rule_sanity": "basic",
+  "loop_iter": "2", // Lets use smaller numbers, like 1,2 or 3. Later try 5.
+  "optimistic_loop": true,
+  "packages": ["openzeppelin-contracts=lib/openzeppelin-contracts"],
+  "optimistic_hashing": true,
+  "solc": "solc8.20",
+  "global_timeout": "7198",
+  "prover_args": [
+    " -contractRecursionLimit 1", // River.resolveRedeemRequests(uint32[]) calls RedeemManager.resolveRedeemRequests(uint32[]) 
+    " -optimisticFallback true", // does not take to much additional time
+    "-depth 11"
+    ],
+  "optimistic_summary_recursion": true,
+  "summary_recursion_limit" : "1",
+  "msg": "Firewall",
+  "rule": ["method_reachability"],
+}