Skip to content

thery/coqprime

Repository files navigation

Build Status

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

# n digits years discoverer checking time
17 2281 687 1952 Robinson < 1s
18 3217 969 1957 Riesel < 1s
19 4253 1281 1961 Hurwitz 2s
20 4423 1332 1961 Hurwitz 2s
21 9689 2917 1963 Gillies 10s
22 9941 2993 1963 Gillies 10s
23 11213 3376 1963 Gillies 13s
24 19937 6002 1971 Tuckerman 1m00s
25 21701 6533 1978 Noll & Nickel 1m20s
26 23209 6987 1979 Noll & Nickel 1m30s
27 44497 13395 1979 Nelson & Slowinski 8m00s
28 86243 25962 1982 David Slowinski 45m20s
29 110503 33265 1988 Walter Colquitt & Luke Welsh 1h22m20s
30 132049 39751 1983 David Slowinski 2h11m43s
31 216091 65050 1985 David Slowinski 8h27m25s

If you have a number you really want to be sure that it is prime 😄 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