Add helper contracts

src/Asserts.sol

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+abstract contract Asserts {
+    function gt(uint256 a, uint256 b, string memory reason) internal virtual;
+
+    function gte(uint256 a, uint256 b, string memory reason) internal virtual;
+
+    function lt(uint256 a, uint256 b, string memory reason) internal virtual;
+
+    function lte(uint256 a, uint256 b, string memory reason) internal virtual;
+
+    function eq(uint256 a, uint256 b, string memory reason) internal virtual;
+
+    function t(bool b, string memory reason) internal virtual;
+
+    function between(uint256 value, uint256 low, uint256 high) internal virtual returns(uint256);
+
+    function precondition(bool p) internal virtual;
+}

src/CryticAsserts.sol

@@ -0,0 +1,74 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "./Asserts.sol";
+
+contract CryticAsserts is Asserts {
+    event Log(string);
+
+    function gt(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        emit Log(reason);
+        assert(a > b);
+    }
+
+    function gte(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        emit Log(reason);
+        assert(a >= b);
+    }
+
+    function lt(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        emit Log(reason);
+        assert(a < b);
+    }
+
+    function lte(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        emit Log(reason);
+        assert(a <= b);
+    }
+
+    function eq(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        emit Log(reason);
+        assert(a == b);
+    }
+
+    function t(bool b, string memory reason) internal virtual override {
+        emit Log(reason);
+        assert(b);
+    }
+
+    function between(
+        uint256 value,
+        uint256 low,
+        uint256 high
+    ) internal virtual override returns (uint256) {
+        if (value < low || value > high) {
+            uint ans = low + (value % (high - low + 1));
+            return ans;
+        }
+        return value;
+    }
+
+    function precondition(bool p) internal virtual override {
+        require(p);
+    }
+}

src/FoundryAsserts.sol

@@ -0,0 +1,69 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "forge-std/Test.sol";
+import "./Asserts.sol";
+
+contract FoundryAsserts is Test, Asserts {
+    function gt(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertGt(a, b, reason);
+    }
+
+    function gte(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertGe(a, b, reason);
+    }
+
+    function lt(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertLt(a, b, reason);
+    }
+
+    function lte(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertLe(a, b, reason);
+    }
+
+    function eq(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertEq(a, b, reason);
+    }
+
+    function t(bool b, string memory reason) internal virtual override {
+        assertTrue(b, reason);
+    }
+
+    function between(
+        uint256 value,
+        uint256 low,
+        uint256 high
+    ) internal virtual override returns (uint256) {
+        if (value < low || value > high) {
+            uint ans = low + (value % (high - low + 1));
+            return ans;
+        }
+        return value;
+    }
+
+    function precondition(
+        bool p
+    ) internal virtual override {
+        vm.assume(p);
+    }
+}

src/HalmosAsserts.sol

@@ -0,0 +1,64 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "forge-std/Test.sol";
+import "./Asserts.sol";
+
+contract HalmosAsserts is Test, Asserts {
+    function gt(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertGt(a, b, reason);
+    }
+
+    function gte(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertGe(a, b, reason);
+    }
+
+    function lt(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertLt(a, b, reason);
+    }
+
+    function lte(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertLe(a, b, reason);
+    }
+
+    function eq(
+        uint256 a,
+        uint256 b,
+        string memory reason
+    ) internal virtual override {
+        assertEq(a, b, reason);
+    }
+
+    function t(bool b, string memory reason) internal virtual override {
+        assertTrue(b, reason);
+    }
+
+    function between(
+        uint256 value,
+        uint256 low,
+        uint256 high
+    ) internal virtual override returns (uint256) {
+        vm.assume(value >= low && value <= high);
+        return value;
+    }
+
+    function precondition(bool p) internal virtual override {
+        vm.assume(p);
+    }
+}

src/Setup.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+abstract contract Setup {
+    function setup() internal virtual;
+}

src/TargetFunctions.sol

@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "./Setup.sol";
+import "./Asserts.sol";
+
+abstract contract TargetFunctions is Setup, Asserts {}