Open and answer this issue on GitHub.
compiler, decision · opened 2026-10-03 · updated 2026-10-31 · 1 comment
This is the largest single row in ADR-276 §3: about 28 sites in dynamic-programming tables. Examples:
d[i - 1][j] + 1d[i - 1][j - 1] + costcommon[i + 1][j + 1] + 1ADR-272 D2 bounds a list’s values only when every write is proved within a bound that does not depend on the list itself. Here every value is computed from other values of the same table, so no constant bound can be found. The truth is a bound like d[i][j] <= i + j, which depends on the position.
<= x.len() + y.len()) would be enough, together with the address-space issue for lengths.Hey Team, quick one before the weekend:
Regarding the open questions on position-dependent bounds in dynamic programming tables:
Hint-Based Invariant Heuristic (Rule A - Primary Path): Rather than attempting full automatic synthesis of complex position-dependent invariants ($d[i][j] \le i + j$), the compiler injects an internal Ghost Invariant Template. For self-referential DP table writes, the verifier automatically tests an input-derived global bound ($\le \text{len}(x) + \text{len}(y)$) as an inductive lemma.
Inductive Verification: The verifier validates this injected lemma against the base cases and the recurrence step. If the inductive step holds, the DP table is proven memory-safe with zero manual annotations and minimal compile-time overhead.
Explicit Contract Fallback (Rule B):
Manual @invariant annotations remain available as a fallback for non-standard DP structures where values cannot be transitively bounded by input dimensions.
This eliminates the annotation burden across the 28 affected DP sites while maintaining deterministic proof performance.