Skip to content

Commit

Permalink
♻️ Use forge-std assert Cheatcodes in halmos-Based Tests (#264)
Browse files Browse the repository at this point in the history
### 🕓 Changelog

The `halmos` PR [#323](a16z/halmos#323)
introduced support for the `forge-std` `assert`
[cheatcodes](https://book.getfoundry.sh/forge/cheatcodes). Consequently,
we refactor all existing `halmos` tests to utilise the latest
`forge-std` `assert` cheatcodes. Furthermore, I also update
`pnpm-lock.yaml` and all outdated submodules.

---------
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
  • Loading branch information
pcaversaccio authored Jul 31, 2024
1 parent 109889f commit 82c0469
Show file tree
Hide file tree
Showing 10 changed files with 169 additions and 177 deletions.
194 changes: 97 additions & 97 deletions .gas-snapshot

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion lib/create-util
Submodule create-util updated 2 files
+2 −2 package.json
+141 −141 pnpm-lock.yaml
2 changes: 1 addition & 1 deletion lib/solady
12 changes: 6 additions & 6 deletions pnpm-lock.yaml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

14 changes: 7 additions & 7 deletions test/governance/TimelockController.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -4338,9 +4338,9 @@ contract TimelockControllerInvariants is Test {
* executed transactions.
*/
function statefulFuzzExecutedLessThanOrEqualToScheduled() public view {
assertTrue(
timelockControllerHandler.executeCount() <=
timelockControllerHandler.scheduleCount()
assertLe(
timelockControllerHandler.executeCount(),
timelockControllerHandler.scheduleCount()
);
}

Expand Down Expand Up @@ -4381,10 +4381,10 @@ contract TimelockControllerInvariants is Test {
* be less than or equal to the number of scheduled proposals.
*/
function statefulFuzzSumOfProposals() public view {
assertTrue(
(timelockControllerHandler.cancelCount() +
timelockControllerHandler.executeCount()) <=
timelockControllerHandler.scheduleCount()
assertLe(
timelockControllerHandler.cancelCount() +
timelockControllerHandler.executeCount(),
timelockControllerHandler.scheduleCount()
);
}

Expand Down
21 changes: 10 additions & 11 deletions test/tokens/halmos/ERC1155TestHalmos.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,6 @@ import {IERC1155Extended} from "../interfaces/IERC1155Extended.sol";
/**
* @dev Sets the timeout (in milliseconds) for solving assertion
* violation conditions; `0` means no timeout.
* @notice Halmos currently does not support the new native `assert`
* cheatcodes in `forge-std` `v1.8.0` and above.
* @custom:halmos --solver-timeout-assertion 0
*/
contract ERC1155TestHalmos is Test, SymTest {
Expand Down Expand Up @@ -225,10 +223,11 @@ contract ERC1155TestHalmos is Test, SymTest {
vm.stopPrank();

for (uint256 i = 0; i < tokenIds.length; i++) {
assert(
erc1155.balanceOf(caller, tokenIds[i]) <= oldBalanceCaller[i]
assertLe(
erc1155.balanceOf(caller, tokenIds[i]),
oldBalanceCaller[i]
);
assert(erc1155.balanceOf(other, tokenIds[i]) >= oldBalanceOther[i]);
assertGe(erc1155.balanceOf(other, tokenIds[i]), oldBalanceOther[i]);
}
}

Expand Down Expand Up @@ -270,20 +269,20 @@ contract ERC1155TestHalmos is Test, SymTest {
}
vm.stopPrank();

(from == caller) ? assert(!approved) : assert(approved);
(from == caller) ? assertTrue(!approved) : assertTrue(approved);

uint256 newBalanceFrom = erc1155.balanceOf(from, tokenIds[0]);
uint256 newBalanceTo = erc1155.balanceOf(to, tokenIds[0]);
uint256 newBalanceOther = erc1155.balanceOf(other, tokenIds[0]);

if (from != to) {
assert(newBalanceFrom == oldBalanceFrom - amounts[0]);
assert(newBalanceTo == oldBalanceTo + amounts[0]);
assertEq(newBalanceFrom, oldBalanceFrom - amounts[0]);
assertEq(newBalanceTo, oldBalanceTo + amounts[0]);
} else {
assert(newBalanceFrom == oldBalanceFrom);
assert(newBalanceTo == oldBalanceTo);
assertEq(newBalanceFrom, oldBalanceFrom);
assertEq(newBalanceTo, oldBalanceTo);
}

assert(newBalanceOther == oldBalanceOther);
assertEq(newBalanceOther, oldBalanceOther);
}
}
29 changes: 13 additions & 16 deletions test/tokens/halmos/ERC20TestHalmos.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,6 @@ import {IERC20} from "openzeppelin/token/ERC20/IERC20.sol";
/**
* @dev Sets the timeout (in milliseconds) for solving assertion
* violation conditions; `0` means no timeout.
* @notice Halmos currently does not support the new native `assert`
* cheatcodes in `forge-std` `v1.8.0` and above.
* @custom:halmos --solver-timeout-assertion 0
*/
contract ERC20TestHalmos is Test, SymTest {
Expand Down Expand Up @@ -108,7 +106,7 @@ contract ERC20TestHalmos is Test, SymTest {
uint256 newBalanceOther = erc20.balanceOf(other);

if (newBalanceOther < oldBalanceOther) {
assert(oldAllowance >= oldBalanceOther - newBalanceOther);
assertGe(oldAllowance, oldBalanceOther - newBalanceOther);
}
}

Expand Down Expand Up @@ -142,14 +140,14 @@ contract ERC20TestHalmos is Test, SymTest {
uint256 newBalanceOther = erc20.balanceOf(other);

if (sender != receiver) {
assert(newBalanceSender == oldBalanceSender - amount);
assert(newBalanceReceiver == oldBalanceReceiver + amount);
assertEq(newBalanceSender, oldBalanceSender - amount);
assertEq(newBalanceReceiver, oldBalanceReceiver + amount);
} else {
assert(newBalanceSender == oldBalanceSender);
assert(newBalanceReceiver == oldBalanceReceiver);
assertEq(newBalanceSender, oldBalanceSender);
assertEq(newBalanceReceiver, oldBalanceReceiver);
}

assert(newBalanceOther == oldBalanceOther);
assertEq(newBalanceOther, oldBalanceOther);
}

/**
Expand Down Expand Up @@ -181,21 +179,20 @@ contract ERC20TestHalmos is Test, SymTest {

uint256 newBalanceFrom = erc20.balanceOf(from);
uint256 newBalanceTo = erc20.balanceOf(to);
uint256 newBalanceOther = erc20.balanceOf(other);

if (from != to) {
assert(newBalanceFrom == oldBalanceFrom - amount);
assert(newBalanceTo == oldBalanceTo + amount);
assert(oldAllowance >= amount);
assert(
assertEq(newBalanceFrom, oldBalanceFrom - amount);
assertEq(newBalanceTo, oldBalanceTo + amount);
assertGe(oldAllowance, amount);
assertTrue(
oldAllowance == type(uint256).max ||
erc20.allowance(from, caller) == oldAllowance - amount
);
} else {
assert(newBalanceFrom == oldBalanceFrom);
assert(newBalanceTo == oldBalanceTo);
assertEq(newBalanceFrom, oldBalanceFrom);
assertEq(newBalanceTo, oldBalanceTo);
}

assert(newBalanceOther == oldBalanceOther);
assertEq(erc20.balanceOf(other), oldBalanceOther);
}
}
26 changes: 12 additions & 14 deletions test/tokens/halmos/ERC721TestHalmos.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,6 @@ import {IERC721Extended} from "../interfaces/IERC721Extended.sol";
/**
* @dev Sets the timeout (in milliseconds) for solving assertion
* violation conditions; `0` means no timeout.
* @notice Halmos currently does not support the new native `assert`
* cheatcodes in `forge-std` `v1.8.0` and above.
* @custom:halmos --solver-timeout-assertion 0
*/
contract ERC721TestHalmos is Test, SymTest {
Expand Down Expand Up @@ -146,8 +144,8 @@ contract ERC721TestHalmos is Test, SymTest {
uint256 newBalanceCaller = erc721.balanceOf(caller);
uint256 newBalanceOther = erc721.balanceOf(other);

assert(newBalanceCaller <= oldBalanceCaller);
assert(newBalanceOther >= oldBalanceOther);
assertLe(newBalanceCaller, oldBalanceCaller);
assertGe(newBalanceOther, oldBalanceOther);
}

/**
Expand Down Expand Up @@ -193,24 +191,24 @@ contract ERC721TestHalmos is Test, SymTest {
}
vm.stopPrank();

assert(from == oldOwner);
assert(approved);
assert(erc721.ownerOf(tokenId) == to);
assert(erc721.getApproved(tokenId) == address(0));
assert(erc721.ownerOf(otherTokenId) == oldOtherTokenOwner);
assertEq(from, oldOwner);
assertTrue(approved);
assertEq(erc721.ownerOf(tokenId), to);
assertEq(erc721.getApproved(tokenId), address(0));
assertEq(erc721.ownerOf(otherTokenId), oldOtherTokenOwner);

uint256 newBalanceFrom = erc721.balanceOf(from);
uint256 newBalanceTo = erc721.balanceOf(to);
uint256 newBalanceOther = erc721.balanceOf(other);

if (from != to) {
assert(newBalanceFrom == oldBalanceFrom - 1);
assert(newBalanceTo == oldBalanceTo + 1);
assertEq(newBalanceFrom, oldBalanceFrom - 1);
assertEq(newBalanceTo, oldBalanceTo + 1);
} else {
assert(newBalanceFrom == oldBalanceFrom);
assert(newBalanceTo == oldBalanceTo);
assertEq(newBalanceFrom, oldBalanceFrom);
assertEq(newBalanceTo, oldBalanceTo);
}

assert(newBalanceOther == oldBalanceOther);
assertEq(newBalanceOther, oldBalanceOther);
}
}
44 changes: 21 additions & 23 deletions test/utils/halmos/MathTestHalmos.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,6 @@ import {IMath} from "../interfaces/IMath.sol";
/**
* @dev Sets the timeout (in milliseconds) for solving assertion
* violation conditions; `0` means no timeout.
* @notice Halmos currently does not support the new native `assert`
* cheatcodes in `forge-std` `v1.8.0` and above.
* @custom:halmos --solver-timeout-assertion 0
*/
contract MathTestHalmos is Test, SymTest {
Expand Down Expand Up @@ -46,15 +44,15 @@ contract MathTestHalmos is Test, SymTest {
}

function testHalmosAssertUint256Average(uint256 x, uint256 y) public view {
assert(math.uint256_average(x, y) == Math.average(x, y));
assertEq(math.uint256_average(x, y), Math.average(x, y));
}

function testHalmosAssertInt256Average(int256 x, int256 y) public view {
assert(math.int256_average(x, y) == FixedPointMathLib.avg(x, y));
assertEq(math.int256_average(x, y), FixedPointMathLib.avg(x, y));
}

function testHalmosAssertCeilDiv(uint256 x, uint256 y) public view {
assert(math.ceil_div(x, y) == Math.ceilDiv(x, y));
assertEq(math.ceil_div(x, y), Math.ceilDiv(x, y));
}

function testHalmosAssertSignum(int256 x) public view {
Expand All @@ -63,7 +61,7 @@ contract MathTestHalmos is Test, SymTest {
assembly ("memory-safe") {
signum := sub(sgt(x, 0), slt(x, 0))
}
assert(math.signum(x) == signum);
assertEq(math.signum(x), signum);
}

/**
Expand All @@ -77,39 +75,39 @@ contract MathTestHalmos is Test, SymTest {
// uint256 denominator,
// Math.Rounding rounding
// ) public view {
// assert(
// math.mul_div(x, y, denominator, Math.unsignedRoundsUp(rounding)) ==
// Math.mulDiv(x, y, denominator, rounding)
// assertEq(
// math.mul_div(x, y, denominator, Math.unsignedRoundsUp(rounding)),
// Math.mulDiv(x, y, denominator, rounding)
// );
// }

function testHalmosAssertLog2(
uint256 x,
Math.Rounding rounding
) public view {
assert(
math.log2(x, Math.unsignedRoundsUp(rounding)) ==
Math.log2(x, rounding)
assertEq(
math.log2(x, Math.unsignedRoundsUp(rounding)),
Math.log2(x, rounding)
);
}

function testHalmosAssertLog10(
uint256 x,
Math.Rounding rounding
) public view {
assert(
math.log10(x, Math.unsignedRoundsUp(rounding)) ==
Math.log10(x, rounding)
assertEq(
math.log10(x, Math.unsignedRoundsUp(rounding)),
Math.log10(x, rounding)
);
}

function testHalmosAssertLog256(
uint256 x,
Math.Rounding rounding
) public view {
assert(
math.log256(x, Math.unsignedRoundsUp(rounding)) ==
Math.log256(x, rounding)
assertEq(
math.log256(x, Math.unsignedRoundsUp(rounding)),
Math.log256(x, rounding)
);
}

Expand All @@ -119,7 +117,7 @@ contract MathTestHalmos is Test, SymTest {
* a lot of memory, causing the CI to crash due to out of memory.
*/
// function testHalmosAssertWadLn(int256 x) public view {
// assert(math.wad_ln(x) == FixedPointMathLib.lnWad(x));
// assertEq(math.wad_ln(x), FixedPointMathLib.lnWad(x));
// }

/**
Expand All @@ -128,7 +126,7 @@ contract MathTestHalmos is Test, SymTest {
* a lot of memory, causing the CI to crash due to out of memory.
*/
// function testHalmosAssertWadExp(int256 x) public view {
// assert(math.wad_exp(x) == FixedPointMathLib.expWad(x));
// assertEq(math.wad_exp(x), FixedPointMathLib.expWad(x));
// }

/**
Expand All @@ -138,9 +136,9 @@ contract MathTestHalmos is Test, SymTest {
*/
// function testHalmosAssertCbrt(uint256 x, bool roundup) public view {
// if (!roundup) {
// assert(math.cbrt(x, roundup) == FixedPointMathLib.cbrt(x));
// assertEq(math.cbrt(x, roundup), FixedPointMathLib.cbrt(x));
// } else {
// assert(
// assertTrue(
// math.cbrt(x, roundup) >= FixedPointMathLib.cbrt(x) &&
// math.cbrt(x, roundup) <= FixedPointMathLib.cbrt(x) + 1
// );
Expand All @@ -153,6 +151,6 @@ contract MathTestHalmos is Test, SymTest {
* a lot of memory, causing the CI to crash due to out of memory.
*/
// function testHalmosAssertWadCbrt(uint256 x) public view {
// assert(math.wad_cbrt(x) == FixedPointMathLib.cbrtWad(x));
// assertEq(math.wad_cbrt(x), FixedPointMathLib.cbrtWad(x));
// }
}

0 comments on commit 82c0469

Please sign in to comment.