# bitrep
**Any order. Any hardware. Same bits.**
Order-invariant, bit-identical floating-point reductions for **Rust, JavaScript,
and Python** — exact sums and dot products whose results (and whole accumulator *state*) are
byte-identical regardless of summation order, thread count, shard split,
batch size, SIMD width, or CPU architecture.
[](https://github.com/KyleClouthier/bitrep/actions/workflows/ci.yml)
[](https://github.com/KyleClouthier/bitrep/actions/workflows/supply-chain.yml)
[](https://securityscorecards.dev/viewer/?uri=github.com/KyleClouthier/bitrep)
[](https://codecov.io/gh/KyleClouthier/bitrep)
*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](https://simgen.dev/bitrep/)** — 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
```bash
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, 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/`](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:
```rust
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`](FORMAT.md) specifies the
289-byte state; a pure-Python reference implementation in
[`conformance/`](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](#bitrep-as-a-crdt-building-block) gives the
recipe and [`float_gcounter`](examples/float_gcounter.rs) 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`](examples/merkle_sum_tree.rs)).
* **Worker-count-invariant gradient aggregation** — the same model bytes
from any number of workers
([`deterministic_training`](examples/deterministic_training.rs)).
* **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`](examples/convergent_stats.rs).
* **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](https://arxiv.org/abs/2101.09408) 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](https://crates.io/crates/xsum)
(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 `add`s 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`](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](https://arxiv.org/abs/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`](#verification)-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`](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/`](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`](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`](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`](proofs/RelSketchMerge.lean),
the format has a second-language reference
([`conformance/relsketch_ref.py`](conformance/relsketch_ref.py)), and the whole
thing is red-teamed ([`tests/quantile_redteam.rs`](tests/quantile_redteam.rs))
and fuzzed.
## Demos that assert
Two runnable constructions in [`examples/`](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/`](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`](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`](proofs/RelSketchMerge.lean)) |
| **Statement spec** | **Lean FRO [comparator](https://github.com/leanprover/comparator)** ([`proofs/comparator/`](proofs/comparator/)) | *Did we prove what we claim?* [`Challenge.lean`](proofs/comparator/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](https://lean-lang.org/doc/reference/latest/ValidatingProofs/) explains the comparator approach.) |
| **Proof (bits)** | **Kani / CBMC** ([`src/kani_proofs.rs`](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`](fuzz/fuzz_targets/toolkit_decoders.rs) 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](https://www.itl.nist.gov/div898/strd/univ/homepage.html); [NASA-HTTP Jul 1995](https://ita.ee.lbl.gov/html/contrib/NASA-HTTP.html) 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`](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`](FORMAT.md) + pure-Python references ([`conformance/`](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](https://arxiv.org/abs/1505.05571) (see the [`xsum`
crate](https://crates.io/crates/xsum) for a direct port), Demmel–Nguyen /
[ReproBLAS](https://bebop.cs.berkeley.edu/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](https://arxiv.org/abs/1802.09883)
(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.