Skip to content

index.md

Latest commit

 

History

History
366 lines (299 loc) · 76.4 KB

index.md

File metadata and controls

366 lines (299 loc) · 76.4 KB
Raw

Algorithms, I/O, and applications

This index lists implementations, behavior, and proved results for library algorithms, WASI stream operations, applications, and compiler examples. The native library aggregate imports the reusable implementations. The compiler manuals describe the verified dialect and the LeanExe dialect.

The compiler's theorem for a module states that the module computes its Lean definition. A byte theorem states execution or a further property, such as an accuracy bound, for the encoded module. A call theorem is a byte theorem for one export, called from a store and with arguments that meet its premises. A file theorem states that an emitted file holds that encoding. Execution theorems use Talos's semantics of WebAssembly with the deterministic floating-point profile. They assume the allocator invariant and, for some functions, borrowed tables, static byte data, and bounds on memory and recursion depth. WASI theorems also assume a host that satisfies the WASI contracts. An implements theorem can permit a trap at unreachable. A trap-free theorem proves a return under its allocation and depth conditions. Each linked guide states its domains, exceptional inputs, and host assumptions. The transcendental development record gives the numerical proofs' history.

Contents

1. Arithmetic

The limb representation stores natural numbers in little-endian arrays of 32-bit limbs carried in UInt64 words. val a denotes the represented natural number, and Limbs a requires every element to be below 2^32. The limb theorems assume that property and their stated array-size, shift, and quotient bounds. The standalone compilation proves execution of these definitions. Decimal parsing and printing include the routines they call in their own modules.

Algorithm Implementation Behavior Proved results and limits
fma Software fused multiply-add Computes a * b + c with one nearest-even rounding, using 128-bit products and shifts implemented in 64-bit words. FmaTheorem.fma_toBits proves equality with IEEE 754 fusedMultiplyAdd for all operands, including exceptional values. The erfc, tgamma, and lgamma byte theorems include its calls.
mulSmall Limb multiplication with carry Returns limbs for val a * m + c, one limb longer than a. mulSmall_spec, for m, c < 2^32 and a.size < 2^64.
shl Limb left shift Returns limbs for val a * 2^k. shl_spec, for a.size < 2^32.
le Limb comparison Compares val a ≤ val b. le_spec, for both array sizes below 2^32.
sub Limb subtraction Returns val a - val b in an array of a.size limbs. sub_spec, for val b ≤ val a, a.size < 2^32, and b.size < 2^64.
wordBits Word bit length Counts the significant bits of a word, returning zero for zero. wordBits_spec proves equality with Nat.size.
bitLen Limb bit length Counts the significant bits of val a. bitLen_spec proves equality with Nat.size, for a.size < 2^32.
divBits Restoring limb division Returns a quotient word and remainder limbs for division of val n by val d. divBits_spec, for positive val d, array sizes below 2^31, bits ≤ 63, and val n < val d * 2^bits.
scaledQuot Cox's exact unrounded scaling Returns the floor of val n * 2^sn / (val d * 2^sd) and a flag for a nonzero remainder. scaledQuot_spec, for positive val d, array sizes and shifts below 2^30, bits ≤ 63, and a quotient below 2^bits.
mulPow10 Limb multiplication by a power of ten Returns limbs for val a * 10^k, multiplying in blocks of nine decimal digits. mulPow10_spec, for a.size < 2^31 and k < 2^20.
pow10 A power of ten as limbs Returns limbs for 10^k. pow10_spec, for k < 2^20.
gcd Euclid's remainder recursion Computes the greatest common divisor of two words. gcd_eq proves equality with Nat.gcd. gcd_bytes states that result for the bytes.
Prime-factor count Trial division Counts prime factors with multiplicity by trial division in increasing order. compute_eq proves equality with the length of Mathlib's Nat.primeFactorsList. primeFactors_bytes states that result for the bytes.
sieve The array-element example Marks multiples of each prime p from p², returning flags for composite numbers below n. Generated compiler correctness. The result uses the definition's word arithmetic.
pow The recursion example Computes b^e modulo 2^64 by repeated squaring. Generated compiler correctness, with the example's guarded recursion premises.
ceilSqrt Bracket halving Performs 17 bracket halvings to find an integer ceiling square root. Sqrt.ceilSqrt_correct proves the least integer whose square is at least n, for n ≤ 2^32. The compilation proves execution of the word definition.

2. Arrays, lists, trees, and sorting

These algorithms use UInt64 words, counts, and indices, with arithmetic modulo 2^64. Each linked compilation supplies execution, allocation, and trap-free theorems under the verified compiler's representation, ownership, memory, and recursion premises. The array guide states the common array conventions.

Algorithm Implementation Behavior Proved results and limits
count Array search Counts occurrences of a word. Generated execution proof.
firstAbove Array search Returns the first index whose element exceeds a limit and a Boolean success flag. A miss returns (0, false). Generated execution proof.
firstZero Array search Searches a specified prefix for zero. Returns the prefix length on a miss. Reads beyond the array return zero. firstZero_cases proves the first-match property. Generated execution proof.
removeAll Array filtering Removes matching words in order by repeated searches and shifts, taking quadratic time. Generated execution proof.
below Array filtering Collects, in order, at most a specified count of words below a limit. Generated execution proof.
clearUntil Array filtering Zeros the prefix before the first matching word, or the whole array when the word is absent. Generated execution proof.
repeated Array repetition Concatenates a specified number of copies of an array. Generated execution proof.
evens Even-word range Builds n elements with element i equal to 2 * i. Generated execution proof.
scaled Word-array scaling Multiplies each element by a word scalar. Generated execution proof.
List range Word lists Builds the list 0 through n - 1 in ascending order. Generated execution proof.
listSum Word lists Folds addition from zero over a word list. Generated execution proof.
List sum Word lists Adds each word to a supplied accumulator by tail recursion. Generated execution proof. The compilation uses a tail loop.
reverse Word lists Reverses the input list onto a supplied accumulator list. Generated execution proof. The compilation uses a tail loop.
List increment Word lists Adds one to every word. Generated execution proof, with guarded structural recursion.
KeyTree.size Word trees Counts the nodes modulo 2^64. Generated execution proof, with guarded recursion.
KeyTree.sum Word trees Sums the keys modulo 2^64. Generated execution proof, with guarded recursion.
KeyTree.height Word trees Returns zero at a leaf and one plus the maximum child height at a node, using word arithmetic. Generated execution proof, with guarded recursion.
KeyTree.incr Word trees Adds one to every key modulo 2^64, preserving the tree's shape. Generated execution proof, with guarded recursion.
KeyTree.setKey Word trees Replaces the root key, leaving an empty tree empty. Generated execution proof.
KeyTree.insert Word trees Inserts left for a smaller key and right for a larger key. Equality leaves the node unchanged. Generated execution proof, with guarded recursion. Search-tree ordering and membership theorems remain future work.
KeyTree.leftChild Word trees Returns the root's left child, or an empty tree for an empty input. Generated execution proof.
KeyTree.splitRoot Word trees Returns the two children, or two empty trees for an empty input. Generated execution proof.
sortInsert Insertion sort Inserts each element at the count of smaller elements already accumulated. The algorithm takes quadratic time. Generated execution proof and the worked allocation-bound proof. Sortedness and permutation theorems remain future work.

