Status: Accepted
Date: October 17, 2026
Answers: whether a claim that reads a call’s result may be decided by what
the callee’s body returns, and who pays for it; how the prover reads / and
%; what a comptime binding is to the prover; what a caller in another
package is told when only a callee’s body would decide its claim (issue #632);
whether a call with constant arguments is run while building where a claim
needs its value (issue #633)
Related:
ADR-269 D5, D8, D9, D14, D18 (claims, refutation, what the prover
reads, observation against promise, the ledger’s inferred);
ADR-314 D3 and its Option D (a one-return body ensures its
value; reading a callee’s body at each call, rejected);
ADR-270 D5 (the certificate’s extension step);
ADR-258 D1-D4 (the weights); Part I 2.2 (constant folding);
ADR-321 D1, D4, D7, D8, D10, D16, D17 and ADR-287
D13, D14 (build-time code is compiled and run, its bounds, what it may call);
Part III 13.3 (refuted-claims), 14.2 (the prover), C.3
fn example(a: i64) -> i64 { let whole = 10 + a; return positive(whole) }
returns 12 for example(2), and assert(4 / example(2) > 10) is false every
time it is reached. The compiler sees every line of it and still checks the
claim at run time, for two reasons: nothing tells the prover what example
returns (it has no claim on its result and is not one return e), and the
prover reads no /. Even let b = 4 / 12; assert(b > 10) is not refused, and
a comptime B = 4 / example(2) the build has computed as 0 is not read either.
The question is how the prover gets that knowledge, and who pays for it: every build, every call, every author of a function, or only the program whose claim needs it.
| Tool | What decides a call’s result | Who pays |
|---|---|---|
| Dafny | the callee’s written ensures; a function body is visible unless opaque |
the author, by writing contracts |
| SPARK / GNATprove | a local subprogram without a contract is inlined into its caller’s proof | every caller of such a subprogram |
| Frama-C WP | written contracts; EVA computes value ranges over the whole program | WP the author, EVA every analysis run |
| Infer / Pulse | a summary per function, computed on demand and cached | only the functions an analysis reaches |
| Kani / CBMC | inlining, bounded | every call, every run |
Zig comptime, C++ constexpr |
a call with constant arguments is evaluated while compiling | the program that writes the constant call |
Infer’s on-demand summary is the shape that matches this language’s rule that only who needs something pays for it.
| Option | Example | Why it lost | See |
|---|---|---|---|
| Keep today’s reading | assert(4 / example(2) > 10) checked when run |
a program the compiler could show wrong builds and stops later | — |
| Read the callee’s body at each call | ADR-314 Option D | every call pays a walk through the callee, and the body crosses the package | D2 |
Publish a derived summary for every pub fn |
example’s result == 10 + a in the ledger as ensures |
every edit to a body becomes a contract change, and NK1208 would warn on almost every refactoring |
D3 |
| Say nothing across a package | lib::example(2) in another package stays a check, silently |
the author of a package in the user’s own hands could promise the result with one line and is not told | D4 |
| Interpret a call with constant arguments while building | example(2) walked by a tree evaluator |
a second implementation of the language’s meaning in the path that refuses a program; build-time code is compiled and run, never interpreted (ADR-321 D1) | D11 |
Run a call only where a comptime asks |
fib(10) in a claim stays a check |
the compiler can run it on the path it already has, and only the claim that needs it pays | D11 |
Run a call that reads cli::args |
count(args) run for a claim |
at build time cli::args are the builder’s arguments, at run time the user’s, so the value would not be the program’s |
D11 |
| Intervals for any quotient | a / b with b in 1..10 |
more than the program needs, and ADR-314 §7 leaves it open | §6 |
A function whose every exit returns a whole number the prover reads, with no
loop that changes a name it reads, no match and no call that can come back to
it on the way, and below the fixed term bound, has a result summary: for
each exit, path → result == e over its parameters. It is computed by the walk
that already goes through every body; a call inside e is read by its
callee’s summary, leaves first.
A claim, or a precondition at a call, is asked first with what is known
without summaries. Where the answer is neither proved nor refuted and the
claim reads a call’s result that the callee’s ensures do not decide, it is
asked once more with the summaries of those calls. A claim decided without
them never reads them.
The summary is written to the ledger as inferred (ADR-269 D18), one line per
exit, the exit’s path written in the line itself (x > 0 → result == x), so a
reviewer sees what a proof leaned on; from stays the key of requires and
ensures. A caller in
another package reads it as absent (ADR-269 D14), and NK1208 does not
compare it. A function that means to promise its result writes an assert on
it, or is one return e (ADR-314 D3).
Where a claim would be proved or refuted by the summary of a function in
another package, and that package is one the build reads from a path - the
user’s own code - the claim stays as it is and the compiler gives a hint,
NK1263: the fact the summary would give (lib::example(2) would be 12) and
the assert on the result that would make it part of example’s contract. A
package fetched from elsewhere gets no hint: its author is not the reader.
e / k is a fresh name q with ADR-270 D5’s extension, for division that
truncates toward zero: e >= 0 → k·q <= e <= k·q + k - 1,
e < 0 → k·q - k + 1 <= e <= k·q; e % k is e - k·q. Two known numbers fold
to their value, as Part I 2.2 folds them.
First by substituting linear equalities; otherwise, where a claim reads the quotient, by a model and a proof that the divisor equals its value there. A divisor not pinned leaves the quotient unread.
comptime binding is its value.It is a name of the proof with the value the build computed.
NK1207’s note gives the value of each call it read and where that came from:
example(2) is 12: example returns positive(10 + a), positive returns
whole.
A claim the prover newly refutes in this repository’s code is a defect found:
it is fixed in the code it names, in the change that builds the refutation.
refuted-claims = "warn" stays the bypass for an emergency, not a way to
carry a refuted claim.
Where a claim is still neither proved nor refuted with what D1-D7 give, and it
reads the result of a call whose arguments are all values the build knows -
literals, folded constants, comptime bindings, results D11 already ran - the
compiler runs that call as ADR-321 runs a comptime: compiled
with the program’s own lowering, never interpreted (ADR-321 D1), its body
sync (ADR-287 D13) with an empty touch set, under ADR-321 D7’s step budget and
D10’s memory bound, its result cached with the package’s build-time crate
(D4). The value is a fact: example(2) == 12. A function of another package
runs only where ADR-321 D8 lets it.
A callee that is not sync, touches anything, is not in this build or runs out
of the budget gives no fact: the claim stays a check where it stands, and the
--asserts report says which of these it was. It is not an error, because no
comptime asked for the value. A run that stops - an overflow, an
assert in the callee - shows that the call stops the program every time it
is reached, as a check the compiler shows fails (NK1207), in the words the
program would print (ADR-321 D16, D17).
A call is run only for a claim that D1-D7 left open, once per call and its arguments, and the answer is kept with the package’s build-time results. A program whose claims are decided without it compiles and runs nothing more. Whether such a call may also be run where no claim needs it, to save work at run time, is #634.
Built in this order: D5’s folding and D7; D11-D13; D5’s quotient by a constant;
D1-D3 with D8; D6; then D4. Done when the program of §1 is refused with NK1207,
lowering the standalone files and std’s tools costs at most 5 % more
instructions, and every new refutation in the corpus was checked by hand.
/ and % by a positive constant or a pinned
divisor and a comptime binding, and a call’s result inside the package by
its callee’s body; Part III 13.3 says refuted-claims = "warn" is for an
emergency; Part III’s table carries NK1263 and widens NK1207’s note.inferred lines in the ledger. Existing
code may meet new NK1207 refusals, each a defect to fix (D9).Not decided here: running a call with constant arguments while building where no claim needs it, as an optimisation (#634); summaries across packages beyond D4’s hint; a quotient by a divisor that is not pinned (intervals, ADR-314 §7); loops and recursion in a summary.
Decided October 17, 2026 (#632; D11-D13 #633).