Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Secp256k1 #413

Merged
merged 16 commits into from
Dec 24, 2024
36 changes: 18 additions & 18 deletions symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
Original file line number Diff line number Diff line change
Expand Up @@ -67,18 +67,18 @@ instance EllipticCurve BLS12_381_G1 where

type BaseField BLS12_381_G1 = Fq

gen = point
pointGen = pointXY
0x17f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb
0x8b3f481e3aaa0f1a09e30ed741d8ae4fcf5e095d5d00af600db18cb2c04b3edd03cc744a2888ae40caa232946c5e7e1

add = addPoints

mul = pointMul

instance StandardEllipticCurve BLS12_381_G1 where
aParameter = zero
instance WeierstrassCurve BLS12_381_G1 where
weierstrassA = zero

bParameter = fromConstant (4 :: Natural)
weierstrassB = fromConstant (4 :: Natural)

------------------------------------ BLS12-381 G2 ------------------------------------

Expand All @@ -91,7 +91,7 @@ instance EllipticCurve BLS12_381_G2 where

type BaseField BLS12_381_G2 = Fq2

gen = point
pointGen = pointXY
(Ext2
0x24aa2b2f08f0a91260805272dc51051c6e47ad4fa403b02b4510b647ae3d1770bac0326a805bbefd48056c8c121bdb8
0x13e02b6052719f607dacd3a088274f65596bd0d09920b61ab5da61bbdc7f5049334cf11213945d57e5ac7d055d042b7e)
Expand All @@ -103,10 +103,10 @@ instance EllipticCurve BLS12_381_G2 where

mul = pointMul

instance StandardEllipticCurve BLS12_381_G2 where
aParameter = zero
instance WeierstrassCurve BLS12_381_G2 where
weierstrassA = zero

bParameter = fromConstant (4 :: Natural)
weierstrassB = fromConstant (4 :: Natural)

------------------------------------ Encoding ------------------------------------

Expand Down Expand Up @@ -143,7 +143,7 @@ instance Binary (Point BLS12_381_G1) where
infinite = testBit byte 1
if infinite then do
skip (if compressed then 47 else 95)
return inf
return pointInf
else do
let byteXhead = bitReverse8 $ clearBit (clearBit (clearBit byte 0) 1) 2
bytesXtail <- replicateM 47 getWord8
Expand All @@ -153,10 +153,10 @@ instance Binary (Point BLS12_381_G1) where
else do
bytesY <- replicateM 48 getWord8
let y = ofBytes bytesY
return (point x y)
return (pointXY x y)

instance Binary (PointCompressed BLS12_381_G1) where
put (PointCompressed x bigY isInf) =
instance Binary (CompressedPoint BLS12_381_G1) where
put (CompressedPoint x bigY isInf) =
if isInf then foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 47 0) else
let
flags = bitReverse8 $ if bigY then bit 0 .|. bit 2 else bit 0
Expand All @@ -168,7 +168,7 @@ instance Binary (PointCompressed BLS12_381_G1) where
infinite = testBit byte 1
if infinite then do
skip (if compressed then 47 else 95)
return inf
return pointInf
else do
let byteXhead = bitReverse8 $ clearBit (clearBit (clearBit byte 0) 1) 2
bytesXtail <- replicateM 47 getWord8
Expand Down Expand Up @@ -197,7 +197,7 @@ instance Binary (Point BLS12_381_G2) where
infinite = testBit byte 1
if infinite then do
skip (if compressed then 95 else 191)
return inf
return pointInf
else do
let byteX1head = bitReverse8 $ clearBit (clearBit (clearBit byte 0) 1) 2
bytesX1tail <- replicateM 47 getWord8
Expand All @@ -211,10 +211,10 @@ instance Binary (Point BLS12_381_G2) where
bytesY0 <- replicateM 48 getWord8
let y0 = ofBytes bytesY0
y1 = ofBytes bytesY1
return (point (Ext2 x0 x1) (Ext2 y0 y1))
return (pointXY (Ext2 x0 x1) (Ext2 y0 y1))

instance Binary (PointCompressed BLS12_381_G2) where
put (PointCompressed (Ext2 x0 x1) bigY isInf) =
instance Binary (CompressedPoint BLS12_381_G2) where
put (CompressedPoint (Ext2 x0 x1) bigY isInf) =
if isInf then foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 95 0) else
let
flags = bitReverse8 $ if bigY then bit 0 .|. bit 2 else bit 0
Expand All @@ -227,7 +227,7 @@ instance Binary (PointCompressed BLS12_381_G2) where
infinite = testBit byte 1
if infinite then do
skip (if compressed then 95 else 191)
return inf
return pointInf
else do
let byteX1head = bitReverse8 $ clearBit (clearBit (clearBit byte 0) 1) 2
bytesX1tail <- replicateM 47 getWord8
Expand Down
28 changes: 14 additions & 14 deletions symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BN254.hs
Original file line number Diff line number Diff line change
Expand Up @@ -70,13 +70,13 @@ data BN254_G1
instance EllipticCurve BN254_G1 where
type ScalarField BN254_G1 = Fr
type BaseField BN254_G1 = Fp
gen = point 1 2
pointGen = pointXY 1 2
add = addPoints
mul = pointMul

