​
Status

  • Supported
  • Partially Supported
  • Not Supported Yet

​
Implementation Details

​
Required Cheatcodes

  • getStateChanges(address aa, bytes32 slot)

​
Example Implementation

Protocol: 
// Example contract code if needed
contract MonotonicallyIncreasingValue {
    uint256 public value;

    function setValue(uint256 value_) external {
        value = value_;
    }
}
Assertion: 
contract StateChangesAssertion is Assertion {
    MonotonicallyIncreasingValue public protocol;

    constructor(MonotonicallyIncreasingValue protocol_) {
        protocol = protocol_;
    }

    function triggers() public view override {
        registerCallTrigger(this.assertionStateChanges.selector);
    }

    function assertionStateChanges() public view {
        uint256[] memory changes = getStateChangesUint(address(protocol), 0x0);
        for (uint256 i = 0; i < changes.length - 1; i++) {
            require(changes[i] < changes[i + 1], "Value is not monotonically increasing");
        }
    }
}

​
Implementation Notes

  • Storage access helpers:
    • The getStateChangesTYPE() helper functions return the changes for the given slot cast to the respective type
    • Storage layout packing has to be handled by the user
  • State change ordering:
    • The getStateChanges() function returns the changes in order of changes being made
    • To access values of a mapping, the slot has to be calculated manually
    • The pre-execution value is not included in the state changes

​
Example Use Cases

  • Make sure that a variable never changes its value:
    • Implementation slot of a proxy
    • Owner of a contract
  • Make sure assigned values meet certain criteria:
    • Price oracle increases/decreases max by x%
    • Address changed to a whitelisted value

​
Known Limitations

  1. Slot granularity
    • User can only request on a slot level, not on a variable level
    • User has to know the storage layout of the contract
    • User has to potentially shift/mask for the correct bits of the slot
  2. Slot Coupling
    • Arrays of state changes of different slots don’t give you timing guarantees
      • i.e. There is no guarantee that changes1[1] and changes2[1] held the value at the same time
      • Unless the user knows exactly when state changes occur, it is not recommended to assume timing guarantees

​
Future Improvements

  • Provide variable level access
  • Allow masking/shifting for correct bits of the slot in helper functions
  • Allow coupling of variables
    • stateChanges provide snapshots of the requested slots