Primality of $2^{255}-19$

Question

I need a test for primality that I apply to $2^{255}-19$ (which is claimed to be prime) and certify to be correct with the ACL2 theorem prover. This means that I must be able to code the test in Common LISP, run it on this case in a reasonable period of time (I'd be happy if it ran in a day), and write a proof of correctness of the test that is simple enough to be mechanized in the ACL2 logic.

Answer 1

It takes my C+GMP code under 0.4s to do a BLS75 theorem 5 proof on the number, so this seems like the easiest option. This involves finding some small factors of p-1, checking conditions, then verifying primality of each factor (note you don't need to factor p-1 completely). This example has lots of small factors, and the large resulting prime minus 1 factors easily, and so does the next one, with the final value being small enough to check with deterministic M-R or BPSW.

You may be able to use one of the earlier theorems, e.g. 3, which is slightly easier. I didn't check whether it could trivially do the whole chain by itself.

Using ECPP plus n-1 and n+1 finishes in about 0.01 seconds on my laptop, but that's a lot more coding. The BLS75-T3 or -T5 would be much easier to code.

BLS75: http://www.ams.org/journals/mcom/1975-29-130/S0025-5718-1975-0384673-1/S0025-5718-1975-0384673-1.pdf

Answer 2

This very small program written in PARI/GP shows the result and the time needed for calculation. I have done this multiple times and the times the program needed, differed, but it took never longer than $200ms$. The routine certifies the primality using the adleman-pomerance-rumely-test (APR-test), which is one of the fastest known algorithms for certifying primes.

? gettime();print(isprime(2^255-19,2));gettime()
1
%1 = 110
?

Asymptotically, there must be a better algorithm because it is now known, that the decision problem : "Is a given natural number $n>1$ prime" is in $P$, that means, it can be solved in polnomial time.