-
Notifications
You must be signed in to change notification settings - Fork 7
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
Elliptic Curve algebra hierarchy proposal #411
Comments
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:
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. |
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. |
It's possible to simplify the proposal if we assume that
And similar for note: It may also make sense to make these ^ instances |
Seems reasonable. Adding @TurtlePU to the conversation. |
Hierarchy in general looks great! Is it possible to define class Planar field point | point -> field where
fieldXY :: field -> field -> point And same for So you'd have for example instance Planar field (Point curve field) |
^ 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 |
One example of an optimized point type would be extended twisted Edwards coordinates but they are a generic 4-tuple of fields. |
Point compression is a little more complicated than I thought. The parity bit is calculated differently for different curves like |
Naming question: Should Note: This class conceptually abstracts over n-dimensional projective spaces for all |
I guess |
-- (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. |
Subsequent to #404 assuming that the type family
BooleanOf
has been moved from theEllipticCurve
class to theConditional
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: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 thepointGen
method ofSubgroupCurve
and the method parameters of eitherWeierstrassCurve
orTwistedEdwardsCurve
and then you should be able to deriveAdditiveMonoid
,Scale
,EllipticCurve
,SymmetricCurve
etc. instances either viaWeierstrass
orTwistedEdwards
newtypes. Point types can be symbolic inputs withisValid = isOnCurve
.notes:
weierstrassA = 0
which is true for all of our examples and simplifies point doubling andisOnCurve
slightly.curve
type parameter is completely phantom. And unlike the current situation a Symboliccurve
doesn't need to know itsContext
since the choice offield
will. Thuscurve
can have any kind. I recommend havingcurve :: 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.The text was updated successfully, but these errors were encountered: