bitrep

Any order. Any hardware. Same bits.

Order-invariant, bit-identical floating-point reductions for Rust, JavaScript, and Python — exact sums, dot products, statistics, and reproducible quantiles whose results (and whole accumulator state) are byte-identical regardless of summation order, thread count, shard split, batch size, SIMD width, or CPU architecture. Sign a total, a pooled regression, or a p99 and it verifies on every machine.

The badge is the claim: CI computes golden test vectors on x86-64 Linux, ARM64 macOS, x86-64 Windows and wasm32, and asserts one SHA-256 across all of them, over multiple permutations and shardings, on every commit.

Try it in your browser — the same crate, compiled to wasm, reproduces the CI-pinned hash on your device, live; then shuffle the data, shard it, and merge accumulator states across two of your devices. Your machine is the fifth architecture in the proof.

Install

cargo add bitrep       # Rust      →  https://crates.io/crates/bitrep
npm  install bitrep    # JS / wasm →  https://www.npmjs.com/package/bitrep
pip  install bitrep    # Python    →  https://pypi.org/project/bitrep/

One Rust engine backs all three: the JavaScript package is the crate compiled to WebAssembly, the Python package is a native PyO3 extension. The full API — exact sums and dot products, convergent statistics, covariance matrices, histograms, reproducible quantiles (RelSketch), receipts, and the CRDT layer — is available in every language, and a receipt hashed in Python matches one hashed in JavaScript byte-for-byte. Binding sources are in bindings/.

Why

Floating-point addition isn't associative, so the order of a reduction changes the answer. Parallelism, SIMD, sharding and batch size all change the order. That's why your replicas drift, your temperature-0 LLM gives different answers under load, your distributed aggregates won't hash the same twice, and your lockstep game desyncs across platforms.

fp64 fixes your decisions — more precision makes the wrong bits smaller. It can't fix your hashes — if you sign, hash, replicate or compare results, "smaller error" is still a different byte string.

bitrep accumulates floats into a fixed-point superaccumulator (a 2176-bit integer in units of 2⁻¹⁰⁷⁴) that holds every finite f64 exactly. Integer addition is associative and commutative, so the state is order-invariant by construction — not by kernel discipline. One correct rounding happens at the end (nearest, ties-to-even).

Named limit — capacity: the 78 bits of headroom above the f64 range hold at least 2⁶³ additions of the largest finite f64 (and far more for typical magnitudes) before the fixed-point integer could overflow — a bound that is unreachable in practice (centuries at a billion adds/sec) and applies across merges, since merging sums the limbs. The value count is a separate u64 used only for mean/variance denominators; it saturates rather than wraps and never affects the exact sum.

The distributed contract

Accumulators merge and serialize. Sum shards on different machines, ship the 289-byte states anywhere, merge in any order — the bytes come out identical, and the value is the exactly rounded sum of everything:

use bitrep::SumF64;

let data = [0.5_f64, 1e100, -1e100, 0.25, 0.125, -0.875, 1e-300];

let sequential: SumF64 = data.iter().copied().collect();

let (a, b) = data.split_at(3);              // "two machines"
let mut left: SumF64  = a.iter().copied().collect();
let right:    SumF64  = b.iter().copied().collect();
left.merge(&right);                          // any merge tree, any order

assert_eq!(sequential.to_bytes(), left.to_bytes());   // identical state
assert_eq!(sequential.value(), 1e-300);               // exactly rounded
// naive summation returns 0.0 here — the 1e-300 is annihilated by 1e100

Also in the box:

