diff options
Diffstat (limited to 'src/SpecificGen/GF25519_32Bounded.v')
| -rw-r--r-- | src/SpecificGen/GF25519_32Bounded.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/SpecificGen/GF25519_32Bounded.v b/src/SpecificGen/GF25519_32Bounded.v index 4c015d25c..264d7c3d3 100644 --- a/src/SpecificGen/GF25519_32Bounded.v +++ b/src/SpecificGen/GF25519_32Bounded.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 : fe25519_32W := +Definition sqrt_m1W' : fe25519_32W := Eval vm_compute in fe25519_32ZToW sqrt_m1. +Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519_32W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519_32W_word64ize sqrt_m1W'. Definition GF25519_32sqrt x : GF25519_32.fe25519_32 := dlet powx := powW (fe25519_32ZToW x) (chain GF25519_32.sqrt_ec) in |