diff options
Diffstat (limited to 'coqprime/gencertif/certif.h')
| -rw-r--r-- | coqprime/gencertif/certif.h | 128 |
1 files changed, 0 insertions, 128 deletions
diff --git a/coqprime/gencertif/certif.h b/coqprime/gencertif/certif.h deleted file mode 100644 index d8f781868..000000000 --- a/coqprime/gencertif/certif.h +++ /dev/null @@ -1,128 +0,0 @@ -/* -(*************************************************************) -(* 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__ */ - |