GF25519: add ErepAdd

1 files changed, 28 insertions, 0 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index fdef4898b..b69d4224e 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -743,3 +743,31 @@ 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).
+Print edwards_extended_add_coordinates.
+
+Local Existing Instance field25519.
+Create HintDb edwards_extended_add_coordinates_correct discriminated.
+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.
\ No newline at end of file