feat: move formal verifications out of the test dir

packages/contracts/foundry.toml

@@ -21,7 +21,7 @@ force = false
 mainnet = "https://rpc.ankr.com/eth"
 
 [profile.SMT.model_checker]
-contracts = { "test/formal/diamond/facets/UbiquityPoolFacetSMT.t.sol" = ["UbiquityPoolFacetSMT"]}
+contracts = { "src/dollar/UbiquityPoolWithInvariants.sol" = ["UbiquityPoolWithInvariants"] }
 engine = 'chc'
 solvers = ['z3']
 show_unproved = true

packages/contracts/foundry.toml.backup

@@ -0,0 +1,48 @@
+[profile.default]
+src = 'src'
+test = 'test'
+out = 'out'
+libs = ['lib']
+script = 'scripts'
+solc_version = '0.8.19'
+evm_version = 'shanghai'
+extra_output = [
+  "abi",
+  "evm.bytecode",
+  "evm.deployedBytecode",
+  "evm.methodIdentifiers",
+]
+optimizer = true
+optimizer_runs = 20_000
+force = false
+# See more config options https://github.com/foundry-rs/foundry/tree/master/config
+
+[rpc_endpoints]
+mainnet = "https://rpc.ankr.com/eth"
+
+[profile.SMT.model_checker]
+contracts = {  }
+engine = 'chc'
+solvers = ['z3']
+show_unproved = true
+timeout = 5000
+targets = [
+  'assert',
+  'constantCondition',
+  'divByZero',
+  'outOfBounds',
+  'overflow',
+  'popEmptyArray',
+  'underflow',
+  'balance',
+]
+
+[profile.docs]
+src = 'src/dollar'
+
+[profile.intense.fuzz]
+runs = 16500000   # 5h 30m
+max_test_rejects = 144000000
+
+[profile.intense.invariant]
+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);
+    }
+}