KeyTree has an empty constructor and nodes containing a word key and two children. Its encoding uses null for empty and fixed-layout records for nodes. The list-tail cases and tree examples check ownership, copying, header reuse, allocation counts, and the guarded recursion limit. The library case registry reuses compiler-fixture cases for the extracted modules, with supplementary native cases.

3. Pseudorandom number generators

Each generator keeps its state in a UInt64. The linked guides state the parameters, valid states, and memory conditions.

Algorithm Implementation Behavior Proved results and limits
Linear congruential generator LCG implementation and proofs Applies a * x + c modulo 2^64, with repeated-step and jump-ahead operations. Period 2^64 from every state, with each word once per period. Jump-ahead equals repeated steps. Exact top-bit counts, hyperplane bounds, and spectral-test values for two to six successive states. lcg_advance and lcg_jump.
Park–Miller Park–Miller implementation and proofs Applies 16807 * x % (2^31 - 1). The seed operation maps every word to a valid state. Period 2^31 - 2 from every state in [1, 2^31 - 2], with each state once per period. parkMiller_advance.
Xorshift64 Xorshift implementation and proofs Applies Marsaglia's shifts (13, 7, 17), with repeated-step and jump-ahead operations. Period 2^64 - 1 from every nonzero state, with each nonzero word once per period. Jump-ahead equals repeated steps. Exact top-bit counts and a 36,920-byte heap-growth bound for jump-ahead. xorshift_advance and xorshift_jump.
SplitMix64 SplitMix64 implementation and proofs Adds a fixed odd increment, then applies Vigna's xorshift and multiplication rounds to produce an output word. prng_bytes proves the Lean definition's state and output word and preservation of the store.
unitFloat Word-to-binary64 conversion Maps x to (x >>> 11) / 2^53 in [0, 1). prng_bytes covers the conversion. unitFloat_pure supplies a reusable store-preserving execution proof.

The reusable splitMix_pure proof permits calls from other compiled modules, as the SplitMix64 guide and the LTG entry describe. The orbit lemmas supply shared results about iteration, minimal periods, unique visits, and top-bit counts.

4. Reductions

Each compilation proves execution of the stated fold under the compiler's representation and memory premises.

4.1. Word reductions

Word reductions use UInt64 arithmetic modulo 2^64.

Algorithm Implementation Behavior Proved results and limits
sumArray Word reductions Folds addition left to right from zero. Generated execution proof.
productArray Word reductions Folds multiplication left to right from one. Generated execution proof.
xorArray Word reductions Folds exclusive or left to right from zero. Generated execution proof.
Word dot The array compiler example Sums products over the first array's length. Missing entries of the second array read as zero. Generated compiler correctness for the word definition.

4.2. Binary64 reductions

Binary64 operations follow the stated order, including the definitions' NaNs and signed zeros. Numerical-error bounds remain future work.

Algorithm Implementation Behavior Proved results and limits
total Binary64 reductions Sums left to right from zero. Generated execution proof.
sumRange Binary64 reductions Sums [lo, hi) by recursive halves for lo ≤ hi. An empty range gives zero, and missing entries read as zero. Generated execution proof, under the generated recursion and allocation conditions.
select Binary64 reductions Sums flagged entries left to right over the numeric array. Missing flags read as false. Generated execution proof.
largest Binary64 reductions Applies Lean's max left to right from negative infinity, which is also the empty-input result. Generated execution proof.

5. Statistics

Mean and sum of squares are reusable library functions. The other entries remain compiler examples or application functions. Their execution proofs preserve each definition's operation order. Numerical-error bounds remain future work.

Algorithm Implementation Behavior Proved results and limits
sumSquares Sum-of-squares implementation and proof Accumulates squares left to right from zero, with separate multiplication and addition. sumSquares_bytes proves bit-for-bit execution, including exceptional results.
mean Mean implementation and proof Divides the left-to-right sum by the length converted to binary64. An empty array gives NaN. mean_bytes proves bit-for-bit execution.
median The selection compiler example Selects the middle of three words by comparisons. Generated compiler correctness for the comparison definition.
histogram The array-update compiler example Counts residues modulo the requested bucket count. Counts wrap modulo 2^64. Zero buckets produce an empty array. Generated compiler correctness for the array-update definition.
layerNorm Binary64 GPT normalization Computes the mean and population variance from left-to-right sums, adds the supplied epsilon to the variance, then normalizes and applies gain and bias. The GPT byte theorem proves execution of the rounded calculation.
layerNorm32 Binary32 GPT normalization Normalizes d values using the supplied binary32 divisor nf, epsilon 0.00001, gain, and bias. Each output recomputes the left-to-right mean and variance. nf = d gives the intended population divisor. The verified compilation proves Wasm execution. The dispatch proofs prove the modeled GPU result and race freedom.

The statistics plan records variance and standard deviation, incremental and merged moments, generalized sample quantiles, weighted quantiles, covariance, correlation, and dispersion measures as future work. Empty samples, exceptional values, probability and weight domains, and numerical-error bounds require specifications.

