Welcome to CoqPrime project!

Certifying Prime Number with the Coq prover


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:
  1. 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.
  2. A library for elliptic curves
  3. 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 developped 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.
  4. A C program that generates Pocklington certificates. This program is based on ECM and some scripts that turn a certificate generated by primo into a Coq file
Here are the benchmark for some Mersenne numbers

# n digits years discoverer checking time
8 31 10 1772 Euler 0.01s
9 61 19 1883 Pervushin 0.01s
10 89 27 1911 Powers 0.02s
11 107 33 1914 Powers 0.02s
12 127 39 1876 Lucas 0.04s
13 521 157 1952 Robinson 1.85s
14 607 183 1952 Robinson 2.78s
15 1279 386 1952 Robinson 20.21s
16 2203 664 1952 Robinson 89.1s
17 2281 687 1952 Robinson 97.59s
18 3217 969 1957 Riesel 237.65s
19 4253 1281 1961 Hurwitz 494.09s
20 4423 1332 1961 Hurwitz 563.27s
21 9689 2917 1963 Gillies 5304.08s
22 9941 2993 1963 Gillies 5650.63s
23 11213 3376 1963 Gillies 7607.00s
24 19937 6002 1971 Tuckerman 34653.12s
25 21701 6533 1978 Noll & Nickel 43746.21s
26 23209 6987 1979 Noll & Nickel 51210.56s
27 44497 13395 1979 Nelson & Slowinski 282784.09s

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:
  1. Download and compile the library
  2. Generate the cerficate for your prime number. For example for 1234567891, the command pocklington 1234567891 generates the file
    Require Import PocklingtonRefl.
    Set Virtual Machine.
    Open Local Scope positive_scope.
    Lemma prime1234567891 : 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)).
    exact_no_check (refl_equal true).
    Qed.
  3. Compile the file with coqc

If your number has more than 100 decimal digits
  1. Download and compile the library
  2. Use primo to generate a cerficiate file.out (the certificate for 1234567890123456789012353). Use the command o2v to generate the file file.v (the file for 1234567890123456789012353). and use the script v2v to add a wrapper aroung the file file.v (the final file for 1234567890123456789012353).
  3. Compile the file with coqc
Proving the primality of a number of about 300 decimal digits takes about an hour (see Research Report).

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

Project Summary
Tracker Tracker
There are no public trackers available
Forums Forums3 messages in 3 forums
Docs Doc Manager
Mail Lists Mailing Lists ( 0 public lists )
Tasks Task Manager
There are no public subprojects available
SCM SCM Tree ( 874 commits, 653 adds )
FTP Released Files

 

 

In case of problems, mail the administrators or file a bug

Powered By GForge Collaborative Development Environment