diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 75 | ||||
| -rw-r--r-- | src/Specific/GF25519ExtendedAddCoordinates.v | 83 | ||||
| -rw-r--r-- | src/SpecificGen/GF2213_32ExtendedAddCoordinates.v | 83 | ||||
| -rw-r--r-- | src/SpecificGen/GF2519_32ExtendedAddCoordinates.v | 83 | ||||
| -rw-r--r-- | src/SpecificGen/GF25519_32ExtendedAddCoordinates.v | 83 | ||||
| -rw-r--r-- | src/SpecificGen/GF25519_64ExtendedAddCoordinates.v | 83 | ||||
| -rw-r--r-- | src/SpecificGen/GF41417_32ExtendedAddCoordinates.v | 83 | ||||
| -rw-r--r-- | src/SpecificGen/GF5211_32ExtendedAddCoordinates.v | 83 |
9 files changed, 582 insertions, 75 deletions
diff --git a/_CoqProject b/_CoqProject index 082d9d0d3..ff4a22fc8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -146,6 +146,7 @@ src/Specific/GF1305.v src/Specific/GF25519.v src/Specific/GF25519Bounded.v src/Specific/GF25519BoundedCommon.v +src/Specific/GF25519ExtendedAddCoordinates.v src/Specific/GF25519Reflective.v src/Specific/SC25519.v src/Specific/FancyMachine256/Barrett.v diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 68e4ff6bb..10ff8d1af 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -13,7 +13,6 @@ Require Import Crypto.Util.Tactics. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Relations. Require Import Crypto.Algebra. Require Crypto.Spec.Ed25519. Import ListNotations. @@ -743,77 +742,3 @@ Definition unpack (f : wire_digits) : fe25519 := Definition unpack_correct (f : wire_digits) : unpack f = unpack_opt params25519 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). - -Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. -Definition edwards_extended_add_coordinates td P Q := -Eval cbv iota beta delta [ - Extended.add_coordinates - add sub mul - ] in - (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). -Definition edwards_extended_carry_add_coordinates td P Q := -Eval cbv iota beta delta [ - Extended.add_coordinates - carry_add carry_sub mul - ] in - (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). -Print edwards_extended_add_coordinates. - -Local Existing Instance field25519. -Create HintDb edwards_extended_add_coordinates_correct discriminated. -Section noncarry. - 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. - reflexivity. - Qed. -End noncarry. -Section carry. - 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. - reflexivity. - Qed. -End carry. - -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 (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. diff --git a/src/Specific/GF25519ExtendedAddCoordinates.v b/src/Specific/GF25519ExtendedAddCoordinates.v new file mode 100644 index 000000000..1b4fac559 --- /dev/null +++ b/src/Specific/GF25519ExtendedAddCoordinates.v @@ -0,0 +1,83 @@ +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 := +Eval cbv iota beta delta [ + Extended.add_coordinates + add sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). +Definition edwards_extended_carry_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + carry_add carry_sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). +Print edwards_extended_add_coordinates. + +Create HintDb edwards_extended_add_coordinates_correct discriminated. +Section noncarry. + 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. + reflexivity. + Qed. +End noncarry. +Section carry. + 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. + reflexivity. + Qed. +End carry. + +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. diff --git a/src/SpecificGen/GF2213_32ExtendedAddCoordinates.v b/src/SpecificGen/GF2213_32ExtendedAddCoordinates.v new file mode 100644 index 000000000..3ab6d9ada --- /dev/null +++ b/src/SpecificGen/GF2213_32ExtendedAddCoordinates.v @@ -0,0 +1,83 @@ +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.SpecificGen.GF2213_32. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. + +Definition edwards_extended_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + add sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). +Definition edwards_extended_carry_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + carry_add carry_sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). +Print edwards_extended_add_coordinates. + +Create HintDb edwards_extended_add_coordinates_correct discriminated. +Section noncarry. + Local Existing Instance field2213_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F2213_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_F2213_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_F2213_32_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. + reflexivity. + Qed. +End noncarry. +Section carry. + Local Existing Instance carry_field2213_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F2213_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_carry_F2213_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_carry_F2213_32_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. + reflexivity. + Qed. +End carry. + +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. diff --git a/src/SpecificGen/GF2519_32ExtendedAddCoordinates.v b/src/SpecificGen/GF2519_32ExtendedAddCoordinates.v new file mode 100644 index 000000000..32ac4258f --- /dev/null +++ b/src/SpecificGen/GF2519_32ExtendedAddCoordinates.v @@ -0,0 +1,83 @@ +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.SpecificGen.GF2519_32. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. + +Definition edwards_extended_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + add sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). +Definition edwards_extended_carry_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + carry_add carry_sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). +Print edwards_extended_add_coordinates. + +Create HintDb edwards_extended_add_coordinates_correct discriminated. +Section noncarry. + Local Existing Instance field2519_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F2519_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_F2519_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_F2519_32_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. + reflexivity. + Qed. +End noncarry. +Section carry. + Local Existing Instance carry_field2519_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F2519_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_carry_F2519_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_carry_F2519_32_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. + reflexivity. + Qed. +End carry. + +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. diff --git a/src/SpecificGen/GF25519_32ExtendedAddCoordinates.v b/src/SpecificGen/GF25519_32ExtendedAddCoordinates.v new file mode 100644 index 000000000..0fdab1b24 --- /dev/null +++ b/src/SpecificGen/GF25519_32ExtendedAddCoordinates.v @@ -0,0 +1,83 @@ +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.SpecificGen.GF25519_32. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. + +Definition edwards_extended_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + add sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). +Definition edwards_extended_carry_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + carry_add carry_sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). +Print edwards_extended_add_coordinates. + +Create HintDb edwards_extended_add_coordinates_correct discriminated. +Section noncarry. + Local Existing Instance field25519_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_F25519_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_F25519_32_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. + reflexivity. + Qed. +End noncarry. +Section carry. + Local Existing Instance carry_field25519_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_carry_F25519_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_carry_F25519_32_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. + reflexivity. + Qed. +End carry. + +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. diff --git a/src/SpecificGen/GF25519_64ExtendedAddCoordinates.v b/src/SpecificGen/GF25519_64ExtendedAddCoordinates.v new file mode 100644 index 000000000..3c6f47518 --- /dev/null +++ b/src/SpecificGen/GF25519_64ExtendedAddCoordinates.v @@ -0,0 +1,83 @@ +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.SpecificGen.GF25519_64. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. + +Definition edwards_extended_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + add sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). +Definition edwards_extended_carry_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + carry_add carry_sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). +Print edwards_extended_add_coordinates. + +Create HintDb edwards_extended_add_coordinates_correct discriminated. +Section noncarry. + Local Existing Instance field25519_64. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_64_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_F25519_64_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_F25519_64_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. + reflexivity. + Qed. +End noncarry. +Section carry. + Local Existing Instance carry_field25519_64. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_64_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_carry_F25519_64_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_carry_F25519_64_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. + reflexivity. + Qed. +End carry. + +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. diff --git a/src/SpecificGen/GF41417_32ExtendedAddCoordinates.v b/src/SpecificGen/GF41417_32ExtendedAddCoordinates.v new file mode 100644 index 000000000..f75f179e8 --- /dev/null +++ b/src/SpecificGen/GF41417_32ExtendedAddCoordinates.v @@ -0,0 +1,83 @@ +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.SpecificGen.GF41417_32. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. + +Definition edwards_extended_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + add sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). +Definition edwards_extended_carry_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + carry_add carry_sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). +Print edwards_extended_add_coordinates. + +Create HintDb edwards_extended_add_coordinates_correct discriminated. +Section noncarry. + Local Existing Instance field41417_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F41417_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_F41417_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_F41417_32_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. + reflexivity. + Qed. +End noncarry. +Section carry. + Local Existing Instance carry_field41417_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F41417_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_carry_F41417_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_carry_F41417_32_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. + reflexivity. + Qed. +End carry. + +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. diff --git a/src/SpecificGen/GF5211_32ExtendedAddCoordinates.v b/src/SpecificGen/GF5211_32ExtendedAddCoordinates.v new file mode 100644 index 000000000..f1dcad937 --- /dev/null +++ b/src/SpecificGen/GF5211_32ExtendedAddCoordinates.v @@ -0,0 +1,83 @@ +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.SpecificGen.GF5211_32. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. + +Definition edwards_extended_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + add sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). +Definition edwards_extended_carry_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + carry_add carry_sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q). +Print edwards_extended_add_coordinates. + +Create HintDb edwards_extended_add_coordinates_correct discriminated. +Section noncarry. + Local Existing Instance field5211_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F5211_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_F5211_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_F5211_32_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. + reflexivity. + Qed. +End noncarry. +Section carry. + Local Existing Instance carry_field5211_32. + Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F5211_32_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_carry_F5211_32_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_carry_F5211_32_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. + reflexivity. + Qed. +End carry. + +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. |