From b68e0ebe9c9064fa90ff47dc794674310d86a8d7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 14 Nov 2016 20:41:22 -0500 Subject: Fix some sqrt things --- src/Specific/GF25519Bounded.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Specific/GF25519Bounded.v') 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 -- cgit v1.2.3