[bgregoir]

Adds Pocklington's primality criterion with computable certificates, and uses it to prove that the Poly1305 modulus 2^130 - 5 is prime. It is a port of coqprime's Pocklington.v; names follow mathcomp where an equivalent exists.

theories/algebra/Pocklington.ec (new)

• modzXm; the multiplicative order on integers order a n with order_spec, order_gt0, expz_order, order_dvdz, order_dvd_pred;
• pdivP (an integer > 1 has a prime divisor) and primePns (characterisation of non-primes by a prime divisor p with p^2 <= n);
• pocklington: if N - 1 = F1 * R1 and, for every prime p | F1, some a satisfies a^(N-1) = 1 mod N and gcd(a^((N-1)/p) - 1, N) = 1, then every prime divisor of N is 1 mod F1; pocklington_prime concludes prime N when N < F1^2. Unlike coqprime, the combination of the prime factors of F1 goes through gcd/Gauss instead of prime powers, and there is no 1 < a hypothesis;
• computable corollary pock_certif : pock_check N c => all (fun pa => prime pa.1) c => prime N, where the certificate c lists pairs (p, a) whose p multiply to F1. Modular exponentiation (powmod) and Euclid's gcd (egcd) are given as hint simplify rules on dedicated operators, so that cbv checks a certificate.

theories/algebra/ZModP.ec: the Ring.Field clone ZModpField now uses <= substitutions, as ZModpRing already does. This keeps its type and operators as definitions, so ZModpField can be given for a field or integral-domain theory parameter, e.g. clone Poly.Poly with type coeff <- zmod, theory IDCoeff <- ZModpField. All of stdlib and examples still check.

examples/ChaChaPoly (new files)

• poly1305_prime.ec: prime_p1305 : prime (2^130 - 5), as a chain of 9 certificates checked in about 3 s;
• poly1305_field.ec: Z/(2^130 - 5) and its polynomial ring;
• poly1305_msg.ec: the RFC 8439 message polynomial (MAC input with padding and little-endian lengths, 16-byte blocks, coefficients le(b) + 2^128), its degree, and its injectivity (topol_inj) for lengths < 2^64.

No new axioms; poly1305_msg.ec is an abstract theory over a byte type, whose three axioms are the specification of the byte/int conversions. These are first steps towards replacing the Poly1305 axioms of examples/ChaChaPoly (topol_inj, pr_zeropol_spec); the root-counting bound needed next is in #1232.

[fdupress]

This would probably be best as 3 separate PRs (stacked):

1. the ZModP change;
2. Pocklington's criterion and computable primality check;
3. the finalization of the ChaCha+Poly proofs.

We can probably merge as a single PR but it would be good to have the commits rebased into the above so each is meaningful in isolation.

[fdupress]

Should this entire section move to IntDiv or a related theory on modular arithmetic without the algebra?

[bgregoir]

I am agree with you, I will do that

[fdupress]

Same, does this belong in IntDiv?

[fdupress]

Or perhaps all of the generic, but computable stuff should be in a ComputableIntDiv theory?