Open and answer this issue on GitHub.
ready · opened 2026-10-17 · updated 2026-10-17 · 3 comments
An assert is proved while the program is built where the prover can read it (ADR-269 D4, D9), and shown false - refused with NK1207 - where what is known rules it out (D8). What the prover reads: comparisons of whole numbers built from names, literals, +, -, unary - and a * by a constant; names are immutable whole-number bindings; a call’s result is known only by the callee’s postconditions (D17), and a sync function whose body is one return e ensures result == e (ADR-314 D3).
The owner’s program (reported in #631):
fn main() {
let b = 4/example(2)
assert(b>10) // checked at run time; the owner expects a refusal
}
fn positive(whole: i64) -> i64 {
assert(whole > 0)
return whole
}
fn example(a:i64) -> i64 {
let whole = 10 + a
return positive(whole)
}example(2) is 12 and 4 / 12 is 0, so b > 10 is false every time it is reached. A refusal needs two things nothing decides today:
example(2) == 12. example’s body is not one return e (ADR-314 D3), and no assert states its result (D17). positive’s assert(whole > 0) before return whole gives positive the postcondition result > 0, nothing more. ADR-269 §6 leaves interprocedural facts beyond contracts undecided; ADR-314 rejected Option D (reading each callee’s body at each call).4 / r. A quotient is outside D9; ADR-314 §7 leaves products and quotients of two unknowns open. The solver has no division term (ADR-270’s certificate format has the extension step for div by a constant, 0 <= L - m*q <= m - 1, but the terms do not use it).#631 built what is already decided (a call inside a let’s value is read with its callee’s ensures, and the report names the unread binding). With it, let b = 2 * example(2) over an expression-function example is refused today.
Computed results
fn example(a: i64) -> i64 sync { return 10 + a } is read; any other body needs an assert on its result.match, no recursion) whose every exit returns a value the prover reads, computed forward: it ensures result == e per exit, under the path. positive would ensure result == whole, example result == 10 + a. Within a package as an observation (ADR-269 D14), or published like D3’s. Cost: more bodies become contracts; D19 warns on more edits; a change in a body changes a caller’s proof (the reason Option D lost, softened because the summary is computed once and kept in the ledger).Quotients
e / k with k > 0 a literal is a fresh name q with k*q <= e <= k*q + k - 1 where e >= 0, and the mirrored bounds where e < 0 (truncation toward zero, Part I 2.2), as ADR-270’s extension step; % alike. Sound and linear; proves n / 2 < n for n > 0.r == 12, then 4 / r is 4 / 12). Needed for the owner’s program.*, /, % beside Fourier-Motzkin (ADR-314 §7).A wrong summary or quotient rule refuses a correct program (an error with a bypass, refuted-claims = "warn") or proves a false claim (a check removed only under remove-*-checks:on). Truncation toward zero for negative dividends is the place a rule would be wrong.
D now (small, linear, decided by ADR-270’s step already), B within a package as an observation, E after D. Together they refuse the owner’s assert(b > 10). Not decided here: whether B’s summaries are published across packages.
How it came up. The owner’s program: let b = 4 / example(2) with fn example(a: i64) -> i64 { let whole = 10 + a; return positive(whole) }, then assert(b > 10), is false every time it is reached (example(2) is 12, 4 / 12 is 0), and it was only checked at run time. #631 fixed one defect (a call inside a let’s value); this issue held the rest. A decision basis checked the code:
let b = 4 / 12; assert(b > 10) is not refused, because the prover has no / term;comptime B = 4 / example(2) is lowered to const B = 0 but the prover doesn’t read it;It also found that ADR-314’s Option D was rejected for two reasons: every call paid for it, and the body crossed the package boundary. Neither reason holds for on-demand use within a package.
Decision (ADR-359, specification Part III 13.3, 14.2 and C.3, 0.0.978): the guiding principle is that only who needs it pays.
inferred in the ledger: an observation, not a promise, and invisible to other packages.NK1263, names the assert on the result that would make it a contract. A package fetched from elsewhere gets no hint./ and % by a positive constant, or by a divisor that what is known pins to one value.comptime binding is its value.NK1207’s note names each call value it read.refuted-claims = "warn" is only for emergencies.Not decided here: evaluating a call with constant arguments while building, quotients by a divisor that is not pinned (intervals), and loops or recursion in a summary.
comptime (D5, D7). prove_terms.nika: / and % of two literals fold, with the same semantics as Part I 2.2’s folder. prover_walk.nika: an integer comptime binding is the fact B == v. Tests (prove.rs):
let b = 4 / 12; assert(b > 10) gives NK1207 with b = 0;comptime B: i64 = 4 / example(2); assert(B > 10) gives NK1207.e / k becomes a fresh name with ADR-270 D5’s bounds (truncation toward zero), and e % k is e - k·q. Tests:
n / 2 < n is proved for n > 0;(-7) / 2 == -3 and (-7) % 2 == -1 are proved;n / 2 > n is refused for n == 4;for n in -10..<10 { assert(n / 3 * 3 + n % 3 == n) } is proved (no wrong refusal for a negative dividend).prover_walk.nika/prover_passes.nika record path → result == e at every exit and compose them through calls, leaves first. A loop that changes a read name, a match, recursion or the term bound means no summary. Unit tests:
positive gives result == whole;example gives result == 10 + a;clamp gives (n < 0 → result == 0) ∧ (n >= 0 → result == n);while gives none.example(2) - 1 == 11 is proved.NK1207’s note lists the call values it read and where they came from.ledger.nika and ledger_text.nika read and write inferred = [...], and only the package itself reads it. Tests (contracts_across.rs):
assert(lib::example(2) > 30) stays a run-time check;NK1208 is not given when an inferred line changes.tests/ program with NAME.stderr) is refused with NK1207, and the note names b = 0 and example(2) = 12.NK1263. A path dependency gets the hint, naming the fact and the assert to write; a fetched package gets none. Tests in contracts_across.rs.lower over the standalone files and lower-std) and record them in docs/solver-workload.md. Fix every new refutation in the corpus and in tools/*.nika in the code (D9), not with warn. Then Fixes #632.Version raises and new NK codes are the supervisor’s (CLAUDE.md); NK1263 is already assigned.
Generated by Claude Code
Folding and comptime (D5, D7).
prove_terms.nika: / and % of two constant terms fold, truncated toward zero as Part I 2.2 folds them. A division by zero or one past the range gives no term.lin_term/claim_term now take pinned: the names whose value the build knows.
comptime is one of them; a local of the same name hides it.prover_walk.nika: a comptime inside a body is the fact B == v, with the value the checker computed.Tests:
prove.rs:
let b = 4 / 12; assert(b > 10) gives NK1207 with b is 0.-7 / 2 == -3, -7 % 2 == -1, 48 / 4 == 12 and 7 % 3 == 1 are proved.comptime LIMIT is read as its value, LIMIT / 5 == 8 included, and a parameter named LIMIT hides it.comptime_compiled.rs: comptime B: i64 = 4 / example(2); assert(B > 10) gives NK1207. It is compiled and run (ADR-321 D1), so the test uses a workshop.Fixed on the way: --asserts now checks the way the build does, with the program’s files, reads and workshop. Before, it ran a second check with no workshop, so a comptime that a call computes reported differently than in the build.
New refutations: none in examples/, tests/samples, tests/language, guide/ or benches/.
Steps 2-9 are still open.
Generated by Claude Code
Built
e / k by a positive constant is a term (SolverTerm::Quot). The solver reads it as a fresh name with ADR-270 D5’s extension for each sign of e. e % k is e - k*(e/k). Quotient names are eliminated last, so 2q = -7 has no integer solution. Proved: n/2 < n for n > 0, -7/2 == -3, -7 % 2 == -1, and n/3*3 + n%3 == n over -10..<10. n/2 > n with n = 4 is NK1207.inferred = [...]. No other package reads it, and NK1208 does not compare it.let.example(2) is 12: example returns positive(whole), positive returns whole.”main(a: int)):
assert(b > 40) is proved.b > 50 stays a run-time check.assert(a>0), --asserts now has a row for 10 + a > 0, main’s precondition carried back from assert(whole > 0).--asserts uses the 0.0.990 layout: red, light blue, green, and no colour under NO_COLOR or off a terminal.NIKAIA_PROVER_COUNTS=1:
lower-std: 0 calls run, 0 second queries, 8 divisors asked.Still open
provenance trusted/untrusted), and to read another package’s inferred lines for a hint query only.Generated by Claude Code