6. Elementary and special functions

Arguments and results are binary64 values. A bound of k steps means that the result lies within k positions of the nearest-even rounding of the exact result on the ordered line of binary64 values, which puts both zeros at one position and the infinities at its ends. Each bound covers finite inputs in its stated domain, or every finite input when the row gives no restriction. The linked guides state the exceptional-value results. The module of each byte theorem has file theorems that identify its encoding in build/verified/, such as ExpFile.exp_file.

Algorithm Implementation Behavior Proved results and limits
exp The exponential e^x, following Arm optimized-routines. 1 step. ExpTheorem.exp_bytes_accuracy.
exp2 Base-2 exponentiation 2^x, following Arm optimized-routines. 1 step. Exp2Bytes.exp2_bytes_accuracy.
exp10 Base-10 exponentiation 10^x, following Arm optimized-routines. 1 step. Exp2Bytes.exp10_bytes_accuracy.
expm1 Exponential minus one e^x - 1, following fdlibm. 1 step. TanhBytes.expm1_bytes_accuracy.
log The natural logarithm ln x, following Arm optimized-routines. 1 step for x > 0. LogTheorem.log_bytes_accuracy.
log2 The base-2 logarithm log₂ x, following Arm optimized-routines. 1 step for x > 0. Exact at representable powers of two by log2_power and log2_one. Log2Theorem.log2_bytes_accuracy.
log10 The base-10 logarithm log₁₀ x, following fdlibm. 1 step for x > 0. Exact at 10^n for 0 ≤ n ≤ 22 by log10_pow10. Log10Theorem.log10_bytes_accuracy.
log1p Logarithm of one plus the input ln (1 + x), following fdlibm. 1 step for x > -1. Log1pBytes.log1p_bytes_accuracy.
pow The power function x^y, following Arm optimized-routines. 1 step for x > 0, for x < 0 with integer y, and for x = 0 with y ≥ 0. PowBytes.pow_bytes_accuracy.
sin Sine Sine of x in radians, following fdlibm. 1 step. TrigTheorem.sin_bytes_accuracy.
cos Cosine Cosine of x in radians, following fdlibm. 1 step. TrigTheorem.cos_bytes_accuracy.
tan Tangent Tangent of x in radians, following fdlibm. 1 step. TanTheorem.tan_bytes_accuracy.
atan The arctangent Arctangent of x, following fdlibm. 1 step. AtanBytes.atan_bytes_accuracy.
atan2 The two-argument arctangent The angle of (x, y), with quadrant selection, following fdlibm. 2 steps for y ≠ 0. AtanBytes.atan2_bytes_accuracy.
asin The arcsine Arcsine of x, following fdlibm. 1 step for -1 ≤ x ≤ 1. AsinBytes.asin_bytes_accuracy.
acos The arccosine Arccosine of x, following fdlibm. 1 step for -1 ≤ x ≤ 1. AsinBytes.acos_bytes_accuracy.
sinpi Pi-scaled sine sin (πx), following FreeBSD msun. 1 step. SinpiTheorem.sinpi_bytes_accuracy.
cospi Pi-scaled cosine cos (πx), following FreeBSD msun. 1 step. SinpiTheorem.cospi_bytes_accuracy.
tanpi Pi-scaled tangent tan (πx), following FreeBSD msun. 1 step outside the half-integers. SinpiTheorem.tanpi_bytes_accuracy.
sinh Hyperbolic sine Hyperbolic sine of x, following fdlibm. 3 steps. SinhBytes.sinh_bytes_accuracy.
cosh Hyperbolic cosine Hyperbolic cosine of x, following fdlibm. 1 step. SinhBytes.cosh_bytes_accuracy.
tanh Hyperbolic tangent Hyperbolic tangent of x, following fdlibm. 3 steps. TanhBytes.tanh_bytes_accuracy.
asinh The inverse hyperbolic sine Inverse hyperbolic sine of x, following fdlibm. 2 steps. AsinhBytes.asinh_bytes_accuracy.
acosh The inverse hyperbolic cosine Inverse hyperbolic cosine of x, following fdlibm. 2 steps for x ≥ 1. AsinhBytes.acosh_bytes_accuracy.
atanh The inverse hyperbolic tangent Inverse hyperbolic tangent of x, following fdlibm. 2 steps for -1 < x < 1. AsinhBytes.atanh_bytes_accuracy.
erf The error function erf x, following fdlibm. 1 step. ErfTheorem.erf_bytes_accuracy.
erfc The complementary error function 1 - erf x, following CORE-MATH. 1 step. ErfcBytes.erfc_bytes_accuracy.
tgamma The gamma function Γ(x), following CORE-MATH. 1 step outside zero and the negative integers. TgammaBytes.tgamma_bytes_accuracy.
lgamma The log-gamma function ln |Γ(x)|, following CORE-MATH. 1 step outside zero and the negative integers. LgammaBytes.lgamma_bytes_accuracy.
lgammaR Log-gamma with its sign (lgamma x, signgam), with the sign represented by ±1.0, following CORE-MATH. lgammaR_sign proves the sign of Γ(x) for finite inputs outside zero and the negative integers. The compilation proves execution of the pair-valued function.

Sine, cosine, and tangent reduce large arguments by the method of Payne and Hanek in 64-bit word arithmetic, following Go's math.trigReduce. TrigDistance.quadrant_distance bounds how close a binary64 value comes to a multiple of π/2.

6.1. Bessel functions

The Bessel implementation follows fdlibm. Let u = 2^-53 and M_n(x) = √(J_n(x)² + Y_n(x)²). The modulus bounds measure absolute error in units of u M_n, which stays positive at the zeros of J_n and Y_n. The order argument of jn and yn is a word whose low 32 bits encode a signed integer.

