aboutsummaryrefslogtreecommitdiff
path: root/coqprime/gencertif/certif.h
blob: d8f781868736457d978788d3fbbcef828b65e7be (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
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__ */