Merge pull request #143 from daejunpark/ci/halmos

test: update halmos tests for new halmos version

Author: MathisGD

.github/workflows/ci-foundry.yml

@@ -47,4 +47,4 @@ jobs:
         run: python3 -m pip install --upgrade halmos
 
       - name: Run halmos
-        run: halmos --function testProve --loop 4 --symbolic-storage --test-parallel --solver-parallel --solver-timeout-assertion 0
+        run: halmos --function testProve --loop 4 --solver-timeout-assertion 0

.gitmodules

@@ -5,6 +5,9 @@
 	path = lib/forge-std
 	url = https://github.com/MathisGD/forge-std
 	branch = feat/real-gas-consumption
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes
 [submodule "lib/openzeppelin-contracts"]
 	path = lib/openzeppelin-contracts
 	url = https://github.com/OpenZeppelin/openzeppelin-contracts

lib/halmos-cheatcodes

@@ -2,6 +2,7 @@
 pragma solidity ^0.8.0;
 
 import {Test} from "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
 import {
     LogarithmicBucketsMock, BucketDLLMock, BucketDLL, LogarithmicBuckets
 } from "./mocks/LogarithmicBucketsMock.sol";
@@ -118,7 +119,11 @@ contract TestLogarithmicBuckets is LogarithmicBucketsMock, Test {
     }
 }
 
-contract TestProveLogarithmicBuckets is LogarithmicBucketsMock, Test {
+contract TestProveLogarithmicBuckets is LogarithmicBucketsMock, Test, SymTest {
+    function setUpSymbolic() public {
+        svm.enableSymbolicStorage(address(this));
+    }
+
     function isPowerOfTwo(uint256 x) public pure returns (bool) {
         unchecked {
             return x != 0 && (x & (x - 1)) == 0;