narrowing conversion of an out-of-range `constant` variable is not truncated, so failing assertions are proved safe

Open
  • Is something wrong?
#17,162 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
43/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Tech stack
cpp, solidity
Domain
compilers, testing

Research direction

Start in libsolidity/formal/SMTEncoder.cpp, at visitTypeConversion and the castSize < argSize branch named in the report. Compare how constant variables are handled with the narrowing conversion semantics described in the Solidity documentation, and use the supplied C.sol reproducer with the given SMTChecker command to inspect the result. Done means the checker reports violations for both assertions that fail on the EVM.

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 (and BMC) report "Assertion violation check is safe!" for assertions that fail on the EVM.

Version: 0.8.37+commit.f401782d (static linux binary). Also reproduces at develop 3eb0c3acb41f (0.8.38-develop.2026.10.20+commit.3eb0c3ac).

Preconditions: default SMTChecker settings; the program narrows a constant variable (or a constant expression over one) whose value does not fit the target type.

Input
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.0;
contract C {
  uint256 constant K = 300;
  function f() public pure returns (uint8) {
    uint8 r = uint8(K); // 44 on the EVM
    assert(r != 44);    // fails on the EVM
    return r;
  }
  function g(uint256 x) public pure {
    uint8 r = uint8(K);
    r;
    assert(x != 5);     // fails for x = 5
  }
}
Command
SOLC=/path/to/solc ./run.sh   # exit 1 = bug reproduced, 0 = fixed, 2 = tool missing / harness error

solc --model-checker-engine chc --model-checker-targets assert --model-checker-show-proved-safe C.sol
Output
Info: CHC: Assertion violation check is safe!
 --> C.sol:7:5:
  |
7 |     assert(r != 44);    // fails on the EVM
  |     ^^^^^^^^^^^^^^^

Info: CHC: Assertion violation check is safe!
  --> C.sol:13:5:
   |
13 |     assert(x != 5);     // fails for x = 5
   |     ^^^^^^^^^^^^^^

Running the compiled runtime on geth 1.17.8 (EELS gives the same result), f() and g(5) both revert with Panic(0x01):

$ evm run --input 26121ff0 "$(solc --bin-runtime C.sol | tail -n 1)"   # f()
$ evm run --input e420264a00…05 "$(solc --bin-runtime C.sol | tail -n 1)"   # g(5)

{"tool": "geth", "fork": "osaka", "status": "revert", "returndata": "0x4e487b710000000000000000000000000000000000000000000000000000000000000001", "gas_used": 21253, "logs": [], "storage": {}, "error": "execution reverted"}
{"tool": "geth", "fork": "osaka", "status": "revert", "returndata": "0x4e487b710000000000000000000000000000000000000000000000000000000000000001", "gas_used": 21663, "logs": [], "storage": {}, "error": "execution reverted"}
Expected

Violations for both assertions. Per the docs (Types > Conversions between Elementary Types > Explicit Conversions): "If an integer is explicitly converted to a smaller type, higher-order bits are cut off", so uint8(K) is 44. docs/smtchecker.rst says a target reported safe is safe.

The modelled value is the untruncated 300, which makes the rest of the function infeasible. Because of that, assert(x != 5) is reported safe even though it never reads r. Using uint8(uint256(300)) or a non-constant argument gives the correct counterexample (r = 44). Location: libsolidity/formal/SMTEncoder.cpp visitTypeConversion, castSize < argSize branch (line 1236 at develop). It takes the isConstant() shortcut ("The TypeChecker guarantees that a constant fits in the cast size", from #11377). Since isConstant() also folds constant variables via ConstantEvaluator, the guarantee only holds for literals. #16653 / #16654 fixed the same isConstant pattern for unary operators only.

Reproducer files

C.sol

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.0;
contract C {
  uint256 constant K = 300;
  function f() public pure returns (uint8) {
    uint8 r = uint8(K); // 44 on the EVM
    assert(r != 44);    // fails on the EVM
    return r;
  }
  function g(uint256 x) public pure {
    uint8 r = uint8(K);
    r;
    assert(x != 5);     // fails for x = 5
  }
}

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 (CHC proves assertions safe that fail on the EVM), 0 = fixed, 2 = harness error
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; }
source "$D/oracle.sh"
"$S" --version | tail -n 1
out="$("$S" --model-checker-engine chc --model-checker-targets assert --model-checker-show-proved-safe "$D/C.sol" 2>&1)" || { echo "harness error"; exit 2; }
echo "$out"; safe=$(echo "$out" | grep -c "Assertion violation check is safe")
code="$("$S" --bin-runtime "$D/C.sol" | tail -n 1)"
fails=0
for cd in 26121ff0 e420264a0000000000000000000000000000000000000000000000000000000000000005; do
  for o in geth; do j="$(oracle "$code" "$cd")" || exit 2; echo "$o 0x$cd: $j"
    echo "$j" | grep -q '4e487b710000000000000000000000000000000000000000000000000000000000000001' && fails=$((fails+1)); done
done
echo "CHC safe: $safe/2, EVM Panic(0x01): $fails/2"
[ $fails -eq 2 ] || exit 2
[ $safe -gt 0 ] && exit 1 || exit 0

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.