Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 44 additions & 0 deletions .github/workflows/certora.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
name: Certora

on:
push:
branches:
- main
pull_request:
workflow_dispatch:

jobs:
verify:
runs-on: ubuntu-latest

steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
with:
submodules: recursive

- uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5
with:
distribution: temurin
java-version: "21"

- uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6
with:
python-version: ">=3.11"

- name: Install certora
run: pip install certora-cli

- name: Install solc (0.8.21)
env:
EXPECTED_SOLC_SHA256: f2857a898be15c69e8de5598dcd3f3e169e94964a0ce9a0bbb1b111f145a81df
run: |
wget https://github.com/ethereum/solidity/releases/download/v0.8.21/solc-static-linux
actual="$(sha256sum solc-static-linux | awk '{print $1}')"
[ "$actual" = "$EXPECTED_SOLC_SHA256" ] || { echo "solc hash mismatch"; exit 1; }
chmod +x solc-static-linux
sudo mv solc-static-linux /usr/local/bin/solc-0.8.21

- name: Verify MorphoChainlinkOracleV2 specification
run: certoraRun certora/confs/MorphoChainlinkOracleV2.conf
env:
CERTORAKEY: ${{ secrets.CERTORAKEY }}
12 changes: 12 additions & 0 deletions certora/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
This folder contains the verification of MorphoChainlinkOracleV2 using CVL, Certora's Verification Language.

# Getting started

Install the `certora-cli` package with `pip install certora-cli`.
The verification requires `solc-0.8.21` and the `CERTORAKEY` environment variable to be set to a valid Certora key.

To prove that every successful deployment has a non-zero scale factor, run from the repository root:

```bash
certoraRun certora/confs/MorphoChainlinkOracleV2.conf --rule scaleFactorCannotBeZero
```
14 changes: 14 additions & 0 deletions certora/confs/MorphoChainlinkOracleV2.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
{
"files": [
"certora/helpers/MorphoChainlinkOracleV2Harness.sol"
],
"solc": "solc-0.8.21",
"solc_evm_version": "paris",
"solc_optimize": "999999",
"solc_via_ir": true,
"verify": "MorphoChainlinkOracleV2Harness:certora/specs/MorphoChainlinkOracleV2.spec",
"optimistic_loop": true,
"rule_sanity": "basic",
"server": "production",
"msg": "MorphoChainlinkOracleV2 scale factor"
}
45 changes: 45 additions & 0 deletions certora/helpers/MorphoChainlinkOracleV2Harness.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
// SPDX-License-Identifier: GPL-2.0-or-later
pragma solidity 0.8.21;

import {MorphoChainlinkOracleV2} from "../../src/morpho-chainlink/MorphoChainlinkOracleV2.sol";
import {AggregatorV3Interface} from "../../src/morpho-chainlink/interfaces/AggregatorV3Interface.sol";
import {IERC4626} from "../../src/morpho-chainlink/interfaces/IERC4626.sol";

contract MorphoChainlinkOracleV2Harness is MorphoChainlinkOracleV2 {
constructor()
MorphoChainlinkOracleV2(
IERC4626(address(0)),
1,
AggregatorV3Interface(address(0)),
AggregatorV3Interface(address(0)),
0,
IERC4626(address(0)),
1,
AggregatorV3Interface(address(0)),
AggregatorV3Interface(address(0)),
0
)
{}

function computeScaleFactor(
uint256 quoteTokenDecimals,
uint256 quoteFeed1Decimals,
uint256 quoteFeed2Decimals,
uint256 baseTokenDecimals,
uint256 baseFeed1Decimals,
uint256 baseFeed2Decimals,
uint256 quoteVaultConversionSample,
uint256 baseVaultConversionSample
) external pure returns (uint256) {
return _scaleFactor(
quoteTokenDecimals,
quoteFeed1Decimals,
quoteFeed2Decimals,
baseTokenDecimals,
baseFeed1Decimals,
baseFeed2Decimals,
quoteVaultConversionSample,
baseVaultConversionSample
);
}
}
14 changes: 14 additions & 0 deletions certora/specs/MorphoChainlinkOracleV2.spec
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
// SPDX-License-Identifier: GPL-2.0-or-later

methods {
function computeScaleFactor(uint256, uint256, uint256, uint256, uint256, uint256, uint256, uint256) external returns (uint256) envfree;
}

