SMTChecker: implicit `bytesN` -> `bytesM` (M > N) conversion is modelled without right-padding, so failing assertions are proved safe

Open
  • Is something wrong?
#17,157 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
48/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Tech stack
cpp, solidity
Domain
compilers, testing-qa

Research direction

Start in libsolidity/formal/SMTEncoder.cpp at SMTEncoder::expr and trace the implicit conversion through SymbolicVariable::currentValue in SymbolicVariables.cpp; compare it with the fixed-bytes widening path in visitTypeConversion. Run the supplied run.sh reproducer and inspect the existing SMTChecker tests for conversion coverage. Done means implicit widening produces the expected CHC verdicts while the explicit conversion control and equality case remain correct.

Written by the indexing model from the issue text.

Description

smt

Found by comparing the semantics described in the Solidity documentation with how the Solidity SMTChecker implements them. An AI agent found this bug, reproduced it with solc 35b1cb80 (develop) and drafted this report. A second agent tried to refute it and searched upstream for duplicates. The methodology is described here.

What went wrong: Wrong result: CHC reports "Assertion violation check is safe!" for an assertion that fails on the EVM, and reports a violation for one that always holds.

Version: 0.8.37+commit.f401782d and 0.8.38+commit.1835d247 (static linux binaries). Also reproduces at develop 672576f386f9 (0.8.39-develop.2026.10.27+commit.672576f3).

Preconditions: none, default settings (--model-checker-engine chc, default targets); the program converts a fixed-size bytes value implicitly to a wider fixed-size bytes type (assignment, declaration, argument, return value, comparison operand, mapping key).

Input
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.0;
contract C {
    function implicitWiden(bytes2 a) public pure {
        bytes4 b = a;               // implicit conversion: 0x1234 -> 0x12340000
        assert(b != 0x12340000);    // fails for a = 0x1234
    }
    function explicitWiden(bytes2 a) public pure {
        bytes4 b = bytes4(a);       // explicit conversion (control)
        assert(b != 0x12340000);    // fails for a = 0x1234
    }
    function implicitEqualsExplicit(bytes2 a) public pure {
        bytes4 b = a;
        assert(b == bytes4(a));     // holds for every a
    }
}
Command
SOLC=/path/to/solc EVM=/path/to/evm ./run.sh   # exit 1 = bug reproduced, 0 = fixed, 2 = tool missing / harness error

solc --model-checker-engine chc --model-checker-show-proved-safe C.sol
Output
Warning: CHC: Assertion violation happens here.
  --> C.sol:10:9:
   |
10 |         assert(b != 0x12340000);    // fails for a = 0x1234
   |         ^^^^^^^^^^^^^^^^^^^^^^^

Warning: CHC: Assertion violation happens here.
  --> C.sol:14:9:
   |
14 |         assert(b == bytes4(a));     // holds for every a
   |         ^^^^^^^^^^^^^^^^^^^^^^

Info: CHC: Assertion violation check is safe!
 --> C.sol:6:9:
  |
6 |         assert(b != 0x12340000);    // fails for a = 0x1234
  |         ^^^^^^^^^^^^^^^^^^^^^^^

On geth 1.17.8 (evm run, runtime from solc --bin-runtime C.sol, calldata selector + 1234 left-aligned in one word), both implicitWiden(0x1234) and explicitWiden(0x1234) revert with Panic(0x01), and implicitEqualsExplicit(0x1234) succeeds:

geth implicitWiden(0x1234): {"status": "error", "error": "execution reverted", "returndata": "0x4e487b710000000000000000000000000000000000000000000000000000000000000001", "storage": {}, "logs": 0}
geth explicitWiden(0x1234): {"status": "error", "error": "execution reverted", "returndata": "0x4e487b710000000000000000000000000000000000000000000000000000000000000001", "storage": {}, "logs": 0}
geth implicitEqualsExplicit(0x1234): {"status": "success", "error": "", "returndata": "0x", "storage": {}, "logs": 0}
Expected

