Skip to content

Conversation

@lassebramer
Copy link
Contributor

A generic implementation of elliptic curves of the weiestrass form.

It supports all 'basic' arithmetic which should be the same across all curves.

Arithmatic is taken from here and the bls curve implementation

Testing is done on the Pallas curve with all the same tests as in the bls implementation.

The linter gives no warnings

cargo hax into coq gives

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> weierstrass-curves/src/weierstrass.rs:160:1
    |
160 | / impl<T: Numeric + NumericCopy + PartialEq + Integer + hacspec_lib::Div<Output = T>>
161 | |     Add<EllipticCurvePoint<T>> for EllipticCurvePoint<T>
162 | | {
163 | |     type Output = Self;
...   |
197 | |     }
198 | | }
    | |_^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> weierstrass-curves/src/weierstrass.rs:200:1
    |
200 | / impl<
201 | |         U: Numeric + NumericCopy + PartialEq + Integer + hacspec_lib::Div<Output = U>,
202 | |         T: Numeric + NumericCopy + PartialEq + Integer + hacspec_lib::Div<Output = T>,
203 | |     > Mul<U> for EllipticCurvePoint<T>
...   |
225 | |     }
226 | | }
    | |_^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node false
   --> weierstrass-curves/src/weierstrass.rs:228:1
    |
228 | / impl<T: Numeric + NumericCopy + PartialEq + Integer> PartialEq for EllipticCurvePoint<T> {
229 | |     /// Checks if two curve points are identical, regardless of underlying curve.
230 | |     fn eq(&self, other: &Self) -> bool {
231 | |         if self.x != other.x {
...   |
241 | |     }
242 | | }
    | |_^

cargo hax into fstar gives

error[CE0001]: (Diagnostics.Context.Backend FStar): something is not implemented yet.
               anonymous impl
  --> weierstrass-curves/src/weierstrass.rs:18:1
   |
18 | / impl<T> WeiestrassCurve<T> {
19 | |     /// Create a weierstrass curve
20 | |     ///
21 | |     /// The form of the weierstrass curve is:
...  |
51 | |     }
52 | | }
   | |_^

error[CE0001]: (Diagnostics.Context.Backend FStar): something is not implemented yet.
               anonymous impl
   --> weierstrass-curves/src/weierstrass.rs:76:1
    |
76  | / impl<T: Numeric + NumericCopy + PartialEq + Integer + hacspec_lib::Div<Output = T>>
77  | |     EllipticCurvePoint<T>
78  | | {
79  | |     /// Create point on a weierstrass curve.
...   |
157 | |     }
158 | | }
    | |_^

@spitters
Copy link
Collaborator

@cmester0 I guess these error messages are expected?

isPointAtInfinity: bool,
curve: WeiestrassCurve<T>,
}

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Have you considered raising an exception instead of using the point at infinity as a default value?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that was the plan but i don't think that is hacspec complient, might be in v2?

@spitters
Copy link
Collaborator

Code looks clean. This is a nice abstraction.

@franziskuskiefer do you want the generated rust-doc in a specific place?

@lassebramer
Copy link
Contributor Author

I can see that, due to my poor organization skills, this has already been merged into the specs folder through #4, so this should probably just be closed:)

@franziskuskiefer
Copy link
Member

I can see that, due to my poor organization skills, this has already been merged into the specs folder through #4, so this should probably just be closed:)

Yeah, this is in already. If there's anything you want to update, just open another PR.

@franziskuskiefer do you want the generated rust-doc in a specific place?

Generated rustdocs go on the gh-pages branch, which is deployed to https://hacspec.org/specs/hacspec_weierstrass/index.html

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants