Primality of $2^{255}-19$ 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.
 A: 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
A: 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.    