implicitWiden behaves like explicitWiden: a violation with a = 0x1234. implicitEqualsExplicit is safe. The docs (Types > Conversions between Elementary Types) say: "If a fixed-size bytes type is explicitly converted to a larger type, it is padded on the right." Both code generators emit the same right-padded value for the implicit form. docs/smtchecker.rst says: "If it determines that a verification target is safe, it is indeed safe, that is, there are no false negatives (unless there is a bug in the SMTChecker)."

Only the explicit bytesM(x) path (visitTypeConversion, FixedBytes widening branch) shifts the value. Implicit conversions go through SMTEncoder::expr(Expression const&, Type const*) (libsolidity/formal/SMTEncoder.cpp:2572). That calls SymbolicVariable::currentValue(Type const*) (SymbolicVariables.cpp:64), which ignores the target type for value types. So bytes4 b = a is modelled as 0x00001234. BMC gives the same wrong verdicts.

Reproducer files

C.sol

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.0;
contract C {
    function implicitWiden(bytes2 a) public pure {
        bytes4 b = a;               // implicit conversion: 0x1234 -> 0x12340000
        assert(b != 0x12340000);    // fails for a = 0x1234
    }
    function explicitWiden(bytes2 a) public pure {
        bytes4 b = bytes4(a);       // explicit conversion (control)
        assert(b != 0x12340000);    // fails for a = 0x1234
    }
    function implicitEqualsExplicit(bytes2 a) public pure {
        bytes4 b = a;
        assert(b == bytes4(a));     // holds for every a
    }
}

oracle.sh

# Concrete EVM oracle: go-ethereum's `evm` tool (set EVM=/path/to/evm; default: from PATH).
# oracle RUNTIME_HEX [CALLDATA_HEX] [VALUE_WEI] -> one JSON line {status, error, returndata, storage, logs}; rc 2 on tool error.
EVM="${EVM:-evm}"
oracle() {
  local o e rc g=(); o=$(mktemp /tmp/oracle-o.XXXXXX); e=$(mktemp /tmp/oracle-e.XXXXXX)
  if [ "${3:-0}" != 0 ]; then  # fund the sender so a value transfer is possible
    g=(--prestate "$o.g" --sender 0x0000000000000000000000000000000000000001)
    echo '{"config":{"chainId":1,"homesteadBlock":0,"eip150Block":0,"eip155Block":0,"eip158Block":0,"byzantiumBlock":0,"constantinopleBlock":0,"petersburgBlock":0,"istanbulBlock":0,"berlinBlock":0,"londonBlock":0,"mergeNetsplitBlock":0,"shanghaiTime":0,"cancunTime":0,"pragueTime":0,"terminalTotalDifficulty":0,"blobSchedule":{"cancun":{"target":3,"max":6,"baseFeeUpdateFraction":3338477},"prague":{"target":6,"max":9,"baseFeeUpdateFraction":5007716}}},"alloc":{"0x0000000000000000000000000000000000000001":{"balance":"0xffffffffffffffff"}},"difficulty":"0x0","gasLimit":"0x1000000","timestamp":"0x0"}' > "$o.g"
  fi
  "$EVM" run --gas 10000000 --input "${2:-}" --value "${3:-0}" "${g[@]}" --dump --trace "$1" >"$o" 2>"$e"; rc=$?
  [ $rc -eq 0 ] && python3 -I - "$o" "$e" <<'PY'
import json,sys
o,e=open(sys.argv[1]).read(),open(sys.argv[2]).read()
tr=[json.loads(l) for l in e.splitlines() if l.startswith('{')]
last=tr[-1]; err=last.get("error","")
logs=sum(1 for t in tr if str(t.get("opName","")).startswith("LOG"))
accts=json.loads(o[o.index('{'):]).get("accounts",{})
st={}
for a in accts.values(): st.update(a.get("storage",{}))
print(json.dumps({"status":"error" if err else "success","error":err,"returndata":"0x"+last.get("output",""),"storage":st,"logs":logs}))
PY
  rc=$?; rm -f "$o" "$o.g" "$e"; [ $rc -eq 0 ] || echo "harness error: evm run failed" >&2; return $rc
}

