diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-17 14:21:26 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-17 14:22:00 -0400 |
| commit | f0fa2edefc549d1d4878016b9e89e7ee7484cbeb (patch) | |
| tree | 3f0cf3ce6d065b183f333dd7b7f58410c07261e8 /src/Curves | |
| parent | d52aa178dd27836d61312053ea39540b9f1ab6d5 (diff) | |
Respond to code review comments
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Montgomery/XZ.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v index a57a51c7a..c31fb26c6 100644 --- a/src/Curves/Montgomery/XZ.v +++ b/src/Curves/Montgomery/XZ.v @@ -64,11 +64,11 @@ Module M. (* Ideally, we would verify that this corresponds to x coordinate multiplication *) Local Open Scope core_scope. - Definition montladder (bound : positive) (testbit:nat->bool) (u:F) := + Definition montladder (bound : positive) (testbit:Z->bool) (u:F) := let '(P1, P2, swap) := - for (int i = BinInt.Z.pos bound; i >= 0%Z; i--) + for (int i = BinInt.Z.pos bound; i >= 0; i--) updating ('(P1, P2, swap) = ((1%F, 0%F), (u, 1%F), false)) {{ - dlet s_i := testbit (BinInt.Z.to_nat i) in + dlet s_i := testbit i in dlet swap := xor swap s_i in let '(P1, P2) := cswap swap P1 P2 in dlet swap := s_i in |