ed25519

zkFold · Jan 9, 2025 · 402cbc0 · 402cbc0
1 parent 80aea4a
commit 402cbc0
Show file tree

Hide file tree

Showing 2 changed files with 42 additions and 24 deletions.
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs
@@ -6,17 +6,17 @@ module ZkFold.Base.Algebra.EllipticCurve.Ed25519
   ( Ed25519_Base
   , Ed25519_Scalar
   , Ed25519_Point
+  , Ed25519_PointOf
   , Fl
   , Fq
   ) where
 
-import           Data.Type.Equality
+import           Prelude                                 (Bool)
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field
 import           ZkFold.Base.Algebra.Basic.Number
 import           ZkFold.Base.Algebra.EllipticCurve.Class
-import           ZkFold.Symbolic.Data.Eq
 
 -- | 2^252 + 27742317777372353535851937790883648493 is the order of the multiplicative group in Ed25519
 -- with the generator point defined below in @instance EllipticCurve (Ed25519 Void r)@
@@ -29,7 +29,8 @@ instance Prime Ed25519_Scalar
 type Ed25519_Base = 57896044618658097711785492504343953926634992332820282019728792003956564819949
 instance Prime Ed25519_Base
 
-type Ed25519_Point = TwistedEdwards "ed25519" AffinePoint Fq
+type Ed25519_PointOf = TwistedEdwards "ed25519" AffinePoint
+type Ed25519_Point = Ed25519_PointOf Fq
 
 type Fl = Zp Ed25519_Scalar
 type Fq = Zp Ed25519_Base
@@ -40,16 +41,10 @@ instance Field field => TwistedEdwardsCurve "ed25519" field where
     negate fromConstant (121665 :: Natural)
         // fromConstant (121666 :: Natural)
 
-instance
-  ( Eq bool baseField
-  , FiniteField baseField
-  , Order baseField ~ Ed25519_Base
-  , scalarField ~ Fl
-  ) => SubgroupCurve "ed25519" bool baseField scalarField (TwistedEdwards "ed25519" AffinePoint) where
-    pointGen = pointXY
-      (fromConstant (15112221349535400772501151409588531511454012693041857206046113283949847762202 :: Natural))
-      (fromConstant (46316835694926478169428394003475163141307993866256225615783033603165251855960 :: Natural))
-
-instance Field field
-  => Scale Fl (TwistedEdwards "ed25519" AffinePoint field) where
-    scale n x = scale (toConstant n) x
+instance SubgroupCurve "ed25519" Bool Fq Fl Ed25519_PointOf where
+  pointGen = pointXY
+    (fromConstant (15112221349535400772501151409588531511454012693041857206046113283949847762202 :: Natural))
+    (fromConstant (46316835694926478169428394003475163141307993866256225615783033603165251855960 :: Natural))
+
+instance Scale Fl Ed25519_Point where
+  scale n x = scale (toConstant n) x
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs
@@ -4,27 +4,49 @@
 
 {-# OPTIONS_GHC -Wno-orphans #-}
 
-module ZkFold.Symbolic.Data.Ed25519 (AcEd25519) where
+module ZkFold.Symbolic.Data.Ed25519 (Ed25519_Point) where
 
-import           Control.DeepSeq                           (NFData, force)
+-- import           Control.DeepSeq                           (NFData, force)
 import           Prelude                                   (fromInteger, type (~), ($))
 import qualified Prelude                                   as P
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number
 import           ZkFold.Base.Algebra.EllipticCurve.Class
-import           ZkFold.Base.Algebra.EllipticCurve.Ed25519
-import qualified ZkFold.Base.Data.Vector                   as V
-import qualified ZkFold.Symbolic.Class                     as S
-import           ZkFold.Symbolic.Class                     (Symbolic)
+import           ZkFold.Base.Algebra.EllipticCurve.Ed25519 (Ed25519_Base, Ed25519_PointOf)
+-- import qualified ZkFold.Base.Data.Vector                   as V
+-- import qualified ZkFold.Symbolic.Class                     as S
+import           ZkFold.Symbolic.Class                     (Symbolic (..))
 import           ZkFold.Symbolic.Data.Bool
 import           ZkFold.Symbolic.Data.ByteString
-import           ZkFold.Symbolic.Data.Class
+-- import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Conditional
-import           ZkFold.Symbolic.Data.Eq
+-- import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.FFA
 import           ZkFold.Symbolic.Data.FieldElement
 
+type Ed25519_Point c = Ed25519_PointOf (FFA Ed25519_Base c)
+
+instance Symbolic c => SubgroupCurve "ed25519" (Bool c) (FFA Ed25519_Base c) (FieldElement c) Ed25519_PointOf where
+  pointGen = pointXY
+    (fromConstant (15112221349535400772501151409588531511454012693041857206046113283949847762202 :: Natural))
+    (fromConstant (46316835694926478169428394003475163141307993866256225615783033603165251855960 :: Natural))
+
+instance
+  ( Symbolic ctx
+  , a ~ BaseField ctx
+  , bits ~ NumberOfBits a
+  ) => Scale (FieldElement ctx) (Ed25519_Point ctx) where
+
+    scale sc x = sum $ P.zipWith (\b p -> bool @(Bool ctx) zero p (isSet bits b)) [upper, upper -! 1 .. 0] (P.iterate (\e -> e + e) x)
+        where
+            bits :: ByteString bits ctx
+            bits = ByteString $ binaryExpansion sc
+
+            upper :: Natural
+            upper = value @bits -! 1
+
+{-
 data AcEd25519 c
 
 -- | Ed25519 with @UInt 256 ArithmeticCircuit a@ as computational backend
@@ -110,3 +132,4 @@ acDouble25519 (Point x1 y1 isInf) =
         x3 = force $ (xy + xy) // (a * xsq + ysq)
         y3 = force $ (ysq - a * xsq) // (one + one - a * xsq  - ysq)
 
+-}