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
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Tactics.Algebra_syntax.Nsatz.
Require Import Crypto.Util.ZUtil.
Local Open Scope Z_scope.
Section Karatsuba.
Context {T : Type} (eval : T -> Z)
(sub : T -> T -> T)
(eval_sub : forall x y, eval (sub x y) = eval x - eval y)
(mul : T -> T -> T)
(eval_mul : forall x y, eval (mul x y) = eval x * eval y)
(add : T -> T -> T)
(eval_add : forall x y, eval (add x y) = eval x + eval y)
(scmul : Z -> T -> T)
(eval_scmul : forall c x, eval (scmul c x) = c * eval x)
(split : Z -> T -> T * T)
(eval_split : forall s x, s <> 0 -> eval (fst (split s x)) + s * (eval (snd (split s x))) = eval x)
.
Definition karatsuba_mul s (x y : T) : T :=
let xab := split s x in
let yab := split s y in
let xy0 := mul (fst xab) (fst yab) in
let xy2 := mul (snd xab) (snd yab) in
let xy1 := sub (mul (add (fst xab) (snd xab)) (add (fst yab) (snd yab))) (add xy2 xy0) in
add (add (scmul (s^2) xy2) (scmul s xy1)) xy0.
Lemma eval_karatsuba_mul s x y (s_nonzero:s <> 0) :
eval (karatsuba_mul s x y) = eval x * eval y.
Proof. cbv [karatsuba_mul]; repeat rewrite ?eval_sub, ?eval_mul, ?eval_add, ?eval_scmul.
rewrite <-(eval_split s x), <-(eval_split s y) by assumption; ring. Qed.
Definition goldilocks_mul s (xs ys : T) : T :=
let a_b := split s xs in
let c_d := split s ys in
let ac := mul (fst a_b) (fst c_d) in
(add (add ac (mul (snd a_b) (snd c_d)))
(scmul s (sub (mul (add (fst a_b) (snd a_b)) (add (fst c_d) (snd c_d))) ac))).
Local Existing Instances Z.equiv_modulo_Reflexive RelationClasses.eq_Reflexive Z.equiv_modulo_Symmetric Z.equiv_modulo_Transitive Z.mul_mod_Proper Z.add_mod_Proper Z.modulo_equiv_modulo_Proper.
Lemma goldilocks_mul_correct (p : Z) (p_nonzero : p <> 0) s (s_nonzero : s <> 0) (s2_modp : (s^2) mod p = (s+1) mod p) xs ys :
(eval (goldilocks_mul s xs ys)) mod p = (eval xs * eval ys) mod p.
Proof. cbv [goldilocks_mul]; Zmod_to_equiv_modulo.
repeat rewrite ?eval_mul, ?eval_add, ?eval_sub, ?eval_scmul, <-?(eval_split s xs), <-?(eval_split s ys) by assumption; ring_simplify.
setoid_rewrite s2_modp.
apply f_equal2; nsatz. Qed.
End Karatsuba.
|