Algorithm Implementation Behavior Proved results and limits
j0 Order-zero Bessel function J₀(x). 10 u M_0(|x|) for every finite x. BesselBytes.j0_bytes_accuracy.
j1 Order-one Bessel function J₁(x). 12 u M_1(|x|) for every finite x. BesselBytes.j1_bytes_accuracy.
y0 Order-zero Bessel function of the second kind Y₀(x). 11 u M_0(x) for finite x > 0. BesselBytes.y0_bytes_accuracy.
y1 Order-one Bessel function of the second kind Y₁(x). 12 u M_1(x) for x ≥ 2^-1022, and 1 step for 0 < x < 2^-54 (1 + 2^-20). Together these cover finite x > 0. BesselBytes.y1_bytes_accuracy.
jn Integer-order Bessel function J_n(x). (23 + 12 |n|) u M_|n|(|x|) for every finite x outside the open range below. BesselBytes.jn_bytes_accuracy.
yn Integer-order Bessel function of the second kind Y_n(x). (250 + 12 |n|) u M_|n|(x) for finite results, with the overflow alternative below, for finite x > 0 outside the open range. BesselBytes.yn_bytes_accuracy.

Both integer-order theorems exclude 2 ≤ |x| < 2^302 with |n| > |x|/2. That range remains open: a proof needs a bound on M_k(x) for every order k through the turning point k = x. For yn, the theorem permits the infinity with the sign of Y_n(x) only when |Y_n(x)| > 2^1023, and BesselYnTheorem.yn_overflow states that the result is that infinity when |Y_n(x)| ≥ 2^1025. Between those thresholds the result is either that infinity or a finite value within the bound. BesselBytes.bessel_module_accuracy combines the byte results. The file theorems identify the encoding in build/verified/bessel.wasm.

7. Linear algebra

The linear-algebra library supplies vector and matrix operations used by both GPT demos. Matrices are row-major flat arrays. Dimensions and indices use UInt64 arithmetic modulo 2^64, and missing entries read as zero. Multiplication and addition round separately, and dot products accumulate left to right from zero. The compilation theorems preserve that order under the generated memory and recursion conditions. Numerical-error bounds remain future work.

Algorithm Implementation Behavior Proved results and limits
dot (binary64) Binary64 dot product Sums products over the first array's length. Generated execution proof.
axpy (binary64) Binary64 vector update Returns a * xs[i] + ys[i] for each index below ys.size. Generated execution proof.
grid (binary64) Binary64 grid construction Builds n values x0 + i.toFloat * dx, with binary64 conversion, multiplication, and addition. Generated execution proof.
matVec (binary64) Binary64 matrix-vector product Multiplies a rows × cols matrix by a vector, returning rows values. Generated execution proof.
matMul (binary64) Binary64 matrix product Multiplies an n × k matrix by a k × m matrix, returning n * m row-major values. Generated execution proof.
matMulT (binary64) Binary64 product with a transposed matrix Multiplies an n × k matrix by the transpose of an m × k matrix, returning n * m row-major values. Generated execution proof.
add (binary64) Binary64 vector addition Adds elementwise over the first array's length. Generated execution proof.
scale32 Binary32 vector scaling Multiplies each element of x by a, returning x.size values. Generated execution proof.
axpyArray32 Binary32 vector multiply-add Builds a * x[i] + y[i] over x.size. Generated execution proof.
matVec32 Binary32 matrix-vector product Multiplies a rows × cols matrix by a vector, returning rows values. Generated execution proof.
add32 Binary32 vector addition Adds elementwise over the first array's length. Generated execution proof.
linear32 Binary32 biased linear transform Multiplies a row of k values by a k × m matrix, returning m values. Each output adds b[c] after its column dot product. Generated execution proof.

8. Discrete Fourier transform

A complex signal is a flat binary64 array with real and imaginary parts interleaved. The direct transform takes quadratic time and ignores an odd final float. Transform and spectrum error bounds remain open. Its trigonometric factors use the sine and cosine implementations in Section 6.

Algorithm Implementation Behavior Proved results and limits
twiddle Fourier implementation Returns (cos θ, sin θ) for θ = 6.283185307179586 * (m.toFloat / n.toFloat), computed in binary64. Generated execution proof.
dft Fourier implementation Computes the direct discrete Fourier transform using n² complex products. Generated execution proof.
inverse Fourier implementation Computes the inverse-sign transform, then divides each component by n. Generated execution proof.
powerSpectrum Fourier implementation Transforms real samples and returns |X_k|² for 0 ≤ k ≤ n/2. An empty input returns an empty array. Generated execution proof.

The native accuracy test compares its test signals with a reference transform computed using exact integer sums and 300-bit approximations to the trigonometric factors, then rounded to binary64. It reports the largest error relative to its test tolerance.

9. Conversion between decimal strings and binary floating point

The parsers take one byte per UInt64 array element and select either RFC 8259's number grammar or the documented superset in the manner of C's strtod. The proofs cover strings of fewer than 2^32 bytes. Binary32 encodings occupy the low 32 bits of a word. The printers return arrays of byte-valued words.

Algorithm Implementation Behavior Proved results and limits
parse64 Decimal-to-binary conversion Parses a binary64 value with Clinger's fast path for short decimal inputs, then exact rounding through Cox's unrounded scaling when the fast path does not apply. ParseFloatBytes.parse64_bytes_accuracy: nearest-even rounding of the denoted number, or rejection outside the selected grammar.
parse32 Decimal-to-binary conversion Parses a binary32 encoding through exact rounding with Cox's unrounded scaling. ParseFloatBytes.parse32_bytes_accuracy: nearest-even rounding of the denoted number, or rejection outside the selected grammar.
print64 Binary-to-decimal conversion Prints a binary64 encoding in scientific layout, using exact scaled-quotient comparisons to select decimal digits. PrintFloatBytes.print64_bytes_accuracy: round trip, RFC 8259 grammar for finite values, and the shortest-decimal property below.
print64Ecma Binary-to-decimal conversion Prints a binary64 encoding with ECMA-262's Number::toString layout. PrintFloatBytes.print64Ecma_bytes_accuracy: round trip, RFC 8259 grammar for finite values, and the shortest-decimal property below.
print32 Binary-to-decimal conversion Prints a binary32 encoding in scientific layout, using exact scaled-quotient comparisons to select decimal digits. PrintFloatBytes.print32_bytes_accuracy: round trip, RFC 8259 grammar for finite values, and the shortest-decimal property below.
print32Ecma Binary-to-decimal conversion Prints a binary32 encoding with ECMA-262's Number::toString layout. PrintFloatBytes.print32Ecma_bytes_accuracy: round trip, RFC 8259 grammar for finite values, and the shortest-decimal property below.