• SumF32 — exact f32 sums, rounded once from the exact state (immune to the classic double-rounding-through-f64 trap; there's a test that proves the trap on your machine, then dodges it).
• DotF64 — exact, order-invariant dot products via FMA two-products. Named limit: partial products that underflow below the normal range lose exactness — this is detected per pair and reported (is_exact() / try_value()), never silent.
• serde (optional feature) — accumulators serialize as their canonical bytes in any format.
• no_std — sums work without std (dot needs std for mul_add).
• A language-neutral format — FORMAT.md specifies the 289-byte state; a pure-Python reference implementation in conformance/ reproduces the Rust crate byte-for-byte from that spec alone. Shard in Python, merge in Rust, verify anywhere.
• #![forbid(unsafe_code)], zero runtime dependencies.

What this makes possible

Everything below is blocked by the same missing property — float addition whose state survives reordering — and unlocked once you have it. The first four are demonstrated by runnable constructions in this repo; the rest are what the v0.2 stats toolkit turns from "trust me" into "check me".

• Float counter CRDTs — counter CRDTs have been integer-only for fifteen years; the CRDT section gives the recipe and float_gcounter tortures it.
• Floats in replicated state machines — replicas that route aggregates through an accumulator compute identical bytes; the float ban becomes selective instead of total.
• Authenticated float aggregates — Merkle trees over exact sums: signed totals with O(log n) verifiable updates (merkle_sum_tree).
• Worker-count-invariant gradient aggregation — the same model bytes from any number of workers (deterministic_training).
• Numeric aggregates for local-first apps — the CRDT ecosystem (Automerge, Yjs, ElectricSQL, Ditto) has counters and text but no exact numeric aggregation, because float sums don't converge. MomentsF64 / CovF64 do: offline replicas accumulate, sync in any order, and every device shows the same mean, variance and regression — see convergent_stats.
• Replicated / streaming database aggregates — SUM, AVG, VAR, STDDEV, COVAR, CORR, REGR_* as mergeable states, keyed by group (ConvergentMap = GROUP BY) or window. With PnMomentsF64's exact retraction, insert-then-delete returns the reads to byte-identical values — so backfills and reprocessing stop changing answers.
• Signable statistics — every state hashes canonically (state_hash), so an SLO report, a risk number, or a pooled regression becomes a receipt: recompute it from the inputs and the hash matches, or a contribution was dropped, duplicated or altered.
• Federated analytics — sites share ~500-byte states instead of raw data and merge to exact pooled mean / variance / covariance / regression. (Auditability, not privacy — compose with DP / secure-aggregation where privacy is required.)

Who this is for

Each of these is a real, documented pain — and each was blocked by the same missing property: float addition whose state survives reordering.

• Replicated state machines. Replicas that carry float state drift when reduction order differs across nodes; deterministic-simulation-testing shops famously ban floats for exactly this reason. Order-invariant reductions make float aggregates safe to replicate: every replica computes the same bytes, and a hash comparison proves it.
• Distributed aggregation. Parallel frameworks sum partitions in whatever order execution delivers them, so the same job on the same data returns different answers run to run — a documented Spark example computes an integral that should be 0 and gets anything from −8192 to +12288. Sum a billion numbers on a hundred workers and merge the 289-byte states in whatever order they arrive — retries, stragglers and rebalancing stop mattering. The combined result is exact and identical no matter how the work was split.
• Anything you sign, hash, or audit. "This total came from these inputs — verify it yourself" only works if recomputation is bit-identical. bitrep gives float pipelines the property that makes signatures and content-addressing meaningful.
• Reproducible ML and science. Batch size, thread count and hardware change reduction order, which is why temperature-0 LLMs answer differently under load. Batch-invariant kernels pin the order; bitrep removes the order from the equation entirely for the reductions you route through it.
• Lockstep and rollback netcode. Cross-platform float determinism has been a two-decade pain in game networking. A deterministic reduction for scores, physics aggregates and state checksums removes a whole class of desyncs.
• Regulated computation. When an auditor asks "prove this number," an exact, replayable, byte-stable aggregation is the difference between an argument and a receipt.

What it costs (honest, measured numbers)

Exactness is not free — but it's cheaper than its reputation. Measured with criterion on x86-64 (mixed magnitudes across ~12 decades; medians; run cargo bench for your hardware). The xsum crate (Neal's superaccumulator, also exact) is included because it's the honest comparison, fed through its fast path (add_list, size-recommended variant):

n	naive	Kahan	xsum	bitrep	vs naive	vs Kahan	vs xsum
1,000	368 ns	1.58 µs	1.52 µs	1.82 µs	4.9×	1.2×	1.2×
100,000	40.8 µs	163 µs	137 µs	395 µs	9.7×	2.4×	2.9×
1,000,000	409 µs	1.65 ms	1.36 ms	4.20 ms	10.3×	2.5×	3.1×
merge 100 shards of 10k	—	—	—	1.35 µs total	shard-combining is effectively free

