Static rule: require a dominating in-bounds guard before dynamic array indexing

[0xGeorgii]

Summary

Add a static analysis rule that requires every dynamic (runtime-index) array access to be protected by a dominating in-bounds guard the programmer wrote, so that an out-of-bounds index becomes recoverable, handled control flow instead of an implicit runtime trap.

Motivation

#164 added array bounds checking in two halves:

• A037 rejects constant-index out-of-bounds at compile time.
• A runtime guard (index >= length -> unreachable) traps dynamic out-of-bounds accesses in Debug builds.

For mission-critical software, an implicit trap is not ideal: the program halts instead of recovering. We want OOB on a dynamic index to be a code path the programmer explicitly handled. Example:

if idx < N {
    arr[idx];          // provably in bounds here
} else {
    // programmer-defined recovery
}

The rule rejects any dynamic arr[idx] that is not dominated by a condition establishing idx < N (and idx >= 0 for signed indices). N is the array length, which is always a compile-time constant in Inference ([T; N]), so the guard compares against the known literal N.

Note: there is no standard library yet, so we cannot require a len(arr) call — no such function exists. The bound is the static literal N the compiler already knows from the array's type, not a runtime len().

Scope

Flow-sensitive analysis — materially larger than the syntactic A0xx rules. It must reason about:

• Dominance: the guard reaches the access on all paths.
• No interfering mutation: idx (and the bound) are not reassigned between guard and use.
• Loop conditions: loop (i < N) { arr[i]; ... } — the loop condition bounds the index in the body.
• Bounds shape: handle &&, and the signed lower bound idx >= 0 (for unsigned indices the lower bound is free).

Accept the decidable common patterns; conservatively reject anything it cannot prove (forcing an explicit guard). False positives ("add a check") are safe; false negatives are not.

Open design decisions

1. Replace vs compose with the runtime trap from Array Bounds Checking #164 — does a proven source-level guard let us elide the runtime guard (safe-by-construction), or do we keep both (defense-in-depth)? Mission-critical usually wants both.
2. What the else may be — require a true recovery, or also allow an explicit assert/halt? The key invariant is that OOB is never implicit.
3. Interaction with the deferred Rocq proof-obligation path (Array Bounds Checking #164 Deferred Work): a source-level dominating guard is itself the evidence and closes the Release "unsafe window" without a silent trap.

Relationship

• Builds on Array Bounds Checking #164 (A037 + runtime guard).
• Context: spun out of Array Bounds Checking #164 during a design discussion on memory safety.

Future work.