Nikaia
Menu
v0.0.1343pre-alpha GitHub

agent: builder model: opus max_turns: 120 budget_usd: 25 —

Brief p4: #1054 step 2, the bounds walk asks a loop’s checks with the prover’s invariants, and states a sum’s goal against a value of its type

Facts: Where things live, Traps already met, Commands

Score: S=3 (ADR-361 D10 is decided and not built for the checks: p2 built it for asserts only; 281 of the tools package’s unproved operations are x += 1), O=3 M (every counter extension of the lane, #432 next, rests on it), C=10 M (two places in bounds_walk.nika, the portfolio reused from prover_loops.nika), area prover.

Problem (probed 2026-10-31 on 1ebd8fc’s binary)

p2 (1ebd8fc) proves an assert inside a loop through the loop. Its step 2, the checks the compiler writes itself (D10), was not built. The report found two causes:

  1. The bounds walk guesses its own loop invariants. bounding_loop_guesses only offers halves of the facts the loop starts with. It never offers the prover’s closed forms (ADR-361 D5 item 1), so s == i is never a candidate. ADR-361 D10 says a check is asked “through the loop’s problem (D2)”, with the same portfolio as an assert. One portfolio, not two.
  2. A sum is proved only below 2^62. bounding_fits asks t <= min(type max, solvable()), where solvable() is 2^62 (#444: the solver counts in i64, so the goal t <= i64::MAX cannot be stated). With while i < n, n: i64 unbounded, i + 1 <= n holds, but n may be above 2^62, so i += 1 stays checked even with no loop reasoning at all.

Probe (target/fast/nikaia check --bounds --optimization prove-through-loops:on probe.nika, outside tests/compiler):

fn k() -> i64 sync {
    let mut i = 0
    let mut s = 0
    while i < 10 {
        s += 1          // checked today; proved after (s == i, i < 10)
        i += 1
    }
    return s
}

fn g(n: i64) -> i64 sync {
    let mut i = 0
    while i < n {
        i += 1          // checked today; proved after (i + 1 <= n, n an i64), also under `off`
    }
    return i
}

fn f(n: i64) -> i64 sync {
    let mut i = 0
    let mut j = 0
    while i < n {
        j += 1          // checked today; proved after (j == i, i + 1 <= n)
        i += 1          // checked today; proved after
    }
    return j
}

fn w(xs: ref Vec[i64]) -> i64 sync {
    let mut i = 0
    let mut s = 0
    while i < xs.len() {
        s += 1          // checked today; proved after (s == i, i < xs.len())
        i += 1          // proved today
    }
    return s
}

fn c(xs: ref Vec[i64]) -> i64 sync {
    let mut n = 0
    for x in xs {
        if x > 0 { n += 1 }   // stays checked: a counter bounded by the turns (#432, the next brief)
    }
    return n
}

fn main() {
    print(k() + g(3) + f(3) + w([1, 2]) + c([1, -1]))
}

Today: 11 operations, 1 proved. Lane figure today (lower-std --bounds, then scripts/proved.nika): 1,493/2,583 indexes and 712/1,594 operations under off; 1,525 and 719 under prove-through-loops:on.

Decision (architect, 2026-10-31, under Language decisions: it changes what is proved, never what a program means)

Locations (scripts/where.nika, 2026-10-31)

Steps

  1. The relative goal in bounding_fits. With check --bounds (under off), g’s i += 1 is proved. Soundness rows, which must stay checked: while i < n { s += 2; i += 1 } with s starting at 0 (s + 2 <= n does not follow); an i32 sum bounded only by an i64 name; while true { s += 1 }. Put these rows in a second probe file and quote its header line under Tests:. Commit.
  2. The portfolio for D10. Under prove-through-loops:on, k’s s += 1, f’s j += 1 and i += 1, and w’s s += 1 are proved. c’s n += 1 stays checked. Soundness rows that must stay checked: while i < 100 { s += 2; i += 1 } with s: i8 (200 leaves i8); a counter assigned s = s * 2 in the body. Keep crates/nikaia/tests/it/prove_through_loops.rs and the prove_* tests in tests/compiler/tests/ passing. Commit.
  3. The figure. Run lower-std --bounds, with and without --optimization prove-through-loops:on, then scripts/proved.nika on each. Give both proved: lines under Tests: and in Body:. tests/compiler cannot show --bounds output, so check --bounds on the probes stands for the tests: add no Rust test (CLAUDE.md). This finishes #1054: the report says Fixes: #1054.

Stop about 15 turns before max_turns. Commit what is finished and report partial, with what you ruled out.

Rules (CLAUDE.md; this block is pasted into every brief, also a fix-forward)

Report (at most 15 lines, to exactly docs/briefs/prover/p4-1054-loop-checks.md.report.md)

Fields of docs/architect.md, Briefs and reports: Result: done|noop|partial|blocked (the bare word alone on that line: Result: done, never a summary after it, which cuts the batch, b869a 2026-10-27; Owner: is a question for the owner or none, never a role), Files, Commit, Body (optional, one paragraph for the commit message), Fixes, Pushed, Tests, Gate (green|red), Deviation, Found, Needs, Changelog, Owner, Disk freed, and for a move Rs2nika: (the kept N of M lines of rs2nika --score, then the three costliest hand edits; none for a task that moves no Rust, none (redesign) for a brief with Shape: redesign and no Convert: line). none where nothing, and then the bare word: Deviation: none (a note) cuts the batch (batch.nika compares exactly); a note goes into the commit message. Found: is only for a defect outside your change (it cuts the batch); a process event such as another session resetting or rewriting your files is no Found:, it goes under Needs: (m3a 2026-10-28); a converter draft that came out wrong is no Found:, it is one of the costliest edits under Rs2nika:, which the converter lane reads (e12-4b 2026-10-27); how you solved your own step goes into the commit message. Deviation: is only a step of the brief built otherwise than written or not built (a choice the brief left to you, such as keep what X needs and say so, is no deviation: it goes into the commit message; nor is building two steps in one commit when every step is built, e12-3a 2026-10-27, nor a step another commit on develop already built, shown by your test failing with that commit’s change reverted, b889 2026-10-27: name the commit in Body:, nor a test’s expected .stdout/.stderr taken from what the program really prints where the brief’s sketch of it was short or wrong, b934 2026-10-29: say so in Body:, nor a lowering that follows the ADR governing it where the brief’s expected lowering contradicts that ADR, b933 2026-10-29: name the ADR in Body:, nor a lowering other than the brief’s where rustc cannot take the brief’s, b1029 2026-10-31: say why in Body:, nor re-keying an allow-list entry (KNOWN) whose hash changed for the same program and the same reason, b-fixforward-sweep2 2026-10-28: say so in Body:, nor an existing test’s expected .stdout/.stderr updated because your change rightly changes the message it prints, b1012b 2026-10-31: name the test in Body:); how you verified (e.g. a test not run against the unfixed compiler) goes under Tests:. A noop says why under Tests: (what was probed), not under Deviation:. Final answer, one line: done <sha>, report <path> (or BLOCKED: ... / PUSH REJECTED ...).

Attribution: Co-Authored-By: Claude Opus 5.5 noreply@anthropic.com Claude-Session: https://claude.ai/code/session_01UVxJDtwVhc6jMtEYAyvwLU

This site is open source. Improve this page.