added more context to certora

.gitignore

@@ -17,4 +17,10 @@ docs/
 
 # Certora
 .certora_internal/
-.hypothesis/ 
+.hypothesis/ 
+
+annotated*
+gambit*
+mutations*
+
+collect.json

Makefile

@@ -39,7 +39,13 @@ slither :; slither . --config-file slither.config.json
 
 aderyn :; aderyn --root .
 
-certora :; certoraRun ./test/invariant-break/formal-verification/certora/FVCatches.conf
+certora :; certoraRun ./test/invariant-break/formal-verification/certora/conf/FVCatches.conf
+
+# Why doesn't this one work?
+certoraInvariant :; certoraRun ./test/invariant-break/formal-verification/certora/conf/FVCatchesInvariant.conf
+
+# createMutation :; certoraRun ./test/invariant-break/formal-verification/certora/conf/FVCatchesInvariant.conf --generate_mutation_conf mutations.mconf 
+# mutate :; certoraMutate --prover_conf ./test/invariant-break/formal-verification/certora/conf/FVCatchesInvariant.conf --mutation_conf  mutations.mconf 
 
 kontrol-build :;  kontrol build --rekompile --require lemmas.k --module-import KontrolTest:FV-LEMMAS
 kontrol-prove :;  kontrol prove --match-test KontrolTest.check_hellFunc_doesnt_revert_kontrol --fail-fast --use-booster --counterexample-information --auto-abstract-gas

src/invariant-break/FormalVerificationCatches.sol

@@ -101,12 +101,12 @@ contract FormalVerificationCatches {
                             );
                     }
                 }
-                if (Int.unwrap(number) > 95) {
-                    return Int.unwrap(Int.wrap((Int.unwrap(number) % 99)) / Int.wrap(1));
-                }
-                if (Int.unwrap(number) > 88) {
-                    return Int.unwrap((Int.wrap((Int.unwrap(number) % 99) + 3)) / Int.wrap(1));
-                }
+                // if (Int.unwrap(number) > 95) {
+                //     return Int.unwrap(Int.wrap((Int.unwrap(number) % 99)) / Int.wrap(1));
+                // }
+                // if (Int.unwrap(number) > 88) {
+                //     return Int.unwrap((Int.wrap((Int.unwrap(number) % 99) + 3)) / Int.wrap(1));
+                // }
                 if (Int.unwrap(number) > 80) {
                     return (Int.unwrap(number) + 19) - (numbr * 10);
                 }

src/invariant-break/HandlerStatefulFuzzCatches.sol

@@ -7,7 +7,7 @@ import {SafeERC20} from "@openzeppelin/contracts/token/ERC20/utils/SafeERC20.sol
 /*
  * This contract represents a vault for ERC20 tokens.
  *
- * INVARIANT: Users must always be able to withdraw the exact balance amout. 
+ * INVARIANT: Users must always be able to withdraw the exact balance amout out. 
  */
 contract HandlerStatefulFuzzCatches {
     error HandlerStatefulFuzzCatches__UnsupportedToken();

test/invariant-break/HandlerStatefulFuzz/Invariant.t.sol

@@ -44,16 +44,16 @@ contract InvariantBreakHardTest is StdInvariant, Test {
         targetContract(address(handler));
     }
 
-    // // THIS however, catches our bug!!!
-    // function statefulFuzz_testInvariantBreakHandler() public {
-    //     vm.startPrank(owner);
-    //     handlerStatefulFuzzCatches.withdrawToken(mockUSDC);
-    //     handlerStatefulFuzzCatches.withdrawToken(yeildERC20);
-    //     vm.stopPrank();
-
-    //     assert(mockUSDC.balanceOf(address(handlerStatefulFuzzCatches)) == 0);
-    //     assert(yeildERC20.balanceOf(address(handlerStatefulFuzzCatches)) == 0);
-    //     assert(mockUSDC.balanceOf(owner) == startingAmount);
-    //     assert(yeildERC20.balanceOf(owner) == startingAmount);
-    // }
+    // THIS however, catches our bug!!!
+    function statefulFuzz_testInvariantBreakHandler() public {
+        vm.startPrank(owner);
+        handlerStatefulFuzzCatches.withdrawToken(mockUSDC);
+        handlerStatefulFuzzCatches.withdrawToken(yeildERC20);
+        vm.stopPrank();
+
+        assert(mockUSDC.balanceOf(address(handlerStatefulFuzzCatches)) == 0);
+        assert(yeildERC20.balanceOf(address(handlerStatefulFuzzCatches)) == 0);
+        assert(mockUSDC.balanceOf(owner) == startingAmount);
+        assert(yeildERC20.balanceOf(owner) == startingAmount);
+    }
 }

