Proof-mode: discharge dynamic array bounds as Rocq proof obligations

[0xGeorgii]

Summary

In Proof mode, discharge dynamic array bounds as Rocq proof obligations, so the verified artifact is provably bounds-safe and a proven module can safely elide the runtime guard.

Background

#164 added array bounds checking:

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

The runtime guard is intentionally not emitted in Proof mode (which always resolves to a release opt level). Proof mode produces the .v translation that downstream Rocq proofs consume. Today, the generated .v lowers a dynamic arr[i] to a bare BI_load/BI_store with no side condition — neither ValidModule (structural well-formedness) nor ValidSpec (per-spec invariant on spec-block functions) currently expresses "every dynamic access is in bounds." So the proven artifact carries no bounds obligation.

Proposal

Make dynamic bounds a discharged proof obligation on the verified path:

1. Emit the bounds guard in Proof mode too, so each dynamic access lowers to if i >= len then BI_unreachable (BI_unreachable is already modeled by the translator).
2. Extend the Rocq contract (core/wasm-to-v/ROCQ_CONTRACT.md): give ValidModule/ValidSpec (or a dedicated predicate) a "no reachable BI_unreachable/trap" component, so proving validity forces proving 0 <= i < length for every guarded access.
3. With that in place, a proven module may safely drop the runtime guard in the deployed (Compile-mode) build — the property is established statically — keeping verified = deployed.

The downstream Rocq-library half (the ValidModule no-trap clause) lives outside this repo; this issue covers the compiler-side emission + the contract change, coordinated with the consumer library.

Relationship

• Builds on Array Bounds Checking #164 (the runtime guard) and the wasm-to-v proof pipeline.
• Complements Static rule: require a dominating in-bounds guard before dynamic array indexing #212 (a source-level dominating-guard rule): Static rule: require a dominating in-bounds guard before dynamic array indexing #212 forces the programmer to write a recoverable guard; this issue discharges bounds via Rocq proof instead. Either path closes the "no silent OOB" gap on the verified artifact.
• Tracked as Array Bounds Checking #164 Deferred Work.

Future work.