i64, and std States How Many Items a Sequence YieldsStatus: Accepted, to build (#1053: D1 by p12, D2 by p13)
Date: October 31, 2026 (architect’s decision under the owner’s rule of
2026-10-31, docs/supervisor.md, Language decisions: a prover fact every
program gets, which nobody pays for and no syntax changes, is the
architect’s)
Answers: two kinds of unproved checks in the compiler’s own Nikaia code
(claim (b), docs/formal-verification.md, #1053): a counter bounded by a
list whose elements the walk does not know to take space, and an index into
a list collected from a std sequence whose length the walk does not know
Related: Part I 2.2 (a length is an i64), Part III 14.2 and the
optimization paragraph of 30-nikaia-tooling.md (what a proof reads),
ADR-306 D12 (a length below 2^60 where elements take space),
ADR-314 (ensures), ADR-375 D5
(ensures_each; “other searches take the same entry when a program needs
it”), ADR-361 D13 (a for counts its turns)
while i < xs.len() { i += 1 } is proved where xs’s elements take space
and left checked where they do not (Vec[Z] with struct Z {}), although
i < xs.len() alone keeps i + 1 inside i64. And
let parts: Vec[ref String] = path.split(".").collect() followed by
parts[0] is left checked, although split never yields nothing. About 160
indexes of constant position and many counters in tools/*.nika stop at
these two.
i64’s greatest valueThe length of a list, text, Bytes, map or set, and the number of turns a
for takes, is a fact 0 <= n <= 2^63 - 1 for every proof, whether or not
its elements take space: len() hands back an i64 (Part I 2.2). ADR-306
D12’s tighter n < 2^60 stays where elements take space. So i < xs.len()
proves i + 1, and a counter that grows by one a turn in a for over xs
is below xs.len() before it grows (D13), for every element type.
Why. It is what the type says; leaving it out made the proof depend on the element type for a bound that does not.
std sequence’s ledger entry may state its countA ledger entry whose result is a Seq may carry ensures_count, facts over
count (the number of items the sequence yields), self and the entry’s
parameters, as ensures does over a result (ADR-314) and ensures_each
over each item (ADR-375 D5). The walk reads them where the count becomes a
length: the list a collect() written right after the producer binds, the
value of .count(), and the turns of a for over it. They hold only where
no write to self stands between the call and the use, as D5’s do.
std states, from Rust’s behaviour, which the lowering keeps:
| Entry | ensures_count |
|---|---|
str::split, str::rsplit |
1 <= count, count <= self.len() + 1 |
String::chars |
count <= self.len(), self.len() <= 4 * count |
String::bytes |
count == self.len() |
Others take the entry when a program needs it. splitn does not yet: what
it yields for n <= 0 is not specified.
Why. The count is what the producer means, like find_all’s positions;
an assert(parts.len() >= 1) would put a run-time check where none is
needed, and is checked at every call. Rust leaves parts[0] checked.
Rejected: an assert in the program; a special rule for split in the walk
(a fact belongs to the ledger entry that states the producer’s other
promises, so a package’s own sequences can state theirs the same way).
optimization paragraph (30-nikaia-tooling.md), gains: “every length
is at most 2^63 - 1” and “a std sequence whose ledger entry has
ensures_count gives a list collected from it, its count() and a for
over it a length of which each holds”.tools/*.nika are measured
before and after (scripts/proved.nika); the gain goes into each report.