From 31d802e9c11094d94c7ae7c13b05bd13639263fc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 17 Jan 2017 18:35:09 -0500 Subject: Fix changed qualified tactic name --- src/Spec/Ed25519.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index aa904fc7e..3d1a30559 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -6,17 +6,17 @@ Require ModularArithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field (* TODO: move this to a separate file *) Require Crypto.Util.Decidable. -Require Crypto.Util.Tactics. +Require Crypto.Util.Tactics.SpecializeBy. Module Pre. Local Open Scope F_scope. Lemma curve25519_params_ok {prime_q:Znumtheory.prime (2^255-19)} : @E.twisted_edwards_params (F (2 ^ 255 - 19)) (@eq (F (2 ^ 255 - 19))) (@F.zero (2 ^ 255 - 19)) - (@F.one (2 ^ 255 - 19)) (@F.add (2 ^ 255 - 19)) (@F.mul (2 ^ 255 - 19)) + (@F.one (2 ^ 255 - 19)) (@F.add (2 ^ 255 - 19)) (@F.mul (2 ^ 255 - 19)) (@F.opp (2 ^ 255 - 19) 1) (@F.opp (2 ^ 255 - 19) (F.of_Z (2 ^ 255 - 19) 121665) / F.of_Z (2 ^ 255 - 19) 121666). Proof. pose (@PrimeFieldTheorems.F.Decidable_square (2^255-19) _); - Tactics.specialize_by Decidable.vm_decide; split; Decidable.vm_decide_no_check. + SpecializeBy.specialize_by Decidable.vm_decide; split; Decidable.vm_decide_no_check. Qed. End Pre. (* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *) @@ -80,4 +80,4 @@ Section Ed25519. (l:=l) (b:=b) (n:=n) (c:=c) (Eenc:=Eenc) (Senc:=Senc) (H:=H). Proof. split; try (assumption || exact _); vm_decide. Qed. -End Ed25519. \ No newline at end of file +End Ed25519. -- cgit v1.2.3