Add Halmos support for formal verification (#5034)

Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>

.github/actions/gas-compare/action.yml

@@ -1,4 +1,5 @@
 name: Compare gas costs
+description: Compare gas costs between branches
 inputs:
   token:
     description: github token

.github/actions/setup/action.yml

@@ -1,4 +1,5 @@
 name: Setup
+description: Common environment setup
 
 runs:
   using: composite

.github/actions/storage-layout/action.yml

@@ -1,4 +1,5 @@
 name: Compare storage layouts
+description: Compare storage layouts between branches
 inputs:
   token:
     description: github token

.github/workflows/formal-verification.yml

@@ -48,8 +48,9 @@ jobs:
         with:
           python-version: ${{ env.PIP_VERSION }}
           cache: 'pip'
+          cache-dependency-path: 'fv-requirements.txt'
       - name: Install python packages
-        run: pip install -r requirements.txt
+        run: pip install -r fv-requirements.txt
       - name: Install java
         uses: actions/setup-java@v3
         with:
@@ -66,3 +67,20 @@ jobs:
           node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY"
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+  halmos:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Set up environment
+        uses: ./.github/actions/setup
+      - name: Install python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ${{ env.PIP_VERSION }}
+          cache: 'pip'
+          cache-dependency-path: 'fv-requirements.txt'
+      - name: Install python packages
+        run: pip install -r fv-requirements.txt
+      - name: Run Halmos
+        run: halmos --match-test '^symbolic|^testSymbolic' -vv

.gitmodules

@@ -5,3 +5,6 @@
 [submodule "lib/erc4626-tests"]
 	path = lib/erc4626-tests
 	url = https://github.com/a16z/erc4626-tests.git
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes

fv-requirements.txt

@@ -0,0 +1,4 @@
+certora-cli==4.13.1
+# File uses a custom name (fv-requirements.txt) so that it isn't picked by Netlify's build
+# whose latest Python version is 0.3.8, incompatible with most recent versions of Halmos
+halmos==0.1.12

lib/halmos-cheatcodes

@@ -0,0 +1 @@
+Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5

requirements.txt

@@ -1 +0,0 @@
-certora-cli==4.13.1

scripts/generate/templates/SlotDerivation.t.js

@@ -6,17 +6,26 @@ const header = `\
 pragma solidity ^0.8.20;
 
 import {Test} from "forge-std/Test.sol";
-
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
 import {SlotDerivation} from "@openzeppelin/contracts/utils/SlotDerivation.sol";
 `;
 
 const array = `\
 bytes[] private _array;
 
+function symbolicDeriveArray(uint256 length, uint256 offset) public {
+  vm.assume(length > 0);
+  vm.assume(offset < length);
+  _assertDeriveArray(length, offset);
+}
+
 function testDeriveArray(uint256 length, uint256 offset) public {
   length = bound(length, 1, type(uint256).max);
   offset = bound(offset, 0, length - 1);
+  _assertDeriveArray(length, offset);
+}
 
+function _assertDeriveArray(uint256 length, uint256 offset) public {
   bytes32 baseSlot;
   assembly {
     baseSlot := _array.slot
@@ -33,10 +42,10 @@ function testDeriveArray(uint256 length, uint256 offset) public {
 }
 `;
 
-const mapping = ({ type, name, isValueType }) => `\
+const mapping = ({ type, name }) => `\
 mapping(${type} => bytes) private _${type}Mapping;
 
-function testDeriveMapping${name}(${type} ${isValueType ? '' : 'memory'} key) public {
+function testSymbolicDeriveMapping${name}(${type} key) public {
   bytes32 baseSlot;
   assembly {
     baseSlot := _${type}Mapping.slot
@@ -52,10 +61,37 @@ function testDeriveMapping${name}(${type} ${isValueType ? '' : 'memory'} key) pu
 }
 `;
 
+const boundedMapping = ({ type, name }) => `\
+mapping(${type} => bytes) private _${type}Mapping;
+
+function testDeriveMapping${name}(${type} memory key) public {
+  _assertDeriveMapping${name}(key);
+}
+
+function symbolicDeriveMapping${name}() public {
+  _assertDeriveMapping${name}(svm.create${name}(256, "DeriveMapping${name}Input"));
+}
+
+function _assertDeriveMapping${name}(${type} memory key) internal {
+  bytes32 baseSlot;
+  assembly {
+      baseSlot := _${type}Mapping.slot
+  }
+
+  bytes storage derived = _${type}Mapping[key];
+  bytes32 derivedSlot;
+  assembly {
+      derivedSlot := derived.slot
+  }
+
+  assertEq(baseSlot.deriveMapping(key), derivedSlot);
+}
+`;
+
 // GENERATE
 module.exports = format(
   header.trimEnd(),
-  'contract SlotDerivationTest is Test {',
+  'contract SlotDerivationTest is Test, SymTest {',
   'using SlotDerivation for bytes32;',
   '',
   array,
@@ -68,6 +104,6 @@ module.exports = format(
         isValueType: type.isValueType,
       })),
     ),
-  ).map(type => mapping(type)),
+  ).map(type => (type.isValueType ? mapping(type) : boundedMapping(type))),
   '}',
 );

test/proxy/Clones.t.sol

@@ -6,7 +6,7 @@ import {Test} from "forge-std/Test.sol";
 import {Clones} from "@openzeppelin/contracts/proxy/Clones.sol";
 
 contract ClonesTest is Test {
-    function testPredictDeterministicAddressSpillage(address implementation, bytes32 salt) public {
+    function testSymbolicPredictDeterministicAddressSpillage(address implementation, bytes32 salt) public {
         address predicted = Clones.predictDeterministicAddress(implementation, salt);
         bytes32 spillage;
         /// @solidity memory-safe-assembly

test/utils/Arrays.t.sol

@@ -3,11 +3,27 @@
 pragma solidity ^0.8.20;
 
 import {Test} from "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
 import {Arrays} from "@openzeppelin/contracts/utils/Arrays.sol";
 
-contract ArraysTest is Test {
+contract ArraysTest is Test, SymTest {
     function testSort(uint256[] memory values) public {
         Arrays.sort(values);
+        _assertSort(values);
+    }
+
+    function symbolicSort() public {
+        uint256[] memory values = new uint256[](3);
+        for (uint256 i = 0; i < 3; i++) {
+            values[i] = svm.createUint256("arrayElement");
+        }
+        Arrays.sort(values);
+        _assertSort(values);
+    }
+
+    /// Asserts
+
+    function _assertSort(uint256[] memory values) internal {
         for (uint256 i = 1; i < values.length; ++i) {
             assertLe(values[i - 1], values[i]);
         }

test/utils/Create2.t.sol

@@ -6,7 +6,7 @@ import {Test} from "forge-std/Test.sol";
 import {Create2} from "@openzeppelin/contracts/utils/Create2.sol";
 
 contract Create2Test is Test {
-    function testComputeAddressSpillage(bytes32 salt, bytes32 bytecodeHash, address deployer) public {
+    function testSymbolicComputeAddressSpillage(bytes32 salt, bytes32 bytecodeHash, address deployer) public {
         address predicted = Create2.computeAddress(salt, bytecodeHash, deployer);
         bytes32 spillage;
         /// @solidity memory-safe-assembly

test/utils/Packing.t.sol

@@ -9,7 +9,7 @@ contract PackingTest is Test {
     using Packing for *;
 
     // Pack a pair of arbitrary uint128, and check that split recovers the correct values
-    function testUint128x2(uint128 first, uint128 second) external {
+    function testSymbolicUint128x2(uint128 first, uint128 second) external {
         Packing.Uint128x2 packed = Packing.pack(first, second);
         assertEq(packed.first(), first);
         assertEq(packed.second(), second);
@@ -20,7 +20,7 @@ contract PackingTest is Test {
     }
 
     // split an arbitrary bytes32 into a pair of uint128, and check that repack matches the input
-    function testUint128x2(bytes32 input) external {
+    function testSymbolicUint128x2(bytes32 input) external {
         (uint128 first, uint128 second) = input.asUint128x2().split();
         assertEq(Packing.pack(first, second).asBytes32(), input);
     }

test/utils/ShortStrings.t.sol

@@ -3,48 +3,102 @@
 pragma solidity ^0.8.20;
 
 import {Test} from "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
 
 import {ShortStrings, ShortString} from "@openzeppelin/contracts/utils/ShortStrings.sol";
 
-contract ShortStringsTest is Test {
+contract ShortStringsTest is Test, SymTest {
     string _fallback;
 
     function testRoundtripShort(string memory input) external {
         vm.assume(_isShort(input));
+        _assertRoundtripShort(input);
+    }
+
+    function symbolicRoundtripShort() external {
+        string memory input = svm.createString(31, "RoundtripShortInput");
+        _assertRoundtripShort(input);
+    }
+
+    function testRoundtripWithFallback(string memory input, string memory fallbackInitial) external {
+        _assertRoundtripWithFallback(input, fallbackInitial);
+    }
+
+    function symbolicRoundtripWithFallbackLong() external {
+        string memory input = svm.createString(256, "RoundtripWithFallbackInput");
+        string memory fallbackInitial = svm.createString(256, "RoundtripWithFallbackFallbackInitial");
+        _assertRoundtripWithFallback(input, fallbackInitial);
+    }
+
+    function symbolicRoundtripWithFallbackShort() external {
+        string memory input = svm.createString(31, "RoundtripWithFallbackInput");
+        string memory fallbackInitial = svm.createString(31, "RoundtripWithFallbackFallbackInitial");
+        _assertRoundtripWithFallback(input, fallbackInitial);
+    }
+
+    function testRevertLong(string memory input) external {
+        vm.assume(!_isShort(input));
+        _assertRevertLong(input);
+    }
+
+    function testLengthShort(string memory input) external {
+        vm.assume(_isShort(input));
+        _assertLengthShort(input);
+    }
+
+    function symbolicLengthShort() external {
+        string memory input = svm.createString(31, "LengthShortInput");
+        _assertLengthShort(input);
+    }
+
+    function testLengthWithFallback(string memory input, string memory fallbackInitial) external {
+        _fallback = fallbackInitial;
+        _assertLengthWithFallback(input);
+    }
+
+    function symbolicLengthWithFallback() external {
+        uint256 length = 256;
+        string memory input = svm.createString(length, "LengthWithFallbackInput");
+        string memory fallbackInitial = svm.createString(length, "LengthWithFallbackFallbackInitial");
+        _fallback = fallbackInitial;
+        _assertLengthWithFallback(input);
+    }
+
+    /// Assertions
+
+    function _assertRoundtripShort(string memory input) internal {
         ShortString short = ShortStrings.toShortString(input);
         string memory output = ShortStrings.toString(short);
         assertEq(input, output);
     }
 
-    function testRoundtripWithFallback(string memory input, string memory fallbackInitial) external {
+    function _assertRoundtripWithFallback(string memory input, string memory fallbackInitial) internal {
         _fallback = fallbackInitial; // Make sure that the initial value has no effect
         ShortString short = ShortStrings.toShortStringWithFallback(input, _fallback);
         string memory output = ShortStrings.toStringWithFallback(short, _fallback);
         assertEq(input, output);
     }
 
-    function testRevertLong(string memory input) external {
-        vm.assume(!_isShort(input));
+    function _assertRevertLong(string memory input) internal {
         vm.expectRevert(abi.encodeWithSelector(ShortStrings.StringTooLong.selector, input));
         this.toShortString(input);
     }
 
-    function testLengthShort(string memory input) external {
-        vm.assume(_isShort(input));
-        uint256 inputLength = bytes(input).length;
+    function _assertLengthShort(string memory input) internal {
         ShortString short = ShortStrings.toShortString(input);
         uint256 shortLength = ShortStrings.byteLength(short);
+        uint256 inputLength = bytes(input).length;
         assertEq(inputLength, shortLength);
     }
 
-    function testLengthWithFallback(string memory input, string memory fallbackInitial) external {
-        _fallback = fallbackInitial;
+    function _assertLengthWithFallback(string memory input) internal {
         uint256 inputLength = bytes(input).length;
         ShortString short = ShortStrings.toShortStringWithFallback(input, _fallback);
         uint256 shortLength = ShortStrings.byteLengthWithFallback(short, _fallback);
         assertEq(inputLength, shortLength);
     }
 
+    /// Helpers
     function toShortString(string memory input) external pure returns (ShortString) {
         return ShortStrings.toShortString(input);
     }

test/utils/SlotDerivation.t.sol

@@ -4,18 +4,27 @@
 pragma solidity ^0.8.20;
 
 import {Test} from "forge-std/Test.sol";
-
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
 import {SlotDerivation} from "@openzeppelin/contracts/utils/SlotDerivation.sol";
 
-contract SlotDerivationTest is Test {
+contract SlotDerivationTest is Test, SymTest {
     using SlotDerivation for bytes32;
 
     bytes[] private _array;
 
+    function symbolicDeriveArray(uint256 length, uint256 offset) public {
+        vm.assume(length > 0);
+        vm.assume(offset < length);
+        _assertDeriveArray(length, offset);
+    }
+
     function testDeriveArray(uint256 length, uint256 offset) public {
         length = bound(length, 1, type(uint256).max);
         offset = bound(offset, 0, length - 1);
+        _assertDeriveArray(length, offset);
+    }
 
+    function _assertDeriveArray(uint256 length, uint256 offset) public {
         bytes32 baseSlot;
         assembly {
             baseSlot := _array.slot
@@ -33,7 +42,7 @@ contract SlotDerivationTest is Test {
 
     mapping(address => bytes) private _addressMapping;
 
-    function testDeriveMappingAddress(address key) public {
+    function testSymbolicDeriveMappingAddress(address key) public {
         bytes32 baseSlot;
         assembly {
             baseSlot := _addressMapping.slot
@@ -50,7 +59,7 @@ contract SlotDerivationTest is Test {
 
     mapping(bool => bytes) private _boolMapping;
 
-    function testDeriveMappingBoolean(bool key) public {
+    function testSymbolicDeriveMappingBoolean(bool key) public {
         bytes32 baseSlot;
         assembly {
             baseSlot := _boolMapping.slot
@@ -67,7 +76,7 @@ contract SlotDerivationTest is Test {
 
     mapping(bytes32 => bytes) private _bytes32Mapping;
 
-    function testDeriveMappingBytes32(bytes32 key) public {
+    function testSymbolicDeriveMappingBytes32(bytes32 key) public {
         bytes32 baseSlot;
         assembly {
             baseSlot := _bytes32Mapping.slot
@@ -84,7 +93,7 @@ contract SlotDerivationTest is Test {
 
     mapping(bytes4 => bytes) private _bytes4Mapping;
 
-    function testDeriveMappingBytes4(bytes4 key) public {
+    function testSymbolicDeriveMappingBytes4(bytes4 key) public {
         bytes32 baseSlot;
         assembly {
             baseSlot := _bytes4Mapping.slot
@@ -101,7 +110,7 @@ contract SlotDerivationTest is Test {
 
     mapping(uint256 => bytes) private _uint256Mapping;
 
-    function testDeriveMappingUint256(uint256 key) public {
+    function testSymbolicDeriveMappingUint256(uint256 key) public {
         bytes32 baseSlot;
         assembly {
             baseSlot := _uint256Mapping.slot
@@ -118,7 +127,7 @@ contract SlotDerivationTest is Test {
 
     mapping(uint32 => bytes) private _uint32Mapping;
 
-    function testDeriveMappingUint32(uint32 key) public {
+    function testSymbolicDeriveMappingUint32(uint32 key) public {
         bytes32 baseSlot;
         assembly {
             baseSlot := _uint32Mapping.slot
@@ -135,7 +144,7 @@ contract SlotDerivationTest is Test {
 
     mapping(int256 => bytes) private _int256Mapping;
 
-    function testDeriveMappingInt256(int256 key) public {
+    function testSymbolicDeriveMappingInt256(int256 key) public {
         bytes32 baseSlot;
         assembly {
             baseSlot := _int256Mapping.slot
@@ -152,7 +161,7 @@ contract SlotDerivationTest is Test {
 
     mapping(int32 => bytes) private _int32Mapping;
 
-    function testDeriveMappingInt32(int32 key) public {
+    function testSymbolicDeriveMappingInt32(int32 key) public {
         bytes32 baseSlot;
         assembly {
             baseSlot := _int32Mapping.slot
@@ -170,6 +179,14 @@ contract SlotDerivationTest is Test {
     mapping(string => bytes) private _stringMapping;
 
     function testDeriveMappingString(string memory key) public {
+        _assertDeriveMappingString(key);
+    }
+
+    function symbolicDeriveMappingString() public {
+        _assertDeriveMappingString(svm.createString(256, "DeriveMappingStringInput"));
+    }
+
+    function _assertDeriveMappingString(string memory key) internal {
         bytes32 baseSlot;
         assembly {
             baseSlot := _stringMapping.slot
@@ -187,6 +204,14 @@ contract SlotDerivationTest is Test {
     mapping(bytes => bytes) private _bytesMapping;
 
     function testDeriveMappingBytes(bytes memory key) public {
+        _assertDeriveMappingBytes(key);
+    }
+
+    function symbolicDeriveMappingBytes() public {
+        _assertDeriveMappingBytes(svm.createBytes(256, "DeriveMappingBytesInput"));
+    }
+
+    function _assertDeriveMappingBytes(bytes memory key) internal {
         bytes32 baseSlot;
         assembly {
             baseSlot := _bytesMapping.slot

test/utils/math/Math.t.sol

@@ -7,12 +7,12 @@ import {Test, stdError} from "forge-std/Test.sol";
 import {Math} from "@openzeppelin/contracts/utils/math/Math.sol";
 
 contract MathTest is Test {
-    function testSelect(bool f, uint256 a, uint256 b) public {
+    function testSymbolicTernary(bool f, uint256 a, uint256 b) public {
         assertEq(Math.ternary(f, a, b), f ? a : b);
     }
 
     // MIN & MAX
-    function testMinMax(uint256 a, uint256 b) public {
+    function testSymbolicMinMax(uint256 a, uint256 b) public {
         assertEq(Math.min(a, b), a < b ? a : b);
         assertEq(Math.max(a, b), a > b ? a : b);
     }

test/utils/math/SignedMath.t.sol

@@ -8,18 +8,18 @@ import {Math} from "../../../contracts/utils/math/Math.sol";
 import {SignedMath} from "../../../contracts/utils/math/SignedMath.sol";
 
 contract SignedMathTest is Test {
-    function testSelect(bool f, int256 a, int256 b) public {
+    function testSymbolicTernary(bool f, int256 a, int256 b) public {
         assertEq(SignedMath.ternary(f, a, b), f ? a : b);
     }
 
     // MIN & MAX
-    function testMinMax(int256 a, int256 b) public {
+    function testSymbolicMinMax(int256 a, int256 b) public {
         assertEq(SignedMath.min(a, b), a < b ? a : b);
         assertEq(SignedMath.max(a, b), a > b ? a : b);
     }
 
     // MIN
-    function testMin(int256 a, int256 b) public {
+    function testSymbolicMin(int256 a, int256 b) public {
         int256 result = SignedMath.min(a, b);
 
         assertLe(result, a);
@@ -28,7 +28,7 @@ contract SignedMathTest is Test {
     }
 
     // MAX
-    function testMax(int256 a, int256 b) public {
+    function testSymbolicMax(int256 a, int256 b) public {
         int256 result = SignedMath.max(a, b);
 
         assertGe(result, a);
@@ -69,7 +69,7 @@ contract SignedMathTest is Test {
     }
 
     // ABS
-    function testAbs(int256 a) public {
+    function testSymbolicAbs(int256 a) public {
         uint256 result = SignedMath.abs(a);
 
         unchecked {