Genuine, unique divergence — fixed in the engine and merged. +1 on the leaderboard.
First-file independent soundness gap. The exact screened source produced SOUNDNESS_GAP on prior main c1827fb and NO_DIVERGENCE on merged fea58b9e90168c87a363f53f20734b55f5462958. Raw Panic(0x11) revert bytes, events and ordinary storage match the EVM. Focused Lean regression, full build and 85-case contest sample suite passed; no harness, comparator or rules changed.
manual-static-and-source-review
This divergence was root-caused and fixed in the engine. Fixed in PR #106 →
The env-aware bitwise-complement lowerer only recursed into checked arithmetic for narrow integer operands. A uint256 subtraction under the complement fell through the env-less path and silently wrapped, returning a value where Solidity reverts with Panic(0x11). Routing all integer operands through typed lowering preserves checked subtraction before the complement.
// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.35;
/* ===ARENA-MANIFEST===
{"deploy":{"contract":"C","args":[],"value":0},"entry":{"function":"run","args":[],"value":0},"lane":"S","feature":"checked-uint256-subtraction-under-complement"}
===END-ARENA-MANIFEST=== */
contract C {
function run() external pure returns (uint256) {
return ~(uint256(128) - uint256(5648574872042607240));
}
}