Move ExtendedAddCoordinates to new file, SpecGen

6 files changed, 498 insertions, 0 deletions

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.