Finish proofs about eliminating useless carries

3 files changed, 59 insertions, 90 deletions

diff --git a/src/Specific/GF25519BoundedAddCoordinates.v b/src/Specific/GF25519BoundedAddCoordinates.v
index ad7f44558..141c950bb 100644
--- a/src/Specific/GF25519BoundedAddCoordinates.v
+++ b/src/Specific/GF25519BoundedAddCoordinates.v
@@ -1,31 +1,10 @@
-Require Import Crypto.BaseSystem.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
-Require Import Crypto.ModularArithmetic.ModularBaseSystem.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Specific.GF25519.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Specific.GF25519ReflectiveAddCoordinates.
-Require Import Bedrock.Word Crypto.Util.WordUtil.
-Require Import Coq.Lists.List Crypto.Util.ListUtil.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemWord.
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Util.ZUtil.
-Require Import Crypto.Util.HList.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Algebra.
-Import ListNotations.
-Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Local Open Scope Z.
 
-
 Local Ltac bounded_t opW blem :=
   apply blem; apply is_bounded_proj1_fe25519.
 
diff --git a/src/Specific/GF25519BoundedExtendedAddCoordinates.v b/src/Specific/GF25519BoundedExtendedAddCoordinates.v
index 695ca335e..3910edab8 100644
--- a/src/Specific/GF25519BoundedExtendedAddCoordinates.v
+++ b/src/Specific/GF25519BoundedExtendedAddCoordinates.v
@@ -1,30 +1,10 @@
-Require Import Crypto.BaseSystem.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
 Require Import Crypto.ModularArithmetic.ModularBaseSystem.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
-Require Import Crypto.Specific.GF25519.
 Require Import Crypto.Specific.GF25519Bounded.
 Require Import Crypto.Specific.GF25519ExtendedAddCoordinates.
 Require Import Crypto.Specific.GF25519BoundedAddCoordinates.
-Require Import Bedrock.Word Crypto.Util.WordUtil.
-Require Import Coq.Lists.List Crypto.Util.ListUtil.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemWord.
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Util.ZUtil.
-Require Import Crypto.Util.HList.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Algebra.
-Import ListNotations.
-Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
-Local Open Scope Z.
 
 Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23
   : Tuple.fieldwise
@@ -37,8 +17,29 @@ Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P2
          (P10, P11, P12, P13) (P20, P21, P22, P23)).
 Proof.
   unfold GF25519BoundedCommon.eq.
-  pose (add_coordinates_correct).
-Admitted.
+  apply -> (fieldwise_map_iff (n:=4) eq GF25519BoundedCommon.proj1_fe25519 GF25519BoundedCommon.proj1_fe25519).
+  rewrite add_coordinates_correct.
+  cbv [AddCoordinates.add_coordinates].
+  setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry.
+  unfold edwards_extended_carry_add_coordinates.
+  match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end.
+  apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF25519BoundedCommon.proj1_fe25519).
+  apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero;
+    intros;
+    repeat match goal with
+           | [ |- context[add _ _] ]
+             => rewrite add_correct
+           | [ |- context[sub _ _] ]
+             => rewrite sub_correct
+           | [ |- context[mul _ _] ]
+             => rewrite mul_correct
+           | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in *
+           | [ |- and _ _ ] => split
+           | [ |- ?x = ?x ] => reflexivity
+           | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct
+           | _ => congruence
+           end.
+Qed.
 
 Definition add_coordinates twice_d P1 P2
   := let '(P10, P11, P12, P13) := P1 in
@@ -54,4 +55,6 @@ Lemma add_coordinates_correct_full twice_d P1 P2
          GF25519BoundedCommon.fe25519
          GF25519Bounded.add GF25519Bounded.sub GF25519Bounded.mul twice_d P1 P2).
 Proof.
-Admitted.
+  destruct_head' prod.
+  rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity.
+Qed.
diff --git a/src/Specific/GF25519ExtendedAddCoordinates.v b/src/Specific/GF25519ExtendedAddCoordinates.v
index 1b4fac559..a390da8ba 100644
--- a/src/Specific/GF25519ExtendedAddCoordinates.v
+++ b/src/Specific/GF25519ExtendedAddCoordinates.v
@@ -10,58 +10,45 @@ 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))
+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))
+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.
+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 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.
 
 Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q :
   Tuple.fieldwise