instance StandardEllipticCurve BN254_G1 where
aParameter = 0
bParameter = 3
instance WeierstrassCurve BN254_G1 where
weierstrassA = 0
weierstrassB = 3

------------------------------- bn254 G2 ---------------------------------------

Expand All @@ -85,17 +85,17 @@ data BN254_G2
instance EllipticCurve BN254_G2 where
type ScalarField BN254_G2 = Fr
type BaseField BN254_G2 = Fp2
gen = point
pointGen = pointXY
(Ext2 0x1800deef121f1e76426a00665e5c4479674322d4f75edadd46debd5cd992f6ed
0x198e9393920d483a7260bfb731fb5d25f1aa493335a9e71297e485b7aef312c2)
(Ext2 0x12c85ea5db8c6deb4aab71808dcb408fe3d1e7690c43d37b4ce6cc0166fa7daa
0x90689d0585ff075ec9e99ad690c3395bc4b313370b38ef355acdadcd122975b)
add = addPoints
mul = pointMul

instance StandardEllipticCurve BN254_G2 where
aParameter = zero
bParameter =
instance WeierstrassCurve BN254_G2 where
weierstrassA = zero
weierstrassB =
Ext2 0x2b149d40ceb8aaae81be18991be06ac3b5b4c5e559dbefa33267e6dc24a138e5
0x9713b03af0fed4cd2cafadeed8fdf4a74fa084e52d1852e4a2bd0685c315d2

Expand Down Expand Up @@ -133,22 +133,22 @@ instance Pairing BN254_G1 BN254_G2 where

instance Binary (Point BN254_G1) where
put (Point xp yp isInf) =
if isInf then put @(Point BN254_G1) (point zero zero) else put xp >> put yp
if isInf then put @(Point BN254_G1) (pointXY zero zero) else put xp >> put yp
get = do
xp <- get
yp <- get
return $
if xp == zero && yp == zero
then inf
else point xp yp
then pointInf
else pointXY xp yp

instance Binary (Point BN254_G2) where
put (Point xp yp isInf) =
if isInf then put @(Point BN254_G2) (point zero zero) else put xp >> put yp
if isInf then put @(Point BN254_G2) (pointXY zero zero) else put xp >> put yp
get = do
xp <- get
yp <- get
return $
if xp == zero && yp == zero
then inf
else point xp yp
then pointInf
else pointXY xp yp
76 changes: 38 additions & 38 deletions symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
Original file line number Diff line number Diff line change
Expand Up @@ -58,31 +58,31 @@ instance
) => SymbolicData (Point curve)

class Planar field plane where
point :: field -> field -> plane
pointXY :: field -> field -> plane

instance
( field ~ BaseField curve
, bool ~ BooleanOf curve
, BoolType bool
) => Planar field (Point curve) where
point x y = Point x y false
pointXY x y = Point x y false

class ProjectivePlanar plane where
inf :: plane
pointInf :: plane

instance
( field ~ BaseField curve
, BoolType (BooleanOf curve)
, AdditiveMonoid field
) => ProjectivePlanar (Point curve) where
inf = Point zero zero true
pointInf = Point zero zero true

instance
( field ~ BaseField curve
, BoolType (BooleanOf curve)
, AdditiveMonoid field
) => ProjectivePlanar (PointCompressed curve) where
inf = PointCompressed zero false true
) => ProjectivePlanar (CompressedPoint curve) where
pointInf = CompressedPoint zero false true

