Add primality testing

[atomb]

Many bits of public-key cryptography use integers modulo primes as their core mathematical foundation, and involve operations that are only well-defined for groups of prime order. For such operations, and even just documentation, it may be useful to have the ability to test whether numbers are prime within Cryptol. This may be especially useful at the type level, but once it's implemented we may want to expose it at the value level, too.

Some existing Haskell packages support both probabilistic and certified primality checking. The former is generally fast enough for regular use. The latter can be very slow for large primes, but is perhaps still useful sometimes.

The arithmoi package is large and complex, but does what we need. Other, simpler packages might also be available.

[brianhuffman]

gmp provides primality tests, so it seems like there ought to be a binding for primality testing for ghc's gmp-based Integer type.

[robdockins]

CF #882, which implements the primality constraint in the type system and finite field inverses.

[robdockins]

With the merge of #882, we now have a prime constraint at the type level, which asserts the primality of a numeric type, and allows Z p to inhabit the Field class for prime p. The constraint uses the probable-prime test from GMP to implement the check.

Certainly, we can expose this capability at the value level, but we should spend some time thinking about the design for this feature. Are probable prime tests enough, or do we want certified primes? If certified, do we want to produce checkable certificates? Do we also want prime sampling/generation algorithms? If so, which ones? At the moment, it isn't clear to me what is actually useful to have.

[robdockins]

I think we can remove this ticket from the 2.10 milestone, as the work on the prime constraint is done and merged, and we don't have a clear idea of what we need WRT value primitives for primality testing and generation.