Elliptic Curve algebra hierarchy proposal

[echatav]

Subsequent to #404 assuming that the type family BooleanOf has been moved from the EllipticCurve class to the Conditional class, it will make sense to also reorganize the elliptic curve classes & datatypes which I have worked on in #396. The two "classes" of elliptic curves all of our examples (so far) fall into are either standard Weierstrass curves or twisted Edwards curves. Here is the proposal sketch:

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

class ProjectivePlanar point where
  pointInf :: point

class
  ( Field field
  , Conditional field
  , Planar (point curve)
  , AdditiveGroup (point curve field)
  ) => EllipticCurve point curve field where
    isOnCurve :: point curve field -> BooleanOf field

class
  ( EllipticCurve point curve baseField
  , FiniteField baseField
  , FiniteField scalarField
  , Scale scalarField (point curve baseField)
  ) => SubgroupCurve point curve baseField scalarField where
    pointGen :: point curve baseField

class EllipticCurve point curve field
  => SymmetricCurve pt point curve field | point -> pt, pt -> point where
    pointCompressed :: field -> BooleanOf field -> pt curve field
    compressPoint :: point curve field -> pt curve field
    decompressPoint :: pt curve field -> point curve field

class EllipticCurve point curve field
  => WeierstrassCurve point curve field where
    weierstrassA :: field
    weierstrassB :: field

class EllipticCurve point curve field
  => TwistedEdwardsCurve point curve field where
    twistedEdwardsA :: field
    twistedEdwardsD :: field

data Point curve field = Point
  { _x :: field
  , _y :: field
  , _isInf :: BooleanOf field
  } deriving Generic

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

data AffinePoint curve field = AffinePoint
  { _x :: field
  , _y :: field
  } deriving Generic

data CompressedAffinePoint curve field = CompressedAffinePoint
  { _bigX :: BooleanOf field
  , _y :: field
  } deriving Generic

newtype Weierstrass point curve field =
  Weierstrass {pointWeierstrass :: point curve field}

newtype TwistedEdwards point curve field =
  TwistedEdwards {pointTwistedEdwards :: point curve field}

Classes maximize polymorphism over different field and point types. All point types are generic records of kind (curve :: k) -> (field :: Type) -> Type so they work in Haskell or Symbolic. When defining instances for a curve, you just fill in the values for the pointGen method of SubgroupCurve and the method parameters of either WeierstrassCurve or TwistedEdwardsCurve and then you should be able to derive AdditiveMonoid, Scale, EllipticCurve, SymmetricCurve etc. instances either via Weierstrass or TwistedEdwards newtypes. Point types can be symbolic inputs with isValid = isOnCurve.

notes:

• the reason the compressed affine point is y-axis symmetric is because of the twisted Edwards form of the curve. Weierstrass curves are x-axis symmetric.
• We could also intro special case where weierstrassA = 0 which is true for all of our examples and simplifies point doubling and isOnCurve slightly.
• We can also introduce new point types like homogeneous coordinates and twisted coordinates.
• The curve type parameter is completely phantom. And unlike the current situation a Symbolic curve doesn't need to know its Context since the choice of field will. Thus curve can have any kind. I recommend having curve :: Symbol and using strings like "ed25519" and "secp256k1" etc. Then you don't need to define a datatype for the curve, it's just its name.

[vlasin]

A note on elliptic curves in Symbolic.

Generally speaking, we can define a circuit over any field. However, in practice, we are constrained by what we want to do with it. Most proving protocols require that the circuit's field is a scalar field of some cyclic group.

There are three possibilities for how the circuit's field can relate to the EC fields:

1. Both the base and scalar fields of the curve are foreign.
2. The circuit's field coincides with the scalar field.
3. The circuit's field coincides with the base field.

Options 1 and 2 make sense for any curve. Option 3 only makes sense for a pair of curves that form a cycle (e.g., Pasta curves) when the base field of one curve is the scalar field of another. So, for each curve we add to Symbolic, we should have those two or three options available.

[echatav]

So, for each curve we add to Symbolic, we should have those two or three options available.

In the current curve class, the fields are associated type families. That means you only get 1 option for the field for a given curve. By making the curve classes be multiparameter and parametric over the choice of field, we can instantiate multiple different field type options that make sense across both Haskell & Symbolic.

