diff --git a/.github/actions/gas-compare/action.yml b/.github/actions/gas-compare/action.yml index e38c48e89..23a756f3d 100644 --- a/.github/actions/gas-compare/action.yml +++ b/.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 diff --git a/.github/actions/setup/action.yml b/.github/actions/setup/action.yml index 2a439a6b2..b68fec649 100644 --- a/.github/actions/setup/action.yml +++ b/.github/actions/setup/action.yml @@ -1,4 +1,5 @@ name: Setup +description: Common environment setup runs: using: composite diff --git a/.github/actions/storage-layout/action.yml b/.github/actions/storage-layout/action.yml index fdfd5a25b..573564b67 100644 --- a/.github/actions/storage-layout/action.yml +++ b/.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 diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 8c51622b5..517ec552c 100644 --- a/.github/workflows/formal-verification.yml +++ b/.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 diff --git a/.gitmodules b/.gitmodules index 08a09bbcf..4939cd2b3 100644 --- a/.gitmodules +++ b/.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 diff --git a/fv-requirements.txt b/fv-requirements.txt new file mode 100644 index 000000000..8a0f1fed3 --- /dev/null +++ b/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 diff --git a/lib/halmos-cheatcodes b/lib/halmos-cheatcodes new file mode 160000 index 000000000..c0d865508 --- /dev/null +++ b/lib/halmos-cheatcodes @@ -0,0 +1 @@ +Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 diff --git a/requirements.txt b/requirements.txt deleted file mode 100644 index bdea09aa8..000000000 --- a/requirements.txt +++ /dev/null @@ -1 +0,0 @@ -certora-cli==4.13.1 diff --git a/scripts/generate/templates/SlotDerivation.t.js b/scripts/generate/templates/SlotDerivation.t.js index 052ada894..7e5ae5ea9 100644 --- a/scripts/generate/templates/SlotDerivation.t.js +++ b/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))), '}', ); diff --git a/test/proxy/Clones.t.sol b/test/proxy/Clones.t.sol index 214de2d5a..9015978fc 100644 --- a/test/proxy/Clones.t.sol +++ b/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 diff --git a/test/utils/Arrays.t.sol b/test/utils/Arrays.t.sol index c3d147562..09c7b66b6 100644 --- a/test/utils/Arrays.t.sol +++ b/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]); } diff --git a/test/utils/Create2.t.sol b/test/utils/Create2.t.sol index d602eded0..e8e2269f6 100644 --- a/test/utils/Create2.t.sol +++ b/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 diff --git a/test/utils/Packing.t.sol b/test/utils/Packing.t.sol index 95961f391..d430ad13f 100644 --- a/test/utils/Packing.t.sol +++ b/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); } diff --git a/test/utils/ShortStrings.t.sol b/test/utils/ShortStrings.t.sol index b854d273c..4aeafd721 100644 --- a/test/utils/ShortStrings.t.sol +++ b/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); } diff --git a/test/utils/SlotDerivation.t.sol b/test/utils/SlotDerivation.t.sol index db9c789a4..300a58b5f 100644 --- a/test/utils/SlotDerivation.t.sol +++ b/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 diff --git a/test/utils/math/Math.t.sol b/test/utils/math/Math.t.sol index 75066f1f4..3d4932eea 100644 --- a/test/utils/math/Math.t.sol +++ b/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); } diff --git a/test/utils/math/SignedMath.t.sol b/test/utils/math/SignedMath.t.sol index c173e0a42..bbad109b7 100644 --- a/test/utils/math/SignedMath.t.sol +++ 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 {