diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-20 17:53:11 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-20 17:53:11 -0400 |
| commit | 95dac930ac0d709402f937c0999b57e5939db271 (patch) | |
| tree | b9c46ffecd6141b3910fc1f68e8a46cc7f0832db /src/Assembly/GF25519.v | |
| parent | 99b704779273707155df1f315cf3231f66004995 (diff) | |
Adjust bounds in assembly
Diffstat (limited to 'src/Assembly/GF25519.v')
| -rw-r--r-- | src/Assembly/GF25519.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 50a886305..7bb367a9f 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -17,11 +17,11 @@ Module GF25519. Section DefaultBounds. Import ListNotations. - Local Notation rr exp := (range N 0%N (2^exp + 2^exp/10)%N). + Local Notation rr exp := (range N 0%N (2^exp + 2^(exp-3))%N). Definition feBound: list (Range N) := - [rr 26; rr 27; rr 26; rr 27; rr 26; - rr 27; rr 26; rr 27; rr 26; rr 27]. + [rr 25; rr 26; rr 25; rr 26; rr 25; + rr 26; rr 25; rr 26; rr 25; rr 26]. End DefaultBounds. Definition FE: type. |