1 files changed, 13 insertions, 0 deletions
diff --git a/src/Experiments/SpecificCurve25519.v b/src/Experiments/SpecificCurve25519.v
new file mode 100644
index 000000000..e1b86d229
--- /dev/null
+++ b/src/Experiments/SpecificCurve25519.v
@@ -0,0 +1,13 @@
+Require Import Crypto.Util.Notations Coq.ZArith.BinInt.
+Require Import Crypto.Specific.GF25519.
+Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
+Local Infix "<<" := Z.shiftr.
+Local Infix "&" := Z.land.
+
+Section Curve25519.
+  Context {twice_d : fe25519}.
+
+  Definition ge25519_add :=
+    Eval cbv beta delta [Extended.add_coordinates fe25519 add mul sub ModularBaseSystemOpt.Let_In] in
+      @Extended.add_coordinates fe25519 add sub mul twice_d.
+End Curve25519.
+\ No newline at end of file