Read the xsum column honestly: for raw single-machine exact sums at large n, xsum is ~3× faster — if that's your whole problem, use xsum. bitrep's price buys the properties xsum doesn't offer: a mergeable, serializable, canonically-encoded accumulator state (the distributed contract above), exact f32 and dot products, and the cross-architecture proof harness. Against Kahan — the compensated summation people already pay for accuracy alone — bitrep is ~1.2–2.5× and is exact, order-invariant, and mergeable. Use it where bits matter — replicated state, signed or hashed outputs, cross-machine aggregation, ill-conditioned sums — not in your inner render loop.

v0.2 adds FastSumF64, a streaming front-end using Neal's small-accumulator technique (the same algorithm family as xsum) that finishes into the same canonical bytes — verified differentially against the direct path on every test run. Measured: ~800 Melem/s at n=1k (xsum-parity+) and ~370 Melem/s at n≥100k (+45% over SumF64::add; xsum's large-n variant remains ~2× faster there — its radix-by-exponent batching is future work). And because merge order is free, parallel exact summation scales with zero determinism caveats: examples/parallel_sum.rs measures ~1.2 Gelem/s on four threads — byte-identical for every thread count, which no naive parallel sum can say.

bitrep as a CRDT building block

Integer counters have had conflict-free replicated types (G-Counter, PN-Counter) for fifteen years. Float sums never did, because the construction requires merge to be commutative and associative — and float addition is neither. bitrep restores exactly those two properties (machine-checked in Kani, proved at the model level in Lean), which makes an exact float counter CRDT the standard recipe:

• each replica keeps its own accumulator and only ever adds to it (append-only, so a replica's states are totally ordered by count);
• the replicated object is a map replica-id -> accumulator state, merged per-entry by highest count wins (idempotent, monotone — a join);
• the value anyone reads is the merge of all entries — exact, order-invariant, and byte-identical on every converged replica.

Stated honestly: SumF64::merge alone is not idempotent (merging the same shard twice double-counts, like adding any counter twice) — deduplication is the map layer's job, same as every counter CRDT. What bitrep contributes is the part that was actually missing for floats: a deterministic, exact, commutative-associative merge, plus a canonical byte encoding so replicas can prove convergence with a hash instead of an epsilon.

The construction's convergence laws are machine-checked in proofs/FloatGCounter.lean: the count-wins join is a semilattice (commutative, associative, idempotent), folding any delivery schedule — any order, any duplicates — yields the same state, and the converged read equals the exact sum of every add that ever happened. For calibration: existing counter CRDTs are integer-valued (Redis Active-Active documents 59-bit integer counters; Akka and Riak counters are integers), and the mechanized-CRDT literature (e.g. the Isabelle/HOL framework of Gomes et al., OOPSLA'17) verifies integer counters — an exact float replicated aggregate needs exactly the merge properties float addition lacks and bitrep restores.

Convergent statistics (feature stats, v0.2)

The counter construction generalizes to a statistics algebra. Any statistic whose sufficient state is a set of exact monomial sums (Σx, Σx², Σx³, Σx⁴, Σxy) inherits the whole contract — and the read is computed from the exact integer state in big-integer arithmetic with one final round-to-nearest-even, so it is the correctly rounded value of the true statistic, bit-identical across any sharding, arrival order, or merge tree:

• [MomentsF64] — exactly rounded mean, variance (population & sample); stddev (one extra IEEE-sqrt rounding, still bit-invariant);
• [Moments4F64] — adds exactly rounded kurtosis (μ₄/μ₂² is a pure rational of the state — the n and unit factors cancel) and skewness;
• [CovF64] — exactly rounded covariance, least-squares slope, intercept, and R²; correlation via one IEEE sqrt.

Why this beats the classical art: Chan/Golub/LeVeque parallel moments (the standard since 1979) are algebraically exact but computed in floats — the bits depend on the merge tree, and the merge double-counts on re-delivery. These states are bit-invariant, honestly bounded (StatsError reports overflow/underflow of the two-product domain — never a silent wrong value), and CRDT-lawful under the same per-replica map layer (examples/convergent_stats.rs checks the laws and demonstrates a variance the textbook formula returns as negative — exactly rounded here). Every read is verified in CI against an independent big-integer oracle with a neighbor-comparison correct-rounding check (tests/stats.rs).

