Nikaia
Menu
v0.0.1343pre-alpha GitHub

ADR-285: An Integer Is int or One of Five Fixed Widths, and Stops the Program Where It Does Not Fit; a Number Without an Annotation Is Typed by Its Uses

Status: Accepted Date: October 3, 2026 History: the records this one replaces are archived in docs/history/adr; read them only for how the decision was reached Answers: what an arithmetic overflow does, which Part III A.2 did not say; what len() hands back and which numeric types a program may write; what an as may name, and how a std parameter counted in usize is written; what type a literal no use constrains takes, and a constant sum (#142); how a number may be spelled (#135); unsigned 64- and 32-bit integers and bit operators, which fixed.rs’s FNV and CHD ask for; and who types an unannotated number when the language below cannot (#176, #177); where one integer type takes another without as (#439) Related: ADR-300 (every abort names the Nikaia line); ADR-002 D1 (the generated Cargo project D8 writes into); ADR-021 D5 and ADR-037 D4 (the cache key, which D8 adds nothing to); ADR-292 D7 (a semantic default that can be switched off - the precedent D8 does not follow); ADR-286 D15 and D22 (a Nikaia dependency is on the program’s side of D8’s split); ADR-081 D3 (the check is on per Nikaia crate, so a number’s + stays in this language’s crates); ADR-296 D17 and ADR-288 (the emitter knows no types, which is why conversions are chosen by name and the checker hands answers over); ADR-024 (the ledger the checker reads); ADR-288 D11 (an entry is written and reviewed, not copied from Rust); ADR-135 D2 (an empty list typed by its use, the walk D24 reuses); ADR-311 and ADR-290 (the table fixed.nika builds, and the route by which Rust moves into Nikaia); ADR-306 (an overflow check a proof shows unneeded is not emitted - D5’s meaning unchanged); ADR-258 (the four weights)

1. Question

What is an integer in this language? Which types a program writes; what happens when a result, a conversion or a literal does not fit; how the bits are reached; how a number is spelled; and what type a number gets when the program writes none.

Without an answer, each part reaches the user in rustc’s words or as two programs: an overflow that aborts in a debug build and wraps in --release; a len() in usize that puts an as i64 in every loop; an as that makes -3 as usize 18,446,744,073,709,551,613 in a language where a conversion that does not fit aborts; let big = 3000000000 refused as literal out of range for i32, about a type the program never wrote; 1_000_000 read as 1 beside an undeclared name; fixed.rs, which cannot be written without ^, >> and a u64; and let i = 0 then v[i].push(x), which leaves rustc no type to settle on.

Each answer leans on the others - the literal rule on the type list, the conversion rule on the overflow rule, the use-site typing on all of them - so they are decided together.

2. How others do it

Question Language / tool Its answer See
Overflow Rust aborts in a debug build, wraps in --release measured
Wrapping on purpose Swift &+, &* operators D6
A length Go, Java, C#, Swift a signed integer; Swift on the ground that unsigned arithmetic causes more bugs than it prevents D1
  Rust usize, and the conversions it demands are a well-known papercut D1
A byte Go, Rust, C#, Swift an unsigned byte type D2
  Java signed only; a masking dance in every byte-handling program, >>>, remainderUnsigned D2
An unconstrained literal Go, Swift the default is the machine word, so 3000000000 fits —
  C, C#, Kotlin the first type from a fixed list that holds it —
  Java, Rust refused (Java without an L) —
  Kotlin no backward inference, so the literal settles where it stands —
Bit operator precedence C & below ==: a & mask == 0 is a & (mask == 0) D10
  Rust, Go shifts, then &, ^, \|, then comparisons D10
Number spelling Rust and its neighbours 1_000, 0xFF, 0b1010, 0o17; 0xFF is 255 —

What does not transfer. Rust’s as is defined to truncate and has no failure case to switch on - 5000000000 as i32 is 705032704 under -C overflow-checks=on and -C debug-assertions=on alike (measured) - so a conversion cannot ride on the overflow switch. And this language promises one meaning in every build (Part I 1.2), which is the promise Rust’s debug/release split breaks.

3. Options, weighed

Every option rejected, with the reason it lost. The choices themselves are §4.

Option Example Why it lost See
Wrapping operators a &+ b & is borrowing here, and a &+ b collides with &a to the eye; if saturating earns no symbol, neither does wrapping D6
A checked helper per arithmetic operation add(a, b) in the generated Rust the same arithmetic, but nobody comparing benchmarks believes a + that became a call D8
An overflow check a build can turn off [build] overflow = off it changes what a program computes, which no build option may (Part I 1.2) - unlike ADR-292 D7’s ordering —
A length as usize xs.len() as i64 in every loop ceremony that cannot fail (a usize exceeds an i64 only past 9,223,372,036,854,775,807 elements - eight exabytes at one byte each) against one abort that already exists D1
A signed byte only b & 0xff at each step Java’s masking dance D2
as naming any type the language below has n as u128, -3 as usize an escape hatch nobody decided, and the one conversion that does not abort D14
A negative count reported as an index index out of bounds: -1 for repeat(-1) it names an access the program does not make D15
Kotlin’s first-type rule as the whole rule let small = 42 then wide(small) refused it costs backward inference, and Part I 2.4’s own example —
Refuse a constant sum instead of widening it 3000000000 + 1 refused breaks a program that compiles and that the page calls correct —
Let an overflowing sum widen the name it reads let a = 2000000000 widened because of a + a a value never decides a type through an operation; the uses do (D24-D26) D25, D26
A second constant fold in the emitter literals only, no lookup it works, and two folds drift —
A hexadecimal literal carries its width 0xFF a u8, 0x0FF a u16 a type that depends on how many zeroes somebody typed D17
Named bit operations hash.bit_xor(byte) says exactly what ^ says; a wrapping name says this may overflow, on purpose, which an operator does not D9
Unsigned questions on signed types >>>, remainderUnsigned Java’s cost, decided against once already for the byte —
No parenthesis rule for bits beside a comparison a & mask == 0 the precedence is right, and a reader who learned C reads it the other way; two characters end the question D10
An index pinned at its one site index::at::<i64>(i) mends #177 there and collides with the first use that asks for anything else —
An index as a use like any other let i = 0 handed to an i32 and used as an index: a conflict the language below converts either —
int whose width follows the caller fn add(a: int) -> int an u8 for one caller, an i64 for another the width changes what a function computes - where it aborts, whether it takes a negative number, which bits a hash gives - so the signature would no longer say what the function does; a function that is meant for several widths says so with a type parameter D36
int as wide as the machine C’s int, Go’s and Swift’s Int one program, other results on another machine (Part I 1.2) D36
int as a second spelling of i64 int and i64 the same promise two names for one promise; the name is worth having only because it promises less D37
A narrower default type to keep room for optimisation let n = 0 an i32 so that it may take 32-bit lanes with an aborting overflow, a narrower type changes what the program computes; the room belongs in the representation D37
Fixed widths only at the C and Rust interfaces, a warning elsewhere let h: u64 warned about 160 widths outside an extern are deliberate - spans, hashes, a solver’s layout, bytes - and no language surveyed warns about a written width D39

The weights pulled apart in one place. Reading every use of a number (D23-D25) is work the compiler could have left to the language below; it is paid so that the developer writes no annotation that the uses already answer (ADR-258 D2), and it costs one list per open number, read once per function body - the cost ADR-135 D2 already pays for an empty list.

4. Decision

The integer types

D1 — A length is an i64, and so is an index.

Every std entry that hands back a length or a count - Vec::len, String::len, a map’s and a set’s len, Seq::count - returns an i64, and an index takes one. The program writes no conversion in either direction; the compiler emits both. Out of a length the conversion cannot fail. Into an index it fails only for a negative number, and that failure reports as an access out of bounds (“the index is -1”), because it is one - not as a failed conversion the program never wrote. An index written only in literals is left bare for the language below’s own inference.

D2 — The integer types a program writes are i64, i32, u8, u64 and u32; no machine-width type is among them.

u8 is named because fs::read hands one back; u64 and u32 because a hash over bytes asks for them (D3). usize and isize stay out: a length is an i64 (D1), and nothing a program writes needs a machine-width type. f64 is the floating-point type. Beside the five fixed widths stands int (D36): the values of an i64, with no width promised.

D3 — u64 and u32 have every rule the other integers have, and no integer value is lost silently.

A result that does not fit aborts (D5); wrapping_, saturating_ and truncating_ are their names (D6, D13). A wider type takes a narrower one without as wherever no value can be lost (D32); every other conversion is as, checked where it may not fit (D12). u64 + i64 has no type that holds both and is refused where both sides are known (NK1199), the message naming both types and the help handing over the as.

Amended October 6, 2026 (#439).

D4 — text.bytes() is the text’s UTF-8, one u8 at a time.

A sequence, as chars() is, so a hash over it is the hash other languages compute over the same text.

Overflow

D5 — An arithmetic overflow aborts, at every build.

The same program computes the same thing under every build, and a benchmark measures what is shipped. Part III A.2’s list of unrecoverable errors carries the overflow beside a division by zero. A check the compiler proves unneeded is not emitted (ADR-306), which changes no result.

D6 — Wrapping and saturating arithmetic get names, not operators.

h.wrapping_mul(31).wrapping_add(c), level.saturating_add(increase). The names are Rust’s, one for one, so the emitted code stays idiomatic.

D7 — The full set, including the three that are always forgotten.

wrapping_add, _sub, _mul, _div, _neg, _abs, _shl, _shr, and saturating_ wherever Rust has it. -x and x.abs() on a signed type’s smallest value overflow, and so does that value divided by -1; a shift by the width or more is an abort of the same category (D11).

D8 — The arithmetic check is carried by the generated project, not by helper functions, and reaches this language’s crates only.

The emitted code says a + b; the generated Cargo project turns overflow-checks on for every crate of this language - the program and every Nikaia dependency - and off for foreign packages, whose hash functions wrap on purpose. The known limit: whoever rebuilds the generated project with other settings gets other numbers, as whoever edits the generated code by hand does.

Bits

D9 — &, |, ^, << and >> are operators, and ! on an integer flips every bit.

On integers only, both sides one type, a shift’s count excepted (any integer). The compound forms &=, |=, ^=, <<=, >>= stand beside +=. On a bool they are refused (NK1198), naming &&, || or !=: a & that does not short-circuit would be a second spelling of one thing.

D10 — Bit operators bind tighter than comparisons, and one beside a comparison is parenthesised.

* / %, + -, << >>, &, ^, |, the comparisons, && and || - Rust’s and Go’s order. A bit operator written beside a comparison without parentheses is NK1197, the help handing over (a & mask) == 0.

D11 — A shift loses the bits it moves out; a count as wide as the type, or negative, aborts.

>> fills with zeros on an unsigned type and with the sign on a signed one.

Conversions

D12 — A narrowing conversion is written as only where it is shown to fit.

A conversion that can lose a value - a wider integer to a narrower one, a signed one to an unsigned one or back, an f64 to an integer or to an f32 - is written as only where the compiler shows it fits:

Which conversions narrow is the checker’s answer, since as i32 narrows or widens by what it is given, and the list is written as the conversions that always fit, so an unforeseen pair is treated as narrowing.

Why not an abort. A value lost in a conversion is a failure the program cannot see where it is written. Where a proof can find it, it is found while building; where none can, the program decides, at the line, between handling it and keeping what the backend makes of it. A stop at run time is what is left when neither was asked for, and a conversion is a place where asking costs one name. Arithmetic overflow (D5) is not changed by this: it has no spelling a program writes in its place on every operator.

Changed October 8, 2026 (#552): a narrowing as aborted where it did not fit.

D13 — Keeping the low digits is said by name; asking whether it fits is said by name; an integer to a float is not checked.

Changed by D42: truncating_ converts out of a wider type only; the same width with the other sign is bits_as_.

truncating_i32, truncating_i64, truncating_u32 and truncating_u64 (and truncating_u8, D41) lower to Rust’s as, from the sources a program can narrow out of: a wider integer and an f64. There is no name out of a machine-width type, because no program can hold one (D1, D2). Out of an f64 the backend’s as makes 1e20 as i32 2147483647 and NaN 0; the name is how a program says that is what it wants. checked_i32, checked_i64, checked_u32, checked_u64 and checked_f32 hand back null where the value does not fit, out of an integer and out of an f64, where a value that is not a number does not fit an integer. An integer to an f64 loses digits at large values without overflowing (9007199254740993 comes back 9007199254740992); every language does this, there is no sensible point to stop, and it is a stated limit, not a check. The f64 helper goes through i128, because i64::MAX as f64 rounds up and the obvious comparison accepts one value too many.

D14 — as names a type this language offers, and nothing else.

i32, i64, u8, u32, u64, f64, bool, char, String and its view. Anything else - n as usize, n as u128 - is NK1122, naming the type and saying that the compiler writes the machine’s conversions itself. This list answers which types a program may write; the narrower list of D12 answers which conversions can lose something.

D15 — A std parameter the language below counts in usize is written as an i64, and the conversion is emitted.

str::repeat(&str, n: i64), and the emitter writes nikaia_std::count::of around the argument, so " ".repeat(indent) needs no conversion. A negative count aborts with a message of its own - “a count cannot be negative: the count is -1” - because it is not an access out of bounds. The list is chosen by name, because it is a fact about Rust’s library and the emitter knows no types; a test keeps the ledger and the emitter from drifting. A count written only in literals is left bare, as an index is. No ledger signature names usize.

How a number is spelled

D16 — A number literal may be written 1_000_000, 0xFF, 0b1010 or 0o17.

Changed by ADR-322: a decimal whole number may end in a scale (1G, 4Gi), and an exponent is written e.

An underscore stands between digits and nowhere else. The prefixes are lower-case; hexadecimal digits either case. A float takes the separator (1_000.5) and no prefix. A digit the radix does not have (0b1210) is refused. A - written directly against the digits is part of the literal, so -9223372036854775808 is i64::MIN and -0xFF is -255; - 5 and -x are the unary operator.

D17 — The radix is a spelling, and a literal is a value.

0xFF is 255 and takes its type exactly as 255 does (D20-D25): let mask = 0xFF is an i32, let mask: u8 = 0xFF a u8.

D18 — The separator is not in the value, anywhere.

1_000 is 1000 to the checker, the ledger, the fold, and a diagnostic’s text.

D19 — A literal may be as large as a u64 holds.

Up to 18446744073709551615. A literal above i64::MAX is a u64’s and nothing else’s; one wider than a u64 is refused by name. With no u64 asking, it is refused against i64 (NK1116), the help naming u64.

What type a number takes

D20 — Where a use asks for a type, the use decides.

Part I 2.4’s first half: let small = 42 handed to fn wide(n: i64) is an i64. This compiler, not the language below, reads the use (D24).

D21 — Where nothing asks, a literal takes the first type that holds it: i32, else i64.

let count = 42 is an i32, let big = 3000000000 an i64. The question is about the value: -2147483648 is an i32. A fallback, not Kotlin’s whole rule, so backward inference survives.

D22 — A constant expression written only in literals takes the first type that holds it.

The unit is the expression, decided once on the outermost expression that folds and reaching every literal under it: 2000000000 + 2000000000 is 2000000000i64 + 2000000000i64. A value no type holds is refused in this language’s words. A sequence index and a repeat count are left bare (D1, D15). A value that fits is untouched.

D23 — A let without an annotation whose value is only numbers is an open number.

A literal, a sum of literals, or an operation over other open numbers. One operation has one type, so a + b, a < b and c = a + b make one number of all of them. A shift’s count joins nothing.

D24 — Its uses ask for its type, and every use in the function is read first.

A use asks where a type stands beside the number: a parameter, a return or last expression, an annotated let, a field, a typed operand or comparison (i < xs.len() asks for an i64), an assignment either way. An index asks for an i64 only where nothing else asks - a preference, never a conflict. Two uses asking two types are NK1200, naming both, with the annotation to write.

D25 — Where no use asks, what it is given decides, and every value it is given must fit.

The first type that holds all of its values - its own and every one assigned to it - i32, else i64 (D21 over every value): let mut n = 1 then n = 3000000000 is an i64. A value the decided type does not hold is NK1116 at that value, with a note that the type came from the uses.

D26 — A name is where the widening stops.

What an operation over a name comes to is held to the name’s type and never decides it. let a = 2000000000 then let c = a + a is refused where nothing asks (“this comes to 4000000000, which does not fit in an i32“, the way out let a: i64), and is an i64 where a use asks for one.

D27 — The decided type is written into the generated let.

let i: i64 = 0;, so the language below infers nothing this compiler decided; a literal that would get an i64 suffix carries the decided type’s. A number no use asked for is written bare.

D28 — One constant fold, and the lookup is what separates its callers.

crate::fold holds the arithmetic - in an i128, every step checked, over a literal, an immutable let whose value folded, + - * / % and a negation - and what a name is worth is a parameter. The checker passes its scope; the emitter, which has none, passes nothing_is_known, and gets exactly D22’s subset.

Refused at compile time

D29 — A constant that does not fit the type beside it is a compile error, not an abort.

let x: i32 = 3000000000 is NK1116, at an annotated let, a return against a declared result, an argument whose parameter says what it takes, and where an operand’s declaration pins the type (let b = a + 1). A fold that stops - a mut local, a parameter, a for binding, a cast - claims nothing, and an expression that does not fold is never refused.

D30 — A constant operation that overflows is refused where it stands.

In an f"…" hole, a condition, a list, a receiver - once, at the innermost operation that overflows. An operation over an open number is measured once that number’s type is decided.

D31 — A division whose divisor is a constant zero is refused.

NK1118, by the fold D29 uses. Every other division by zero stays where Part III A.2 has it: unrecoverable at run time, naming the Nikaia line. A divisor the fold cannot evaluate is one nothing is claimed about.

D32 — An integer widens where no value can be lost, between types already decided.

Added October 6, 2026 (#439).

fn area(x: i32, y: i32) -> i64 {
    x * y                       // computed in i64
}

let n: u64 = xs.len()           // a length is never negative
let total = count + offset      // u32 + i64 is an i64
if small < big { … }            // u64 against i64, compared as numbers

1. The common type. Two integer types have a common type when one type holds every value of both:

  u8 u32 u64 i32 i64
u8 u8 u32 u64 i32 i64
u32   u32 u64 i64 i64
u64     u64 none none
i32       i32 i64
i64         i64

A typed slot - a let with an annotation, an argument for a parameter of a stated type, a return or a body’s last expression, a field in a struct literal, an assignment, an element of a list whose element type is stated - takes a value of a narrower type that its type holds. An operator whose two sides are two integer types computes in their common type, and a list literal whose elements are two integer types holds their common type, whichever comes first. Where there is none, NK1199 and NK1154 stand.

2. A comparison of two integer types compares the numbers, for every pair, u64 against i64 included.

3. Inference first, widening after. A number without an annotation (D23-D25) and a generic parameter are typed by their uses, each use asking for exactly its type, as before. Widening is a check between two types already decided and never one of a use’s answers: let n = 5 handed to an i64 and to a u32 is NK1200, and pick(a, b) for fn pick[T](a: T, b: T) over an i32 and an i64 is refused with a as i64 as the help.

4. A slot’s type reaches through +, -, *, /, % and a negation. let t: i64 = x * y over two i32 computes in i64: each operand is widened before the operation. It does not reach into what a name was given, into a call’s arguments, a method’s receiver or an index, and it stops at the operators whose result depends on the width - &, |, ^, !, <<, >> - and at the wrapping_, saturating_ and truncating_ names. There, a computation in a narrower type is refused (NK1215), the help naming both readings: (a as i64) << 3 and (a << 3) as i64.

5. A value shown non-negative goes into an unsigned type without as. let n: u64 = xs.len() and, after if k >= 0, let n: u64 = k are taken where the proof says k >= 0 (ADR-306 D12 and D16; a callee’s postcondition, ADR-269 D17). Where it does not, the slot is NK1103, NK1102 or its neighbour, with as u64 and assert k >= 0 as the help.

Why a lost value and not a mix. Every refusal D3 made for a mix that loses nothing was answered with an as that could not fail; it marked no place a value might not fit, which is what D3 asked of it, and taught that as is noise. Java, Kotlin and C# widen at the same places; C widens too, but to a type that does not hold both (u32 + i32 is a u32 there), which is the mistake D3 was written against and the common-type table rules out.

Why inference does not widen. With widening among a use’s answers, let n = 5 handed to an i64 and a u32 has two types that work and no rule that picks one, and a generic T over an i32 and an i64 has two as well. C# picks the wider one for a generic; Swift admits no implicit widening at all, in part because its inference is already costly with literals and overloads. Between two types already decided the common type is unique, so keeping widening out of inference keeps both.

Why the slot’s type reaches the operands. Overflow aborts (D5), so +, -, *, / and % in a narrow type either give the number the wide computation gives or stop the program; computing wider changes no value a program prints and only removes a stop. That is untrue of the bit operators: !a for a: u32 = 0 is 4294967295 as a u32 and -1 as an i64, and x << 31 for x: i32 = 1 is -2147483648 and 2147483648. So those stop the slot’s type, and an expression of them is refused rather than read either way. Computing the narrow type and widening the result (the rule for a name) was the other choice for arithmetic: it is the long t = x * y; mistake C is known for, kept as an abort.

Why a proof may admit a value. The proof a build uses is the committed nikaia.proofs entry, replayed from its certificate (ADR-270 D4, D21), so the answer does not depend on the machine or on the search; a change that removes the fact is a refusal with a help, never a wrong value. Facts about std calls are their postconditions and D12’s length bound, so nothing is added to the ledger.

Rejected. A ledger column never negative for std results: a second place for what a postcondition already says, and blind to if k >= 0. Refusing a narrow computation in a wide slot: safe, but let p = x * y then let t: i64 = p is allowed, and the rule would forbid the spelling that means what the annotation says. Computing a whole expression in its widest operand’s type wherever it stands: one x * y would compute in three types in three places. Converting a finished list (Vec[u32] into Vec[i64]): a new allocation and a copy, and no longer the same list.

What it costs. A reader meets an expression whose type is the slot’s, not its operands’: x * y as an i64 and, moved into its own let, as an i32 that may stop. A computation into a wide slot handles half as many elements per vector register (not measured). No mainstream language passes a slot’s type to its operands.

D33 — f32 is a type of the language, beside f64.

Half the size per value is what a picture, a model’s weights, a sensor’s samples and most wire formats are made of, and every language this one is measured against offers it (C, Rust, Go, Swift, Java, C#). It follows the rules already set for numbers, so it adds no rule of its own:

This is D12’s rule for every narrowing conversion. The prover reasons about integers and not yet about floats (ADR-270 D11), so until it does, a non-constant f64 as f32 is NK1241 and a program writes one of the two names.

Decided October 8, 2026 (#470, #552).

D34 — The elements of a list written in number literals are one open number.

[12, 14, 13] is a Vec[T] whose T is decided as D23-D25 decide a let’s: the uses ask - a parameter Vec[u8], an annotated let, an element read into a typed place (let x: u8 = xs[0]), a push of a typed value, an element in a typed operation - and two uses asking two types are NK1200. Where no use asks, the first type that holds every element, and every value written into the list, is the element type: i32, else i64 (D21, D25). D26 holds for an element as for a name: xs[0] + xs[1] over two 2000000000s is NK1116 where nothing asks for an i64.

Why. A list of literals is the same question as a let of one, one level down, as ADR-135 D2 already answers it for []. A fixed Vec[i64] would refuse total([1, 2, 3]) against fn total(xs: Vec[u8]), and a list left untyped stops at run time where the same sum over a name is refused while building.

Decided October 8, 2026 (#513).

D35 — Text becomes a number by a function per type, and the name carries the type.

text::parse_i32, parse_i64, parse_u8, parse_u32, parse_u64, parse_f32 and parse_f64 each hand back a T?: the number the whole text writes, or null where it writes none or one the type does not hold. An integer is an optional sign and decimal digits (an unsigned type takes no -); a float is an optional sign, digits, an optional . and digits, and an optional exponent (e or E), or one of inf, -inf and nan in any case (NaN, -Inf), which a float holds and a data file writes. Nothing else: no space, no _. A program that has to say why a text is not a number reads it with a grammar (dec[T](p), Part II 10.8).

Why. The name carries the type, as checked_i32 and truncating_i32 do, so no signature has to take its type from the place its result goes, and no conversion follows the parse: text::parse_i32(s) ?? 1000 instead of an i64 narrowed by checked_i32 (D12). Java, C# and Go name the type the same way; Rust’s and Swift’s generic parse would be the one function in std whose result is typed by its use. Rust’s str::parse is not offered (ADR-286 D36).

Decided October 8, 2026 (#504).

The ordinary integer

D36 — int holds the values of an i64 and stops the program where an i64 would.

int is an integer type of the language, beside the five fixed widths. Its values are an i64’s; its arithmetic, its bit operators, its conversions, its literals and the places an overflow aborts are an i64’s (D5-D19). An int and an i64 take each other without as, in both directions: no value can be lost. Against the other widths an int widens and narrows as an i64 does (D12, D32).

Why. A programmer who writes i64 means 64 bits, and the language keeps that promise; one who only means an integer has had no way to say so. The values are fixed, not the machine’s: a C int that is 16, 32 or 64 bits wide gives one program other results on another machine, which Part I 1.2 does not allow. And the width does not follow the caller: an int whose width a call decided would let one function abort for one caller and not for another, with nothing in its signature to say so.

D37 — The representation of an int is the compiler’s choice; a fixed width is exactly that width.

The compiler may hold and compute an int in fewer bits where it shows that no value, no result and no abort changes - an index below the length of a short list, a list of literals whose sums cannot leave 32 bits. Where it does not show it, an int is an i64. A written i64, i32, u8, u32 or u64 is exactly that width, in memory and in arithmetic.

Why. A narrower type was kept as a fallback (D21) so that 32-bit targets, SIMD lanes and smaller lists stay within reach. Under an overflow that aborts (D5), a narrower type changes what the program computes; a narrower representation that is shown not to does not. It is the split String already has: the program says what the value is, the compiler chooses how it is held. ADR-306 shows a check unneeded by the same kind of proof.

D38 — Where the representation shows, a fixed width is written.

An extern "C" signature and a described Rust contract take a fixed width; an int there is refused with a code in Part III’s table, the help naming i64.

Why. At an interface the other side reads the bits, so a width chosen by the compiler would be a width nobody decided.

D39 — int is the integer ordinary code writes; a fixed width says that the width is the point.

Part I 2.2 recommends int for a number and a fixed width for a layout, a byte, a hash and an interface. Neither is a warning anywhere.

Why. The width that is written then carries information: a u32 field or a u64 hash is read as a decision, not a habit. A warning on a fixed width was weighed and rejected (§3).

Decided October 17, 2026 (#630).

D40 — A shift written only in literals is folded exactly, as + and * are.

D22 covers << and >>: 1 << 40 is the value 1099511627776 and takes the first type that holds it, an i64; 1 << 31 is 2147483648, also an i64; 1 << 63 no type holds, and it is refused. A shift loses the bits it moves out (Part I 2.2) only in a type, so where a use asks for one (let m: i32 = 1 << 31, an i32 parameter or field), the shift is that type’s and nothing changes. An open let given a shift of literals (D23, D25) is typed by the folded value.

Why. 1 << 40, 1099511627776 and 1024 * 1024 * 1024 * 1024 are one number and get one type; an exception for shifts would make a shift the only operator whose literal result is cut to an i32 where nothing asked for one. Go, Swift and Zig give 1 << 40 its exact value. Rejected: a shift of literals as an i32 (Rust’s choice, 1 << 40 refused and 1 << 31 negative), because it splits D22 by operator, and Java’s masking of the count (1 << 40 is 256), which is a wrong value without a word.

Decided October 19, 2026 (#661).

D41 — u8 has every name the other fixed widths have.

wrapping_, saturating_ and checked_ arithmetic (ADR-315 D1) exist for u8 as for u32, without _neg and _abs; truncating_u8 and checked_u8 convert into it out of a wider integer and out of an f64, as D13 and ADR-315 D4 say for the other destinations. c.wrapping_sub(b'0') is a digit’s value read with no check, n.truncating_u8() a byte’s low digits.

Why. u8 is one of the five integer types (D2) and the element of every Bytes; reading bytes - digits, ASCII ranges, a checksum - is where a program most often means to wrap or to stop. The families are the same on every width, as Rust’s are (D6, D7); a width that lacks them forces a widening the program did not mean ((b as i32) - 48). Rejected: leaving u8 without them, which no record decided and nothing argues for.

Decided October 19, 2026 (#729).

D42 — Reading the same bits with the other sign is bits_as_; truncating_ only narrows.

u.bits_as_i32() out of a u32, i.bits_as_u32() out of an i32, bits_as_i64() out of a u64 and bits_as_u64() out of an i64 keep every bit and read it as the other type: 4000000000 as a u32 comes out -294967296, -1 as an i64 comes out 18446744073709551615. There is no bits_as_ between different widths and none for u8, which has no signed partner.

truncating_T converts out of every integer type wider than T, whatever its sign, and out of an f64 (D13): the low bits of T’s width, read as T. u64::truncating_i32 joins the existing names, and f64::truncating_u32 and f64::truncating_u64 round toward zero and clamp as the signed ones do. Out of a type of the same width there is no truncating_ name: u64::truncating_i64 and i64::truncating_u64 go, and a call is refused (NK1210) with help naming bits_as_i64 or bits_as_u64. A widening with the other sign is written in two steps, each named for what it does: (x as i64).bits_as_u64().

Why. Truncating says that digits are lost, and between types of the same width none are: what changes is how the top bit is read. A program that reinterprets a hash or a signed word read from a file means something else than one that cuts a counter down, and a reader should see which one it is, as Zig separates @truncate from @bitCast and Rust 1.87 added cast_signed and cast_unsigned beside as. A name that does both hides a sign error behind a width change, the mistake C’s and Java’s implicit conversions make easy. The name carries the destination, as the other families do (D13), and stays apart from as, which in this language never changes a value.

Rejected: same-width conversions under truncating_ (as u64::truncating_i64 was), which keeps one name for two meanings; a direction without a type (cast_signed), against the naming of every other conversion here; leaving the 32-bit pair out, so that the rule would differ by width.

Decided October 20, 2026 (#742).

D43 — A map takes its key and value types from what is written into it, and numbers among them stay one open number.

collections::HashMap() without an annotation takes its key type and its value type from the first write that says them: m.insert("a", 1), m["a"] = 1 or m.entry("a").or_insert(1) make a HashMap[String, N], where N is one number without a type. That number is decided as D34 decides a list’s elements: by the uses of the values and of the keys (a value read into a typed place, handed to a typed parameter, written from a typed value), two uses asking two types are NK1200, and where none asks it is i32, or i64 where a written value does not fit. Keys written in number literals are one open number in the same way. A key written as a view of text (a line of a kept text, a part split cut) is a text position like any other, and its tier is the one ADR-282 D13 decides: a map of views of a kept text holds views. A map that nothing ever writes into and nothing types is refused with NK1153, as [] is.

Why. A map filled with insert("a", 1) is not a map of unknown types: its key is text and its value is an integer, and only the integer’s width is open. Leaving both open (HashMap[?, ?]) loses what the program already says, and what is lost reaches rustc as an error the checker never sees, such as += on an &mut {integer} in an and_modify. A map’s value is the same question as a list’s element (D34) one level further, which is a let’s one level down; answering it the same way keeps one rule for every place a number literal is stored.

Rejected: requiring an annotation on every map, against D34 and ADR-135 D2 for lists; fixing the value to i64 at the first write, which refuses fn total(m: HashMap[String, u8]) for a map of small literals, as a fixed Vec[i64] would.

Decided October 20, 2026 (#700).

5. Consequences

6. What this does not decide

This site is open source. Improve this page.