Skip to content

Commit

Permalink
test: revert changes to examples
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Jul 18, 2024
1 parent a174e85 commit 70635a9
Show file tree
Hide file tree
Showing 9 changed files with 53 additions and 58 deletions.
2 changes: 1 addition & 1 deletion examples/simple/test/BadElections.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ contract BadElectionsTest is SymTest, Test {

// when we vote again with the same signature, it reverts
try elections.vote(proposalId, support, voter, signature) {
assertTrue(false);
assert(false);
} catch {
// expected
}
Expand Down
10 changes: 4 additions & 6 deletions examples/simple/test/IsPowerOfTwo.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,8 @@ pragma solidity >=0.8.0 <0.9.0;

import "../src/IsPowerOfTwo.sol";

import {Test} from "forge-std/Test.sol";

/// @custom:halmos --solver-timeout-assertion 0
contract IsPowerOfTwoTest is Test {
contract IsPowerOfTwoTest {
IsPowerOfTwo target;

function setUp() public {
Expand All @@ -16,7 +14,7 @@ contract IsPowerOfTwoTest is Test {
function check_isPowerOfTwo_small(uint8 x) public view {
bool result1 = target.isPowerOfTwo(x);
bool result2 = x == 1 || x == 2 || x == 4 || x == 8 || x == 16 || x == 32 || x == 64 || x == 128;
assertEq(result1, result2);
assert(result1 == result2);
}

/// @custom:halmos --loop 256
Expand All @@ -29,13 +27,13 @@ contract IsPowerOfTwoTest is Test {
break;
}
}
assertEq(result1, result2);
assert(result1 == result2);
}

/// @custom:halmos --loop 256
function check_eq_isPowerOfTwo_isPowerOfTwoIter(uint x) public view {
bool result1 = target.isPowerOfTwo(x);
bool result2 = target.isPowerOfTwoIter(x);
assertEq(result1, result2);
assert(result1 == result2);
}
}
16 changes: 8 additions & 8 deletions examples/simple/test/Multicaller.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -120,8 +120,8 @@ contract MulticallerWithSenderSymTest is SymTest, Test {
impl = new MulticallerWithSenderMock();
spec = new MulticallerWithSenderSpec();

assertEq(impl.sender(), spec.sender());
assertEq(impl.reentrancyUnlocked(), spec.reentrancyUnlocked());
assert(impl.sender() == spec.sender());
assert(impl.reentrancyUnlocked() == spec.reentrancyUnlocked());

vm.deal(address(this), 100_000_000 ether);
vm.assume(address(impl).balance == address(spec).balance);
Expand All @@ -134,21 +134,21 @@ contract MulticallerWithSenderSymTest is SymTest, Test {
(bool success_spec, bytes memory retdata_spec) = address(spec).call{value: value}(data);

// Check: `impl` succeeds if and only if `spec` succeeds.
assertEq(success_impl, success_spec);
assert(success_impl == success_spec);
// Check: the return data must be identical.
assertEq(keccak256(retdata_impl), keccak256(retdata_spec));
assert(keccak256(retdata_impl) == keccak256(retdata_spec));

// Check: the storage states must remain the same.
assertEq(impl.sender(), spec.sender());
assertEq(impl.reentrancyUnlocked(), spec.reentrancyUnlocked());
assert(impl.sender() == spec.sender());
assert(impl.reentrancyUnlocked() == spec.reentrancyUnlocked());

// Check: the remaining balances must be equal.
assertEq(address(impl).balance, address(spec).balance);
assert(address(impl).balance == address(spec).balance);
// Check: the total amounts sent to each target must be equal.
for (uint i = 0; i < targetMocks.length; i++) {
bytes32 target_balance_impl = vm.load(targetMocks[i], keccak256(abi.encode(impl, _BALANCEOF_SLOT)));
bytes32 target_balance_spec = vm.load(targetMocks[i], keccak256(abi.encode(spec, _BALANCEOF_SLOT)));
assertEq(target_balance_impl, target_balance_spec);
assert(target_balance_impl == target_balance_spec);
}
}

Expand Down
10 changes: 4 additions & 6 deletions examples/simple/test/TotalPrice.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,8 @@ pragma solidity >=0.8.0 <0.9.0;

import "../src/TotalPrice.sol";

import {Test} from "forge-std/Test.sol";

/// @custom:halmos --solver-timeout-assertion 0
contract TotalPriceTest is Test {
contract TotalPriceTest {
TotalPrice target;

function setUp() public {
Expand All @@ -15,17 +13,17 @@ contract TotalPriceTest is Test {

function check_totalPriceBuggy(uint96 price, uint32 quantity) public view {
uint128 total = target.totalPriceBuggy(price, quantity);
assertTrue(quantity == 0 || total >= price);
assert(quantity == 0 || total >= price);
}

function check_totalPriceFixed(uint96 price, uint32 quantity) public view {
uint128 total = target.totalPriceFixed(price, quantity);
assertTrue(quantity == 0 || total >= price);
assert(quantity == 0 || total >= price);
}

function check_eq_totalPriceFixed_totalPriceConservative(uint96 price, uint32 quantity) public view {
uint128 total1 = target.totalPriceFixed(price, quantity);
uint128 total2 = target.totalPriceConservative(price, quantity);
assertEq(total1, total2);
assert(total1 == total2);
}
}
7 changes: 3 additions & 4 deletions examples/simple/test/Vault.t.sol
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
// SPDX-License-Identifier: AGPL-3.0
pragma solidity >=0.8.0 <0.9.0;

import {Test} from "forge-std/Test.sol";
import {SymTest} from "halmos-cheatcodes/SymTest.sol";

import {Vault} from "../src/Vault.sol";
Expand All @@ -17,7 +16,7 @@ contract VaultMock is Vault {
}

/// @custom:halmos --solver-timeout-assertion 0
contract VaultTest is SymTest, Test {
contract VaultTest is SymTest {
VaultMock vault;

function setUp() public {
Expand All @@ -39,7 +38,7 @@ contract VaultTest is SymTest, Test {
uint S2 = vault.totalShares();

// assert(A1 / S1 <= A2 / S2);
assertLe(A1 * S2, A2 * S1); // no counterexample
assert(A1 * S2 <= A2 * S1); // no counterexample
}

function check_mint(uint shares) public {
Expand All @@ -52,6 +51,6 @@ contract VaultTest is SymTest, Test {
uint S2 = vault.totalShares();

// assert(A1 / S1 <= A2 / S2);
assertLe(A1 * S2, A2 * S1); // counterexamples exist
assert(A1 * S2 <= A2 * S1); // counterexamples exist
}
}
2 changes: 1 addition & 1 deletion examples/tokens/ERC20/test/CurveTokenV3.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ contract CurveTokenV3Test is ERC20Test {
minter = token_.minter();
vm.prank(minter);
token_.mint(address(this), 1_000_000_000e18);
assertEq(token_.balanceOf(address(this)), 1_000_000_000e18);
assert(token_.balanceOf(address(this)) == 1_000_000_000e18);

holders = new address[](3);
holders[0] = address(0x1001);
Expand Down
2 changes: 1 addition & 1 deletion examples/tokens/ERC20/test/DEIStablecoin.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ contract DEIStablecoinTest is ERC20Test {

lossless = address(new SymAccount());
token_.initialize(1_000_000_000e18, address(this), address(this), 0, lossless);
assertEq(token_.balanceOf(address(this)), 1_000_000_000e18);
assert(token_.balanceOf(address(this)) == 1_000_000_000e18);

holders = new address[](3);
holders[0] = address(0x1001);
Expand Down
34 changes: 17 additions & 17 deletions examples/tokens/ERC20/test/ERC20Test.sol
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ abstract contract ERC20Test is SymTest, Test {

// ensure that the caller cannot spend other' tokens without approvals
if (newBalanceOther < oldBalanceOther) {
assertGe(oldAllowance, oldBalanceOther - newBalanceOther);
assert(oldAllowance >= oldBalanceOther - newBalanceOther);
}
}

Expand All @@ -51,17 +51,17 @@ abstract contract ERC20Test is SymTest, Test {
IERC20(token).transfer(receiver, amount);

if (sender != receiver) {
assertLe(IERC20(token).balanceOf(sender), oldBalanceSender); // ensure no subtraction overflow
assertEq(IERC20(token).balanceOf(sender), oldBalanceSender - amount);
assertGe(IERC20(token).balanceOf(receiver), oldBalanceReceiver); // ensure no addition overflow
assertEq(IERC20(token).balanceOf(receiver), oldBalanceReceiver + amount);
assert(IERC20(token).balanceOf(sender) <= oldBalanceSender); // ensure no subtraction overflow
assert(IERC20(token).balanceOf(sender) == oldBalanceSender - amount);
assert(IERC20(token).balanceOf(receiver) >= oldBalanceReceiver); // ensure no addition overflow
assert(IERC20(token).balanceOf(receiver) == oldBalanceReceiver + amount);
} else {
// sender and receiver may be the same
assertEq(IERC20(token).balanceOf(sender), oldBalanceSender);
assertEq(IERC20(token).balanceOf(receiver), oldBalanceReceiver);
assert(IERC20(token).balanceOf(sender) == oldBalanceSender);
assert(IERC20(token).balanceOf(receiver) == oldBalanceReceiver);
}
// make sure other balance is not affected
assertEq(IERC20(token).balanceOf(other), oldBalanceOther);
assert(IERC20(token).balanceOf(other) == oldBalanceOther);
}

function check_transferFrom(address caller, address from, address to, address other, uint256 amount) public virtual {
Expand All @@ -78,17 +78,17 @@ abstract contract ERC20Test is SymTest, Test {
IERC20(token).transferFrom(from, to, amount);

if (from != to) {
assertLe(IERC20(token).balanceOf(from), oldBalanceFrom);
assertEq(IERC20(token).balanceOf(from), oldBalanceFrom - amount);
assertGe(IERC20(token).balanceOf(to), oldBalanceTo);
assertEq(IERC20(token).balanceOf(to), oldBalanceTo + amount);
assert(IERC20(token).balanceOf(from) <= oldBalanceFrom);
assert(IERC20(token).balanceOf(from) == oldBalanceFrom - amount);
assert(IERC20(token).balanceOf(to) >= oldBalanceTo);
assert(IERC20(token).balanceOf(to) == oldBalanceTo + amount);

assertGe(oldAllowance, amount); // ensure allowance was enough
assertTrue(oldAllowance == type(uint256).max || IERC20(token).allowance(from, caller) == oldAllowance - amount); // allowance decreases if not max
assert(oldAllowance >= amount); // ensure allowance was enough
assert(oldAllowance == type(uint256).max || IERC20(token).allowance(from, caller) == oldAllowance - amount); // allowance decreases if not max
} else {
assertEq(IERC20(token).balanceOf(from), oldBalanceFrom);
assertEq(IERC20(token).balanceOf(to), oldBalanceTo);
assert(IERC20(token).balanceOf(from) == oldBalanceFrom);
assert(IERC20(token).balanceOf(to) == oldBalanceTo);
}
assertEq(IERC20(token).balanceOf(other), oldBalanceOther);
assert(IERC20(token).balanceOf(other) == oldBalanceOther);
}
}
28 changes: 14 additions & 14 deletions examples/tokens/ERC721/test/ERC721Test.sol
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,8 @@ abstract contract ERC721Test is SymTest, Test {
vm.assume(success);

// ensure that the caller cannot spend other's tokens
assertLe(IERC721(token).balanceOf(caller), oldBalanceCaller);
assertGe(IERC721(token).balanceOf(other), oldBalanceOther);
assert(IERC721(token).balanceOf(caller) <= oldBalanceCaller);
assert(IERC721(token).balanceOf(other) >= oldBalanceOther);
}

function _isApprovedOrOwner(address spender, uint256 tokenId) internal view returns (bool) {
Expand Down Expand Up @@ -81,26 +81,26 @@ abstract contract ERC721Test is SymTest, Test {
}

// ensure requirements of transfer
assertEq(from, oldOwner);
assertTrue(approved);
assert(from == oldOwner);
assert(approved);

// ensure the owner is updated correctly
assertEq(IERC721(token).ownerOf(tokenId), to);
assertEq(IERC721(token).getApproved(tokenId), address(0)); // ensure the approval is reset
assert(IERC721(token).ownerOf(tokenId) == to);
assert(IERC721(token).getApproved(tokenId) == address(0)); // ensure the approval is reset

// ensure the other token's owner is unchanged
assertEq(IERC721(token).ownerOf(otherTokenId), oldOtherTokenOwner);
assert(IERC721(token).ownerOf(otherTokenId) == oldOtherTokenOwner);

// balance update
if (from != to) {
assertLt(IERC721(token).balanceOf(from), oldBalanceFrom);
assertEq(IERC721(token).balanceOf(from), oldBalanceFrom - 1);
assertGt(IERC721(token).balanceOf(to), oldBalanceTo);
assertEq(IERC721(token).balanceOf(to), oldBalanceTo + 1);
assert(IERC721(token).balanceOf(from) < oldBalanceFrom);
assert(IERC721(token).balanceOf(from) == oldBalanceFrom - 1);
assert(IERC721(token).balanceOf(to) > oldBalanceTo);
assert(IERC721(token).balanceOf(to) == oldBalanceTo + 1);
} else {
assertEq(IERC721(token).balanceOf(from), oldBalanceFrom);
assertEq(IERC721(token).balanceOf(to), oldBalanceTo);
assert(IERC721(token).balanceOf(from) == oldBalanceFrom);
assert(IERC721(token).balanceOf(to) == oldBalanceTo);
}
assertEq(IERC721(token).balanceOf(other), oldBalanceOther);
assert(IERC721(token).balanceOf(other) == oldBalanceOther);
}
}

0 comments on commit 70635a9

Please sign in to comment.