Named limits, stated: products must stay clear of overflow and the subnormal range (|x| ≲ 1.3e154 for squares; 3rd/4th moments narrow it further) — violations are detected and reported. Order statistics (median, quantiles) and arrival-order-dependent aggregates (EWMA) are outside this family.

The rest of the toolkit rounds out what real aggregation needs, all under one [Mergeable] trait so containers and transports are generic:

• [WeightedMomentsF64] — exactly rounded weighted mean/variance (weights travel with samples, so timestamp-derived weights stay order-invariant);
• [PnMomentsF64] — exact retraction (add/remove, PN-counter style): insert-then-delete returns reads to byte-identical values — the incremental-view-maintenance primitive;
• [CovMatrixF64] — exact covariance matrices and deterministic multiple linear regression (normal equations over exactly rounded entries; fixed-pivot solve — bit-invariant, honestly not exactly rounded);
• [ExtremaF64] — exact min/max (no_std, idempotent by nature);
• [HistogramF64] — fixed-bucket exact counts with honest quantile bounds (order statistics have no exact mergeable form — stated, not worked around);
• [ConvergentMap] — keyed states: GROUP BY, tumbling windows, per-metric fleets; [Replicated] — the lawful per-replica CRDT layer, generic over any state; [Deltas] — delta-state transport (Almeida–Shoker–Baquero style);
• state_hash (feature receipts) — the canonical 32-byte commitment for signing converged aggregates.

Reproducible quantiles (feature quantile)

Order statistics are the one aggregate outside the exact-monomial algebra: there is no exact mergeable representation of a median. The honest exact primitive is [HistogramF64]'s bucket bounds; the useful approximate one is [RelSketch], a relative-error quantile sketch whose state is exact and byte-identical even though the estimate is not.

The sketch itself is DDSketch (Masson, Rim & Lee, PVLDB 2019, arXiv:1908.10693): map a value to a bucket by its logarithm, keep integer per-bucket counts, read a quantile off the bucket boundaries with a bounded relative error alpha. What bitrep adds is the same thing it adds for sums — a canonical byte encoding so that two sketches over the same multiset, in any order, any sharding, any merge tree, on any architecture, are byte-identical and therefore state_hash-identical. A p99 you can sign, hash and content-address. To get there without breaking bit-identity, RelSketch drops DDSketch's log-based mapping — libm's log differs by an ULP across platforms, which silently reshuffles buckets — for DDSketch's own BitwiseLinearlyInterpolatedMapping: the bucket key is a pure right-shift of the IEEE-754 bits, key = bits(x) >> (52 − sub_bits), integer-only and identical on every architecture (worst-case relative error 2^-(sub_bits+1)).

Measured on a realistic web-latency stream (lognormal body + heavy Pareto tail

• periodic spikes), 2M samples, against the exact sorted quantile (tests/quantile_realdata.rs):

target alpha	guarantee	buckets	serialized	vs raw f64	worst rel-err (p50…p9999)
1%	0.0078	715	1 862 B	~8 600× smaller	0.0064
0.1%	0.00098	4 494	10 859 B	~1 470× smaller	0.0007

And on a real dataset — 6 421 HTTP response sizes from the NASA-HTTP July 1995 trace (heavy-tailed, 0 B–1.27 MB; committed under tests/data/ and freely redistributable, so this runs hermetically in CI) — every measured error stays inside the guarantee too (≤ 0.0046 at 1%, ≤ 0.00076 at 0.1%). The state is constant in N: the same few kilobytes whether you summarize a thousand requests or a trillion, and thousands of times smaller than the raw samples at scale. The delta-varint encoding (sorted keys stored as LEB128 gaps + varint counts) cut the state from a flat 16 bytes/bucket to ~2.7, roughly 6× (FORMAT.md). A hostile stream spanning every exponent can't blow memory: past a bucket cap the resolution halves deterministically — a pure function of the multiset, so byte-identity survives the collapse (only the guarantee coarsens, and it says so).

