1module Std.Natural
2
3family NaturalArithmeticErrorCode : Type 0
4constructor NaturalArithmeticModuloByZero
5constructor NaturalArithmeticDivideByZero
6
7end-family
8
9family NaturalModuloResult : Type 0
10constructor NaturalModuloSucceeded
11field unrestricted naturalModuloValue : Nat
12constructor NaturalModuloFailed
13field unrestricted naturalModuloError : (family NaturalArithmeticErrorCode)
14
15end-family
16
17family NaturalDivisionState : Type 0
18constructor NaturalDivisionStateValue
19field unrestricted naturalDivisionRemainder : Nat
20field unrestricted naturalDivisionQuotient : Nat
21
22end-family
23
24family NaturalDivideResult : Type 0
25constructor NaturalDivideSucceeded
26field unrestricted naturalDivideValue : Nat
27constructor NaturalDivideFailed
28field unrestricted naturalDivideError : (family NaturalArithmeticErrorCode)
29
30end-family
31
32def naturalArithmeticErrorCodeBytes =
33 (lambda unrestricted code : (family NaturalArithmeticErrorCode) .
34 (eliminate
35 NaturalArithmeticErrorCode
36 (lambda unrestricted current : (family NaturalArithmeticErrorCode) . Bytes)
37 code
38 (branch NaturalArithmeticModuloByZero . b"ALPHA-STD-001")
39 (branch NaturalArithmeticDivideByZero . b"ALPHA-STD-002")))
40
41def naturalSelect =
42 (lambda unrestricted condition : Nat .
43 (lambda unrestricted whenTrue : Nat .
44 (lambda unrestricted whenFalse : Nat .
45 (nat-eliminate
46 (lambda unrestricted current : Nat . Nat)
47 whenFalse
48 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . whenTrue))
49 condition))))
50
51def naturalMinimum =
52 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
53 (nat-eliminate (lambda unrestricted current : Nat . Nat) right (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . left)) (nat-less-than left right))))
54
55-- Zero tests and ordering go through the ONE constant-time primitive the
56-- runtime offers on naturals, `nat-less-than`. A `nat-eliminate` over a
57-- natural is executed as a loop over its whole magnitude (measured
58-- 2026-09-16: asking whether the length of a 1 MiB string is zero cost 68 ms
59-- per call, about 65 ns per unit; the same question through nat-less-than
60-- costs nothing measurable), so no comparison may recurse on the value it
61-- compares. The 0/1 flag nat-less-than returns is the only thing eliminated.
62def naturalNonzero =
63 (lambda unrestricted value : Nat . (nat-less-than zero value))
64
65def naturalIsZero =
66 (lambda unrestricted value : Nat .
67 (nat-eliminate
68 (lambda unrestricted current : Nat . Nat)
69 (succ zero)
70 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
71 (nat-less-than zero value)))
72
73-- The flag operations below are written on the primitives themselves, not
74-- on one another: a realization calls them millions of times, and each call
75-- of one helper from another costs the machine an application chain (an
76-- equality through naturalAnd, naturalIsZero and naturalSelect took 44 steps
77-- where these take a handful; they were three fifths of realizing a tiled
78-- product). Each eliminates only a 0/1 flag from nat-less-than.
79def naturalAnd =
80 (lambda unrestricted left : Nat .
81 (lambda unrestricted right : Nat .
82 (nat-eliminate (lambda unrestricted current : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (nat-less-than zero right))) (nat-less-than zero left))))
83
84def naturalOr =
85 (lambda unrestricted left : Nat .
86 (lambda unrestricted right : Nat .
87 (nat-eliminate (lambda unrestricted current : Nat . Nat) (nat-less-than zero right) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero))) (nat-less-than zero left))))
88
89-- D21: the arithmetic below is the language's own (`nat-add` and friends run in
90-- one machine operation at run time and fold at compile time); the folds that
91-- counted step by step are gone. Semantics are unchanged: subtraction
92-- saturates at zero, x / 0 = 0, x mod 0 = x.
93def naturalAdd =
94 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-add left right)))
95
96def naturalPredecessor =
97 (lambda unrestricted value : Nat . (nat-subtract value 1))
98
99def naturalSaturatingSubtract =
100 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-subtract left right)))
101
102def naturalMultiply =
103 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-multiply left right)))
104
105def naturalEqual =
106 (lambda unrestricted left : Nat .
107 (lambda unrestricted right : Nat .
108 (nat-eliminate (lambda unrestricted current : Nat . Nat)
109 (nat-eliminate (lambda unrestricted current : Nat . Nat) (succ zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero)) (nat-less-than left right))
110 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
111 (nat-less-than right left))))
112
113def naturalLess =
114 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-less-than left right)))
115
116def naturalLessOrEqual =
117 (lambda unrestricted left : Nat .
118 (lambda unrestricted right : Nat .
119 (nat-eliminate (lambda unrestricted current : Nat . Nat) (succ zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero)) (nat-less-than right left))))
120
121def naturalModuloUnchecked =
122 (lambda unrestricted value : Nat .
123 (lambda unrestricted divisor : Nat . (nat-modulo value divisor)))
124
125def naturalModulo =
126 (lambda unrestricted value : Nat .
127 (lambda unrestricted divisor : Nat .
128 (nat-eliminate
129 (lambda unrestricted current : Nat . (family NaturalModuloResult))
130 (constructor
131 NaturalModuloResult
132 NaturalModuloFailed
133 (constructor NaturalArithmeticErrorCode NaturalArithmeticModuloByZero))
134 (lambda unrestricted predecessor : Nat .
135 (lambda unrestricted induction : (family NaturalModuloResult) .
136 (constructor
137 NaturalModuloResult
138 NaturalModuloSucceeded
139 (naturalModuloUnchecked value divisor))))
140 divisor)))
141
142def naturalDivisionStep =
143 (lambda unrestricted divisor : Nat .
144 (lambda unrestricted state : (family NaturalDivisionState) .
145 (eliminate
146 NaturalDivisionState
147 (lambda unrestricted current : (family NaturalDivisionState) .
148 (family NaturalDivisionState))
149 state
150 (branch
151 NaturalDivisionStateValue
152 remainder
153 quotient
154 .
155 (app
156 (lambda unrestricted incremented : Nat .
157 (nat-eliminate
158 (lambda unrestricted condition : Nat . (family NaturalDivisionState))
159 (constructor NaturalDivisionState NaturalDivisionStateValue incremented quotient)
160 (lambda unrestricted predecessor : Nat .
161 (lambda unrestricted induction : (family NaturalDivisionState) .
162 (constructor
163 NaturalDivisionState
164 NaturalDivisionStateValue
165 zero
166 (succ quotient))))
167 (naturalEqual incremented divisor)))
168 (succ remainder))))))
169
170def naturalDivisionState =
171 (lambda unrestricted value : Nat .
172 (lambda unrestricted divisor : Nat .
173 (nat-eliminate
174 (lambda unrestricted current : Nat . (family NaturalDivisionState))
175 (constructor NaturalDivisionState NaturalDivisionStateValue zero zero)
176 (lambda unrestricted predecessor : Nat .
177 (lambda unrestricted induction : (family NaturalDivisionState) .
178 (naturalDivisionStep divisor induction)))
179 value)))
180
181def naturalDivideUnchecked =
182 (lambda unrestricted value : Nat .
183 (lambda unrestricted divisor : Nat . (nat-divide value divisor)))
184
185def naturalDivide =
186 (lambda unrestricted value : Nat .
187 (lambda unrestricted divisor : Nat .
188 (nat-eliminate
189 (lambda unrestricted current : Nat . (family NaturalDivideResult))
190 (constructor
191 NaturalDivideResult
192 NaturalDivideFailed
193 (constructor NaturalArithmeticErrorCode NaturalArithmeticDivideByZero))
194 (lambda unrestricted predecessor : Nat .
195 (lambda unrestricted induction : (family NaturalDivideResult) .
196 (constructor
197 NaturalDivideResult
198 NaturalDivideSucceeded
199 (naturalDivideUnchecked value divisor))))
200 divisor)))
201
202def naturalPowerOfTwo =
203 (lambda unrestricted exponent : Nat .
204 (nat-eliminate
205 (lambda unrestricted current : Nat . Nat)
206 (succ zero)
207 (lambda unrestricted predecessor : Nat .
208 (lambda unrestricted induction : Nat . (naturalAdd induction induction)))
209 exponent))
210
211-- 256, by doubling: the divisor behind "fits in N bytes".
212def naturalTwoHundredFiftySix =
213 (naturalPowerOfTwo (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))
214
215-- "value < 256^byteCount" WITHOUT ever building 256^byteCount: divide by 256
216-- byteCount times and ask whether anything is left.
217--
218-- A runtime natural costs about 164 bytes and 300 ns PER UNIT of its magnitude
219-- (measured 2026-09-16: 2^20 takes 0.8 s and 195 MB, 2^24 takes 5 s and
220-- 2.75 GB, and 2^32 cannot be built at all -- the image exits 125). So a bound
221-- such as 2^32 must never be materialised, and `naturalLess x (naturalPowerOfTwo
222-- 32)` is not a comparison but an out-of-memory. This is how "fits in a 32-bit
223-- field" is asked instead; it costs about value/256 steps.
224def naturalBelowBytePower =
225 (lambda unrestricted byteCount : Nat .
226 (lambda unrestricted value : Nat .
227 (naturalIsZero
228 (nat-eliminate
229 (lambda unrestricted current : Nat . Nat)
230 value
231 (lambda unrestricted predecessor : Nat .
232 (lambda unrestricted quotient : Nat .
233 (naturalDivideUnchecked quotient naturalTwoHundredFiftySix)))
234 byteCount))))
235
236-- "value <= 256^byteCount", as (value - 1) < 256^byteCount with the saturating
237-- predecessor: 0 qualifies, 256^byteCount itself qualifies, one more does not.
238-- Callers that wrote `naturalLessOrEqual x bound` keep exactly that bound.
239def naturalAtMostBytePower =
240 (lambda unrestricted byteCount : Nat .
241 (lambda unrestricted value : Nat . (naturalBelowBytePower byteCount (naturalPredecessor value))))
242
243-- value < 2^32: it fits a 32-bit word
244def naturalFitsWord32 =
245 (lambda unrestricted value : Nat . (naturalBelowBytePower (succ (succ (succ (succ zero)))) value))
246
247-- "value < 2^bits" WITHOUT building 2^bits: halve bits times and ask whether
248-- anything is left. The general form of naturalBelowBytePower (a byte is eight
249-- halvings); it is what a limit such as "fits int64" (bits = 63) or "at most
250-- 16 MiB of input" (bits = 24) must use at runtime, since 2^24 alone costs
251-- 2.75 GB to materialise and 2^63 cannot be materialised at all.
252def naturalBelowTwoPower =
253 (lambda unrestricted bits : Nat .
254 (lambda unrestricted value : Nat .
255 (naturalIsZero
256 (nat-eliminate
257 (lambda unrestricted current : Nat . Nat)
258 value
259 (lambda unrestricted predecessor : Nat .
260 (lambda unrestricted quotient : Nat .
261 (naturalDivideUnchecked quotient (succ (succ zero)))))
262 bits))))
263
264-- value <= 2^32
265def naturalAtMostTwoPower32 =
266 (lambda unrestricted value : Nat .
267 (naturalAtMostBytePower (succ (succ (succ (succ zero)))) value))
268
269-- How many of f 0, f 1, ..., f (count - 1) are zero: a plain fold over a
270-- closed count, so the checker runs it as a strict loop -- one cell at a
271-- time, each forgotten once counted. (The first formulation nested each
272-- cell's select inside the previous one; a verdict of 40 cells that each run
273-- a program kept every earlier cell alive: 51 s against 7.6 s, two thirds of
274-- it garbage collection.)
275def naturalFailuresBelow =
276 (lambda unrestricted count : Nat .
277 (lambda unrestricted f : (pi unrestricted index : Nat . Nat) .
278 (nat-eliminate
279 (lambda unrestricted current : Nat . Nat)
280 0
281 (lambda unrestricted predecessor : Nat .
282 (lambda unrestricted induction : Nat . (naturalAdd (naturalIsZero (f predecessor)) induction)))
283 count)))
284
285-- 1 when f 0, f 1, ..., f (count - 1) are all nonzero, else 0: a bounded
286-- universal verdict the checker can compute. With a statement for every
287-- f (count + b), Std.Equality.stdNaturalAllBelowSound turns it into a
288-- statement for every natural -- a finite region decided by computation, the
289-- rest by an argument over an open offset.
290def naturalAllBelow =
291 (lambda unrestricted count : Nat .
292 (lambda unrestricted f : (pi unrestricted index : Nat . Nat) .
293 (naturalIsZero (naturalFailuresBelow count f))))
294
295-- The decimal digits of a natural, most significant first ("0" for zero):
296-- the text form of a counter, a sequence number or a tick in an AOS-JSON/1
297-- stream (Observe.Value), and of a token cache path's ranges
298-- (Data.TokenCachePath). `fuel` is the caller's bound on the number of
299-- digits LESS ONE: a natural with more than `fuel + 1` digits keeps only its
300-- last `fuel + 1`, so every caller names a bound its values cannot exceed
301-- (a u64 has at most 20 digits).
302def naturalDecimalBuilder =
303 (lambda unrestricted fuel : Nat .
304 (nat-eliminate
305 (lambda unrestricted current : Nat . (pi unrestricted value : Nat . BytesBuilder))
306 (lambda unrestricted value : Nat .
307 (bytes-builder-chunk (bytes (nat-to-byte (naturalAdd 48 (naturalModuloUnchecked value 10))))))
308 (lambda unrestricted predecessor : Nat .
309 (lambda unrestricted induction : (pi unrestricted value : Nat . BytesBuilder) .
310 (lambda unrestricted value : Nat .
311 (let unrestricted quotient = (naturalDivideUnchecked value 10)
312 in (nat-eliminate
313 (lambda unrestricted nonzero : Nat . BytesBuilder)
314 (bytes-builder-chunk (bytes (nat-to-byte (naturalAdd 48 (naturalModuloUnchecked value 10)))))
315 (lambda unrestricted quotientPredecessor : Nat .
316 (lambda unrestricted quotientInduction : BytesBuilder .
317 (bytes-builder-append
318 (induction quotient)
319 (bytes-builder-chunk (bytes (nat-to-byte (naturalAdd 48 (naturalModuloUnchecked value 10))))))))
320 (naturalNonzero quotient))))))
321 fuel))
322
323def naturalDecimalBytesWithin =
324 (lambda unrestricted fuel : Nat . (lambda unrestricted value : Nat .
325 (bytes-builder-build (naturalDecimalBuilder fuel value))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.