Parsing a printer's output recovers the input, with a NaN replaced by the canonical NaN. For a finite nonzero input, the output has the fewest significant digits among decimals that round to the input, the least distance from the input among those, and an even last digit at a tie. The search finds the largest power of ten with a multiple in the input's rounding interval, using the exact limb arithmetic. ParseFloatFile.parse_file and PrintFloatFile.print_file identify the emitted module encodings.

10. Outward rounding and limiters

The checked operations return Checked: status zero accepts a finite endpoint, and status one rejects it. The direction flag selects a lower or upper bound. The flat encoding stores status and value. The checked arithmetic operations test their inputs, the rounded result, and the endpoint before acceptance.

Algorithm Implementation Behavior Proved results and limits
absBits Binary64 magnitude bits Clears the sign bit of a word. Generated execution proof.
finite Binary64 finiteness test Tests whether the magnitude bits are below the infinity encoding. Generated execution proof and the word-level correspondence proofs.
nextUpBits Adjacent binary64 word For a finite input word, returns the encoding of the next larger binary64 value. Either signed-zero encoding maps to the encoding of 2^-1074. Generated execution proof. The adjacent-real interpretation requires finite input and output, as the endpoint proof states.
nextDownBits Adjacent binary64 word For a finite input word, returns the encoding of the next smaller binary64 value. Either signed-zero encoding maps to the encoding of -2^-1074. Generated execution proof. The adjacent-real interpretation requires finite input and output, as the endpoint proof states.
endpoint Checked adjacent endpoint Moves a rounded binary64 result one adjacent value in the selected direction. Rejects nonfinite results or endpoints. endpoint_word identifies the word-level operation. Generated execution proof.
outAdd Checked outward addition Adds two finite inputs and returns an outward endpoint when the result and endpoint are finite. outAdd_accepted proves a real lower or upper bound on the exact sum. Generated execution proof.
outSub Checked outward subtraction Subtracts two finite inputs and returns an outward endpoint when the result and endpoint are finite. outSub_accepted proves a real lower or upper bound on the exact difference. Generated execution proof.
outMul Checked outward multiplication Multiplies two finite inputs and returns an outward endpoint when the result and endpoint are finite. outMul_accepted proves a real lower or upper bound on the exact product. Generated execution proof.
outDiv Checked outward division Divides finite inputs, rejects a zero denominator, and returns an outward endpoint when the result and endpoint are finite. outDiv_accepted proves a real lower or upper bound on the exact quotient. Generated execution proof.
outSqrt Checked outward square root Checks a finite nonnegative input and returns an outward endpoint when the result and endpoint are finite. outSqrt_accepted proves a real lower or upper bound on the square root. Generated execution proof.
minmod Minmod implementation and real theory Returns the input with smaller word magnitude when sign bits agree, and zero when they differ. real_minmod relates the implementation through CodeLib.IEEE64.value to real minmod. The real theory proves symmetry, sign reversal, bounds, a Lipschitz bound, and constant- and linear-profile reconstruction properties. Generated execution proof.

The Euler enclosure proofs use the checked operations. The reconstruction analysis uses minmod to bound the differences and faces computed from rounded inputs.

11. Hash functions

The hashing guide describes the arguments: a message of n bytes is an Array UInt64 with eight bytes per word in little-endian order. A digest of SHA-2, HMAC, or a SHA-3 hash function is a structure of words in the same packing, a SHAKE output is an array of words, and a CRC, SipHash, or XXH64 result is one word. Each call theorem states that the export, called from a ready store with borrowed arrays, returns without a trap the result of its family's transcription for the message's bytes, and that the caller's heap keeps its bytes. Each row states the limits on the lengths. The compiler's allocation bound, bound_eq, is zero for every export except SHAKE, whose bound is its output array. The file theorems of SHA-256, SHA-512, HMAC-SHA-256, HMAC-SHA-512, SHA-3, CRC, SipHash, and XXH64 identify the emitted modules.

The SHA-2 specification is a literate transcription of FIPS 180-4, copied with its implementation and equivalence proofs from fips-180-4-lean, and the HMAC specification transcribes FIPS 198-1 over it. The SHA-2 and HMAC call theorems read message, key, and digest bytes most significant bit first, as FIPS 180-4 does. The Merkle–Damgård module proves that two distinct messages with equal SHA-256 or SHA-512 digests give a collision of the compression function of FIPS 180-4. The SHA-3 specification transcribes FIPS 202 and agrees with every CAVP vector, and its call theorems read message and digest bytes least significant bit first, as FIPS 202 does. The CRC specification transcribes ITU-T V.42 and RFC 3720 with Mathlib's polynomials over GF(2), and its result is the CRC as zlib and the Linux kernel report it. The SipHash and XXH64 specifications transcribe the SipHash paper and the xxHash specification on 64-bit words. Independent reviews compared the SHA-3, CRC, SipHash, and XXH64 transcriptions with their sources.