Integrates with what you already run. RelSketch's bit-shift mapping is the same family as OpenTelemetry exponential histograms / Prometheus native histograms: at scale = sub_bits they share resolution and octave alignment, so you can emit a signed RelSketch receipt alongside the histogram you already export (examples/otel_bridge.rs). Honest caveat, measured in that example: the interior mapping is not identical — RelSketch interpolates the mantissa linearly (DDSketch's choice) while OTel spaces buckets geometrically, so a value's bucket index can differ by up to ≈ 0.086·2^scale mid-octave; the two agree at power-of-two boundaries and both stay within the shared alpha, but a faithful conversion re-buckets rather than shifting indices.

When to reach for it, and when not. RelSketch is the choice when you must verify, sign or federate a percentile — a receipt that recomputes byte-identically on every replica. It is not trying to beat t-digest on tail-quantile adaptivity, or the incumbent sketches on raw throughput; it trades those for a canonical, mergeable, signable state. The estimate carries relative error up to alpha (named limit, not hidden). The merge laws are machine-checked in proofs/RelSketchMerge.lean, the format has a second-language reference (conformance/relsketch_ref.py), and the whole thing is red-teamed (tests/quantile_redteam.rs) and fuzzed.

Demos that assert

Two runnable constructions in examples/ — each is a probe that would have failed loudly if the property it rests on were weaker than claimed:

• cargo run --example float_gcounter — the counter CRDT above, tortured: 8 replicas, 300 random gossip schedules with duplicate and stale delivery, hostile values (subnormals, exact cancellations). Every replica converges byte-identically and every total equals the exactly rounded sum. The built-in contrast: re-summing the same converged entries forward vs backward in naive f64 disagreed in 184/300 schedules — exactness is load-bearing, not decorative.
• cargo run --example merkle_sum_tree — authenticated float aggregates: a Merkle tree whose nodes carry merged accumulator states, so the root commits to every leaf and the exact total. Change one leaf in a 4096-leaf total and recompute O(log n) nodes — byte-identical to a full rebuild; verify any leaf against the root with 12 hashes. Meaningless with ordinary float sums (no canonical bytes to hash); routine with bitrep.
• cargo run --release --example deterministic_training — bit-identical data-parallel training. The gradient all-reduce is a float sum whose order depends on worker count, so the "same" SGD run yields different model bytes at 1 vs 4 vs 16 workers even in pure f64 — measured here: 4 worker configurations, 4 distinct naive-f64 models, 1 identical bitrep model. Named limit: this fixes the reduction; batch-invariant worker kernels are the other half of the problem and are not claimed.

Verification

The claim is proved, checked, fuzzed, and cross-examined — each by an independent method, so no single mistake can hide:

