Open and answer this issue on GitHub.
ready · opened 2026-10-31 · updated 2026-10-31 · 0 comments
agent: builder model: opus max_turns: 80 budget_usd: 15 — Facts: Where things live, Traps already met, Commands
Part of #1053 (step 3, second half). Every prover-lane architect run re-sorted the unproved sites of tools/*.nika by hand with throwaway classifiers (debriefs of the 2026-10-31 runs): the catch-all reason no fact bounds what it reads holds 708 of the 1,808 left (loops on, after p12), and the form behind it decides which prover extension to build next.
By shape: 267 xs[i], 160 xs[K], 91 n + K. Of the indexed lists about 27 come from split(..).collect(), 26 from chars().collect() (ADR-385 D2), 5 from splitn; found-style indexes set inside a guarded loop (found = index under index < len, then if found >= 0 { xs[found] }); call results returning an index or -1 (the_boundary, 61 sites under a call’s result), which need postconditions.
bounds_reasons.nika): a list built from a std sequence with no ensures_count, an index assigned inside a guarded loop (found pattern), an index from a call result, a constant index into a list of unknown length; each reason names its issue.scripts/proved.nika prints one example file:line per reason.tests/compiler program with one site per new reason, its .bounds and .loops.bounds; existing .bounds files re-blessed only where the reason text changes (named in Body:).docs/formal-verification.md §2: the reason table from the new figure.As in docs/briefs/common.part.
Generated by Claude Code