// Checks that every successful scale factor computation returns a non-zero value.
rule scaleFactorCannotBeZero(uint256 quoteTokenDecimals, uint256 quoteFeed1Decimals, uint256 quoteFeed2Decimals, uint256 baseTokenDecimals, uint256 baseFeed1Decimals, uint256 baseFeed2Decimals, uint256 quoteVaultConversionSample, uint256 baseVaultConversionSample) {
uint256 scaleFactor = computeScaleFactor@withrevert(quoteTokenDecimals, quoteFeed1Decimals, quoteFeed2Decimals, baseTokenDecimals, baseFeed1Decimals, baseFeed2Decimals, quoteVaultConversionSample, baseVaultConversionSample);

require !lastReverted;

assert scaleFactor != 0, "scale factor is zero after a successful computation";
}
33 changes: 28 additions & 5 deletions src/morpho-chainlink/MorphoChainlinkOracleV2.sol
Original file line number Diff line number Diff line change
Expand Up @@ -134,14 +134,37 @@ contract MorphoChainlinkOracleV2 is IMorphoChainlinkOracleV2 {

// So SCALE_FACTOR = 1e36 * 1e(-dB1) * 1e(dQ1) * 1e(-fpB1) * 1e(-fpB2) * 1e(fpQ1) * 1e(fpQ2)
// = 1e(36 + dQ1 + fpQ1 + fpQ2 - dB1 - fpB1 - fpB2)
SCALE_FACTOR = 10
SCALE_FACTOR = _scaleFactor(
quoteTokenDecimals,
quoteFeed1.getDecimals(),
quoteFeed2.getDecimals(),
baseTokenDecimals,
baseFeed1.getDecimals(),
baseFeed2.getDecimals(),
quoteVaultConversionSample,
baseVaultConversionSample
);
}

function _scaleFactor(
uint256 quoteTokenDecimals,
uint256 quoteFeed1Decimals,
uint256 quoteFeed2Decimals,
uint256 baseTokenDecimals,
uint256 baseFeed1Decimals,
uint256 baseFeed2Decimals,
uint256 quoteVaultConversionSample,
uint256 baseVaultConversionSample
) internal pure returns (uint256 scaleFactor) {
scaleFactor = 10
** (36
+ quoteTokenDecimals
+ quoteFeed1.getDecimals()
+ quoteFeed2.getDecimals()
+ quoteFeed1Decimals
+ quoteFeed2Decimals
- baseTokenDecimals
- baseFeed1.getDecimals()
- baseFeed2.getDecimals()) * quoteVaultConversionSample / baseVaultConversionSample;
- baseFeed1Decimals
- baseFeed2Decimals) * quoteVaultConversionSample / baseVaultConversionSample;
require(scaleFactor != 0, ErrorsLib.SCALE_FACTOR_IS_ZERO);
}

/* PRICE */
Expand Down
3 changes: 3 additions & 0 deletions src/morpho-chainlink/libraries/ErrorsLib.sol
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,7 @@ library ErrorsLib {

/// @notice Thrown when the vault conversion sample is not 1 while vault = address(0).
string constant VAULT_CONVERSION_SAMPLE_IS_NOT_ONE = "vault conversion sample is not one";

/// @notice Thrown when the scale factor is 0.
string constant SCALE_FACTOR_IS_ZERO = "scale factor is zero";
}
16 changes: 16 additions & 0 deletions test/MorphoChainlinkOracleV2ScaleFactorTest.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
// SPDX-License-Identifier: GPL-2.0-or-later
pragma solidity ^0.8.0;

import "../lib/forge-std/src/Test.sol";
import "../src/morpho-chainlink/MorphoChainlinkOracleV2.sol";
import "../src/morpho-chainlink/interfaces/IERC4626.sol";
import "./helpers/Constants.sol";

contract MorphoChainlinkOracleV2ScaleFactorTest is Test {
function testConstructorScaleFactorZero() public {
vm.expectRevert(bytes(ErrorsLib.SCALE_FACTOR_IS_ZERO));
new MorphoChainlinkOracleV2(
IERC4626(address(1)), 2, feedZero, feedZero, 36, vaultZero, 1, feedZero, feedZero, 0
);
}
}