Algorithm Implementation Behavior Proved results and limits
sha256 SHA-256 and SHA-224 The 32-byte digest of FIPS 180-4 §6.2. The program holds each 32-bit word in the low half of a UInt64, masking before shifts to the right and rotations. sha256_call, from sha256_spec, for messages below 2^61 bytes.
sha224 SHA-256 and SHA-224 The 28-byte digest of §6.3, in four words whose last four bytes are zero. sha224_call, for messages below 2^61 bytes.
sha512 The SHA-512 family The 64-byte digest of FIPS 180-4 §6.4. The program reads each padded word from the packed message and keeps the message schedule in a window of sixteen words. sha512_call, from sha512_spec, for messages below 2^61 bytes.
sha384 The SHA-512 family The 48-byte digest of §6.5, from the initial value of §5.3.4. sha384_call, for messages below 2^61 bytes.
sha512_256 The SHA-512 family The 32-byte digest of §6.7. sha512_256_call, for messages below 2^61 bytes.
sha512_224 The SHA-512 family The 28-byte digest of §6.6, in four words whose last four bytes are zero. sha512_224_call, for messages below 2^61 bytes.
hmacSha256 HMAC The 32-byte MAC of FIPS 198-1 with SHA-256. The program forms K_0 as one block, hashes the key block and the message without copying them, and hashes the outer message as two blocks. hmacSha256_call, from hmacSha256_spec, for keys below 2^61 bytes and messages below 2^61 - 64 bytes.
hmacSha512 HMAC The 64-byte MAC of FIPS 198-1 with SHA-512, formed in the same way with blocks of 128 bytes. hmacSha512_call, from hmacSha512_spec, for keys below 2^61 bytes and messages below 2^61 - 128 bytes.
sha3_224, sha3_256, sha3_384, sha3_512 SHA-3 The digests of FIPS 202 §6.1. The program holds the state in 25 lanes, XORs message words into lanes without a byte swap, and reads the padded message in place. sha3_256_call and its companions, from sha3_256_spec, for messages below 2^61 bytes.
shake128, shake256 SHA-3 The outputs of FIPS 202 §6.2 to d bytes, in an array of ⌈d/8⌉ words that the squeeze fills in place. shake128_call and shake256_call, from shake128_spec, for messages and outputs below 2^61 bytes, with room for one block of ⌈d/8⌉ words.
crc32, crc32c CRC-32 and CRC-32C The CRCs of ITU-T V.42 and RFC 3720. The program holds the remainder in the low 32 bits of a word and reads one entry of a 256-word table for each byte. crc32_call and crc32c_call, from crc32_spec, for messages of any length.
crc32Update, crc32cUpdate CRC-32 and CRC-32C The CRC of earlier bytes followed by the message, from the CRC of the earlier bytes, as zlib's crc32(crc, buf, len) computes it. crc32Update_call and crc32cUpdate_call, from crc32Update_spec, for messages of any length and the CRC of any bytes.
siphash24, siphash13 SipHash SipHash-2-4 and SipHash-1-3 of a 128-bit key given as two words. The program reads the message words in place and forms the last word from the remaining bytes and n mod 256. siphash24_call and siphash13_call, from siphash24_spec, for messages of any length.
xxh64 XXH64 XXH64 with a 64-bit seed. The program reads the stripes, the lanes of 8 bytes, the lane of 4 bytes, and the single bytes in place. xxh64_call, from xxh64_eq, for messages of any length.

12. Regular expressions

The regex guide describes the pattern and the input: a regular expression over bytes in postfix order, one word for each operator and five for each set of bytes, and an input of n bytes packed eight to a word. The specification defines the language of an expression with Mathlib's Language and proves it equal to the language of Mathlib's RegularExpression. Glushkov's theorem relates the language to the position automaton. The call theorem states that, for every pattern of pn words with 3 pn < 2^64 and every input, the export returns the specification's code without a trap in a heap with room for 24 pn + 21,272 bytes, and the file theorems identify the emitted module.

Algorithm Implementation Behavior Proved results and limits
matchWith Regular expressions Builds the position automaton of the pattern in one pass over its words, with each state a set of at most 63 positions in one word, and runs it over the input with nine table reads per byte. matchWith_call, from matchWith_eq: 2 for a pattern that does not decode, 3 for one of more than 63 sets, and otherwise 1 or 0 for whether the whole input is in the language.

13. WASI stream operations

LeanExe.Wasi provides native action descriptions and an interpreter. verified_compile_wasi compiles accepted actions to core WebAssembly with three Preview 1 imports. Its exported-entry proofs preserve the native result or terminal outcome, committed world, and joint ordered trace under the host, representation, ownership, and scratch premises. Conditional total execution requires a typed resource-prefix bound and assumptions about reached host operations. Each compiled read or write makes at most one WASI import call, which the host may implement with several operating-system calls. The WASI manual gives the exact API and proof scope.

Algorithm Implementation Behavior Proved results and limits
readSome Stdin action Requests at most a UInt64 capacity from stdin. Every valid request, including zero capacity, calls fd_read once after any required allocation succeeds. Capacity at least 2^32 returns errno 61 without I/O. Error returns empty bytes. Read-wrapper correctness proves exact successful bytes, owned results, cleanup after error or empty success, and preserved caller regions outside scratch. Committed input effects on error remain in the trace and world.
writeStdoutSome Stdout action Calls fd_write once for stdout. Success returns the transferred count, possibly short or zero. Error returns errno and count zero. Write-wrapper correctness proves the source transfer and preservation of borrowed bytes and caller regions outside scratch. Count zero on error supplies no zero-progress guarantee.
writeStderrSome Stderr action Calls fd_write once for stderr, with the same short-transfer and errno rules. Write-wrapper correctness covers descriptor 2. A shared event journal preserves order with stdout, including hosts where both refer to the same destination.
exit Terminal action Requests exit with the low 32 bits of a UInt64 status. No continuation executes. Exit correctness distinguishes accepted exit with its recorded status from rejected exit as a host trap. Both preserve prior I/O. The manual states Wasmtime 44's accepted status range.
LeanExe.Wasi.loop Bounded effectful loop Carries state through at most a UInt64 count of effectful steps, with a pure early-stop test and UInt64 index. Exit or trap terminates the action. Loop correctness and cost-aware loop correctness preserve state, ordered effects, ownership, and resource-prefix bounds.
LeanExe.Wasi.Process Unbounded process Executes bounded action steps until a returned control flag stops the process, an exit occurs, or the host traps. Compiled process refinement preserves completed steps and pending effects for every target run that completes without exhausting Talos fuel. The total-process theorem proves accepted exit under an application-supplied well-founded progress relation, a charge for the cost of each step with room for the copies of the state before and after it, and final-exit acceptance.
Action.runStdio Native stream interpreter Runs actions against Lean's stdio. Writes flush and report full count on success. Exit returns an outcome to Lean. Stream errors propagate as IO.Error. Native interpreter cases test this adapter policy. OS-stream behavior and adapter conformance to the formal host assumptions remain outside the compiler theorem.

14. Applications

Application definitions and proofs live in Demos, with shared algorithms imported from Library. The linked guides state the domains, execution premises, and host assumptions. GPU theorems concern the modeled device and host commands. Execution tests cover the host processes, file I/O, engines, and device arithmetic described in the guides.

