Enable some math tests to be run by halmos (#5824)

Co-authored-by: ernestognw <[email protected]>

Author: daejunpark

.github/workflows/formal-verification.yml

@@ -84,3 +84,5 @@ jobs:
         run: pip install -r fv-requirements.txt
       - name: Run Halmos
         run: halmos --match-test '^symbolic|^testSymbolic' -vv
+        env:
+          HALMOS_ALLOW_DOWNLOAD: 1

test/utils/Bytes.t.sol

@@ -14,7 +14,7 @@ contract BytesTest is Test {
     }
 
     // INDEX OF
-    function testIndexOf(bytes memory buffer, bytes1 s) public pure {
+    function testSymbolicIndexOf(bytes memory buffer, bytes1 s) public pure {
         uint256 result = Bytes.indexOf(buffer, s);
 
         if (buffer.length == 0) {
@@ -48,7 +48,7 @@ contract BytesTest is Test {
         }
     }
 
-    function testLastIndexOf(bytes memory buffer, bytes1 s) public pure {
+    function testSymbolicLastIndexOf(bytes memory buffer, bytes1 s) public pure {
         uint256 result = Bytes.lastIndexOf(buffer, s);
 
         if (buffer.length == 0) {

test/utils/math/Math.t.sol

@@ -12,7 +12,7 @@ contract MathTest is Test {
     }
 
     // ADD512 & MUL512
-    function testAdd512(uint256 a, uint256 b) public pure {
+    function testSymbolicAdd512(uint256 a, uint256 b) public pure {
         (uint256 high, uint256 low) = Math.add512(a, b);
 
         // test against tryAdd
@@ -60,7 +60,8 @@ contract MathTest is Test {
     }
 
     // CEILDIV
-    function testCeilDiv(uint256 a, uint256 b) public pure {
+    /// @custom:halmos --solver cvc5-int
+    function testSymbolicCeilDiv(uint256 a, uint256 b) public pure {
         vm.assume(b > 0);
 
         uint256 result = Math.ceilDiv(a, b);
@@ -112,17 +113,18 @@ contract MathTest is Test {
         _testInvMod(value, p, true);
     }
 
-    function testInvMod2(uint256 seed) public pure {
+    function testSymbolicInvMod2(uint256 seed) public pure {
         uint256 p = 2; // prime
         _testInvMod(bound(seed, 1, p - 1), p, false);
     }
 
-    function testInvMod17(uint256 seed) public pure {
+    function testSymbolicInvMod17(uint256 seed) public pure {
         uint256 p = 17; // prime
         _testInvMod(bound(seed, 1, p - 1), p, false);
     }
 
-    function testInvMod65537(uint256 seed) public pure {
+    /// @custom:halmos --solver bitwuzla-abs
+    function testSymbolicInvMod65537(uint256 seed) public pure {
         uint256 p = 65537; // prime
         _testInvMod(bound(seed, 1, p - 1), p, false);
     }

test/utils/math/SignedMath.t.sol

@@ -47,8 +47,9 @@ contract SignedMathTest is Test {
         assertEq(result, (a + b) / 2);
     }
 
-    // 2. more complex test, full int256 range
-    function testAverage2(int256 a, int256 b) public pure {
+    // 2. more complex test, full int256 range (solver timeout 0 = no timeout)
+    /// @custom:halmos --solver-timeout-assertion 0
+    function testSymbolicAverage2(int256 a, int256 b) public pure {
         (int256 result, int256 min, int256 max) = (
             SignedMath.average(a, b),
             SignedMath.min(a, b),