diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-25 19:07:38 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-25 19:07:38 -0400 |
| commit | 6c3c953d836ac43a8acff1975d73eb3204902ef2 (patch) | |
| tree | 568f815a4ef0715c8bf0cc91e0e318a2151137ec /src/Specific | |
| parent | b9c8f539cf3e9f9fdcd6861ef9691fe079bcd321 (diff) | |
Reorganization and revision of Encoding code and redefinition of sign_bit function.
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/Ed25519.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 2bafd4c8a..8ff80ebb9 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -5,7 +5,8 @@ Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. Require Import ModularArithmetic.ModularArithmeticTheorems. Require Import ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. +Require Import Crypto.Encoding.PointEncodingPre. +Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.PointEncoding. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.Util.IterAssocOp. @@ -465,8 +466,6 @@ Proof. set_evars. rewrite !FRepOpp_correct. - rewrite <-!enc_rep2F_correct. - rewrite <-wltu_correct. rewrite (if_map rep2F). lazymatch goal with |- ?e = Let_In (rep2F ?x, rep2F ?y) (fun p => @?r p) => |