From 0e8a3822b105ac927633af9e1046060f4bd73d83 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Tue, 10 Nov 2026 19:57:10 +0100 Subject: [PATCH] algebra(Pocklington): Pocklington's criterion and computable primality certificates IntDiv: a ^ k mod d (modzXm), the multiplicative order of a modulo n (mulorder), existence of a prime divisor (pdivP) and the sqrt bound for composites (primePns). Reduction rules for computing, kept out of the default database: modular exponentiation by squaring (powmod0, powmodE) in the hint database powmod, and Euclid's algorithm (gcdE) in the hint database gcd; use them with cbv delta hint +powmod +gcd. Pocklington: Pocklington's criterion (after coqprime) and a checker for certificates (list of prime factors of N - 1 with witnesses), sound by pock_certif and evaluated by cbv. --- theories/algebra/IntDiv.ec | 135 +++++++++++++++++++++++++++++ theories/algebra/Pocklington.ec | 148 ++++++++++++++++++++++++++++++++ 2 files changed, 283 insertions(+) create mode 100644 theories/algebra/Pocklington.ec diff --git a/theories/algebra/IntDiv.ec b/theories/algebra/IntDiv.ec index 8e6f9ef271..15cfc08389 100644 --- a/theories/algebra/IntDiv.ec +++ b/theories/algebra/IntDiv.ec @@ -1469,3 +1469,138 @@ case: (y = 0) => [->|nz_y] /=; first by rewrite divz0. case/dvdzP => [q ->]; rewrite mulzK //. by rewrite fromintM RField.mulrK // eq_fromint. qed. + +(* -------------------------------------------------------------------- *) +lemma modzXm (m d k : int) : 0 <= k => (m %% d) ^ k %% d = m ^ k %% d. +proof. +elim: k => [|k ge0_k ih]; first by rewrite !expr0. +by rewrite !exprS // -(modzMmr (m %% d)) ih modzMmr modzMml. +qed. + +(* -------------------------------------------------------------------- *) +(* Multiplicative order of a modulo n: the least k > 0 such that *) +(* a ^ k %% n = 1 (meaningful when such a k exists). *) +op mulorder (a n : int) = + argmin (fun k => k + 1) (fun k => a ^ k %% n = 1) + 1. + +lemma mulorder_spec (a n k0 : int) : 0 < k0 => a ^ k0 %% n = 1 => + 0 < mulorder a n + /\ a ^ mulorder a n %% n = 1 + /\ forall k, 0 < k < mulorder a n => a ^ k %% n <> 1. +proof. +move=> gt0_k0 h. +have [#] := argminP_r (fun k => k + 1) (fun k => a ^ k %% n = 1) (k0 - 1) _ _ => //=. +- by smt(). +rewrite /mulorder => ge0_m hm hmin; do! split => //. +- by smt(). +by move=> k [gt0_k lt_k]; have := hmin (k - 1) _ => /#. +qed. + +lemma mulorder_gt0 (a n k0 : int) : 0 < k0 => a ^ k0 %% n = 1 => 0 < mulorder a n. +proof. by move=> gt0_k0 h; have [#] := mulorder_spec a n k0 gt0_k0 h. qed. + +lemma expz_mulorder (a n k0 : int) : 0 < k0 => a ^ k0 %% n = 1 => + a ^ mulorder a n %% n = 1. +proof. by move=> gt0_k0 h; have [#] := mulorder_spec a n k0 gt0_k0 h. qed. + +lemma mulorder_dvdz (a n k0 k : int) : 0 < k0 => a ^ k0 %% n = 1 => 0 <= k => + (mulorder a n %| k <=> a ^ k %% n = 1). +proof. +move=> gt0_k0 h ge0_k; have [# gt0_o ho omin] := mulorder_spec a n k0 gt0_k0 h. +pose o := mulorder a n; have mod1 : 1 %% n = 1 by rewrite -h modz_mod. +have ge0_q : 0 <= k %/ o by smt(divz_ge0). +have [ge0_r lt_r] : 0 <= k %% o < o by smt(modz_ge0 ltz_pmod). +have -> : a ^ k %% n = a ^ (k %% o) %% n. +- rewrite {1}(divz_eq k o) exprD_nneg 1:/# //. + by rewrite (mulrC (k %/ o)) exprM -modzMml -modzXm // ho expr1z mod1 mul1r. +rewrite dvdzE; split => [->|]; first by rewrite expr0. +by apply: contraLR => nz_r; apply: omin; smt(). +qed. + +lemma mulorder_dvd_pred (a p : int) : prime p => ! (p %| a) => + mulorder a p %| (p - 1). +proof. +move=> prime_p Ndvd; have gt1_p := gt1_prime p prime_p. +have h : a ^ (p - 1) %% p = 1. +- have := Fermat_little p a prime_p Ndvd. + by rewrite eqz_mod_dvd => ->; rewrite modz_small; smt(). +by rewrite (mulorder_dvdz a p (p - 1)) 1,3:/#. +qed. + +(* -------------------------------------------------------------------- *) +lemma pdivP (n : int) : 1 < n => exists p, prime p /\ p %| n. +proof. +move=> gt1_n; have ge0_n : 0 <= n by smt(). +elim/sintind: n ge0_n gt1_n => n ge0_n ih gt1_n. +case: (prime n) => [pn|]; first by exists n; rewrite pn dvdzz. +rewrite /prime gt1_n /= negb_forall => -[q] /=; rewrite negb_imply negb_or. +case=> dvd_qn [nq1 nqn]; have := dvdz_le q n _ dvd_qn; 1: smt(). +have nz_q : q <> 0 by apply: contraL dvd_qn => ->; rewrite dvd0z /#. +move=> le_qn; case: (ih `|q| _ _) => [| |p [pp dvd_pq]]; 1,2: smt(). +by exists p; split => //; apply: (dvdz_trans `|q|) => //; rewrite dvdz_norml. +qed. + +lemma primePns (n : int) : + ! prime n <=> (n < 2 \/ exists p, prime p /\ p ^ 2 <= n /\ p %| n). +proof. +split=> [npr_n|]; last first. +- case=> [lt2_n|[p [pr_p [le_p2n dvd_pn]]]]; first by smt(gt1_prime). + apply/negP => pr_n; have := pr_n; rewrite /prime => -[gt1_n /(_ p dvd_pn)]. + have := gt1_prime p pr_p; move: le_p2n; rewrite expr2 => le_p2n gt1_p. + by have := ltr_pmul2l p _ 1 p; smt(). +case: (n < 2) => [lt2_n|ge2_n]; first by left. +right; have gt1_n : 1 < n by smt(). +move: npr_n; rewrite /prime gt1_n /= negb_forall => -[q] /=. +rewrite negb_imply negb_or => -[dvd_qn [nq1 nqn]]. +have le_qn := dvdz_le q n _ dvd_qn; 1: smt(). +have nz_q : q <> 0 by apply: contraL dvd_qn => ->; rewrite dvd0z /#. +pose d := `|q|; pose e := n %/ d. +have dvd_dn : d %| n by rewrite dvdz_norml. +have de : e * d = n by rewrite divzK. +have [gt1_d gt1_e] : 1 < d /\ 1 < e by smt(). +pose m := min d e; have dvd_mn : m %| n. +- rewrite /m /min; case: (d < e) => _ //. + by rewrite -{1}de; apply/dvdz_mulr/dvdzz. +have mm : m * m <= n by rewrite -de; apply: ler_pmul => /#. +case: (pdivP m _) => [/#|p [pp dvd_pm]]. +have := dvdz_le p m _ dvd_pm; 1: smt(). +move=> le_pm; exists p; split => //; rewrite expr2; split. +- have := gt1_prime p pp => gt1_p. + by apply: (ler_trans (m * m)) => //; apply: ler_pmul => /#. +exact: (dvdz_trans m). +qed. + +(* ==================================================================== *) +(* Computable modular arithmetic: reduction rules in the hint databases *) +(* [powmod] and [gcd], used as [cbv delta hint +powmod +gcd]. *) +(* -------------------------------------------------------------------- *) +(* Modular exponentiation by squaring, as reduction rules. *) +op powmod (a n x : int) = a ^ x %% n. + +lemma powmod0 a n : powmod a n 0 = 1 %% n. +proof. by rewrite /powmod expr0. qed. + +lemma powmodE a n x : 0 < x => + powmod a n x = + let p = powmod a n (x %/ 2) in let p2 = p * p %% n in + if x %% 2 = 1 then p2 * a %% n else p2. +proof. +move=> gt0_x; rewrite /powmod /=. +have ge0_h : 0 <= x %/ 2 by smt(divz_ge0). +have ex : a ^ x = a ^ (x %/ 2) * a ^ (x %/ 2) * a ^ (x %% 2). +- rewrite -!exprD_nneg //; 1,2: smt(modz_ge0). + by congr; smt(divz_eq). +rewrite ex; case: (x %% 2 = 1) => [->|ne1]. +- by rewrite expr1 modzMml eq_sym -(modzMml (_ %% n * _)) modzMm modzMml. +have -> : x %% 2 = 0 by smt(modz_ge0 ltz_pmod). +by rewrite expr0 mulr1 modzMm. +qed. + +hint simplify in powmod : powmod0, powmodE. + +(* -------------------------------------------------------------------- *) +(* Euclid's algorithm. *) +lemma gcdE a b : gcd a b = if b = 0 then `|a| else gcd b (a %% b). +proof. by case: (b = 0) => [->|nz_b]; rewrite ?gcdz0 // gcd_modr gcdC. qed. + +hint simplify in gcd : gcdE. diff --git a/theories/algebra/Pocklington.ec b/theories/algebra/Pocklington.ec new file mode 100644 index 0000000000..b0260ef345 --- /dev/null +++ b/theories/algebra/Pocklington.ec @@ -0,0 +1,148 @@ +require import AllCore List IntDiv StdOrder. +import IntOrder. + +(* -------------------------------------------------------------------- *) +(* Pocklington's criterion (after coqprime, PrimalityTest/Pocklington.v) *) + +(* F divides m as soon as, for each prime p dividing F, some divisor o *) +(* of both m and D leaves a cofactor D %/ o that p does not divide. *) +lemma pocklington_dvd (F D m : int) : 0 < D => F %| D => + (forall p, prime p => p %| F => + exists o, o %| m /\ o %| D /\ ! p %| (D %/ o)) => + F %| m. +proof. +move=> gt0_D dvd_FD hp; pose L := gcd D m. +have nz_L : L <> 0 by rewrite /L gcd_eq0 /#. +have dvd_LD : L %| D by apply: dvdz_gcdl. +have nz_F : F <> 0 by apply: contraL dvd_FD => ->; rewrite dvd0z /#. +have cop : coprime F (D %/ L). +- rewrite /coprime; pose g := gcd F (D %/ L). + have ge0_g : 0 <= g by apply: ge0_gcd. + have nz_g : g <> 0 by rewrite /g gcd_eq0 /#. + case: (g = 1) => // ne1_g; case: (pdivP g _); 1: smt(). + move=> p [pr_p dvd_pg]. + have dvd_pF : p %| F by apply: (dvdz_trans g) => //; apply: dvdz_gcdl. + have dvd_pDL : p %| D %/ L by apply: (dvdz_trans g) => //; apply: dvdz_gcdr. + case: (hp p pr_p dvd_pF) => o [dvd_om [dvd_oD ndvd]]. + have dvd_oL : o %| L by apply: dvdz_gcd. + have nz_o : o <> 0 by apply: contraL dvd_oD => ->; rewrite dvd0z /#. + have hDo : D %/ o = D %/ L * (L %/ o). + - have hD : D = D %/ L * (L %/ o) * o by rewrite -mulrA !divzK. + by rewrite {1}hD mulzK. + have : p %| D %/ o by rewrite hDo; apply: dvdz_mulr. + by move=> h; have := ndvd; rewrite h. +have dvd_FL : F %| L. +- by apply: (Gauss _ (D %/ L)) => //; rewrite divzK. +by apply: (dvdz_trans L) => //; apply: dvdz_gcdr. +qed. + +lemma pocklington_mulorder (N q p a : int) : 1 < N => prime q => q %| N => + prime p => p %| (N - 1) => + a ^ (N - 1) %% N = 1 => coprime (a ^ ((N - 1) %/ p) - 1) N => + mulorder a q %| (q - 1) + /\ mulorder a q %| (N - 1) + /\ ! p %| ((N - 1) %/ mulorder a q). +proof. +move=> gt1_N pr_q dvd_qN pr_p dvd_pD haN cop. +have gt1_q := gt1_prime q pr_q; have gt1_p := gt1_prime p pr_p. +have haq : a ^ (N - 1) %% q = 1. +- by rewrite -(modz_dvd _ N q) // haN modz_small /#. +have ndvd_qa : ! q %| a. +- apply/negP => dvd_qa; move: haq; rewrite (_ : N - 1 = (N - 2) + 1) 1:/#. + rewrite exprS 1:/#; have := dvdz_mulr q a (a ^ (N - 2)) dvd_qa. + by rewrite dvdzE => ->. +have dvd_oD : mulorder a q %| (N - 1) by rewrite (mulorder_dvdz a q (N - 1)) 1,3:/#. +do! split => //; first by apply: mulorder_dvd_pred. +apply/negP => dvd_p; pose o := mulorder a q; have gt0_o : 0 < o. +- by apply: (mulorder_gt0 a q (N - 1)) => /#. +case/dvdzP: dvd_p => t ht. +have hD : N - 1 = t * o * p by rewrite -(divzK o (N - 1)) // ht; ring. +have dvd_oDp : o %| ((N - 1) %/ p). +- by rewrite hD mulzK 1:/#; apply: dvdz_mull; apply: dvdzz. +have : a ^ ((N - 1) %/ p) %% q = 1. +- have gt0_D : 0 < N - 1 by smt(). + have ge0_Dp : 0 <= (N - 1) %/ p by rewrite divz_ge0 /#. + by rewrite -(mulorder_dvdz a q (N - 1) _ gt0_D haq ge0_Dp). +move=> h1; have dvd_q1 : q %| (a ^ ((N - 1) %/ p) - 1). +- by rewrite eqz_mod_dvd h1 modz_small /#. +have := dvdz_gcd q _ _ dvd_q1 dvd_qN; move: cop; rewrite /coprime => ->. +by rewrite dvdz1; smt(). +qed. + +lemma pocklington (N F1 R1 : int) : 1 < F1 => 0 < R1 => N - 1 = F1 * R1 => + (forall p, prime p => p %| F1 => + exists a, a ^ (N - 1) %% N = 1 /\ coprime (a ^ ((N - 1) %/ p) - 1) N) => + forall q, prime q => q %| N => q %% F1 = 1. +proof. +move=> gt1_F gt0_R hN hp q pr_q dvd_qN. +have le_F : F1 <= F1 * R1 by apply: ler_pemulr => /#. +have gt1_N : 1 < N by smt(). +have dvd_F : F1 %| (q - 1). +- apply: (pocklington_dvd F1 (N - 1)); 1: smt(). + + by rewrite hN; apply: dvdz_mulr; apply: dvdzz. + move=> p pr_p dvd_pF; case: (hp p pr_p dvd_pF) => a [haN cop]. + have dvd_pD : p %| (N - 1) by rewrite hN; apply: dvdz_mulr. + have [#] := pocklington_mulorder N q p a gt1_N pr_q dvd_qN pr_p dvd_pD haN cop. + by move=> h1 h2 h3; exists (mulorder a q). +by rewrite (_ : q = (q - 1) + 1) 1:/# dvdz_modzDl // modz_small /#. +qed. + +lemma pocklington_prime (N F1 R1 : int) : + 1 < F1 => 0 < R1 => N - 1 = F1 * R1 => N < F1 * F1 => + (forall p, prime p => p %| F1 => + exists a, a ^ (N - 1) %% N = 1 /\ coprime (a ^ ((N - 1) %/ p) - 1) N) => + prime N. +proof. +move=> gt1_F gt0_R hN lt_N hp; apply: contraT => npr_N. +have gt1_N : 1 < N by smt(). +move: npr_N; rewrite primePns => -[/#|[q [pr_q [le_q2 dvd_qN]]]]. +have hq := pocklington N F1 R1 gt1_F gt0_R hN hp q pr_q dvd_qN. +have gt1_q := gt1_prime q pr_q. +have lt_Fq : F1 < q. +- have := divz_eq q F1; rewrite hq; pose k := q %/ F1; move=> eq_q. + have ge0_k : 0 <= k by rewrite /k divz_ge0 /#. + have : F1 <= k * F1 by case: (k = 0) => [/#|nz_k]; apply: ler_pemull => /#. + smt(). +have := ltr_pmul F1 q F1 q _ _ lt_Fq lt_Fq; 1,2: smt(). +by move: le_q2; rewrite expr2; smt(). +qed. + +(* -------------------------------------------------------------------- *) +(* A certificate for N is a list of pairs (p, a): F1 is the product of *) +(* the p's (with multiplicity), and a is the witness for p. *) +op pock_F1 (c : (int * int) list) = + foldr (fun (pa : int * int) f => pa.`1 * f) 1 c. + +op pock_check (N : int) (c : (int * int) list) = + let F1 = pock_F1 c in + 1 < N /\ 1 < F1 /\ (N - 1) %% F1 = 0 /\ N < F1 * F1 + /\ all (fun (pa : int * int) => + powmod pa.`2 N (N - 1) = 1 + /\ gcd ((powmod pa.`2 N ((N - 1) %/ pa.`1) - 1) %% N) N = 1) c. + +lemma pock_F1P (p : int) (c : (int * int) list) : prime p => + p %| pock_F1 c => exists pa, pa \in c /\ p %| pa.`1. +proof. +move=> pr_p; elim: c => [|pa c ih] /=. +- by rewrite /pock_F1 /= dvdzE modz_small; smt(gt1_prime). +rewrite /pock_F1 /= -/(pock_F1 c) => /Euclide /(_ pr_p). +case=> [h|/ih [qa [qa_in h]]]; first by exists pa. +by exists qa; rewrite /= qa_in h. +qed. + +lemma pock_certif (N : int) (c : (int * int) list) : + pock_check N c => all (fun (pa : int * int) => prime pa.`1) c => prime N. +proof. +rewrite /pock_check /=; pose F1 := pock_F1 c. +move=> [#] gt1_N gt1_F dvd_F lt_N /allP hc /allP pr_c. +have eq_N : N - 1 = F1 * ((N - 1) %/ F1). +- by rewrite mulrC divzK // dvdzE. +apply: (pocklington_prime N F1 ((N - 1) %/ F1)) => //. +- by rewrite ltz_divRL // ?dvdzE /#. +move=> p pr_p /(pock_F1P p c pr_p) [[q a] [qa_in dvd_pq]]. +have pr_q := pr_c _ qa_in; have [#] := hc _ qa_in => /=. +rewrite /powmod => h1 h2; exists a; split => //. +have -> : p = q. +- case: pr_q => _ /(_ p dvd_pq); smt(gt1_prime). +by move: h2; rewrite modzDml -coprime_modl /coprime. +qed.