Issue #388: Two lists known to be as long as each other (rv[i] beside rc[i])

Open and answer this issue on GitHub.

compiler, decision · opened 2026-10-03 · updated 2026-10-31 · 1 comment

This comes from ADR-272 §6: 4 of the 9 index sites in the solver kernels that stay unproved index one list with a counter bounded by another list’s length. Examples:

• rv[i] with i < rc.len()
• blocks[k] beside list[k]

The lists are filled pairwise (one push each per turn) or are handed in as parameters that belong together. What is missing is a relation (rv.len() == rc.len()), not a bound.

Open

• From the fill: derive a.len() == b.len() where two lists are always pushed together.
• For parameters: across a call, this is a precondition. That relates to ADR-269 D5 and to ADR-276 D3.
• Measure: the rows kernel and the watch kernel.

Comments

keywan-ghadami, 2026-10-31

Prover lane (#1053), 2026-10-31, measured on tools/*.nika with lower-std --bounds --asserts (loops on): 112 unproved sites have the reason another list’s length.

• Parameter case: works today. assert(a.len() == b.len()) at the top of a function is a precondition the bounds walk uses (probed); callers must prove it (ADR-269 D5). Placing such asserts in the tools is #1053 step 8.
• Fill case: still open, and the bulk of the 112. Lists filled pairwise, e.g. for _ in handles { held.push(false) } then held[index] under index < handles.len(), or two lists pushed once each per turn. Architect’s reading (not decided yet, so the label stays decision): no syntax, every user gains, which makes it look obvious under the language principles; the open part is the rule (pushed once each on every path of a turn; built from the other’s length) and where it lives (bounds walk bounding_built, the D13 turn count).

Next step for the lane: decide the fill rule (ADR), then a brief. It ranks after #1103 (ADR-385 D2) in docs/briefs/prover/state.md.

---

Generated by Claude Code

Back to Open Issues