From a0e038a7ed560eca806c79de207467be1c00bb11 Mon Sep 17 00:00:00 2001 From: thery Date: Fri, 14 Jun 2024 15:01:41 +0200 Subject: [PATCH] montgomery --- README.md | 2 + _CoqProject | 3 +- coq-mathcomp-extra.opam | 2 + fft.v | 29 ++++++ meta.yml | 2 + montgomery.v | 192 ++++++++++++++++++++++++++++++++++++++++ 6 files changed, 229 insertions(+), 1 deletion(-) create mode 100644 montgomery.v diff --git a/README.md b/README.md index 097ce96..f2dd18e 100644 --- a/README.md +++ b/README.md @@ -56,6 +56,8 @@ Some extra material for mathcomp [A port to mathcomp of the elliptic curve of CoqPrime](./elliptic.v) [A formalisation of some sudoku solvers ](./sudoku.v) + + [A formalisation of Montgomery reduction ](./montgomery.v) A note about sorting network is available [here](https://hal.inria.fr/hal-03585618). diff --git a/_CoqProject b/_CoqProject index c7f0a70..baac058 100644 --- a/_CoqProject +++ b/_CoqProject @@ -23,4 +23,5 @@ bjsort.v puzzleFF.v elliptic.v iterative.v -sudoku.v \ No newline at end of file +sudoku.v +montgomery.v diff --git a/coq-mathcomp-extra.opam b/coq-mathcomp-extra.opam index c851164..65a182e 100644 --- a/coq-mathcomp-extra.opam +++ b/coq-mathcomp-extra.opam @@ -56,6 +56,8 @@ Some extra material for mathcomp [A port to mathcomp of the elliptic curve of CoqPrime](./elliptic.v) [A formalisation of some sudoku solvers ](./sudoku.v) + + [A formalisation of Montgomery reduction ](./montgomery.v) A note about sorting network is available [here](https://hal.inria.fr/hal-03585618).""" diff --git a/fft.v b/fft.v index 236c42f..ba88f11 100644 --- a/fft.v +++ b/fft.v @@ -1,5 +1,34 @@ (* Copyright (c) Inria. All rights reserved. *) From mathcomp Require Import all_ssreflect all_algebra ssrnum. + +Context (i : Type). +Context (Rich : i -> Prop). +Context (mother : i -> i). +Context (h : i). + +Theorem rich_mothers : +(forall x, ~Rich(x) -> Rich(mother(x))) -> +(forall x, ~Rich(mother(mother(x))) \/ ~Rich(x)) -> +False. +Proof. +move=> H1 H2. +have [H3|H3] := (H2) h. + have H4 := H1 _ H3. + case: (H2 (mother h)) => [[]//|/H1 H6]. + by case: H3. +have H4 := (H1) _ H3. +case: (H2 (mother h))=> [[]|/(_ (H1 _ H3))//]; last first. +apply: (H1) => H5. +case: (H2 (mother (mother h)))=> [[]|[]//]. +apply: (H1) => H6. +by case: (H2 (mother h)) => [] []. +Qed. + +Goal forall m n, m + n.+1 = n + m. +elim =>[n|n IH [|m]]; last first. + rewrite !addSn IH addSn. + + Require Import digitn. (******************************************************************************) diff --git a/meta.yml b/meta.yml index 793ad47..3c01783 100644 --- a/meta.yml +++ b/meta.yml @@ -53,6 +53,8 @@ description: |- [A port to mathcomp of the elliptic curve of CoqPrime](./elliptic.v) [A formalisation of some sudoku solvers ](./sudoku.v) + + [A formalisation of Montgomery reduction ](./montgomery.v) A note about sorting network is available [here](https://hal.inria.fr/hal-03585618). diff --git a/montgomery.v b/montgomery.v new file mode 100644 index 0000000..a0bf584 --- /dev/null +++ b/montgomery.v @@ -0,0 +1,192 @@ +From mathcomp Require Import all_ssreflect. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(******************************************************************************) +(* *) +(* Formalisation of Montgomery reduction *) +(* *) +(******************************************************************************) + + +Section Montgomery. + +Record montgomery := { + p : nat; + b : nat; + n : nat; + co: [&& coprime p b & b ^ n.-1 < p < b ^ n] + }. + +Lemma coprime_bp m : coprime (b m) (p m). +Proof. by rewrite coprime_sym; case: m => p b n /= /and3P[]. Qed. + +Implicit Type m : montgomery. + +Lemma p_pos m : 0 < p m. +Proof. by case: m => [] [|p] [|b] n /andP[] /=. Qed. + +Lemma b_pos m : 0 < b m. +Proof. +by case: m => [] p [|b] [|[|n]] /andP[_ /andP[]] //=; case: (ltngtP 1 p). +Qed. + +Lemma b_gt1 m : 1 < b m. +Proof. +case: m (b_pos m) => [] p [|[|b]] n //=. +by rewrite !exp1n; case: ltngtP; rewrite !andbF. +Qed. + +Definition w m := b m ^ n m. + +Lemma pLw m : p m < w m. +Proof. by rewrite /w; case: m => p b n /= /and3P[]. Qed. + +Lemma w_pos m : 0 < w m. +Proof. by rewrite expn_gt0 b_pos. Qed. + +Definition oppw m v := + let v1 := v %% w m in if v1 == 0 then 0 else w m - v1. + +Lemma ltn_oppw m v : oppw m v < w m. +Proof. +rewrite /oppw; case: (v %% w m) (ltn_pmod v (w_pos m)) => //= v1 v1Lw. +by case: w v1Lw => //= w1 _; rewrite subSS ltnS leq_subr. +Qed. + +Lemma oppwE m v : v + oppw m v = 0 %[mod w m]. +Proof. +rewrite /oppw -modnDml. +case: (v %% w m) (ltn_pmod v (w_pos m)) => //= v1 v1Lw. +by rewrite mod0n addnC subnK ?modnn // ltnW. +Qed. + +Lemma oppw_mod m v : oppw m (v %% w m) = oppw m v. +Proof. by rewrite /oppw modn_mod. Qed. + +Lemma oppwMr m v1 v2 : oppw m v1 * v2 = oppw m (v1 * v2) %[mod w m]. +Proof. +have w_pos := w_pos m. +rewrite /oppw -[(v1 * v2) %% _]modnMml. +case: (v1 %% _) (ltn_pmod v1 w_pos) => [|v3]; rewrite /= ?mod0n // => v3Lw. +case: eqP => [wL|wL]. + rewrite mulnBl modnB //. + by rewrite wL subn0 modnMr addn0 ltnn mod0n. + by rewrite leq_mul2r ltnW ?orbT. +rewrite mulnBl !modnB //; last 2 first. +- by rewrite ltnW // ltn_mod. +- by rewrite leq_mul2r ltnW ?orbT. +rewrite !modnn modn_mod. +by rewrite -modnMml modnn mod0n. +Qed. + +Lemma coprime_pw m : coprime (p m) (w m). +Proof. by apply: coprimeXr; case: m => /= p b n /and3P[]. Qed. + +(* A_h *) +Definition high m a := a %/ w m. +(* A_l *) +Definition low m a := a %% w m. + +Lemma high_low m a : a = high m a * w m + low m a. +Proof. by exact: divn_eq. Qed. + +(* P ^ -1 mod b ^ n *) +Definition invp m := (egcdn (p m) (w m)).1 %% w m. + +Lemma invpE m : p m * invp m = 1 %[mod w m]. +Proof. +rewrite /invp. +case: egcdnP => [|/= km kn Hm _]; first by exact: p_pos. +by rewrite modnMmr mulnC Hm (eqP (coprime_pw m)) modnMDl. +Qed. + +(* b ^ -1 mod P *) +Definition invb m := (egcdn (b m) (p m)).1 %% p m. + +Lemma invbE m : b m * invb m = 1 %[mod p m]. +Proof. +rewrite /invb. +case: egcdnP => [|/= km kn Hm _]; first by exact: b_pos. +by rewrite modnMmr mulnC Hm (eqP (coprime_bp m)) modnMDl. +Qed. + +(* Q = - A0 * P ^-1 mod b ^ n *) +Definition q m a := oppw m ((low m a * invp m) %% w m). + +Lemma q_bound m a : q m a < w m. +Proof. by apply: ltn_oppw. Qed. + +Definition reduce m a := + let v := high m (a + q m a * p m) in + if v < p m then v else v - p m. + +Definition invw m := invb m ^ n m. + +Lemma invwE m : w m * invw m = 1 %[mod p m]. +Proof. by rewrite -expnMn -modnXm invbE modnXm exp1n. Qed. + +Lemma reduceE m a : a < w m * p m -> reduce m a = (a * invw m) %% p m. +Proof. +move=> aLwp. +rewrite /reduce. +set a1 := _ + _ * _. +have a1w : a1 = 0 %[mod w m]. + rewrite /a1 /q -modnDmr oppwMr modnDmr. + rewrite -oppw_mod modnMml -mulnA -modnMmr [_ * p m]mulnC invpE modnMmr muln1. + by rewrite oppw_mod {1}[a](high_low m) -addnA modnMDl oppwE. +have a1P : a1 = a %[mod p m] by rewrite /a1 -modnDmr modnMl addn0. +rewrite -modnMml -a1P modnMml [a1 in RHS](high_low m) /low a1w mod0n addn0. +rewrite -mulnA -modnMmr invwE modnMmr muln1. +case: leqP => // Hp; last by rewrite modn_small. +suff hL2p : high m a1 < (p m).*2. + rewrite -[in RHS](subnK Hp) -modnDmr modnn addn0 modn_small //. + by rewrite ltn_subLR ?addnn. +rewrite ltn_divLR ?w_pos // /a1 -addnn mulnDl. +apply: leq_ltn_trans (_ : a + p m * w m < _). + by rewrite leq_add2l mulnC leq_mul2l ltnW ?orbT // q_bound. +by rewrite ltn_add2r mulnC. +Qed. + +Definition w2 m := (b m ^ (n m).*2) %% p m. + +Definition encode m a := reduce m (a * w2 m). + +Lemma encodeE m a : a < w m -> encode m a = (a * w m) %% p m. +Proof. +move=> aLp. +rewrite /encode reduceE /w2 -addnn expnD // -[b m ^ n m]/(w m). + by rewrite -modnMml modnMmr modnMml !mulnA -mulnA -modnMmr invwE modnMmr muln1. +apply: leq_ltn_trans (_ : a * p m < _). + by rewrite leq_mul2l ltnW ?orbT // ltn_mod p_pos. +by rewrite ltn_mul2r p_pos. +Qed. + +Definition decode m a := reduce m a. + +Definition mult m a b := decode m (reduce m (encode m a * encode m b)). + +Lemma multE m a b : a < w m -> b < w m -> mult m a b = a * b %% p m. +Proof. +move=> aL bL. +rewrite /mult /decode !encodeE // !reduceE. +- rewrite modnMml -!mulnA modnMml mulnC -!mulnA modnMml. + rewrite [invw m * (a * _)]mulnC !mulnA -mulnA. + rewrite -modnMmr invwE modnMmr muln1 mulnC !mulnA -mulnA. + by rewrite -modnMmr invwE modnMmr muln1. +- apply: leq_ltn_trans (_ : (a * w m) %% p m * p m < _). + by rewrite leq_mul2l ltnW ?orbT // ltn_mod p_pos. + rewrite ltn_mul2r p_pos. + by apply: leq_ltn_trans (pLw m); rewrite ltnW // ltn_mod p_pos. +- apply: leq_trans (_ : 1 * p m <= _). + by rewrite mul1n ltn_mod p_pos. + by rewrite leq_mul2r w_pos orbT. +apply: leq_ltn_trans (_ : (a * w m) %% p m * p m < _). + by rewrite leq_mul2l ltnW ?orbT // ltn_mod p_pos. +rewrite ltn_mul2r p_pos. +by apply: leq_ltn_trans (pLw m); rewrite ltnW // ltn_mod p_pos. +Qed. + +End Montgomery.