Additional tests and specifications

certora/specs/SharePrice.spec

@@ -2,6 +2,7 @@ using MockERC20 as token;
 using MockMErc20DelegateFixer as fixer;
 
 methods {
+    function getCash() external returns (uint256) envfree;
     function badDebt() external returns (uint256) envfree;
     function fixUser(address liquidator, address user) external;
     function borrowIndex() external returns (uint256) envfree;
@@ -125,6 +126,51 @@ filtered {
      "bad debt should only increase when fixing users";
 }
 
+rule badDebtRulesCash(env e, uint256 amount) {
+    require e.msg.sender != fixer;
+
+    uint256 startingBadDebt = badDebt();
+    uint256 startingCash = token.balanceOf(fixer);
+
+    /// bound input as to not overflow (safe math is not used)
+    require startingCash + startingBadDebt <= to_mathint(uintMax());
+
+    repayBadDebtWithCash(e, amount);
+
+    uint256 endingBadDebt = badDebt();
+
+    /// starting cash + starting bad debt == ending bad debt + ending cash == getCash()
+
+    assert startingCash + startingBadDebt == endingBadDebt + to_mathint(token.balanceOf(fixer)),
+     "cash not the same";
+
+    assert startingCash + startingBadDebt == to_mathint(getCash()),
+     "bad debt should not increase when repaying with cash";
+}
+
+rule allBadDebtRulesCash(method f, env e, calldataarg args)
+filtered {
+    f -> 
+    f.selector == sig:repayBadDebtWithCash(uint256).selector ||
+    f.selector == sig:repayBadDebtWithReserves().selector
+} {
+    require e.msg.sender != fixer;
+
+    uint256 startingBadDebt = badDebt();
+    uint256 startingCash = token.balanceOf(fixer);
+
+    /// bound input as to not overflow (safe math is not used)
+    require startingCash + startingBadDebt <= to_mathint(uintMax());
+
+    f(e, args);
+
+    uint256 endingBadDebt = badDebt();
+
+    /// bad debt + cash == getCash()
+
+    assert to_mathint(getCash()) == endingBadDebt + to_mathint(token.balanceOf(fixer)),
+     "cash not correct";
+}
 
 rule repayBadDebtWithReservesSuccess(env e) {
     uint256 startingReserves = totalReserves();

test/integration/proposals/mips/mip-m17/mip-m17.t.sol

@@ -274,6 +274,21 @@ contract MIPM17IntegrationTest is PostProposalCheck {
         );
     }
 
+    function testCashEqualsUnderlyingBalancePlusBalance() public {
+        assertEq(
+            mxcDotDelegator.badDebt() +
+                xcDotToken.balanceOf(address(mxcDotDelegator)),
+            mxcDotDelegator.getCash(),
+            "xcDot cash incorrect"
+        );
+        assertEq(
+            fraxDelegator.badDebt() +
+                fraxToken.balanceOf(address(fraxDelegator)),
+            fraxDelegator.getCash(),
+            "frax cash incorrect"
+        );
+    }
+
     function testEthMadMarketsCeaseFunction() public {
         address madEthMTokenHolder = 0xDD15c08320F01F1b6348b35EeBe29fDB5ca0cDa6;
 
@@ -285,6 +300,28 @@ contract MIPM17IntegrationTest is PostProposalCheck {
         assertTrue(returnCode != 0, "incorrect return code on redeem");
     }
 
+    function testUsdcMadMarketsCeaseFunction() public {
+        address madUsdcMTokenHolder = 0xE0B2026E3DB1606ef0Beb764cCdf7b3CEE30Db4A;
+
+        uint256 balance = nomadUSDCDelegator.balanceOf(madUsdcMTokenHolder);
+
+        vm.prank(madUsdcMTokenHolder);
+        uint256 returnCode = nomadUSDCDelegator.redeem(balance);
+
+        assertTrue(returnCode != 0, "incorrect return code on redeem");
+    }
+
+    function testBtcMadMarketsCeaseFunction() public {
+        address madBTCMTokenHolder = 0xb587526953Ad321C1aB2eA26F7311d2aA1A98a4a;
+
+        uint256 balance = nomadBTCDelegator.balanceOf(madBTCMTokenHolder);
+
+        vm.prank(madBTCMTokenHolder);
+        uint256 returnCode = nomadBTCDelegator.redeem(balance);
+
+        assertTrue(returnCode != 0, "incorrect return code on redeem");
+    }
+
     function testSetUpxcDot() public {
         {
             /// @dev check that the borrows, reserves and index calculations match