Algorithm Implementation Behavior Proved results and limits
Euler solvers Euler application and proofs The finite-volume solvers use Rusanov fluxes for the two-dimensional Euler equations, with minmod reconstruction in the second solver. Execution and total execution within 1,407 pages for the LeanExe module under its fresh-store and cap premises. The solver proofs establish admissibility, hyperbolicity, conservation with rounding residuals, flux and update error bounds, and a reconstructed CFL bound. The verified compilation computes the same solvers under its generated bounds. Convergence to a continuous solution remains open.
Binary64 GPT-2 Binary64 model and proofs Computes full-sequence inference and cached generation with layer normalization, causal attention, an MLP, and top-k sampling using SplitMix64. The byte theorem proves execution of the Lean model. forward_causal proves causality, steps_exact proves bit-for-bit equivalence of cached steps and full inference, and the generation proof composes the host's calls. The verified compilation adds generated allocation and trap-free theorems under their bounds.
Binary32 GPT-2 Binary32 model and proofs Runs thirteen kernels for a cached generation step, compiled to Wasm and WGSL, with a modeled host program. The dispatch proofs and generate_host prove the native step's scores and race-free dispatch under strict binary32 device semantics and shape, buffer, and token bounds. The verified compilation proves Wasm execution and supplies the proved WGSL path. Its host theorem reuses the application proof.
Drone planner Drone application and proofs Uses dynamic programming over station altitudes and speeds to minimize duration, then excess altitude. The byte theorems prove optimality and safety in the ideal point-mass model for valid terrain. Total execution uses at most 70 pages under its initial-allocator and cap premises. The verified compilation transports the safety and optimality results and proves trap-free execution under its bounds.
Order book Order-book application and proofs Inserts and cancels levels, fills market orders, computes depth, and processes three-word commands over word arrays. The byte and command-stream theorems prove the fifteen functions' execution, equivalence when a chunk boundary falls between commands, and equality of the books returned by runOut and runCommands. The verified version has its own typed definitions and command-stream proofs, using the shared command lemmas.
Running sum Decimal stream application Reads signed decimal integers through EOF, prints each cumulative total, and handles split lines, CRLF, and short writes. The integer and byte theorems prove canonical decimal output for each prefix sum before the first line that is not a decimal integer, and eventual accepted exit with status 0 when every line is one and 28 otherwise. Premises include stream-host progress, line and prefix-sum size bounds, limits L and D on the bytes of each line and the digits of each total such that 220 · (L + D) + 1,010,000 bytes fit in the memory cap above the literal pool, and final-exit acceptance.
Floating-point running sum Binary64 stream application Parses binary64 values through EOF, adds each to a total starting at positive zero, and prints each total in scientific notation. Input supports decimal and hexadecimal floats, infinities, NaNs, and CRLF. The arithmetic proof connects parsing, sequential IEEE-754 addition, and printing. The compiled and byte theorems require fewer than 2^32 bytes per line. They prove cumulative output before the first line that denotes no number and eventual accepted exit with status 0 or 28. Premises include host progress, a limit L on the bytes of each line up to and including the first line that denotes no number such that 80 · L + 64,031,000 bytes fit in the memory cap above the heap's start, and final-exit acceptance.
Slew planner Slew application and proofs Finds, with Dijkstra's algorithm, the sequence of rest-to-rest eigenaxis rotations from a start attitude to a goal attitude through waypoint attitudes that keeps body vectors outside keep-out cones and inside keep-in cones and has the least total duration in whole milliseconds among the walks of the graph that its checks define, or returns a status for no path, an invalid input, or a start or goal that violates a cone. plan_safe proves that every output of status 1, which only an input that passes validInput can give, starts and ends at the input's attitudes and that every attitude within 1e-9 of each commanded rotation keeps every cone. plan_premise carries this to a flown slew whose attitude stays within angle ε of the commanded one, for cones whose true axes lie within angle d of the input axes and whose input half-angles differ from the true half-angles by at least ε + d toward the safe side. plan_optimal proves, when the start and goal also pass the static check, that status 1 holds exactly when the graph that the program's checks define has a walk to the goal, and that the plan is a least-cost walk of that graph. These three theorems concern plan in Lean, and compiled.plan.implements carries them to the module's outputs. plan_finite proves, for every input that passes validInput, every floating-point value of the evaluation in Lean finite, except inside the library's atan2 and atan, and states nothing about the module's instructions. plan_bound and slew_trapFree prove trap-free execution when top can rise by 68,020,488 bytes within the memory's cap, and the file theorems state that slew.wasm holds the module. The motion model is rest-to-rest rotation about a fixed axis with exact real rotations, and optimality covers only the edges that the conservative edge check accepts, with the program's costs.

15. Compiler examples

These algorithms remain in Examples or Verified/Examples as demonstrations of language forms, ownership, and proof procedures. Execution theorems relate compiled programs to their Lean definitions under the compiler's premises. Word arithmetic wraps modulo 2^64. The WGSL dispatch results assume the device model's shape, buffer, and invocation bounds.

