crnumerics

Floating-point results that are the same bits on every machine, with proofs anyone can rerun.

MIT licence · C, with checks against MPFR · a companion to crmvec

1e16 + 1 − 1e16 + 1, in binary64, added left to right

in the order written1.0
the two 1s first2.0
the large terms first2.0
crsum, in any order, split or thread count2.0

The exact sum is 2. Ordinary floating-point addition rounds after every step, so the order of a reduction changes its result, and a parallel reduction's order changes with the thread count. A correctly rounded sum has one answer.

Why

Correctly rounded functions give one right answer, so they agree everywhere; crmvec does that for the vector functions compilers call. But most differences between machines come from elsewhere: the order of a sum, fast approximations inside larger operations, formats with no standard math library, and tools that can't tell you where a difference comes from. The libraries here close those gaps one at a time.

What is in it

crsum

Correctly rounded sums, dot products and matrix products in binary64 and binary32, in all four rounding modes: the same bits in any order, split or thread count. crgemm_oz gives exact matrix products through any binary64 BLAS you already have (the Ozaki scheme).

For simulation, training and inference, finance: anyone who needs a reduction to come out the same twice.

crnn

sigmoid, silu, gelu, softplus and rsqrt correctly rounded in binary32, binary16 and bfloat16, and logsumexp, softmax, layernorm and rmsnorm specified bit for bit on top of crsum. Neither a rounding mode nor -ffast-math's flush-to-zero changes a result.

For inference and training that must give the same output on every machine.

crdist

The normal distribution correctly rounded in binary32, binary16 and bfloat16, every input checked against MPFR on x86-64 and aarch64: erfinv, erfcinv, probit (the quantile: R's qnorm, SciPy's ndtri), ndtr, log_ndtr (also where the probability underflows), normpdf and logit. And samplers (normal, exponential, gamma, beta, chi-squared, t, Poisson, binomial; uniform and exponential also in binary64) from a Philox stream, whose bits a written specification fixes on every machine. Linux and macOS; from Python, pip install crdistr. Neither a rounding mode nor flush-to-zero changes a result.

For sampling and statistics that must give the same draws on every machine.

crlin

Verified linear algebra: for A x = b, an enclosure of the exact solution, about an ulp wide, at about 10 times the cost of an unverified solve; or a refusal, never a wrong answer. It never switches the rounding mode, so a threaded BLAS can't break the proof. Also several right-hand sides, interval data, least squares, very ill-conditioned systems, banded and sparse systems, symmetric eigenvalues and proofs of positive definiteness. From Python, pip install crlin.

For anyone who needs a solve they can trust to the last bit.

crfix

exp, exp2, log, log2, sigmoid, tanh, sqrt, rsqrt, reciprocal, division, silu and the exact gelu on fixed-point numbers (int8, int16 or int32, uint8 and uint16, any fractional bits): each the exact value rounded once, in the mode asked for, then saturated, checked against MPFR on every 16-bit input in every format. Also exact layer normalization, int8 and uint8 lookup tables, TFLite's affine formats and softmax. Integer arithmetic only, with no floating point at all, so it gives the same bits on x86-64, aarch64, 32-bit ARM and a Cortex-M0. From Python, pip install crfix; python -m crfix table prints a lookup table as C.

For integer-only inference kernels and microcontrollers that must give the same bits everywhere.

lowp

Correctly rounded math for the OCP 8-bit formats (E4M3, E5M2) and OCP MX blocks (MXFP8, MXFP6, MXFP4, MXINT8): the 41 functions CORE-MATH has for binary16, proven on every input or correct by construction.

For low-precision machine learning, and hardware and emulator writers.

ival

The tightest binary64 interval enclosures of 32 elementary functions, and of atan2, hypot and pow on boxes. From Python, pip install crival.

For verified and interval computing.

repro-scan, repro-diff

What in a binary or a build makes its results machine-dependent; and a program run under changed conditions (threads, flush-to-zero, an older CPU) with its output compared.

For anyone chasing a result that changes between machines.

the checking kit

Number formats down to FP4, correctly rounded references through MPFR, and runs with controls and verdicts.

For building checks like these.

How it is checked

Each library is checked against answers it did not make, with controls that must fail, and with deliberately planted bugs that the checks must catch. Every check ends in one verdict line:

IDENTICAL · exit 0DIFFERS · exit 1VOID · exit 2

VOID means nothing was tested: a control did not fail, or the check could not run. CI runs every check on x86-64 and natively on arm64, the libraries' checks on macOS (Apple Silicon), and crfix on a Cortex-M0 under qemu.

Build and check

make          # the kit and every library, and their checks
make check    # every check: the kit, repro-scan, lowp, lowp's MX, ival, crsum, crnn, crdist, crlin, crfix
make install  # ival, crdist, crlin and crfix, for pkg-config

Needs gcc 13 or later (for _Float16 and __bf16), MPFR 4.2 or later, and OpenMP. repro-scan needs Python 3 and binutils.

From Python, each with its library in the wheel (x86-64 and aarch64 Linux, Apple Silicon macOS):

pip install crival crdistr crlin crfix