Variable State Change Tracking

​

Status

• Supported
• Partially Supported
• Not Supported Yet

​

Implementation Details

​

Required Cheatcodes

• getStateChanges(address aa, bytes32 slot)

​

Example Implementation

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

    function setValue(uint256 value_) external {
        value = value_;
    }
}

import {AssertionSpec} from "credible-std/SpecRecorder.sol";

contract StateChangesAssertion is Assertion {
    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

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

    function assertionStateChanges() public view {
        MonotonicallyIncreasingValue protocol = MonotonicallyIncreasingValue(ph.getAssertionAdopter());
        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

​

Implementation Considerations

1. Slot granularity
   • Request state changes at the slot level
   • Use the target contract’s storage layout to select the right slot
   • Shift or mask values when the relevant variable occupies only part of a packed slot
2. Slot Coupling
   • Treat arrays of state changes for different slots as independent observations
     • Align values across slots only when your assertion explicitly establishes that relationship
     • Use protocol-specific knowledge of write order when timing relationships matter

​

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