[RFC] Constraint discovery using symbolic execution

[gustavo-grieco]

This is some very experimental code produced after a discussion started by @GalloDaSballo asking if symbolic execution could be used to extract simple constraints for inputs that do NOT trigger reverts (and speed up the exploration). I created this very crude prototype to experiment with this idea. This is an example on how to use it:

1. Start with a simple smart contract:

pragma solidity ^0.8.13;

contract C {
  uint256 internal state = 0x123;
  address internal actor;
  mapping(address => uint256) internal balance;
  constructor() {
    balance[address(this)] = 0x999;
    balance[msg.sender] = 0x888;
    actor = msg.sender;
  }
  function oneConstraint(uint256 x1, uint256 x2, uint256 x3, uint256 x4) external {
      require(x4 <= balance[actor]);
      require(x3 + 1 >= 0x99);
      state = 1;
  }
}

2. Download and install the binary produced by this PR.
3. Run echidna model.sol --sym-exec true --test-mode assertion --format text

It will output a lot of data with raw SMT data. In particular, you should look for this:

Constraints inferred:
arg3 >= 0x99
arg4 <= 0x888

The code we have right now only provides an approximation for the constraints (as you can see in this example). It can be extended for more operands (probably you can vibe code it).

If this results in useful constraints, this simple range information could be passed to the fuzzing engine to be able to discard or generate valid values faster. Right now, there is nothing else except printing constraints.

This PR should be merged as it is, but it is intended to open for the discussion and experimentation.

[gustavo-grieco]

Made some modification to make it work with this example to obtain upper bounds for ticks:

pragma solidity ^0.8.13;

contract C {
  uint160 internal currentTick;
  function useTickForSomething(int24 tick) public {
    currentTick = getSqrtRatioAtTick(tick);
  }

  /**
   * @notice Minimum tick that may be passed to #getSqrtRatioAtTick computed from log base 1.0001 of 2**-128
   */
  int24 internal constant _MIN_TICK = -887272;

  /**
   * @notice Maximum tick that may be passed to #getSqrtRatioAtTick computed from log base 1.0001 of 2**128
   */
  int24 internal constant _MAX_TICK = -_MIN_TICK;

  function getSqrtRatioAtTick(
    int24 tick
  ) internal pure returns (uint160 sqrtPriceX96) {
    uint256 absTick = tick < 0 ? uint256(-int256(tick)) : uint256(int256(tick));
    require(absTick <= uint256(int256(_MAX_TICK)), 'T'); // TODO need convert int24 to uint256
    
    return 1; // CHANGE: Introduced early return

    uint256 ratio = absTick & 0x1 != 0
      ? 0xfffcb933bd6fad37aa2d162d1a594001
      : 0x100000000000000000000000000000000;
    if (absTick & 0x2 != 0) {
      ratio = (ratio * 0xfff97272373d413259a46990580e213a) >> 128;
    }
    if (absTick & 0x4 != 0) {
      ratio = (ratio * 0xfff2e50f5f656932ef12357cf3c7fdcc) >> 128;
    }
    if (absTick & 0x8 != 0) {
      ratio = (ratio * 0xffe5caca7e10e4e61c3624eaa0941cd0) >> 128;
    }
    if (absTick & 0x10 != 0) {
      ratio = (ratio * 0xffcb9843d60f6159c9db58835c926644) >> 128;
    }
    if (absTick & 0x20 != 0) {
      ratio = (ratio * 0xff973b41fa98c081472e6896dfb254c0) >> 128;
    }
    if (absTick & 0x40 != 0) {
      ratio = (ratio * 0xff2ea16466c96a3843ec78b326b52861) >> 128;
    }
    if (absTick & 0x80 != 0) {
      ratio = (ratio * 0xfe5dee046a99a2a811c461f1969c3053) >> 128;
    }
    if (absTick & 0x100 != 0) {
      ratio = (ratio * 0xfcbe86c7900a88aedcffc83b479aa3a4) >> 128;
    }
    if (absTick & 0x200 != 0) {
      ratio = (ratio * 0xf987a7253ac413176f2b074cf7815e54) >> 128;
    }
    if (absTick & 0x400 != 0) {
      ratio = (ratio * 0xf3392b0822b70005940c7a398e4b70f3) >> 128;
    }
    if (absTick & 0x800 != 0) {
      ratio = (ratio * 0xe7159475a2c29b7443b29c7fa6e889d9) >> 128;
    }
    if (absTick & 0x1000 != 0) {
      ratio = (ratio * 0xd097f3bdfd2022b8845ad8f792aa5825) >> 128;
    }
    if (absTick & 0x2000 != 0) {
      ratio = (ratio * 0xa9f746462d870fdf8a65dc1f90e061e5) >> 128;
    }
    if (absTick & 0x4000 != 0) {
      ratio = (ratio * 0x70d869a156d2a1b890bb3df62baf32f7) >> 128;
    }
    if (absTick & 0x8000 != 0) {
      ratio = (ratio * 0x31be135f97d08fd981231505542fcfa6) >> 128;
    }
    if (absTick & 0x10000 != 0) {
      ratio = (ratio * 0x9aa508b5b7a84e1c677de54f3e99bc9) >> 128;
    }
    if (absTick & 0x20000 != 0) {
      ratio = (ratio * 0x5d6af8dedb81196699c329225ee604) >> 128;
    }
    if (absTick & 0x40000 != 0) {
      ratio = (ratio * 0x2216e584f5fa1ea926041bedfe98) >> 128;
    }
    if (absTick & 0x80000 != 0) {
      ratio = (ratio * 0x48a170391f7dc42444e8fa2) >> 128;
    }

    if (tick > 0) ratio = type(uint256).max / ratio;

    // this divides by 1<<32 rounding up to go from a Q128.128 to a Q128.96
    // we then downcast because we know the result always fits within 160 bits due to our tick input constraint
    // we round up in the division so getTickAtSqrtRatio of the output price is always consistent
    sqrtPriceX96 = uint160((ratio >> 32) + (ratio % (1 << 32) == 0 ? 0 : 1));
  }
}

The result of running this is:

Constraints inferred:
arg1 <= 0xd89e8

This is only the upper bound. The lower bound is harder since there is a sign operation, and it must be inferred that the program is computing the absolute value (which is hard). In any case, note that I introduced an early return. I need to check exactly how the partial computations are obtained from the model returned by hevm (otherwise, the contraints are empty 🤔 ).

[gustavo-grieco]

The issue with the partials is solved in argotorg/hevm#822, waiting for upstream response.

[gustavo-grieco]

The latest revision is able to handle partials executions and also advanced interval resolution with basic arithmetics. For instance:

  constructor() {
    balance[address(this)] = 0x999;
    balance[msg.sender] = 0x888;
    actor = msg.sender;
  }
  function oneConstraint(uint256 x1, uint256 x2, uint256 x3, uint256 x4) external {
      require(x4 >= balance[actor]);
      require(!(x3 - 100 >= 0x99));
      ...
  }

the response is:

Constraints inferred:
arg3 <= 0xfd
arg3 >= 0x64
arg4 >= 0x888
Constraints resolved:
arg3 in [0x64, 0xfd]
arg4 >= 0x888