Comments URL: https://news.ycombinator.com/item?id=49775383

Points: 6

# Comments: 0

GNATprove uses SMT solvers, meaning it's basically a brute force proof system.

Yes, brute-force proofs are easier than symbolic proofs (lean, bend, etc.) because you don't have to supply a proof. It's all automatic.

But brute-force proofs don't scale to nearly anything of interest, which is why formal verification has been a niche field for 30 years, until now where LLM can write _actual_ proofs.

    P_i = x_{2i} + (x_{2i+1} + z^3)(P_{i-1} + z^2)

Not really. Our method is also 2x faster than xxh3.

Sure, AES make the heuristic hashes harder to break, but they still provide (1) slower performance, (2) no guarantees.

See section 5.7 and 5.8 in the paper for experiments against other hashes.

But maybe this work can inspire looking for other small, constant factor saving circuits for different classes of polynomials. Would be cool!

Do you mean hashes like xxh3? We have a section in the paper showing for a bunch of these that they collide much more often than universal hashes on bad inputs.

There is no preprocessing at hash time in either use.

Universal hashing: the message words are the parameters of the chain, a_i and b_i in P_i = a_i + (b_i + y)(P_{i−1} + u), not coefficients of a target polynomial. Distinct messages give distinct polynomials, which is all a universal hash needs; the decoder never runs. Same as Bernstein's BRW.

k-independent hashing: the key should be a uniformly random monic polynomial of degree k. Our parameterisation is a bijection onto those polynomials, with the rational preprocessing as its inverse, so uniformly random gate constants give a uniformly random polynomial. You draw the ⌊k/2⌋+1 constants and evaluate; the coefficients are never computed. That is why the paper needs bijective rather than just injective constructions, and the Section 5 speedups are for the whole hash.

Preprocessing only appears when a fixed polynomial (a Taylor approximation, a secret-sharing polynomial) is evaluated at many points, and then it runs once.

> have a separate source node for each x, x^2, x^4 used

Do you mean a graph like this R&W? https://thomasahle.com/fast-polynomials/#ex=bessel&mode=Q&me... there are nodes labeled x2, x4, x8; but it's the output of multiplications, and we want to make the number of mults visually clear.

However, in section "5.9 Injective Polynomial Hashing" we actually study the problem of universal hashing, which is a lot more like CRC8.

It takes advantage of FMA (fused multiply add), has good numeric stability and uses pipelining optimally.

A while ago I suggested using Estrin's method in Boost, for functions like std::exp. There's some interesting discussions here: https://github.com/boostorg/math/issues/924 if you are interested in all the practical details.

However, for finite fields (e.g. used for hashing and cryptography) multiplication is much more expensive than addition, which is the main use of this algorithm.

It's a very nice construction (based on Rabin & Winograd's polynomial multiplication method) for building universal hashes with n/2+O(logn) multiplications.

The annoying part is that it's a tree structure, which is not usually what you want in a fast hash that you're folding over a data stream. Some papers like https://eprint.iacr.org/2017/328.pdf try to fix this, but there are a lot of annoying trade-offs.

A famous fast hash is NH, which is just:

   H(x) = sum_i (x_{2i} + a_{2i}) * (x_{2i+1} + a_{2i+1})

Our construction (section 5.9 Injective Polynomial Hashing) shows that you can do something a bit similar with polynomials:

    P_0 = z
    P_i = x_{2i} + (x_{2i+1} + z^3)(x_{2i} + z^2)

Many "practical" hashes use heuristics instead of real field multiplications to be faster. But it means they are vulnerable to adversarial inputs. That means, it's possible to design a set of keys that have much higher probability (under random hash seeds/keys) to collide than you'd expect under a correct hash function.

We actually analyze both WyHash and xxh3 in this setting in section "Adversarial inputs for heuristic hashes" - https://arxiv.org/pdf/2609.06022#page=165

I thought in the EU the maximum interchange fee for consumer credit cards is capped at 0.3% of the transaction value.