Formal verification for LibUbiquityPool

packages/contracts/foundry.toml

@@ -21,11 +21,11 @@ force = false
 mainnet = "https://rpc.ankr.com/eth"
 
 [profile.SMT.model_checker]
-contracts = { }
+contracts = { "src/dollar/UbiquityPoolWithInvariants.sol" = ["UbiquityPoolWithInvariants"] }
 engine = 'chc'
 solvers = ['z3']
 show_unproved = true
-timeout = 0
+timeout = 5000
 targets = [
   'assert',
   'constantCondition',
@@ -45,4 +45,4 @@ runs = 16500000   # 5h 30m
 max_test_rejects = 144000000
 
 [profile.intense.invariant]
-runs = 350000     # 5h 40m
+runs = 350000     # 5h 40m

packages/contracts/package.json

@@ -14,7 +14,10 @@
     "url": "https://github.com/ubiquity/ubiquity-dollar.git"
   },
   "dependencies": {
+    "@chainlink/contracts": "^1.2.0",
+    "@openzeppelin/contracts": "^5.1.0",
     "@types/command-line-args": "5.2.0",
+    "abdk-libraries-solidity": "^3.2.0",
     "command-line-args": "5.2.1",
     "dotenv": "^16.0.3",
     "ethers": "^6.6.0",

packages/contracts/src/dollar/UbiquityPoolWithInvariants.sol

@@ -0,0 +1,83 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.19;
+
+import {LibUbiquityPool} from "./libraries/LibUbiquityPool.sol";
+import {AppStorage, LibAppStorage} from "./libraries/LibAppStorage.sol";
+import {IERC20Ubiquity} from "./interfaces/IERC20Ubiquity.sol";
+import {SafeMath} from "@openzeppelin/contracts/utils/math/SafeMath.sol";
+
+contract UbiquityPoolWithInvariants {
+    using SafeMath for uint256;
+
+    function mintDollar(
+        uint256 _collateralIndex,
+        uint256 _dollarAmount,
+        uint256 _dollarOutMin,
+        uint256 _maxCollateralIn,
+        uint256 _maxGovernanceIn,
+        bool _isOneToOne
+    )
+        public
+        returns (
+            uint256 totalDollarMint,
+            uint256 collateralNeeded,
+            uint256 governanceNeeded
+        )
+    {
+        (totalDollarMint, collateralNeeded, governanceNeeded) = LibUbiquityPool
+            .mintDollar(
+                _collateralIndex,
+                _dollarAmount,
+                _dollarOutMin,
+                _maxCollateralIn,
+                _maxGovernanceIn,
+                _isOneToOne
+            );
+
+        (
+            uint256 totalDollarSupplyInUsd,
+            uint256 collateralUsdBalance
+        ) = getDollarSupplyAndCollateralBalance();
+
+        assert(totalDollarSupplyInUsd <= collateralUsdBalance);
+    }
+
+    function redeemDollar(
+        uint256 _collateralIndex,
+        uint256 _dollarAmount,
+        uint256 _governanceOutMin,
+        uint256 _collateralOutMin
+    ) public returns (uint256 collateralOut, uint256 governanceOut) {
+        (collateralOut, governanceOut) = LibUbiquityPool.redeemDollar(
+            _collateralIndex,
+            _dollarAmount,
+            _governanceOutMin,
+            _collateralOutMin
+        );
+
+        (
+            uint256 totalDollarSupplyInUsd,
+            uint256 collateralUsdBalance
+        ) = getDollarSupplyAndCollateralBalance();
+
+        assert(collateralUsdBalance >= totalDollarSupplyInUsd);
+    }
+
+    function getDollarSupplyAndCollateralBalance()
+        public
+        view
+        returns (uint256 totalDollarSupplyInUsd, uint256 collateralUsdBalance)
+    {
+        uint256 totalDollarSupply = IERC20Ubiquity(
+            LibAppStorage.appStorage().dollarTokenAddress
+        ).totalSupply();
+
+        collateralUsdBalance = LibUbiquityPool.collateralUsdBalance();
+
+        require(collateralUsdBalance > 0, "Collateral balance is zero");
+        require(totalDollarSupply > 0, "Dollar supply is zero");
+
+        uint256 dollarPrice = LibUbiquityPool.getDollarPriceUsd();
+        totalDollarSupplyInUsd = totalDollarSupply.mul(dollarPrice).div(1e6);
+    }
+}

packages/contracts/test/formal/diamond/facets/UbiquityPoolFacetSMT.t.sol

@@ -0,0 +1,188 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.19;
+
+import "forge-std/Test.sol";
+import {UbiquityPoolFacet} from "../../../../src/dollar/facets/UbiquityPoolFacet.sol";
+import {LibUbiquityPool} from "../../../../src/dollar/libraries/LibUbiquityPool.sol";
+import {MockERC20} from "../../../../src/dollar/mocks/MockERC20.sol";
+import {DiamondTestSetup} from "../../../../test/diamond/DiamondTestSetup.sol";
+import {MockChainLinkFeed} from "../../../../src/dollar/mocks/MockChainLinkFeed.sol";
+import {IERC20Ubiquity} from "../../../../src/dollar/interfaces/IERC20Ubiquity.sol";
+import {MockCurveStableSwapNG} from "../../../../src/dollar/mocks/MockCurveStableSwapNG.sol";
+import {MockCurveTwocryptoOptimized} from "../../../../src/dollar/mocks/MockCurveTwocryptoOptimized.sol";
+import {SafeMath} from "@openzeppelin/contracts/utils/math/SafeMath.sol";
+
+contract UbiquityPoolFacetSMT is DiamondTestSetup {
+    using SafeMath for uint256;
+
+    // mock three tokens: collateral token, stable token, wrapped ETH token
+    MockERC20 collateralToken;
+    MockERC20 stableToken;
+    MockERC20 wethToken;
+
+    // mock three ChainLink price feeds, one for each token
+    MockChainLinkFeed collateralTokenPriceFeed;
+    MockChainLinkFeed ethUsdPriceFeed;
+    MockChainLinkFeed stableUsdPriceFeed;
+
+    // mock two curve pools Stablecoin/Dollar and Governance/WETH
+    MockCurveStableSwapNG curveDollarPlainPool;
+    MockCurveTwocryptoOptimized curveGovernanceEthPool;
+
+    address user = address(1);
+
+    function setUp() public override {
+        super.setUp();
+
+        vm.startPrank(admin);
+
+        collateralToken = new MockERC20("COLLATERAL", "CLT", 18);
+        wethToken = new MockERC20("WETH", "WETH", 18);
+        stableToken = new MockERC20("STABLE", "STABLE", 18);
+
+        collateralTokenPriceFeed = new MockChainLinkFeed();
+        ethUsdPriceFeed = new MockChainLinkFeed();
+        stableUsdPriceFeed = new MockChainLinkFeed();
+
+        curveDollarPlainPool = new MockCurveStableSwapNG(
+            address(stableToken),
+            address(dollarToken)
+        );
+
+        curveGovernanceEthPool = new MockCurveTwocryptoOptimized(
+            address(governanceToken),
+            address(wethToken)
+        );
+
+        // add collateral token to the pool
+        uint256 poolCeiling = 50_000e18; // max 50_000 of collateral tokens is allowed
+        ubiquityPoolFacet.addCollateralToken(
+            address(collateralToken),
+            address(collateralTokenPriceFeed),
+            poolCeiling
+        );
+
+        // set collateral price initial feed mock params
+        collateralTokenPriceFeed.updateMockParams(
+            1, // round id
+            100_000_000, // answer, 100_000_000 = $1.00 (chainlink 8 decimals answer is converted to 6 decimals pool price)
+            block.timestamp, // started at
+            block.timestamp, // updated at
+            1 // answered in round
+        );
+
+        // set ETH/USD price initial feed mock params
+        ethUsdPriceFeed.updateMockParams(
+            1, // round id
+            2000_00000000, // answer, 2000_00000000 = $2000 (8 decimals)
+            block.timestamp, // started at
+            block.timestamp, // updated at
+            1 // answered in round
+        );
+
+        // set stable/USD price feed initial mock params
+        stableUsdPriceFeed.updateMockParams(
+            1, // round id
+            100_000_000, // answer, 100_000_000 = $1.00 (8 decimals)
+            block.timestamp, // started at
+            block.timestamp, // updated at
+            1 // answered in round
+        );
+
+        // set ETH/Governance initial price to 20k in Curve pool mock (20k GOV == 1 ETH)
+        curveGovernanceEthPool.updateMockParams(20_000e18);
+
+        curveDollarPlainPool.updateMockParams(1.01e18);
+
+        // set price feed for collateral token
+        ubiquityPoolFacet.setCollateralChainLinkPriceFeed(
+            address(collateralToken), // collateral token address
+            address(collateralTokenPriceFeed), // price feed address
+            1 days // price feed staleness threshold in seconds
+        );
+
+        // set price feed for ETH/USD pair
+        ubiquityPoolFacet.setEthUsdChainLinkPriceFeed(
+            address(ethUsdPriceFeed), // price feed address
+            1 days // price feed staleness threshold in seconds
+        );
+
+        // set price feed for stable/USD pair
+        ubiquityPoolFacet.setStableUsdChainLinkPriceFeed(
+            address(stableUsdPriceFeed), // price feed address
+            1 days // price feed staleness threshold in seconds
+        );
+
+        // enable collateral at index 0
+        ubiquityPoolFacet.toggleCollateral(0);
+        // set mint and redeem initial fees
+        ubiquityPoolFacet.setFees(
+            0, // collateral index
+            10000, // 1% mint fee
+            20000 // 2% redeem fee
+        );
+        // set redemption delay to 2 blocks
+        ubiquityPoolFacet.setRedemptionDelayBlocks(2);
+        // set mint price threshold to $1.01 and redeem price to $0.99
+        ubiquityPoolFacet.setPriceThresholds(1010000, 990000);
+        // set collateral ratio to 100%
+        ubiquityPoolFacet.setCollateralRatio(1_000_000);
+        // set Governance-ETH pool
+        ubiquityPoolFacet.setGovernanceEthPoolAddress(
+            address(curveGovernanceEthPool)
+        );
+
+        // set Curve plain pool in manager facet
+        managerFacet.setStableSwapPlainPoolAddress(
+            address(curveDollarPlainPool)
+        );
+
+        // stop being admin
+        vm.stopPrank();
+
+        // mint 2000 Governance tokens to the user
+        deal(address(governanceToken), user, 2000e18);
+        // mint 2000 collateral tokens to the user
+        collateralToken.mint(address(user), 2000e18);
+        // user approves the pool to transfer collateral
+        vm.prank(user);
+        collateralToken.approve(address(ubiquityPoolFacet), 100e18);
+
+        vm.prank(user);
+        ubiquityPoolFacet.mintDollar(0, 1e18, 0.9e18, 1e18, 0, true);
+    }
+
+    function testCannotMintMoreDollarsThanCollateral() public view {
+        (
+            uint256 totalDollarSupplyInUsd,
+            uint256 collateralUsdBalance
+        ) = getDollarSupplyAndCollateralBalance();
+        assert(totalDollarSupplyInUsd <= collateralUsdBalance);
+    }
+
+    function testCannotRedeemMoreCollateralThanDollarValue() public view {
+        (
+            uint256 totalDollarSupplyInUsd,
+            uint256 collateralUsdBalance
+        ) = getDollarSupplyAndCollateralBalance();
+        assert(collateralUsdBalance >= totalDollarSupplyInUsd);
+    }
+
+    function getDollarSupplyAndCollateralBalance()
+        public
+        view
+        returns (uint256 totalDollarSupplyInUsd, uint256 collateralUsdBalance)
+    {
+        uint256 totalDollarSupply = IERC20Ubiquity(
+            managerFacet.dollarTokenAddress()
+        ).totalSupply();
+
+        collateralUsdBalance = ubiquityPoolFacet.collateralUsdBalance();
+
+        require(collateralUsdBalance > 0, "Collateral balance is zero");
+        require(totalDollarSupply > 0, "Dollar supply is zero");
+
+        uint256 dollarPrice = ubiquityPoolFacet.getDollarPriceUsd();
+        totalDollarSupplyInUsd = totalDollarSupply.mul(dollarPrice).div(1e6);
+    }
+}