Algorithm Implementation Behavior Proved results and limits
Fixed-table lookup The lookup example Returns the first matching value among ten key-value pairs encoded after a query in 21 words. A miss or another input length gives [0, 0]. lookup_bytes proves equality with the independent specification.
Fixed-tree lookup The tree-lookup example Traverses a seven-node tree in a 15-word array through three levels. A miss or another input length gives [0, 0]. treeLookup_bytes proves equality with the specified traversal.
Bounded filtering The below-100 example Keeps words below 100 in their original order for an input of at most eight words. Longer inputs give an empty array. below100_bytes proves equality with the filtering specification.
Bounded increment The increment example Adds one to each word for an input of at most eight words. Longer inputs give an empty array. increment_bytes proves the specification. increment_total proves trap-free execution under the stated 16-page memory premises.
First-zero removal The removal example Removes the first zero from at most eight words while preserving the other words' order. An input without a zero is unchanged, and a longer input gives an empty array. removeZero_bytes proves the independent specification.
Byte identity The packed-byte examples Moves the input buffer to the result. compiled.identity.implements and compiled.bytes prove execution, owned results, and heap preservation.
Byte duplication The packed-byte examples Returns two independently owned copies of the byte value. compiled.duplicate.implements and compiled.bytes, with disjoint result allocations.
Byte selection The packed-byte examples Returns the selected buffer and releases the other. compiled.choose.implements and compiled.bytes.
Byte cleanup The packed-byte examples Returns 7 after consuming the input buffer and discarding an intermediate byte result. compiled.discard.implements and compiled.bytes. Execution cases check allocated-empty cleanup.
Byte swapping The packed-byte examples Returns two input buffers in reverse order. compiled.swap.implements and compiled.bytes, with owned results.
Empty bytes The packed-byte examples Returns a null root and length zero without allocating. compiled.emptyBuffer.implements and compiled.bytes.
Byte length The packed-byte examples Returns the buffer's length as a UInt64. compiled.readSize.implements and compiled.ownedSize.implements prove execution and cleanup of an owned input.
Byte indexing The packed-byte examples Returns the indexed byte as a UInt64, or zero past the end. compiled.readByte.implements, compiled.ownedByte.implements, and compiled.bytes. Execution cases cover 255, empty input, and the maximum UInt64 index.
Byte construction The packed-byte examples Builds a packed buffer from the low eight bits of a UInt64 callback at each index. compiled.buildPattern.implements, compiled.copyByBuild.implements, compiled.nestedBuild.implements, and compiled.bytes. The construction proof covers zero count, checked narrowing, allocation, nested callbacks, and capture cleanup.
Byte literals The byte-literal examples Copies a deduplicated static byte sequence into a fresh owned buffer at each evaluation. Empty literals allocate nothing. Literal-copy correctness and the examples' generated execution theorems cover nested pure helpers, callbacks, branches, loops, and guarded recursion under static-pool premises.
Scalar axpy The binary64 arithmetic example Computes a * x + y with separate multiplication and addition. axpy_bytes proves bit-for-bit execution.
hypot The binary64 compiler examples Computes sqrt (x * x + y * y) / s. Generated compiler correctness. The sum of squares can overflow even when the exact result is finite.
newtonSqrt The bounded-repeat compiler examples Starts from a and applies x ↦ (x + a/x)/2 while 10^-12 a < |x² - a|, for at most 64 steps. Generated compiler correctness. A numerical-error bound remains future work.
scaleByPower The binary64 compiler examples Multiplies by 2^k, built from the binary64 exponent field, for 0 ≤ k ≤ 1023. Generated compiler correctness for the word-and-float definition.
Mean of indices The binary64 compiler examples Computes (0 + 1 + ⋯ + (n - 1))/n in binary64, with NaN for n = 0. Generated compiler correctness. A numerical-error bound remains future work.
harmonic The binary64 compiler examples Accumulates 1/1 + 1/2 + ⋯ + 1/n left to right. The binary64 denominator stops increasing at 2^53. Generated compiler correctness. A numerical-error bound remains future work.
fall The bounded-repeat compiler examples Advances a falling body by explicit Euler steps under gravity while height is positive, for at most 100,000 steps. Generated compiler correctness for the rounded update.
Histogram bucket The bucket example Computes ((x - lo) / width).toUInt64 with Lean's saturating conversion. bucket_bytes proves execution.
axpy32 The binary32 arithmetic example Computes a * x + y with separate binary32 multiplication and addition. axpy32_implements and binary32_bytes.
hypot32 The binary32 arithmetic example Computes sqrt (x * x + y * y) in binary32. hypot32_implements and binary32_bytes.
ratio32 The binary32 arithmetic example Computes (a - b) / c in binary32. ratio32_implements and binary32_bytes.
piecewise32 The binary32 arithmetic example Selects a binary32 expression from comparisons with lo and hi, using negation, absolute value, min, and max. piecewise32_implements and binary32_bytes.
condMix32 The conditional binary32 kernel For x[i] < lo, returns its group-of-four mirror when that index is below n, and max lo x[i] otherwise. For remaining inputs, returns hi when hi ≤ x[i], and max lo x[i] otherwise. condMixKernel_dispatch proves the modeled GPU result and race freedom. A WebAssembly execution theorem remains open.
WGSL scale The verified kernel examples Multiplies each binary32 array element by a gain. Generated Wasm correctness and scale_dispatch: the native result and race-free modeled dispatch.
WGSL branchSum The verified kernel examples Builds n outputs. Below limit, each output multiplies the input by the left-to-right sum of the first limit inputs. Other outputs negate the input. Generated Wasm correctness and branch_dispatch: the native result and race-free modeled dispatch.
WGSL flags The verified kernel examples Builds n Boolean values, inverting each input when requested. Missing values read as false. Generated Wasm correctness and the proved WGSL lowering.
WGSL wordScan The verified kernel examples Starts output i from input i, then applies acc ↦ 3 * acc + xs[j] for 0 ≤ j < i % 4. Generated Wasm correctness and the proved WGSL lowering.
WGSL roundRoot The verified kernel examples Rounds each binary32 input to the nearest-even integer, then takes its square root. Generated Wasm correctness and the proved WGSL lowering.
triangle The counted-loop compiler examples Sums the words 0 through n - 1. Generated compiler correctness.
fib The counted-loop compiler examples Advances a Fibonacci pair from (0, 1) for n iterations and returns its first word. Generated compiler correctness.
power The counted-loop compiler examples Multiplies an accumulator by x for n iterations, starting from one. Generated compiler correctness.
sumPowers The counted-loop compiler examples Sums x^i for 0 ≤ i < n, using the counted-loop power function. Generated compiler correctness.
fibPair The recursion compiler examples Advances a supplied Fibonacci pair by a specified number of steps. Generated compiler correctness, with this example's guarded recursion.
collatz The counted-loop compiler examples Applies the word Collatz map a specified number of times. Generated compiler correctness.
collatzSteps The bounded-repeat compiler examples Counts word Collatz steps while the state exceeds one, stopping after at most 1,000 steps. Generated compiler correctness.

The LeanExe worked examples and the verified compiler examples index further language and ownership examples: scalar tuples and sums, records, arrays, calls, module composition, lists, and recursive types.