Skip to content

Commit

Permalink
feat: symb exec halmos
Browse files Browse the repository at this point in the history
  • Loading branch information
simon-something committed May 16, 2024
1 parent 3c27899 commit ed45d89
Showing 1 changed file with 55 additions and 0 deletions.
55 changes: 55 additions & 0 deletions test/invariants/Greeter.symbolic.t.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.23;

import {Greeter, IERC20} from 'contracts/Greeter.sol';

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

contract GreeterSymbolic is SymTest, Test {
Greeter public targetContract;

function setUp() public {
string memory _initialGreeting = svm.createString(64, 'initial greeting');
address _token = svm.createAddress('token');

targetContract = new Greeter(_initialGreeting, IERC20(_token));
}

function check_validState_greeterNeverEmpty(address caller, bytes4 selector) public {

Check warning on line 19 in test/invariants/Greeter.symbolic.t.sol

View workflow job for this annotation

GitHub Actions / Lint Commit Messages

Function name must be in mixedCase
// Input conditions: any caller
vm.prank(caller);

// Execution
(bool success,) = address(targetContract).call(gen_calldata(selector));

// Output condition check
vm.assume(success); // discard failing calls
assert(keccak256(bytes(targetContract.greeting())) != keccak256(''));
}

function check_setGreeting_onlyOwnerSetsGreeting(address caller) public {

Check warning on line 31 in test/invariants/Greeter.symbolic.t.sol

View workflow job for this annotation

GitHub Actions / Lint Commit Messages

Function name must be in mixedCase
// Input conditions
string memory newGreeting = svm.createString(64, 'new greeting');

// Execution
vm.prank(caller);
(bool success,) = address(targetContract).call(abi.encodeCall(Greeter.setGreeting, (newGreeting)));

// Output condition check
if (success) {
assert(caller == targetContract.OWNER());
assert(keccak256(bytes(targetContract.greeting())) == keccak256(bytes(newGreeting)));
} else {
assert(caller != targetContract.OWNER() || keccak256(bytes(newGreeting)) == keccak256(''));
}
}

// either return a valid call to setGreeting or nothing (avoid halmos panicking on unknown contract call)
function gen_calldata(bytes4 selector) public view returns (bytes memory newCalldata) {

Check warning on line 49 in test/invariants/Greeter.symbolic.t.sol

View workflow job for this annotation

GitHub Actions / Lint Commit Messages

Function name must be in mixedCase
if (selector == targetContract.setGreeting.selector) {
string memory greeting = svm.createString(64, 'greeting');
newCalldata = abi.encodeWithSelector(selector, greeting);
}
}
}

0 comments on commit ed45d89

Please sign in to comment.