xs.all(|x| ...)), and std’s sorted contracts (decision)Open and answer this issue on GitHub.
decision · opened 2026-10-24 · updated 2026-10-24 · 2 comments
Owner, 2026-10-24 (#796, claim (b)): a program should be able to say this list is sorted and this tree has only valid nodes, and the compiler should use it. Step 1 is decided and ready: ADR-381 and #797. A property is proved by name, carried to callers and checked once. It removes only its own check, because the property’s body is not read. The basis, the probes and the ladder are in docs/facts-about-data.md. The owner takes one question at a time.
binary_search requires is_sorted(). Where the order cannot be shown (data from outside, or an order lost over many steps), the program has two ways:
return … if !xs.is_sorted()), which costs O(n) and makes the property known until the list changes;unsafe { assume(xs.is_sorted()) } (ADR-376, exists today).Record: ADR-381 D5. D2 now also counts a guard and an assume. Spec: Part I (lists, after sort) and Part III 14.2.
Facts checked:
std has no binary_search or is_sorted today.assume in the default build (every remove-* switch off) and believes it only when a switch is on. So in the default build the O(n) walk is still paid.assume - decided 2026-10-24 (owner: option B)How it came up: Q2 made assume a common way out, and claim (b) is counted from --bounds. Probed on 0.0.1204: with unsafe { assume(0 <= i && i < v.len()) }, --bounds reports v[i] proved, and --asserts reports assumed 1. Nothing ties the proof to the assume, and nikaia.proofs does not record it either.
Decision: --bounds and --asserts report a check or claim that is proved only with an assume’s fact as proved from an assume (line N), and scripts/proved.nika counts these apart. Record: ADR-381 D6, Part III 14.2 (the assume paragraph). Option A (no marking) is rejected.
Does the certificate already name the facts it used? Partly.
LgRefutation (tools/logic_lia.nika) names the query’s atoms it used (LgStep::Hypothesis(n)). It does not name the facts those atoms came from. After normalisation, one atom can stand for more than one fact.basic loop, intervals. Those proofs carry no certificate.std: Vec::is_sorted() (natural order, every element at most the next). sort() ensures it in std.contracts; sort_by_key ensures nothing. Tests:
xs.sort(); assert(xs.is_sorted()) is proved;xs.sort(); xs.push(0); assert(xs.is_sorted()) is not proved.std: Vec::binary_search(x) with the precondition self.is_sorted(). Its result shape follows the existing find/position entries; stop and report if none fits. Tests:
sort(), no check;NK1300 naming the property;warn, one check at the call;return … if !xs.is_sorted(), no check;unsafe { assume(xs.is_sorted()) }, no check with remove-bounds-checks:on, and a check with it off.assume’s fact is in scope and a goal is proved, ask the goal once more without the assumed facts. If it is still proved, report proved; otherwise proved from an assume with the assume’s line. Do the same for the walk’s own proofs that read such a fact. The extra query is asked only where an assume is in scope. Tests in crates/nikaia/tests/it/prove.rs:
assume(0 <= i && i < v.len()); v[i] gives proved from an assume (line 2);return 0 if i < 0 || i >= v.len() before it gives proved;assume that the goal does not need leaves proved;--asserts’s summary counts them apart.scripts/proved.nika (owed for #796): count proved from an assume apart from proved.scripts/proved.nika to count how many unproved indexes are reads through a stored index): a rule over every element that the prover reads, xs.all(|x| …).assume in tools/*.nika, as std does (NK1295).assume in nikaia.contracts. No caller in another package needs it yet.Q2 prepared for the owner (Q1 is not asked yet: it waits for the count from scripts/proved.nika).
Today: std has no binary_search, is_sorted or binary_search_by (std.contracts). A program writes the loop itself. On an unsorted list that loop silently returns a wrong position: no crash, no message.
Recommendation: binary_search requires self.is_sorted() (an ADR-381 property). sort() ensures it, so xs.sort(); xs.binary_search(x) costs nothing extra. Reason: the language’s promise is that a program does not silently compute a wrong answer where the compiler can know it might. A contract is how that promise is kept, and once ADR-381 is built it costs no new word.
Who pays: the callers whose list is not provably sorted.
unproved-claims = "error", such a call is refused (NK1300) until the program shows the order. It can do that by sorting, with a type rule (struct Sorted { items, assert(items.is_sorted()) }), or with a guard. With a guard, the walk is paid once, where the data arrives. Data from a file needs that guard anyway (ADR-269 D6).warn, an unproved call checks the property once, at the call. That walk is O(n). For a single search on unproved data, this does defeat O(log n): a linear scan would have been as cheap. Later searches on the same unchanged list pay nothing more (ADR-381 D2), so many searches pay the walk once.return … if !xs.is_sorted()) as making the property known.If the decision is wrong:
Elsewhere (only what is certain):
slice::binary_search: on unsorted input the result is unspecified. There is no check and no undefined behaviour.std::lower_bound and binary_search: the range must be partitioned, and breaking that is undefined behaviour. Debug modes of the standard library can check it.Arrays.binarySearch: “the results are undefined” on unsorted input.bisect: assumes the list is sorted and does not check.requires forall i, j :: 0 <= i < j < |a| ==> a[i] <= a[j], and the verifier proves it statically.Pre with for all, proved by GNATprove or checked at run time.Dependency: this builds after #797 (ADR-381 properties).
Generated by Claude Code
Next question for the owner: should a check removed because of an assume be shown as “assumed, not proved”?
From zero. The compiler keeps records of what it knows about a program. nikaia.contracts (the ledger, Part I 6.7) publishes each function’s borrows, requires and ensures. nikaia.proofs stores each answer the prover found, with a certificate that is checked again on every build. nikaia check --bounds and --asserts print, line by line, which checks were proved. unsafe { assume(c) } (ADR-376) is the programmer’s word that c holds. The prover then uses c like a proved fact. Example (probed on 0.0.1204):
fn at(v: ref Vec[i64], i: i64) -> i64 sync {
unsafe { assume(0 <= i && i < v.len()) }
return v[i]
}--asserts reports assumed 1: a fact the program vouches for. But --bounds reports v[i] proved. Nothing in that line, and nothing in nikaia.proofs, says that the proof rests on the assume.
Where it comes from. Claim (b) of #796 is counted from --bounds, which scripts/proved.nika will sum. Q2 (ADR-381 D5) gave binary_search a second way out, assume(xs.is_sorted()), so assumed facts will now feed proofs more often. As things stand, every assume raises the “proved” count. No program is wrong because of this today. What is at stake is how honest the count is.
Facts.
assume in the default build and believes it only when a remove-* switch is on.std may not use assume (NK1295). tools/*.nika may.assume would be cheap.Options.
--bounds and --asserts say proved from an assume (line N), and proved.nika counts these apart. Cost: the walk tracks where each fact came from.nikaia.contracts. Callers in other packages see that a contract rests on an assume. Cost: a ledger field, and a breaking-change rule for it.assume in tools/*.nika, as std already does. Then claim (b) stays clean by construction. A tool that needs a vouched fact must use a guard instead.Elsewhere.
sorry warns declaration uses ‘sorry’, and #print axioms lists everything a theorem rests on.Admitted lemmas and axioms are listed by Print Assumptions.assume without {:axiom} is reported, and the program is not compiled.pragma Assume as an assumption in its report.assume specification is trusted without being checked. I know of no report that lists them.Recommendation: (B), plus (D) for the compiler’s own code. Claim (b) then means “proved”, and every program still has its way out. (C) is not decided here: no caller in another package needs it yet. The risk of (B): the walk gets a new property, the origin of each fact, that must stay right. If it is wrong, an assumed proof shows as proved again.
Generated by Claude Code