diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-11-11 20:52:57 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-11-11 20:52:57 -0500 |
| commit | e3be69fe4a9d42e19711fcd72adb5ecc11430748 (patch) | |
| tree | 333b143ac5015b9a90cc9a21a4698c9e7704c2e1 /src | |
| parent | 6f43ded103e47b4cf81f3c78909c3f1aa0bcf750 (diff) | |
GF25519: add optimized addition chain
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/GF25519.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index de6a47c01..fdef4898b 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -96,11 +96,11 @@ Definition pow2_chain p := | _ => pow2Chain' p 0 end. -Definition invChain := Eval compute in pow2_chain (Z.to_pos (modulus - 2)). +(* From Daniel Bernstein's "ref" implementation (Public Domain) *) +Definition invChain := [(0, 0); (0, 0); (0, 0); (0, 3); (0, 3); (0, 0); (0, 2); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 5); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 10); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 20); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 42); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 50); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 100); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 202); (0, 0); (0, 0); (0, 0); (0, 0); (0, 0); (0, 259)]%nat. Instance inv_ec : ExponentiationChain (modulus - 2). - apply Build_ExponentiationChain with (chain := invChain). - reflexivity. + apply Build_ExponentiationChain with (chain := invChain); vm_decide_no_check. Defined. (* Note : use caution copying square root code to other primes. The (modulus / 8 + 1) chains are |