Promote shifts across blocks in reconstruct_fallible_operations

[MavenRain]

Fixes #1041.

Root cause

The issue suggested the promotion pattern fails to match shifts assigned through a dereferenced pointer, but the pattern never inspects the assignment destination at all (make_binop_overflow_panic visits every Rvalue). The actual mechanism: rustc evaluates the shift operands, and emits the overflow check, before computing the destination place. When that computation involves a function call, as with the overloaded IndexMut in the MWE, the call is a block terminator in ULLBC, so the deferred shift lands in the block the call returns to:

bb0: {
    ...
    _4 = cast<i32, u32>(const 20i32);
    _5 = move _4 < const 64u32;
    assert(move _5 == true) (overflow) else panic;
    ...
    _6 = index_mut<'6>(move _7, const 0usize) -> bb2 (unwind: bb1);
}
bb2: {
    ...
    (*_6) = move _3 wrap.>> const 20i32;
    ...
}

remove_dynamic_checks pattern-matches within a single statement sequence, never finds the shift, and conservatively leaves the wrapping shift, which is what Aeneas then extracts.

The fix

The two shift arms now record a PendingShiftCheck (block, checked amount operand) when the shift is not in the same block. After the per-block sweep, resolve_pending_shift_check follows the Goto/Call chain out of the block, traversing only single-predecessor blocks so the shift cannot be reached without passing the check, and promotes the first still-wrapping shift by the checked amount (reusing make_binop_overflow_panic). The walk gives up if the checked operand is not a constant or a plain local, or if the call destination or any statement scanned before the shift could touch that local. Pending checks are only recorded for Overflow asserts, so the bounds checks that share the second pattern never trigger a cross-block walk.

Unlike the per-block path, the check statements are deliberately NOT removed here, for two reasons:

1. The check fires before the interposed call; removing it would move the failure point past the call's side effects, and past its potential divergence (a user index_mut that loops forever on some input would turn a must-panic execution into a non-terminating one).
2. It makes the resolution robust by construction. Matching is by amount operand, so two shifts by the same constant amount (a literal or a const generic) around interposed calls could in principle cross-match. Since promoting a shift that rustc guards with an overflow check never changes behavior (the check makes the panic-on-overflow unreachable), and no check is ever dropped, even a mispaired promotion leaves the emitted ULLBC semantically exact. I verified this on a two-widths const-generic torture case (o8[{ o64[0] = x >> N; 0 }] = w >> N; with W64/W8 wrappers): both shifts get promoted and both checks stay.

The leftover assert is redundant next to the promoted shift, but harmless to consumers. If you would rather have the assert removed for output cleanliness, that requires deciding the two points above; happy to iterate.

Testing

• New UI test issue-1041-shift-through-index-mut.rs with the issue's MWE plus a variable shift amount (exercises both the cast and no-cast check shapes, and the local-operand tracking). Both now produce panic.>>/panic.<<.
• Full charon test suite passes; no other test output changed, so the blast radius is exactly the issue's case. cargo clippy clean, cargo fmt clean.
• The AST is unchanged, so charon-ml is unaffected and no version bump should be needed.

Drafted with AI assistance; the analysis, code, and tests were reviewed and run by me.

[Nadrieril]

Hi! Thank you for your contribution. Would you mind re-writing your PR description yourself? It is currently decent but still full of unnecessary details that LLMs love to add.

Then, instead of leaving the check, I would like to remove the check and do the arithmetic computation early instead (and store it in a fresh variable). That's always correct since the only side-effects are the panic and the memory accesses, all of which are already done by the overflow check.

Also your solution is doing too much work to be correct compared to what we need: we don't need to follow the graph structure since these asserts are only ever emitted by the compiler: let's simply look for all the uses the given local in the body.

Also I'd like to handle the shift checks in a single pass: iterate over the whole body looking for shifts that use the operand in question, and replace them all. To know where to insert the original computation, record the StmtLoc for the original assert. I expect this will generalize better, since it's likely we'll need something like this for other fallible operations in the future.