feat: initial Certora development

.gitignore

@@ -16,6 +16,9 @@ docs/
 # Node modules
 /node_modules
 
+# Certora
+.certora**
+
 # Hardhat
 /types
 /cache_hardhat

certora/scripts/verifyBlue.sh

@@ -0,0 +1,12 @@
+#!/bin/sh
+
+certoraRun \
+    src/Blue.sol \
+    --verify Blue:certora/specs/Blue.spec \
+    --solc_allow_path src \
+    --solc solc \
+    --loop_iter 3 \
+    --optimistic_loop \
+    --msg "Blue" \
+    --send_only \
+    "$@"

certora/specs/Blue.spec

@@ -0,0 +1,17 @@
+methods {
+    function supply(Blue.Market, uint256 amount) external;
+
+
+    function _.borrowRate(Blue.Market) external returns (uint256) => DISPATCH(true);
+
+    function _.safeTransfer(address, uint256) internal returns (bool) envfree => DISPATCH(true);
+    function _.safeTransferFrom(address, address, uint256) internal returns (bool) envfree => DISPATCH(true);
+}
+
+rule supplyRevertZero(Blue.Market market) {
+    env e;
+
+    supply@withrevert(market, 0);
+
+    assert lastReverted;
+}

src/Blue.sol

@@ -26,7 +26,7 @@ struct Market {
 
 using {toId} for Market;
 
-function toId(Market calldata market) pure returns (Id) {
+function toId(Market memory market) pure returns (Id) {
     return Id.wrap(keccak256(abi.encode(market)));
 }
 
@@ -89,7 +89,7 @@ contract Blue {
 
     // Markets management.
 
-    function createMarket(Market calldata market) external {
+    function createMarket(Market memory market) external {
         Id id = market.toId();
         require(isIrmEnabled[market.irm], "IRM not enabled");
         require(isLltvEnabled[market.lltv], "LLTV not enabled");
@@ -100,7 +100,7 @@ contract Blue {
 
     // Supply management.
 
-    function supply(Market calldata market, uint256 amount) external {
+    function supply(Market memory market, uint256 amount) external {
         Id id = market.toId();
         require(lastUpdate[id] != 0, "unknown market");
         require(amount != 0, "zero amount");
@@ -121,7 +121,7 @@ contract Blue {
         market.borrowableAsset.safeTransferFrom(msg.sender, address(this), amount);
     }
 
-    function withdraw(Market calldata market, uint256 amount) external {
+    function withdraw(Market memory market, uint256 amount) external {
         Id id = market.toId();
         require(lastUpdate[id] != 0, "unknown market");
         require(amount != 0, "zero amount");
@@ -141,7 +141,7 @@ contract Blue {
 
     // Borrow management.
 
-    function borrow(Market calldata market, uint256 amount) external {
+    function borrow(Market memory market, uint256 amount) external {
         Id id = market.toId();
         require(lastUpdate[id] != 0, "unknown market");
         require(amount != 0, "zero amount");
@@ -165,7 +165,7 @@ contract Blue {
         market.borrowableAsset.safeTransfer(msg.sender, amount);
     }
 
-    function repay(Market calldata market, uint256 amount) external {
+    function repay(Market memory market, uint256 amount) external {
         Id id = market.toId();
         require(lastUpdate[id] != 0, "unknown market");
         require(amount != 0, "zero amount");
@@ -184,7 +184,7 @@ contract Blue {
     // Collateral management.
 
     /// @dev Don't accrue interests because it's not required and it saves gas.
-    function supplyCollateral(Market calldata market, uint256 amount) external {
+    function supplyCollateral(Market memory market, uint256 amount) external {
         Id id = market.toId();
         require(lastUpdate[id] != 0, "unknown market");
         require(amount != 0, "zero amount");
@@ -196,7 +196,7 @@ contract Blue {
         market.collateralAsset.safeTransferFrom(msg.sender, address(this), amount);
     }
 
-    function withdrawCollateral(Market calldata market, uint256 amount) external {
+    function withdrawCollateral(Market memory market, uint256 amount) external {
         Id id = market.toId();
         require(lastUpdate[id] != 0, "unknown market");
         require(amount != 0, "zero amount");
@@ -212,7 +212,7 @@ contract Blue {
 
     // Liquidation.
 
-    function liquidate(Market calldata market, address borrower, uint256 seized) external {
+    function liquidate(Market memory market, address borrower, uint256 seized) external {
         Id id = market.toId();
         require(lastUpdate[id] != 0, "unknown market");
         require(seized != 0, "zero amount");
@@ -248,7 +248,7 @@ contract Blue {
 
     // Interests management.
 
-    function accrueInterests(Market calldata market, Id id) private {
+    function accrueInterests(Market memory market, Id id) private {
         uint256 marketTotalBorrow = totalBorrow[id];
 
         if (marketTotalBorrow != 0) {
@@ -263,7 +263,7 @@ contract Blue {
 
     // Health check.
 
-    function isHealthy(Market calldata market, Id id, address user) private view returns (bool) {
+    function isHealthy(Market memory market, Id id, address user) private view returns (bool) {
         uint256 borrowShares = borrowShare[id][user];
         if (borrowShares == 0) return true;
         // totalBorrowShares[id] > 0 when borrowShares > 0.

src/interfaces/IIrm.sol

@@ -4,5 +4,5 @@ pragma solidity >=0.5.0;
 import {Market} from "src/Blue.sol";
 
 interface IIrm {
-    function borrowRate(Market calldata market) external returns (uint256);
+    function borrowRate(Market memory market) external returns (uint256);
 }

src/mocks/IrmMock.sol

@@ -14,7 +14,7 @@ contract IrmMock is IIrm {
         blue = Blue(blueInstance);
     }
 
-    function borrowRate(Market calldata market) external view returns (uint256) {
+    function borrowRate(Market memory market) external view returns (uint256) {
         Id id = Id.wrap(keccak256(abi.encode(market)));
         uint256 utilization = blue.totalBorrow(id).wDiv(blue.totalSupply(id));