Genuine, unique divergence — fixed in the engine and merged. +1 on the leaderboard.
Independent in-scope soundness gap, first-file review in submission timestamp order. The exact screened source produced SOUNDNESS_GAP on the previous main and NO_DIVERGENCE on merged c1827fb64e6a; raw return bytes, events, and full ordinary storage match the EVM. The 2,326-job full build, 85-case contest suite, focused Lean witnesses, and four neighboring credited controls passed. No harness, comparator, contest rule, or exclusion changed.
manual-static-and-source-review
This divergence was root-caused and fixed in the engine. Fixed in PR #105 →
A memory-copy initializer evaluated the indexed storage alias base before selecting its dynamic-array member. That materialized a mapping-bearing Box and panicked. Evaluating the complete storage-rooted path before loading the selected member fixes the copy. This is independent of the earlier full-width returned-reference index issue: this source uses literal indexes and does not exercise its narrow-cast guard.
// SPDX-License-Identifier: MIT
pragma solidity 0.8.35;
/* ===ARENA-MANIFEST===
{
"deploy": {
"contract": "C",
"args": [],
"value": 0
},
"entry": {
"function": "run",
"args": [],
"value": 0
},
"lane": "S",
"feature": "fixed-mapping-struct-access-after-dynamic-array-copy",
"note": "After copying a dynamic-array field from a fixed mapping-bearing struct element to memory, accessing the same field through a different fixed-array element succeeds on the EVM but panics in Solidity-Lean. The copy alone and the later access without the copy both agree."
}
===END-ARENA-MANIFEST=== */
struct Box {
uint256[] words;
mapping(uint256 => uint256) values;
}
contract C {
Box[2] boxes;
function run() external returns (uint256) {
Box storage box0 = boxes[0];
box0.words.push(18);
uint256[] memory copied = box0.words;
return boxes[1].words.length;
}
}