SMTChecker is unable to accurately determine the output of abi.decoder

[Subway2023]

Description

SMTChecker is unable to determine whether the decoded value after using abi.decode is equal to the initial value encoded using abi.encode.

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 C{    
  function f() public{
      bytes memory corrupt = abi.encode(uint(1));
      uint decoded = abi.decode(corrupt, (uint));
      assert(decoded==1);
  }
}

solc C.sol --model-checker-engine all

[blishko]

SMTChecker cannot model precisely what ABI methods like encode and decode compute.
To stay sound, it over-approximates the possible behaviour.
This means that it only models the basic functional property: they yield equal output for equal inputs.
Otherwise, it assumes that the result can be any value.
This results in false positives that you see in this issue, but keeps the encoding sane.