assert(is_sorted(xs)) Is Proved by Name, Carried to the Caller and Checked OnceStatus: Accepted
Date: October 24, 2026
Answers: the first step of #797,
how does a program say “this list is sorted” or “this tree is valid”, and what
does the compiler do with it?
Amends: ADR-269 D9 (what the prover reads)
Related: ADR-269 D3, D5, D17, D18 (a pure claim; preconditions,
postconditions, the ledger), ADR-369 (a struct’s rule),
ADR-306 D17 (a field is a name while nothing can change it),
ADR-380 (not proved is refused unless warn)
fn is_sorted(v: ref Vec[i64]) -> bool sync { … }
fn first_at_least(v: ref Vec[i64], x: i64) -> i64 sync {
assert(is_sorted(v))
…
}The claim is allowed today (its call is pure, ADR-269 D3), but the prover
reads only comparisons of whole numbers: the claim is refused (NK1300), or at
unproved-claims = "warn" the whole list is walked at every call. It is not a
precondition, so no caller is asked, and nothing after it knows it.
predicate is a function the verifier can unfold; an
opaque one is used by name until revealed. Liquid Haskell: measures and
abstract refinements. SPARK: an expression function used in Pre/Post,
proved or checked at run time. Whiley: a type sorted defined by a
predicate (type sorted is (int[] xs) where …). Eiffel: a require that
calls a query, checked at run time.bool call is a name of the prover.In a claim, a call p(a, …) or a.p(…) of a sync function that returns
bool, throws nothing, touches nothing and changes nothing (ADR-269 D3),
whose arguments are names the prover reads or bindings and paths of fields
that nothing can change (ADR-306 D17, D20), is a property: a name of its
own, true or false, as xs.len() is a whole number of its own. Two
properties are the same name when they call the same function with the same
arguments. The body is not read.
A property is known after an assert of it is reached (proved or checked),
from a precondition at the function’s entry, from a callee’s postcondition
(assert(p(result)) at every exit), from a type’s rule (assert(p(items))
in a struct, ADR-369 D2) wherever a value of the type is seen, after a guard
that leaves when it is false (return … if !p(xs), throw … if !p(xs), as
ADR-276’s jumps rule out their condition), and from unsafe { assume(p(xs)) }
(ADR-376). It stops being
known where an argument may change, as a field does (ADR-306 D17).
At a function’s entry it is a precondition carried to the caller (ADR-269 D5,
D15); the ledger publishes it as written (requires = "is_sorted(v)"), with the
callee’s package path of p. A call proves it when the same property, with the
arguments in place of the parameters, is known there. Not proved, it is
NK1300, or at warn checked where it stands: at the call, once, so a value
handed down a chain of calls is walked once.
The property’s own check - a call of p, as long as the list - is not
emitted where it is proved. Nothing else follows from it: since the body is
not read, it drops no index or overflow check and chooses no algorithm. A
property whose body the prover reads (every element, an order between
neighbours) is a later decision, #798.
binary_search requires its list sorted.std has xs.is_sorted() (every element at most the next, in the natural
order) and xs.sort() ensures it; xs.binary_search(x) requires it, as a
precondition by D3. Where the order cannot be shown - data from outside, an
order lost over many steps - the program has two ways: check once where the
data arrives (a guard on xs.is_sorted(), O(n), the property known afterwards
until the list changes), or vouch for it, unsafe { assume(xs.is_sorted()) },
which ADR-376 D2 checks in a build that drops no checks and believes in one
that does.
Why. A binary search over an unsorted list answers wrongly and silently;
the language’s promise is that what the compiler could know is not left to
luck. The cost lands where the order is lost, once, not at every search.
Rejected: Rust’s, Java’s and Python’s unspecified result on unsorted input
(a silent wrong value); a check inside every call (O(n) per O(log n) search);
a separate SortedVec type as the only way in (a type rule, ADR-369, already
gives it to a program that wants one). Owner’s decision, 2026-10-24 (#798 Q2).
assume says so.nikaia check --bounds and --asserts name a check or claim that is proved
only with the fact of an unsafe { assume(…) } (ADR-376) as proved from an
assume, with the assume’s line; one that is proved without it is proved.
scripts/proved.nika counts the two apart.
Why. An assume is the programmer’s word, and D5 gives it a common use;
a count of proved that silently includes it would let claim (b) weaken
without anyone seeing it. The reports are where a reader looks, as Lean’s
#print axioms and Rocq’s Print Assumptions list what a theorem rests on.
Rejected: (A) leaving the reports as they are, for that reason.
Not decided: (C) marking it in nikaia.contracts for callers in other
packages - no caller needs it yet; (D) refusing assume in tools/*.nika, as
std does (NK1295) - a later question. Owner’s decision, 2026-10-24 (#798).
predicate, requires, a refinement type): ADR-269 decided
that a written assert is the contract; a property is an ordinary function.--asserts lists a
property proved by name as proved: known from … (the assert, the
precondition, the postcondition or the rule it came from).p does not change the
contract’s text; NK1208 does not warn of it. The property’s meaning is its
body, as a function’s is.