PolyXOR128

A keyed 128-bit universal hash function written in Rust by Orson Peters (GitHub orlp), aimed at fast, keyed integrity checking of files and data streams. It is not built for general-purpose public checksums. zlib license, single-commit repository as read on 2026-09-28. Came in via Telegram from Lucsw. Read from the repository README; the detailed construction is in design.md, not fetched.

What it is for, and what it is not

The stated target is CRC-style integrity checking where the threat is corruption, not an adversary who doesn't know the key: "suitable for CRC-style integrity checks where malicious tampering is not a concern." Used bare, it is not a drop-in replacement for a collision-resistant hash on a public checksum (a package manifest, say). A universal hash's security guarantee depends on the key staying secret, and an observed hash value can leak information about that key. For the adversarial, untrusted-channel case the repository ships finalize_mac, which derives an AES-based MAC from the hash value that is safe to publish. Both the hash and the MAC need the key to stay secret; the raw hash and the MAC serve different threat models, not one upgrading the other.

Construction

Input is processed in 128-byte blocks. Key material is combined into each block, which is split into four parts; a parity-check code produces a fifth part, bringing the working data to 160 bytes. Each of the five parts is hashed with a carryless-multiplication variant of NH, described as similar to CLHASH, and the five results are XOR-accumulated, all in SIMD. Carryless multiplication is polynomial multiplication over GF(2)[x], so this is the same field-size move binary-fields already tracks in this spoke's proof-system corpus, applied here to hashing instead of polynomial commitment. Once the precomputed 4 KiB key buffer is exhausted, the five running hashes are recombined into two (which together carry a claimed combined 2⁻¹²⁸ collision probability) and absorbed into a polynomial hash. Each 128-byte block costs ten 64×64→128-bit carryless multiplies. See universal-hash for the family this belongs to.

The proven bound, and what "proven" covers here

Under the precondition that the key is random and independent of the input, the README states a collision bound for two inputs of up to n bytes: Pr[collision] ≤ (n/4096 + 3) / 2¹²⁸. The bound is formalized and proved in Lean, in the repository's proofs directory.

The proof's provenance is stated by the author and worth recording precisely. LLMs wrote the Lean universality proofs, plus some benchmarking/plotting code and the SIMD diagram; the author wrote the rest of the code and prose. The author's own check was narrower than "the proof is correct": they confirmed the Lean definitions match the Rust implementation and checked the final security-claim statements. They write that they have not checked the proof steps connecting the two, only that Lean's kernel accepts the proof and that it rests on no hidden axioms. So what is verified is that some Lean proof of the stated theorem exists and type-checks against stated definitions the author read; the reasoning inside it is unaudited by a human. The proof also does not cover side channels or implementation bugs.

Performance claims (self-reported, flag per this spoke's standing caveat)

Peak throughput reported: up to 130 GB/s on a Ryzen 9950X (AVX-512; _mm512_clmulepi64_epi128 issues once per two cycles doing four multiplies each, a theoretical ceiling of 25.6 bytes/cycle the implementation is said to nearly reach) and 60 GB/s on an Apple M2 Pro; an Intel Xeon 8488C was also tested, with throughput dropping past 2 MiB once the working set exceeds L2 cache. Method: single- threaded, Rust 1.98.1 stable, RUSTFLAGS="-C target-cpu=native", a ~0.1 s warm-up then the best of five ~0.1 s runs, against popular crates.io implementations of competing hashes. The author states the test data was aligned and power-of-two sized, calling that a favorable case, and claims this is the fastest 128-bit hash they know of. None of this is independently measured. This spoke's standing caveat about self-reported, author-chosen benchmarks (../CLAUDE.md → Standing caveats) applies exactly as it does to binius and flock.

No third-party cryptanalysis exists yet. The README says so directly: "Do not use it if security is paramount."

Requirements

Needs hardware-accelerated carryless multiplication; the portable fallback is, in the author's words, "unusably slow," which the README flags as likely ruling out embedded devices. The crate dispatches at runtime to x86-64 or AArch64 SIMD paths without requiring compile-time feature flags. About 5 KB of memory per key-expanded instance. Small inputs are zero-padded up to 128 bytes and are not optimized; the README flags this as something a future breaking release might change.

Lineage

The README credits universal hashing generally to Carter and Wegman, and the specific technique lineage to Krovetz, Rogaway (NH, UMAC family), Thorup, Bernstein, Lemire, Dietzfelbinger, Appleby, Apple, Nandi, Ghosh and Ahle. It is not the author's first universal hash: polymur-hash, an earlier, unproven C implementation by the same author, is a pinned repository on their GitHub profile. PolyXOR128 is not described as a successor or replacement for it in anything read here.

Cross-spoke context

The construction runs on hardware carryless-multiplication instructions and SIMD XOR-accumulation, instruction-level integer technique that ../bit-manipulation-wiki owns per this spoke's scope boundary. Routed here because the load-bearing content is the scheme (a keyed universal hash with a machine-checked collision bound and a MAC construction on top), not the instruction usage. ../bit-manipulation-wiki was logged as a runner-up at the hub and gets no page from this ingest.

Tiering

T1 — the page's load-bearing claim is what the construction is and what it provably bounds, an artifact fact checkable against the repository and the Lean proof's existence, per ../QUALITY.md → "tier by the claim, not the URL." The throughput figures are the maker's self-run benchmark and are flagged above rather than folded into the grade; so is the caveat that the Lean proof's internal steps are author-unaudited.

universal-hash · binary-fields · orson-peters · concrete-efficiency