Machine-checked statements
Snapshot: 19 September 2026. The statements below describe the mathematical models checked in Lean. Execution tests and compiler correctness are separate claims.
highway
exact full-key trail count 56165·2^184, unconditional state and all three output collision bounds, and score enclosure 59.807–59.808; C/Lean vectors are execution evidence, not compiler correctness.
polymur
The exact restricted-key cardinality lower bound and numerical idealHash collision/score theorems are unconditional; the shipped seed distribution and C arithmetic refinement remain outside scope.
halftimehash-64, halftimehash-128, halftimehash-256, halftimehash-512
The abstract Style construction is checked; the implementation correspondence remains partial because the universal executable/Style connection and fixed-header premises are not discharged in Lean.
umash, umash128
The earlier 46.52-bit envelope and ENH-only closure are machine-checked. The 53.38-bit refinement, 56.18-bit bound, joint PH+ENH closure and fingerprint headline are verified paper proofs; not yet machine-checked.
clhash
Ideal Algorithm-4 bound for distinct byte strings shorter than 2^64 bytes, including empty, partial and unequal-length inputs; no implementation or seed-expander theorem.
poly1305
Ideal byte-string families: explicit clamped Poly1305 keys and single-stream GHASH with uniform field key; excludes seeded samplers, AES and OpenSSL C/assembly.
ghash
Ideal byte-string families: explicit clamped Poly1305 keys and single-stream GHASH with uniform field key; excludes seeded samplers, AES and OpenSSL C/assembly.
halftime24-fixed
Independent uniform entropy words; supported V4 byte lengths <168·8·(19173960+1). Distance-3 encoder and scalar byte length as last tail word. The certified normalized score is 96 bits for every tree width, attained by the one-byte pair 00/01 (the plotted value until 28 September 2026 was the conservative 6804·2−96 label, 83.27 bits). Construction M1–M4 checked in Lean; complete C++ refinement is not claimed. Concrete fixed-header encoder/layout refinement remains partial;
chainhash
ChainHash, 64 uniformly random key bytes: collision bound (p(L)+d(L))/2^64 for distinct byte strings of at most 8L bytes, including empty, partial-word and unequal-length inputs; evaluation independence (serial = k-lane exact-count schedule = lazy state for every stride); exact score minimum 63.0. 89 theorems, standard axioms only; 464 C/Lean vectors. Compiler correctness and the benchmark seed expansion are outside scope.
chainhash128
ChainHash-128, 128 uniformly random key bytes: collision bound (p_B(L)+d_B(L))/2^128 for distinct byte strings of at most 8L bytes, including empty, partial-word and unequal-length inputs; evaluation independence for every stride; exact score minimum 127. 116 theorems, standard axioms only; 625 C/Lean vectors. Compiler correctness and the benchmark seed expansion are outside scope.
polyxor
PolyXOR128 0.1.0, Orson Peters’s Lean development rebuilt here (Lean 4.34.0, Mathlib v4.34.0). The key is 4096 uniformly random block-key bytes and three uniform field words. For distinct byte strings of at most n < 2^64 bytes, including empty, partial-block and unequal-length inputs, the collision bound is (n/4096+3)/2^128 (PolyXOR.polyxor128_axu); the compression lemma gives 2^-128 (PolyXOR.compress_axu128_is_axu). Standard axioms only, plus our non-vacuity lemmas and 1,658 model/crate vectors across five backends. The score is attained at L = 1 to within 0.001 bits: the pair 00/01 has exact probability 2^-128(3 − 2^-64 − 2^-127 + 2^-192), computed by hand, not in Lean. The AES from_key expander, the benchmark seed expansion and compiler correctness are outside scope. Sources, build and axiom audit: polyxor/.
horner
Horner / unrolled polynomial over GF(2^64): collision probability at most (L-1)/2^64 for distinct fixed-length word vectors (polynomial_collision_gf64). Sources, build and axiom audit: lean-textbook/. Standard axioms only.
brw
BRW polynomial of degree at most 2L-1 over GF(2^64); finite-domain score minimum strictly between 63 and 64, whole-bit floor 63 (BRW.collision_bound_gf64, ChartScores.brw_whole_bits). Sources, build and axiom audit: lean-textbook/. Standard axioms only.
recurrence
Injective recurrence, one chain, three independent keys: ceil(L/2)/2^64 (Recurrence.collision_bound_gf64). Sources, build and axiom audit: lean-textbook/. Standard axioms only.
lanes
Injective recurrence, eight lanes: (rounds(L)+J-1)/2^64 with J = min(8, ceil(L/2)) nonempty lanes, at most L/2^64, so the score is at least 64 (LanesRefined.word_collision_bound_refined_gf64, LanesRefined.refined_ratio); lanes empty at the common length cancel, which the earlier envelope (rounds(L)+7)/2^64 (61 bits) did not use. Sources, build and axiom audit: lean-textbook/. Standard axioms only.
nh
NH over GF(2^64): 2^-64 (nh_collision_bound). The integer NH row relies on the UMAC theorem; this file covers the field version only. Sources, build and axiom audit: lean-textbook/. Standard axioms only.
tabulation
Simple tabulation on single words: exactly 2^-64 (tabulation_collision_exact). Sources, build and axiom audit: lean-textbook/. Standard axioms only.
multiply
Vector multiply-add-shift with independent uniform 128-bit coefficients and additive key, high 64-bit output, fixed-length vectors: exactly 2^-64 (vectorMultiplyAddShift_collision_exact, vectorMultiplyAddShift64_formula_bound). The scalar multiply-shift proposition in MultiplyShift.lean is recorded, not proved. Sources, build and axiom audit: lean-textbook/. Standard axioms only.
ChainHash and ChainHash-128 attain their L = 1 certificates: the one-byte pair "\x00" / "\x01" collides with probability exactly (2q-1)/q^2, so the scores 63 and 127 are exact.