test/invariant-break/StatefulFuzzCatchesTest.t.sol

@@ -22,7 +22,7 @@ contract StatefulFuzzCatchesTest is StdInvariant, Test {
     // // Stateful fuzz
     // // also can use the prefix `invariant_`
     // // Uncomment this to see it catch the issue!
-    // function statefulFuzz_testMathDoesntReturnZero() public view {
-    //     assert(sfc.storedValue() != 0);
-    // }
+    function statefulFuzz_testMathDoesntReturnZero() public view {
+        assert(sfc.storedValue() != 0);
+    }
 }

test/invariant-break/StatelessFuzzCatchesTest.t.sol

@@ -12,9 +12,14 @@ contract StatelessFuzzCatchesTest is Test {
         sfc = new StatelessFuzzCatches();
     }
 
+    // function testFuzzCatchesBugStateless() public view {
+    //     uint128 rng = 2;
+    //     assert(sfc.doMath(rng) != 0);
+    // }
+
     // // Stateless fuzz
     // // Uncomment this and you'll see it catches the bug!
-    // function testFuzzCatchesBugStateless(uint128 randomNumber) public view {
-    //     assert(sfc.doMath(randomNumber) != 0);
-    // }
+    function testFuzzCatchesBugStateless(uint128 randomNumber) public view {
+        assert(sfc.doMath(randomNumber) != 0);
+    }
 }

test/invariant-break/formal-verification/certora/FVCatches.conf → test/invariant-break/formal-verification/certora/conf/FVCatches.conf

@@ -2,7 +2,7 @@
     "files": [
         "./src/invariant-break/FormalVerificationCatches.sol"
     ],
-    "verify": "FormalVerificationCatches:./test/invariant-break/formal-verification/certora/FVCatches.spec",
+    "verify": "FormalVerificationCatches:./test/invariant-break/formal-verification/certora/spec/FVCatches.spec",
     "wait_for_results": "all",
     "rule_sanity": "basic",
     "optimistic_loop": true,

test/invariant-break/formal-verification/certora/conf/FVCatchesInvariant.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "./test/invariant-break/formal-verification/certora/harness/FVCatchesHarness.sol",
+    ],
+    "verify": "FVCatchesHarness:./test/invariant-break/formal-verification/certora/spec/FVCatchesInvariant.spec",
+    "wait_for_results": "all",
+    "rule_sanity": "basic",
+    "optimistic_loop": true,
+    "msg": "Verification of FVCatchesHarness"
+}

test/invariant-break/formal-verification/certora/harness/FVCatchesHarness.sol

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.20;
+
+import {FormalVerificationCatches} from "../../../../../src/invariant-break/FormalVerificationCatches.sol";
+
+contract FVCatchesHarness {
+    FormalVerificationCatches public fvc;
+
+    constructor() {
+        fvc = new FormalVerificationCatches();
+    }
+
+    function tryCatchHellFunc(uint128 number) public view returns (bool) {
+        try fvc.hellFunc(number) returns (uint256) {
+            return true;
+        } catch {
+            return false;
+        }
+    }
+}

test/invariant-break/formal-verification/certora/mconf/mutation.mconf

@@ -0,0 +1,10 @@
+{
+  "gambit": {
+    "filename": "test/invariant-break/formal-verification/certora/harness/FVCatchesHarness.sol",
+    "solc": "solc",
+    "num_mutants": 3,
+    "solc_allow_paths": [
+      "."
+    ]
+  }
+}

test/invariant-break/formal-verification/certora/FVCatches.spec → test/invariant-break/formal-verification/certora/spec/FVCatches.spec

@@ -21,4 +21,12 @@ rule hellFuncMustNeverRevert(uint128 number) {
 
   hellFunc@withrevert(number);
   assert(lastReverted == false);
-}
+}
+
+// // Wait... isn't this just a rule? 
+// "If i point at the contract in some state, is it reasonable for me to ask if X holds?" 
+// if the answer to this is yes, then X is an invariant.
+
+// invariant hell_func_never_reverts(uint128 number)
+//   hellFunc@withrevert(number)
+//   { preserved with (env e) { require e.msg.sender != 0; } }

test/invariant-break/formal-verification/certora/spec/FVCatchesInvariant.spec

@@ -0,0 +1,16 @@
+/*
+ * ./src/invariant-break/FormalVerificationCatches.sol 
+ *
+ * Certora Formal Verification Spec
+ */ 
+
+methods {
+  function tryCatchHellFunc(uint128) external returns bool envfree;
+}
+
+// This is technically unsound... and doesn't work anyways! 
+invariant hell_func_never_reverts(uint128 number)
+  tryCatchHellFunc(number) == true
+  { 
+    preserved with (env e) { require e.msg.sender != 0; } 
+  }