diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-14 20:41:22 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-14 20:41:22 -0500 |
| commit | b68e0ebe9c9064fa90ff47dc794674310d86a8d7 (patch) | |
| tree | 3dfdce965f73599c29a8aeb8b1b72711950a177b /src/Specific | |
| parent | e2cac8ba391a9f173d32a79ce612a88ee36f94cb (diff) | |
Fix some sqrt things
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519Bounded.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v index 055c5fa72..778c3b3ed 100644 --- a/src/Specific/GF25519Bounded.v +++ b/src/Specific/GF25519Bounded.v @@ -286,9 +286,9 @@ Proof. exact (proj2_sig (eqbW_sig f' g')). Qed. -(* TODO(jgross): use NToWord or such for this constant too *) -Definition sqrt_m1W : fe25519W := +Definition sqrt_m1W' : fe25519W := Eval vm_compute in fe25519ZToW sqrt_m1. +Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519W_word64ize sqrt_m1W'. Definition GF25519sqrt x : GF25519.fe25519 := dlet powx := powW (fe25519ZToW x) (chain GF25519.sqrt_ec) in |