BitVec and polynomials over GF(2)

Stream: lean4

[François G. Dorais]

There's been very consistent work on BitVec in Lean. This is fantastic but I'm afraid I haven't been able to keep up!

I'm needing to work with BitVec as coefficients of polynomials over the two element field. Is there existing/planned work in that direction? It is not hard to give a reference implementation for the few things I need, but I don't want to reinvent the wheel. It's tough to go straight with two wheels of different size!

[Kim Morrison]

I don't think there's any work in progress with the interpretation as coefficients of polynomials. What exactly are you doing?

[François G. Dorais]

For the Mersenne Twister (batteries#984) the trick to jump ahead 2^128 steps is to calculate the minimal polynomial p(x) of the twist transform, calculate x^(2^128) mod p(x) using quick exponentiation, and then evaluate the resulting polynomial using Horner's method, substituting the twist transformation for x.

PS: The polynomial p(x) has degree 19968 for the most common practical use case. So this is not something where it's easier to do with ad hoc code.

[Henrik Böving]

Are you sure that you want to implement your Mersenne twister on top of BitVec instead of UIntX btw? If you are doing all of these bitwise ops on BitVec's that always carries a performance penalty while it doesn't for UInt.

[François G. Dorais]

This is a reference implementation that allows for all possible variations of parameters. The MT19937 and MT19937-64 special cases are part of the C++11 standard, so I think we just need to link those in for efficiency.

The reason for the reference implementation is that it is not opaque and we can verify its statistical properties, eventually...

[François G. Dorais]

PS:The Philox PRNG is coming up soon. Maybe some more after that...

[François G. Dorais]

PS2: I already had UIntX versions, this is the BitVec upgrade!!!