run.sh

#!/usr/bin/env bash
# exit 1 = bug (implicit bytes2 -> bytes4 widening modelled without right-padding), 0 = fixed, 2 = harness error
# Spec-correct verdicts: implicitWiden VIOLATED, explicitWiden VIOLATED (control), implicitEqualsExplicit SAFE.
set -u
D="$(cd "$(dirname "$0")" && pwd)"
# Tools (override via env; defaults are looked up on PATH): SOLC, EVM (go-ethereum `evm`, the concrete oracle).
S="$(command -v "${SOLC:-solc}")" || { echo "harness error: solc not found (set SOLC)"; exit 2; }
command -v "${EVM:-evm}" >/dev/null || { echo "harness error: evm not found (set EVM)"; exit 2; }
source "$D/oracle.sh"
"$S" --version | tail -n 1
out="$("$S" --model-checker-engine chc --model-checker-show-proved-safe "$D/C.sol" 2>&1)" || { echo "harness error: solc"; echo "$out"; exit 2; }
echo "$out" | grep -E "^(Info|Warning): CHC|-->"
verdict() { # line -> safe | violated | none
  if echo "$out" | grep -A1 "Assertion violation check is safe" | grep -q "C.sol:$1:"; then echo safe
  elif echo "$out" | grep -A1 "Assertion violation happens here" | grep -q "C.sol:$1:"; then echo violated
  else echo none; fi; }
v_imp=$(verdict 6); v_exp=$(verdict 10); v_eq=$(verdict 14)
echo "CHC: implicitWiden=$v_imp (expected violated), explicitWiden=$v_exp (expected violated, control), implicitEqualsExplicit=$v_eq (expected safe)"
code="$("$S" --bin-runtime "$D/C.sol" | tail -n 1)"
ARG=1234000000000000000000000000000000000000000000000000000000000000   # a = 0x1234
for fn in implicitWiden explicitWiden implicitEqualsExplicit; do
  sel="$("$S" --hashes "$D/C.sol" | grep -oE "^[0-9a-f]{8}: $fn\(" | cut -c1-8)"
  j="$(oracle "$code" "$sel$ARG")" || exit 2; echo "geth $fn(0x1234): $j"
  case $fn in
    implicitEqualsExplicit) echo "$j" | grep -q '"status": "success"' || { echo "harness error: expected success"; exit 2; } ;;
    *) echo "$j" | grep -q '4e487b710000000000000000000000000000000000000000000000000000000000000001' || { echo "harness error: expected Panic(0x01)"; exit 2; } ;;
  esac
done
[ "$v_exp" = violated ] || { echo "harness error: control explicitWiden not reported violated"; exit 2; }
bug=0
[ "$v_imp" = safe ] && { echo "BUG: implicitWiden assertion proved safe, fails on the EVM"; bug=1; }
[ "$v_eq" = violated ] && { echo "BUG (second symptom): implicitEqualsExplicit reported violated, holds on the EVM"; bug=1; }
[ $bug -eq 1 ] && exit 1
[ "$v_imp" = violated ] && [ "$v_eq" = safe ] && { echo OK; exit 0; }
echo "harness error: unexpected verdicts"; exit 2

If this is intended behaviour or a duplicate, feel free to close it, and I'll use that as feedback to improve future reports. For questions, or to have this re-checked on a newer version of the Solidity SMTChecker, mention @JeroenRobben or email [email protected].

Dominant language
C++
Stars
25.8k
Forks
6.2k
Avg merge
1d 22h
Merged PRs (30d)
43

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from argotorg/solidity

All issues in argotorg/solidity

Similar issues

More C++ issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.