[echatav]

It's possible to simplify the proposal if we assume that Point is always on a Weierstrass curve and AffinePoint is always on a twisted Edwards curve. Then we don't need the Weierstrass & TwistedEdwards newtypes. We just need these instances instead:

instance WeierstrassCurve Point curve field => EllipticCurve Point curve field
instance WeierstrassCurve Point curve field => SymmetricCurve CompressedPoint Point curve field
instance WeierstrassCurve Point curve field => AdditiveSemigroup (Point curve field)
instance WeierstrassCurve Point curve field => AdditiveMonoid (Point curve field)
instance WeierstrassCurve Point curve field => AdditiveGroup (Point curve field)
instance WeierstrassCurve Point curve field => Scale Natural (Point curve field)
instance WeierstrassCurve Point curve field => Scale Integer (Point curve field)

And similar for TwistedEdwardsCurve AffinePoint.

note: It may also make sense to make these ^ instances {-# OVERLAPPABLE #-} so for specific curves you could overwrite them, for example, if you want to be able use projective Points on "ed25519".

[vlasin]

Seems reasonable. Adding @TurtlePU to the conversation.

[TurtlePU]

Hierarchy in general looks great!

Is it possible to define point in Planar to be just a Type, not a type operator? Like

class Planar field point | point -> field where
  fieldXY :: field -> field -> point

And same for *Curve classes. The reason I'm asking is the case when, for example, we might want to introduce some highly efficient point type which is specific for some curve and field, rather than a general datatype

So you'd have for example

instance Planar field (Point curve field)

[echatav]

^ I think both planar and curve classes can be subject to this change. When you introduce a highly efficient point type we can alter them accordingly. For now their designs are such that pointXY, pointInf, and pointCompressed "smart constructors" work (or don't) sensibly across the generic field-parameterized record point types Point, CompressedPoint, AffinePoint & CompressedAffinePoint.

[echatav]

One example of an optimized point type would be extended twisted Edwards coordinates but they are a generic 4-tuple of fields.

[echatav]

Point compression is a little more complicated than I thought. The parity bit is calculated differently for different curves like secp256k1, bls12-381 and ed25519 and so compression/decompression is not always the same algorithm even among Weierstrass curves. These are relevant for binary serializations which likewise don't standardize across curves.

[echatav]

Naming question: Should ProjectivePlanar just be Projective? Any dimension projective space has a point at infinity, pointInf. The only reason I don't like it is that "projective" is very overloaded terminology but I guess within the curve hierarchy & module the algebraic geometry context is clear. Maybe it should be PointAtInfinity? Actually, what really happens is that projective space of dimension n has a projective subspace of dimension n-1 at infinity!

Note: This class conceptually abstracts over n-dimensional projective spaces for all n : Natural by having a smart constructor for their 0-dimensional common point at infinity which is their intersection over their embeddings at infinity pointInf = KP0 < KP1 < KP2 < .... This point is not necessarily on any given planar curve but it is on any Weierstrass curve in KP2.

[vlasin]

I guess PointAtInfinity is fine.

[echatav]

-- (X : Y : Z) ~ (X/Z , Y/Z)
data HomogeneousPoint curve field = HomogeneousPoint
  { _x :: field
  , _y :: field
  , _z :: field
  } deriving Generic
instance Field field => PointAtInfinity (HomogeneousPoint curve field) where
  pointInf = HomogeneousPoint zero one zero

homogeneousCoords
  :: (Conditional field, Field field)
  => Point curve field
  -> HomogeneousPoint curve field
homogeneousCoords (Point x y isInf) =
  HomogeneousPoint x y (if isInf then zero else one)

inhomogeneousCoords
  :: (Eq field, Field field)
  => HomogeneousPoint curve field
  -> Point curve field
inhomogeneousCoords (HomogeneousPoint x y z) =
  if z == zero then Point x y true else Point (x/z) (y/z) false

-- (X : Y : T : Z)
-- X*Y = T*Z 
data ExtendedTwistedPoint curve field = ExtendedTwistedPoint
  { _x :: field
  , _y :: field
  , _t :: field
  , _z :: field
  } deriving Generic

^ these are potentially useful/optimized point (coordinate) types that can be instantiated for curve classes.

[echatav]

Instead of incurring being blocked by reorganizing logical hierarchy as in #404 and #421 one could add a bool parameter to this proposal. This construction feels a bit more complex but also more consistent. Should I do this instead?

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

class ProjectivePlanar point where
  pointInf :: point

class
  ( Field field
  , Conditional bool field
  , Planar (point curve)
  , AdditiveGroup (point curve field)
  ) => EllipticCurve point bool curve field where
    isOnCurve :: point curve field -> bool

class
  ( EllipticCurve point bool curve baseField
  , FiniteField baseField
  , FiniteField scalarField
  , Scale scalarField (point curve baseField)
  ) => SubgroupCurve point bool curve baseField scalarField where
    pointGen :: point curve baseField

class EllipticCurve (point bool) bool curve field
  => SymmetricCurve pt point bool curve field | point -> pt, pt -> point where
    pointCompressed :: field -> bool -> pt bool curve field
    compressPoint :: point bool curve field -> pt bool curve field
    decompressPoint :: pt bool curve field -> point bool curve field

class WeierstrassCurve curve field where
  weierstrassA :: field
  weierstrassB :: field

class MontgomeryCurve curve field where
  montgomeryA :: field
  montgomeryB :: field

class TwistedEdwardsCurve curve field where
  twistedEdwardsA :: field
  twistedEdwardsD :: field

data Point bool curve field = Point
  { _x :: field
  , _y :: field
  , _zBit :: bool
  } deriving Generic

data CompressedPoint bool curve field = CompressedPoint
  { _x :: field
  , _yBit :: bool
  , _zBit :: bool
  } deriving Generic

data AffinePoint curve field = AffinePoint
  { _x :: field
  , _y :: field
  } deriving Generic

data CompressedAffinePoint bool curve field = CompressedAffinePoint
  { _xBit :: bool
  , _y :: field
  } deriving Generic

data HomogeneousPoint curve field = HomogeneousPoint
  { _x :: field
  , _y :: field
  , _z :: field
  } deriving Generic

data TwistedExtendedPoint curve field = TwistedExtendedPoint
  { _x :: field
  , _y :: field
  , _t :: field
  , _z :: field
  } deriving Generic

newtype Weierstrass point curve field =
  Weierstrass {pointWeierstrass :: point curve field}

newtype Montgomery point curve field =
  Montgomery {pointMontgomery :: point curve field}

newtype TwistedEdwards point curve field =
  TwistedEdwards {pointTwistedEdwards :: point curve field}

[vlasin]

Instead of incurring being blocked by reorganizing logical hierarchy as in #404 and #421 one could add a bool parameter to this proposal. This construction feels a bit more complex but also more consistent. Should I do this instead?

The general idea that I propose to follow is that if there are several options of one type parameter corresponding to the same value of another type parameter, then multi-parametric type classes are justified. However, if there's only one option, then it makes sense to use associated type families.

In this case, there are many options for bool because it is determined by the base field of the context (not to be confused with the base field of an elliptic curve). That is to say, I agree with your proposal, @echatav. Let's do it.

[echatav]

I will start on this soon. With this modified proposal, elliptic curve hierarchy is not blocked by logical hierarchy changes (I think) so we can continue discussing the latter.

[TurtlePU]

    pointCompressed :: field -> bool -> pt bool curve field
    compressPoint :: point bool curve field -> pt bool curve field

I think that instead of being included as part of the point type, bool has to be inferred from field (this would happen anyway because EllipticCurve instances would surely need (==) :: field -> field -> bool)

Also I'd like to mention that this decision of whether to include bool in the point type or not would be deferred to the instance implementation stage if classes were defined for point :: Type instead of point :: Type -> k -> Type -> Type or something like this.

[vlasin]

I think that instead of being included as part of the point type, bool has to be inferred from field (this would happen anyway because EllipticCurve instances would surely need (==) :: field -> field -> bool)

Meaning that if we are working with a symbolic point type, we get the corresponding symbolic bool, and if we are working with, say, Zp p, we get the Haskell bool?

[TurtlePU]

Meaning that if we are working with a symbolic point type, we get the corresponding symbolic bool, and if we are working with, say, Zp p, we get the Haskell bool?

Exactly!