Layer	Tool	What it establishes
Proof (math)	Lean 4 (proofs/, zero sorry, axiom-audited in CI)	Order/merge-tree/permutation invariance of exact accumulation; the rounding kernel is round-to-nearest-ties-to-even in full (half-ulp bound, minimality over every grid point, tie parity, exactness); the float-G-Counter convergence laws; and the toolkit merge algebra (proofs/ToolkitAlgebra.lean): products, per-key maps, min/max and boolean joins, saturating counters — the laws every v0.2 state instantiates; and the RelSketch quantile-sketch bucket merge (commutative, associative, empty-identity) over the pointwise count-map model (proofs/RelSketchMerge.lean)
Statement spec	Lean FRO comparator (proofs/comparator/)	Did we prove what we claim? Challenge.lean is a self-contained, human-auditable spec: every definition the statements depend on plus all 37 audited theorems restated with sorry. On every push, the comparator verifies the real proofs prove exactly those statements, use only the standard axiom base (propext / Quot.sound / Classical.choice), and replay in the Lean kernel — and CI separately asserts the solution file is byte-for-byte the five proof files. A reviewer only needs to read Challenge.lean. (Background: the Lean reference manual's Validating a Lean Proof explains the comparator approach.)
Proof (bits)	Kani / CBMC (src/kani_proofs.rs)	The Rust implementation's merges commute and associate and the codecs round-trip — for all inputs, symbolically, proven on every push (six harnesses: sum merge/codec + extrema merge laws/codec). Kani's first catch on v0.2: adversarial ExtremaF64 decodes broke merge commutativity — the decoder now rejects non-canonical states. The add-path harnesses (add commutes, exact cancellation) decompose a symbolic f64 across all 34 limbs and are beyond CBMC's practical reach (did not close in ~3h on CI), so they're kani_slow-gated for local runs; those properties are proved at the model level in Lean and exercised by the oracle tests and the fuzzer
Differential fuzzing	cargo-fuzz vs a BigInt oracle	290M+ executions hunting order variance, oracle disagreement, codec breakage. Catches so far: a real count-overflow bug (fixed), a bug in its own oracle (powi(-1067) = 1/∞ = 0 — the crate was right), and on v0.2 a length-prefix overflow in the CovMatrixF64 decoder, found in under a minute of fuzzing the new toolkit_decoders target (fixed, with the crashing input kept in-tree under fuzz/artifacts as a regression record)
Independent oracle	proptest + BigInt + a separately written IEEE reference rounding	Correct rounding on arbitrary finite inputs, subnormals and ±MAX included; f32 rounds once (no double-rounding)
Real datasets	NIST StRD NumAcc1–4; NASA-HTTP Jul 1995 response sizes (committed, hermetic); realistic web-latency	Certified means reproduced to the representational limit (LRE ≥ 14.5); RelSketch quantiles within the relative-error guarantee at p50…p9999 on heavy-tailed real and synthetic data, plus byte-identity under reordering/sharding on the real slice (tests/quantile_realdata.rs)
Cross-architecture	golden SHA-256 vectors in CI	Identical hashes on x86-64 Linux, ARM64 macOS, x86-64 Windows and wasm32, over permutations and shardings, every commit
Cross-language	FORMAT.md + pure-Python references (conformance/)	A second implementation in a second language reproduces the canonical bytes and rounded values exactly, from a spec — the accumulator (bitrep_ref.py) and the RelSketch sketch (relsketch_ref.py), both proven portable
Supply chain	cargo-deny · reproducible-build CI · signed SLSA provenance · OpenSSF Scorecard	The same thesis, applied to the build: dependencies are advisory/license/yanked-scanned on every push (deny.toml); the release libbitrep.rlib rebuilds byte-for-byte across independent build trees (CARGO_INCREMENTAL=0, --remap-path-prefix); published wheels, npm tarball and .crate carry keyless Sigstore/SLSA provenance on every tag; the repo's security posture is scored weekly
Hygiene	Miri, clippy -D warnings, rustfmt, MSRV 1.74, forbid(unsafe_code), zero runtime deps	The boring foundations

The honest division of labor: Lean proves the algorithm's mathematics, Kani checks the Rust bits, the oracle and NIST check the encoding plumbing, the golden vectors tie all of it to hardware reality, and the Python reference proves the format stands on its own. No single layer is asked to carry a claim it can't.

Prior art (stand on shoulders, cite them)

The long-accumulator idea is classic: Kulisch's accumulator, Neal's superaccumulators (see the xsum crate for a direct port), Demmel–Nguyen / ReproBLAS reproducible BLAS, and Ogita–Rump–Oishi error-free transformations. Shewchuk's adaptive arithmetic and Kahan summation solve related problems with different trade-offs. The closest database-side work is reproducible aggregation in RDBMSs (ICDE'18) — single-node GroupBy reproducibility, without a mergeable or serializable accumulator state.

What bitrep adds is the packaging for distributed systems: a mergeable, serializable, canonically-encoded accumulator state with breadth beyond sum (f32, dot), a named-limits API that refuses to be silently wrong, and a CI harness that proves bit-identity across architectures on every commit. (An exactly rounded mean() — one correct rounding of the exact sum divided by the count — is planned; means today are value()/count, one extra rounding, which is how the NIST means below are reproduced.) If you need raw single-machine exact-sum speed, xsum is ~3× faster at large n (measured above) — pick per workload.

Non-goals

Making your existing pipeline bit-reproducible (that depends on your kernels' order — see batch-invariant kernels for that approach); general arbitrary-precision arithmetic; being the fastest sum on one machine.

License

MIT or Apache-2.0, at your option.