class
( BoolType (BooleanOf curve)
Expand All @@ -98,7 +98,7 @@ class
type BooleanOf curve :: Type
type BooleanOf curve = P.Bool

gen :: Point curve
pointGen :: Point curve

add :: Point curve -> Point curve -> Point curve

Expand Down Expand Up @@ -127,7 +127,7 @@ instance EllipticCurve curve => Scale Natural (Point curve) where
scale = natScale

instance EllipticCurve curve => AdditiveMonoid (Point curve) where
zero = inf
zero = pointInf

instance (EllipticCurve curve, AdditiveGroup (BaseField curve)) => Scale Integer (Point curve) where
scale = intScale
Expand All @@ -136,7 +136,7 @@ instance (EllipticCurve curve, AdditiveGroup (BaseField curve)) => AdditiveGroup
negate = pointNegate

instance (EllipticCurve curve, Arbitrary (ScalarField curve)) => Arbitrary (Point curve) where
arbitrary = arbitrary <&> (`mul` gen)
arbitrary = arbitrary <&> (`mul` pointGen)

class (EllipticCurve curve1, EllipticCurve curve2, ScalarField curve1 ~ ScalarField curve2,
P.Eq (TargetGroup curve1 curve2), MultiplicativeGroup (TargetGroup curve1 curve2),
Expand All @@ -153,8 +153,8 @@ pointAdd
pointAdd p@(Point x1 y1 isInf1) q@(Point x2 y2 isInf2) =
if isInf2 then p
else if isInf1 then q
else if x1 == x2 then inf
else point x3 y3
else if x1 == x2 then pointInf
else pointXY x3 y3
where
slope = (y1 - y2) // (x1 - x2)
x3 = slope * slope - x1 - x2
Expand All @@ -164,7 +164,7 @@ pointDouble
:: EllipticCurve curve
=> Field (BaseField curve)
=> Point curve -> Point curve
pointDouble (Point x y isInf) = if isInf then inf else point x' y'
pointDouble (Point x y isInf) = if isInf then pointInf else pointXY x' y'
where
slope = (x * x + x * x + x * x) // (y + y)
x' = slope * slope - x - x
Expand All @@ -182,7 +182,7 @@ pointNegate
:: EllipticCurve curve
=> AdditiveGroup (BaseField curve)
=> Point curve -> Point curve
pointNegate (Point x y isInf) = if isInf then inf else point x (negate y)
pointNegate (Point x y isInf) = if isInf then pointInf else pointXY x (negate y)

pointMul
:: forall curve s
Expand All @@ -196,76 +196,76 @@ pointMul
pointMul = natScale . fromBinary . castBits . binaryExpansion

-- An elliptic curve in standard form, y^2 = x^3 + a * x + b
class EllipticCurve curve => StandardEllipticCurve curve where
aParameter :: BaseField curve
bParameter :: BaseField curve

data PointCompressed curve = PointCompressed
{ _x :: BaseField curve
, _bigY :: BooleanOf curve
, _inf :: BooleanOf curve
class EllipticCurve curve => WeierstrassCurve curve where
weierstrassA :: BaseField curve
weierstrassB :: BaseField curve

data CompressedPoint curve = CompressedPoint
{ _x :: BaseField curve
, _bigY :: BooleanOf curve
, _isInf :: BooleanOf curve
} deriving Generic

pointCompressed :: BoolType (BooleanOf curve) => BaseField curve -> BooleanOf curve -> PointCompressed curve
pointCompressed x bigY = PointCompressed x bigY false
pointCompressed :: BoolType (BooleanOf curve) => BaseField curve -> BooleanOf curve -> CompressedPoint curve
pointCompressed x bigY = CompressedPoint x bigY false

instance
( EllipticCurve curve
, bool ~ BooleanOf curve
) => Conditional bool (PointCompressed curve)
) => Conditional bool (CompressedPoint curve)

instance
( EllipticCurve curve
, bool ~ BooleanOf curve
) => Eq bool (PointCompressed curve)
) => Eq bool (CompressedPoint curve)

instance
( EllipticCurve curve
, BooleanOf curve ~ P.Bool
) => P.Eq (PointCompressed curve) where
) => P.Eq (CompressedPoint curve) where
(==) = (==)
(/=) = (/=)

instance
( Show (BaseField curve)
, Conditional (BooleanOf curve) P.String
, Show (BooleanOf curve)
) => Show (PointCompressed curve) where
show (PointCompressed x bigY isInf) =
) => Show (CompressedPoint curve) where
show (CompressedPoint x bigY isInf) =
if isInf then "InfCompressed" else "(" ++ show x ++ ", " ++ show bigY ++ ")"

instance
( EllipticCurve curve
, AdditiveGroup (BaseField curve)
, Ord (BooleanOf curve) (BaseField curve)
, Arbitrary (ScalarField curve)
) => Arbitrary (PointCompressed curve) where
) => Arbitrary (CompressedPoint curve) where
arbitrary = compress <$> arbitrary

compress
:: ( AdditiveGroup (BaseField curve)
, EllipticCurve curve
, Ord (BooleanOf curve) (BaseField curve)
)
=> Point curve -> PointCompressed curve
=> Point curve -> CompressedPoint curve
compress = \case
Point x y isInf -> if isInf then inf else PointCompressed x (y > negate y) false
Point x y isInf -> if isInf then pointInf else CompressedPoint x (y > negate y) false

decompress
:: forall curve .
( StandardEllipticCurve curve
( WeierstrassCurve curve
, FiniteField (BaseField curve)
, Ord (BooleanOf curve) (BaseField curve)
)
=> PointCompressed curve -> Point curve
decompress (PointCompressed x bigY isInf) =
if isInf then inf else
let a = aParameter @curve
b = bParameter @curve
=> CompressedPoint curve -> Point curve
decompress (CompressedPoint x bigY isInf) =
if isInf then pointInf else
let a = weierstrassA @curve
b = weierstrassB @curve
p = order @(BaseField curve)
sqrt_ z = z ^ ((p + 1) `P.div` 2)
y' = sqrt_ (x * x * x + a * x + b)
y'' = negate y'
y = if bigY then max @(BooleanOf curve) y' y'' else min @(BooleanOf curve) y' y''
in
point x y
pointXY x y
Loading
Loading