diff options
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Specific/GF25519ExtendedAddCoordinates.v | 81 |
2 files changed, 0 insertions, 82 deletions
diff --git a/_CoqProject b/_CoqProject index 842881408..213e82552 100644 --- a/_CoqProject +++ b/_CoqProject @@ -190,7 +190,6 @@ src/Specific/GF25519Bounded.v src/Specific/GF25519BoundedAddCoordinates.v src/Specific/GF25519BoundedCommon.v src/Specific/GF25519BoundedExtendedAddCoordinates.v -src/Specific/GF25519ExtendedAddCoordinates.v src/Specific/GF25519Reflective.v src/Specific/GF25519ReflectiveAddCoordinates.v src/Specific/SC25519.v diff --git a/src/Specific/GF25519ExtendedAddCoordinates.v b/src/Specific/GF25519ExtendedAddCoordinates.v deleted file mode 100644 index 255792cf9..000000000 --- a/src/Specific/GF25519ExtendedAddCoordinates.v +++ /dev/null @@ -1,81 +0,0 @@ -Require Import Crypto.BaseSystem. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.ModularArithmetic.ModularBaseSystem. -Require Import Crypto.Algebra. -Require Import Crypto.Util.Relations. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Tactics. - -Require Import Crypto.Specific.GF25519. -Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. - -Definition edwards_extended_add_coordinates td P Q := - (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). -Definition edwards_extended_carry_add_coordinates td P Q := - (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). - -Create HintDb edwards_extended_add_coordinates_correct discriminated. -Local Existing Instance field25519. -Hint Rewrite - (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_decode)) - (Ring.homomorphism_add(H1 :=homomorphism_F25519_decode)) - (Ring.homomorphism_sub(H1 :=homomorphism_F25519_decode)) - : edwards_extended_add_coordinates_correct. -Lemma edwards_extended_add_coordinates_correct td P Q : - Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q) - = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)). -Proof. - change (edwards_extended_add_coordinates td P Q) - with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). - destruct_head' prod. - simpl. - (*rewrite_strat topdown hints edwards_extended_add_coordinates_correct.*) (* loops on Coq 8.4 *) - repeat (rewrite ?(Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_decode)), - ?(Ring.homomorphism_add(H1 :=homomorphism_F25519_decode)), - ?(Ring.homomorphism_sub(H1 :=homomorphism_F25519_decode))). - reflexivity. -Qed. -Local Existing Instance carry_field25519. -Hint Rewrite - (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_decode)) - (Ring.homomorphism_add(H1 :=homomorphism_carry_F25519_decode)) - (Ring.homomorphism_sub(H1 :=homomorphism_carry_F25519_decode)) - : edwards_extended_add_coordinates_correct. -Lemma edwards_extended_carry_add_coordinates_correct td P Q : - Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q) - = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)). -Proof. - change (edwards_extended_carry_add_coordinates td P Q) - with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). - destruct_head' prod. - simpl. - (*rewrite_strat topdown hints edwards_extended_add_coordinates_correct.*) (* loops on Coq 8.4 *) - (* This is an annoying replacement for rewrite_strat loopiness *) - generalize (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_decode)). - generalize (Ring.homomorphism_add(H1 :=homomorphism_carry_F25519_decode)). - generalize (Ring.homomorphism_sub(H1 :=homomorphism_carry_F25519_decode)). - generalize mul; generalize carry_sub; generalize carry_add. - intros carry_add' carry_sub' mul'. - intros H0 H1 H2. - repeat rewrite ?H2, ?H1, ?H0. - reflexivity. -Qed. - -Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q : - Tuple.fieldwise - (n:=4) eq - (edwards_extended_carry_add_coordinates td P Q) - (edwards_extended_add_coordinates td P Q). -Proof. - pose proof (edwards_extended_carry_add_coordinates_correct td P Q) as H0. - pose proof (edwards_extended_add_coordinates_correct td P Q) as H1. - rewrite <- H0 in H1; clear H0. - assert (Tuple.fieldwise - (fun x y => x = y) - (Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)) - (Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q))) - by (rewrite H1; reflexivity). - clear H1. - destruct (edwards_extended_carry_add_coordinates td P Q), (edwards_extended_add_coordinates td P Q). - destruct_head' prod; simpl; unfold eq; trivial. -Qed. |