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;
+}