Storage pointer bound to an index containing a function call fails closed with Panic(0)

Source

// SPDX-License-Identifier: MIT
pragma solidity 0.8.35;

/* ===ARENA-MANIFEST===
{
  "deploy": { "contract": "T", "args": [], "value": 0 },
  "entry": { "function": "run", "args": [] },
  "feature": "storage-pointer-bound-to-index-containing-a-function-call",
  "note": "Binding a storage pointer whose INDEX EXPRESSION CONTAINS A FUNCTION CALL makes solidity-lean fail closed with Panic(0) (generic/internal), while solc+EVM executes normally. Here the EVM returns 0 (unset mapping entry) and the model reverts.\n\nKNOCKOUT MATRIX (each adjudicated separately on this rig; the FIRST FOUR are the ones that matter because they eliminate the obvious explanations):\n  - hoist the call into a local first: `uint256 k = key(); items[k]`  -> NO_DIVERGENCE. So it is not the call per se; moving it one line earlier fixes it. The defect is specifically a call INSIDE the index expression.\n  - index read from a plain STATE VARIABLE (no call)                 -> NO_DIVERGENCE. Not about non-literal indices.\n  - index as an arithmetic expression `items[base + 2]` (no call)    -> NO_DIVERGENCE. Not about expression complexity.\n  - literal index `items[3]`                                          -> NO_DIVERGENCE (control).\n  - WRITE through the pointer instead of reading                      -> still diverges.\n  - dynamic ARRAY receiver instead of a mapping                       -> still diverges.\n  - `view` (state-reading) call in the index instead of `pure`        -> still diverges.\n  - two pointers bound together in a TUPLE with literal indices       -> NO_DIVERGENCE. The tuple binder is NOT implicated.\nNecessary+sufficient: a storage-pointer binding whose index expression contains a call. Neither the tuple, nor the write, nor the receiver kind is required. This is the smallest form: no tuple, no write.\n\nWHY THIS FRAMING MATTERS: the same underlying defect is reachable via an all-storage tuple declaration, where it surfaces instead as SILENTLY DROPPED WRITES (the model returns the right value but persists nothing). Attributing it to the tuple binder would be wrong -- the tuple with literal indices is clean, and the single-pointer form with a call index is both smaller and more severe (revert-vs-success rather than wrong-state)."
}
===END-ARENA-MANIFEST=== */

contract T {
    struct Item {
        uint256 value;
    }

    mapping(uint256 => Item) items;

    function key() internal pure returns (uint256) {
        return 3;
    }

    function run() external returns (uint256) {
        Item storage a = items[key()];
        return a.value;
    }
}