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. 83.27 is the conservative collision-bound label (exactly 83.2678325743); the source theorem gives stronger bounds on the retained stack-safe domain. 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.