diff --git a/test/invariants/PROPERTIES.md b/test/invariants/PROPERTIES.md index e48439c9..bb8837e9 100644 --- a/test/invariants/PROPERTIES.md +++ b/test/invariants/PROPERTIES.md @@ -1,4 +1,4 @@ -| Properties | Type | -|---------------------------------------------------|------------| -| Greeting should never be empty | Valid state | -| Only the owner can set the greeting | State transition | \ No newline at end of file +| id | Properties | Type | +| --- | --------------------------------------------------- | ------------ | +| 1 | Greeting should never be empty | Valid state | +| 2 | Only the owner can set the greeting | State transition | diff --git a/test/invariants/fuzz/Greeter.t.sol b/test/invariants/fuzz/Greeter.t.sol index 96e2b1eb..a8f6cf95 100644 --- a/test/invariants/fuzz/Greeter.t.sol +++ b/test/invariants/fuzz/Greeter.t.sol @@ -2,36 +2,39 @@ pragma solidity 0.8.23; import {Greeter, IERC20} from 'contracts/Greeter.sol'; +import {CommonBase} from 'forge-std/Base.sol'; -interface IHevm { - function prank(address) external; -} - -contract InvariantGreeter { - IHevm internal _hevm = IHevm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D); - +contract InvariantGreeter is CommonBase { Greeter internal _targetContract; constructor() { _targetContract = new Greeter('a', IERC20(address(1))); } - function checkGreeterNeverEmpty(string memory _newGreeting) public { - // Execution - (bool _success,) = address(_targetContract).call(abi.encodeCall(Greeter.setGreeting, _newGreeting)); - - // Check output condition - assert((_success && keccak256(bytes(_targetContract.greeting())) != keccak256(bytes(''))) || !_success); + /// @custom:property-id 2 + /// @custom:property Only the owner can set the greeting + function handler_unguided_setGreeting(address _caller, string memory _newGreeting) external { + vm.prank(_caller); + try _targetContract.setGreeting(_newGreeting) { + assert(keccak256(bytes(_targetContract.greeting())) == keccak256(bytes(_newGreeting))); + assert(_caller == _targetContract.OWNER()); + } catch { + assert(_caller != _targetContract.OWNER() || keccak256(bytes(_newGreeting)) == keccak256('')); + } } - function checkOnlyOwnerSetsGreeting(address _caller) public { - // Input conditions - _hevm.prank(_caller); - - // Execution - (bool _success,) = address(this).call(abi.encodeCall(Greeter.setGreeting, 'hello')); + function handler_guided_setGreeting(string memory _newGreeting) external { + // no need to prank since this contract deployed the greeter and is therefore its owner + try _targetContract.setGreeting(_newGreeting) { + assert(keccak256(bytes(_targetContract.greeting())) == keccak256(bytes(_newGreeting))); + } catch { + assert(keccak256(bytes(_newGreeting)) == keccak256('')); + } + } - // Check output condition - assert((_success && msg.sender == _targetContract.OWNER()) || (!_success && msg.sender != _targetContract.OWNER())); + /// @custom:property-id 1 + /// @custom:property Greeting should never be empty + function property_greetingIsNeverEmpty() external view { + assert(keccak256(bytes(_targetContract.greeting())) != keccak256('')); } }