From 402cbc02e3dfc2d81a968fa0fa970d62d168ba4d Mon Sep 17 00:00:00 2001 From: Eitan Chatav Date: Thu, 9 Jan 2025 12:20:11 -0800 Subject: [PATCH] ed25519 --- .../Base/Algebra/EllipticCurve/Ed25519.hs | 27 ++++++------- .../src/ZkFold/Symbolic/Data/Ed25519.hs | 39 +++++++++++++++---- 2 files changed, 42 insertions(+), 24 deletions(-) diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs index 3b1b58b2..a69ad942 100644 --- 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 index 39986314..6ea66f0c 100644 --- 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) +-} \ No newline at end of file