coqprime

CoqPrime is a library built on top of the Coq proof system to certify primality using Pocklington certificate and Elliptic Curve Certificate. It is a nice illustration of what we can do with safe computation inside a prover. The library consists of 4 main parts:

• A library of facts from number theory: the goal was to prove the theorems relative to Pocklington certificate. The library includes some very nice theorems like Lagrange theorem, Euler-Fermat theorem. A note about some of the primality tests is available here
• A library for elliptic curves
• An efficient library to perform modular arithmetic: using the standard representation of integers in Coq was not sufficient to tackle large prime numbers so we have developed our own modular arithmetic based on tree-like structures. The library includes comparison, successor, predecessor, complement, addition, subtraction, multiplication, square, division, square root, gcd, power and modulo.
• A C program pocklington that generates Pocklington certificates (this program is based on ECM). An ocaml program o2v that turns a certificate generated by primo into Coq files. These programs are in gencertif.

Here are the benchmarks for some Mersenne numbers

If you have a number you really want to be sure that it is prime :smile: what should you do? If your number has less than 100 decimal digits:

• Download and compile the library
• Generate the certificate for your prime number. For example for 1234567891, the command pocklington 1234567891 generates the file

From Coqprime Require Import PocklingtonRefl.

Local Open Scope positive_scope.

Lemma myPrime : prime 1234567891.
Proof.
 apply (Pocklington_refl
         (Pock_certif 1234567891 2 ((3607, 1)::(2,1)::nil) 12426)
        ((Proof_certif 3607 prime3607) ::
         (Proof_certif 2 prime2) ::
          nil)).
 native_cast_no_check (refl_equal true).
Qed.

If your number has more than 100 decimal digits

• Download and compile the library

• Configure primo to generate Coq-friendly certificates :

  • Set the flag Elliptic curve tests onlyin the SetUp tab.
  • Add in the configuration file primo.ini (this file is generated after the first invocation of primo), the lines

    [Undocumented]
    SHB=FALSE
    LTM=32
    

• Use primo to generate a cerficiate file.out. Here is a certificate for 1234567890123456789012353.

PRIMO - Primality Certificate]
Version=4.3.1 - LX64
WebSite=http://www.ellipsa.eu/
Format=4
ID=B40A002B26D66
Created=Jan-16-2020 12:34:07 PM
TestCount=3
Status=Candidate certified prime

[Comments]
Certificate for 1234567890123456789012353

[Running Times (Wall-Clock)]
1stPhase=0.06s
2ndPhase=0.02s
Total=0.08s

[Running Times (Processes)]
1stPhase=0.06s
2ndPhase=0.02s
Total=0.08s

[Candidate]
File=/home/thery/soft/newprimo/work/nn.in
N=$1056E0F36A6443DE2DF81
HexadecimalSize=21
DecimalSize=25
BinarySize=81

[1]
S=$14
W=$1675F8F1ACE
A=$2
B=0
T=$3

[2]
S=$96C7B0CC0
W=$6CFE1D714A
A=0
B=$7
T=$1

[3]
S=$60FD0
W=$225406
A=0
B=$2
T=$1

[Signature]
1=$0326D77C06A10B7170DAB6DAEC0D12B7F744F88BBC7F34D5
2=$773B9CD197CA741F91B93381877FBF23E7CDCF49BFE7EF5C

• Use the command o2v to generate the file file.v. The file for 1234567890123456789012353 is the following.

From Coqprime Require Import PocklingtonRefl.
Local Open Scope positive_scope.

Lemma my_prime0:
  prime  61728394506095664626953->
  prime  1234567890123456789012353.
Proof.
intro H.
apply (Pocklington_refl
     (Ell_certif
      1234567890123456789012353
      20
      ((61728394506095664626953,1)::nil)
      2178
      0
      99
      1089)
     ((Proof_certif _ H) :: nil)).
native_cast_no_check (refl_equal true).
Time Qed.

Lemma my_prime1:
  prime  1525110266389->
  prime  61728394506095664626953.
Proof.
intro H.
apply (Pocklington_refl
     (Ell_certif
      61728394506095664626953
      40474709184
      ((1525110266389,1)::nil)
      0
      3584
      8
      64)
     ((Proof_certif _ H) :: nil)).
native_cast_no_check (refl_equal true).
Time Qed.

Lemma my_prime2:
  prime  3839029->
  prime  1525110266389.
Proof.
intro H.
apply (Pocklington_refl
     (Ell_certif
      1525110266389
      397264
      ((3839029,1)::nil)
      0
      54
      3
      9)
     ((Proof_certif _ H) :: nil)).
native_cast_no_check (refl_equal true).
Time Qed.
Lemma my_prime3 : prime 3839029.
Proof.
 apply (Pocklington_refl
         (Pock_certif 3839029 2 ((319919, 1)::(2,2)::nil) 1)
        ((Pock_certif 319919 13 ((103, 1)::(2,1)::nil) 316) ::
         (Proof_certif 103 prime103) ::
         (Proof_certif 2 prime2) ::
          nil)).
 native_cast_no_check (refl_equal true).
Qed.


Lemma  my_prime: prime 1234567890123456789012353.
Proof.
exact
(my_prime0 (my_prime1 (my_prime2 my_prime3))).
Qed.

• Compile the file with coqc

Proving the primality of a number of about 1200 decimal digits takes about 9 hours but can be easy parallelized using the -split command of o2v (for example, it takes 15m on a 20-core machime).

If you are too lazy to install the Coq system, or have no spare cpu-time, you can put your prime number in an issue, we will do the job for you.

How to install it

You can download the source and use make. There is also some opam packages : coq-coqprime for the library and coq-coqprime-generator for the certificate generator pocklington