Issue #1217: Prover: an index computed by division keeps its bounds check although its bound is proved

Open and answer this issue on GitHub.

ready · opened 2026-11-03 · updated 2026-11-03 · 0 comments

Probe

fn mid(xs: Vec[int]) -> int {
    assert(xs.len() > 0)
    let h = xs.len() / 2
    assert(h >= 0 && h < xs.len())
    return xs[h]
}

Both asserts are proved, but check --bounds reports xs[h] checked: no fact bounds what it reads. Writing xs[xs.len() / 2] under the same precondition reports a parameter no precondition bounds.

The check removal does not use facts the prover has already proved: a proved assert(h < xs.len()) must bound xs[h] (Part III 14.2, 13.3, ADR-306). The prover also does not read n / 2 < n for n > 0, which the direct form needs.

Found while writing the prover chapter of the guide.

To build

1. A proved assert about an index (h >= 0 && h < xs.len()) removes the check of xs[h] that follows, while h and xs are unchanged. Test in tests/compiler/ with check --bounds output.
2. Division by a positive constant: 0 <= a and c >= 2 give a / c < a when a > 0, and 0 <= a / c <= a. Then xs[xs.len() / 2] under xs.len() > 0 is unchecked. Test.

Back to Open Issues