diff options
Diffstat (limited to 'coqprime/gencertif/certif.h')
| -rw-r--r-- | coqprime/gencertif/certif.h | 128 |
1 files changed, 128 insertions, 0 deletions
diff --git a/coqprime/gencertif/certif.h b/coqprime/gencertif/certif.h new file mode 100644 index 000000000..d8f781868 --- /dev/null +++ b/coqprime/gencertif/certif.h @@ -0,0 +1,128 @@ +/* +(*************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(*************************************************************) +(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) +(*************************************************************) +*/ + +#include <stdio.h> +#include "gmp.h" + +#ifndef __CERTIF_H__ + +extern int flag_verbose; +void my_set_verbose(); + +/**********************************************/ +/* Pocklington certificate */ +/**********************************************/ + + +typedef struct +{ + mpz_ptr _N; /* the prime number to prove */ + mpz_ptr _F1; /* product of the pseudo factorization */ + mpz_ptr _R1; /* R1 = (N - 1)/F1 */ + unsigned long int _a; /* the witness */ + mpz_ptr _sqrt; /* The sqrt root needed by the certif ... */ + int _pow2; /* Number of power of 2 in F1 */ + int _allocated; /* allocated size in words of _dec */ + int _used; /* used words in _dec */ + mpz_ptr *_dec; /* pseudo factorization of N-1 */ + /* increasing first */ + /* F1 = 2^pow2 * PROD dec */ +} __pock_struct; + +typedef __pock_struct *pock_certif_t; + +pock_certif_t pock_init (mpz_t N); +void dec_add_ui (pock_certif_t c, unsigned long int ui); +void dec_add_mpz (pock_certif_t c, mpz_t n); +int check_pock (pock_certif_t c); + +void finalize_pock(pock_certif_t c); + +/**********************************************/ +/* Proof certificate */ +/**********************************************/ + +typedef struct +{ + mpz_ptr _N; /* The prime number to prove */ + char *_lemma; /* The name of the lemma */ +} __proof_struct; + +typedef __proof_struct *proof_certif_t; + +/**********************************************/ +/* Lucas certificate */ +/**********************************************/ + +typedef struct +{ + mpz_ptr _N; /* The prime number to prove */ + unsigned long int _n; /* N = 2^n - 1 */ +} __lucas_struct; + +typedef __lucas_struct *lucas_certif_t; + + + +/**********************************************/ +/* Pre certificate */ +/**********************************************/ + + +typedef struct +{ + int _kind; /* kind of certificate: */ + /* 0 : proof; 1 : pock_cerif; + 2: lucas_certif */ + union { + pock_certif_t _pock; + proof_certif_t _proof; + lucas_certif_t _lucas; + } _certif; +} __pre_struct; + +typedef __pre_struct *pre_certif_t; + +pre_certif_t mk_proof_certif(mpz_t N); +pre_certif_t mk_pock_certif(pock_certif_t c); +pre_certif_t mk_lucas_certif(mpz_t N, unsigned long int n); + + + +/**********************************************/ +/* Certificate */ +/**********************************************/ + + +typedef struct +{ + int _allocated; + int _used; + pre_certif_t *_list; +} __certif_struct; + +typedef __certif_struct *certif_t; + +void set_proof_limit (unsigned int max); + +certif_t init_certif(); +int _2_is_in (certif_t lc); +int is_in (mpz_t t, certif_t lc); +void add_pre(pre_certif_t, certif_t lc); + + +void print_pock_certif(FILE *out, pock_certif_t c); +void print_file(char *filename, char *name, pre_certif_t c, certif_t lc); +pock_certif_t read_file(char * filename, certif_t lc); + +void print_lemma(FILE *out, char* name, pre_certif_t p, certif_t lc); +void print_prelude(FILE *out); +#define __CERTIF_H__ +#endif /* __CERTIF_H__ */ + |