ABI-decoded checked int8 addition reports empty revert instead of Panic(0x11)

Credited

Genuine, unique divergence — fixed in the engine and merged. +1 on the leaderboard.

Details

First-file independent soundness gap. Exact screened source produced SOUNDNESS_GAP before fix and NO_DIVERGENCE on merged 2c55e7b018234469f17d8169268447b11b9d8a16. Raw Panic(0x11) bytes, events and ordinary storage agree with EVM. Focused Lean witness, full build and 85-case contest sample suite passed.

manual-static-and-source-review

Author: @rappie_eth
Points: 1
Verdict: SOUNDNESS_GAP
Resolution: Valid gap — fixed in the engine
Submitted: Oct 4, 2026, 01:24 PM
Reviewed: Oct 4, 2026, 08:15 PM

This divergence was root-caused and fixed in the engine. Fixed in PR #108 →

Root cause

The ABI builtin environment-cleanup gate recognized abi.encode but failed to inspect the outer abi.decode call. Its nested abi.encode argument containing checked int8 addition was lowered without the checked environment, producing a wrapped word and empty revert instead of Panic(0x11). Recursing through abi.decode preserves checked arithmetic.

Source

// 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":"abi-decoded-checked-int8-addition-local"}
===END-ARENA-MANIFEST=== */

contract C {
    int8 value;

    function run() external returns (int8) {
        int8 local = abi.decode(
            abi.encode(int8(int256(uint256(410))) + int8(int256(uint256(410)))),
            (int8)
        );
        value = local;
        return local;
    }
}