SMTChecker: Unable to support ripemd160, sha256 well - Githubissues

ethereum / solidity

Solidity, the Smart Contract Programming Language

https://soliditylang.org

GNU General Public License v3.0

22.66k stars 5.62k forks source link

SMTChecker: Unable to support ripemd160, sha256 well #15143

Closed Subway2023 closed 1 month ago

Subway2023 commented 1 month ago

Description

Similar to 14983， the SMTChecker cannot evaluate the results of these functions

Environment

Compiler version: 0.8.25
Target EVM version (as per compiler settings): No restrictions
Framework/IDE (e.g. Truffle or Remix): Command-line
EVM execution environment / backend / blockchain client: None
Operating system: Linux

Steps to Reproduce

contract test {

    function f()public returns (int) {
        bytes memory t0="1";
        bytes memory t1="1";
        bytes32 a=ripemd160(t0);
        bytes32 b=ripemd160(t1);
        assert(a==b);
    }
}

contract test {

    function f()public returns (int) {
        bytes memory t0="1";
        bytes memory t1="1";
        bytes32 a=sha256(t0);
        bytes32 b=sha256(t1);
        assert(a==b);
    }
}

1716521695310

blishko commented 1 month ago

This has the same underlying issue as #14983 and has been fixed by #15050. At develop, and in the latest release, v0.8.26, SMTChecker already proves this assertions safe.