scribble icon indicating copy to clipboard operation
scribble copied to clipboard

Support structural equality comparison of non-value types in Scribble

Open cd1m0 opened this issue 4 years ago • 1 comments

We have use cases for comparing strings, arrays and structs in properties. However the base Solidity language doesn't support equality comparison of non-value types.

We could add structural equality comparison support to Scribble, by transpiling it into comparison between the abi.encode-ed versions of the data structures. So for example this:

contract Foo {
   /// #if_succeeds a == b;
   function main(string memory a, string calldata b) public { ... }
}

Would be transpiled to:

contract Foo is __scribble_ReentrancyUtils  {
    event AssertionFailed(string message);

    function main(string memory a, string calldata b) public {
        _original_Foo_main(a, b);
        unchecked {
            if (!(bytesEq(abi.encode(a), abi.encode(b)))) {
                emit AssertionFailed("0: ");
                assert(false);
            }
        }
    }

    function _original_Foo_main(string memory a, string calldata b) private { ... }
}
/// Utility contract holding a stack counter
contract __scribble_ReentrancyUtils {
    bool __scribble_out_of_contract = true;
    
    function bytesEq(bytes memory a, bytes memory b) internal returns (boolean) {
      if (a.length != b.length) { return false; }
      
      for (uint i = 0; i < a.length; i++) {
        if (a[i] != b[i]) return false;
      }
      
      return true;
    }
}

cd1m0 avatar Nov 18 '21 22:11 cd1m0

@cd1m0 Maybe we should use a different operator (e.g., encodingEq(a, b)) instead of == to avoid confusion. What do you think?

In general, it seems like this can become very expensive in terms of gas and we might want to be careful with supporting it. Hashing the bytes might be cheaper. Maybe bytesEq could have a separate early-return if the hashes are not equal.

wuestholz avatar Dec 20 '21 12:12 wuestholz

I started implementation in #224 to have some PoC. There are several questions to address:

  1. Do we want to extend ==, use custom operator (like =^= for example), or provide builtin for this functionality?
  2. Do we want to apply abi.encode() / abi.encodePacked() for the user (slightly rewrite code on call sites)?
  3. Do we want to refactor builtins addition flow to Scribble (as in current state it requires minor chages in multiple places to support new builtin function) or leave it to a followup pass?

Let me know what you think. Thanks.

blitz-1306 avatar May 10 '23 07:05 blitz-1306

This is implemented in #224 and would be a part of next release.

blitz-1306 avatar Jun 02 '23 11:06 blitz-1306