Struct EdwardsPoint

pub struct EdwardsPoint { /* private fields */ }

An EdwardsPoint represents a point on the Edwards form of Curve25519.

Implementations

impl EdwardsPoint

pub fn to_montgomery(&self) -> MontgomeryPoint

Convert this EdwardsPoint on the Edwards model to the corresponding MontgomeryPoint on the Montgomery model.

This function has one exceptional case; the identity point of the Edwards curve is sent to the 2-torsion point \((0,0)\) on the Montgomery curve.

Note that this is a one-way conversion, since the Montgomery model does not retain sign information.

✓✓ Lean specification

theorem to_montgomery_spec (self : EdwardsPoint)
    (hvalid : self.IsValid)
    (h_Y_bounds : ∀ i < 5, self.Y[i]!.val < 2 ^ 53)
    (h_Z_bounds : ∀ i < 5, self.Z[i]!.val < 2 ^ 53) :
    to_montgomery self ⦃ (mp : montgomery.MontgomeryPoint) =>
      let Y := Field51_as_Nat self.Y
      let Z := Field51_as_Nat self.Z
      let u := U8x32_as_Nat mp
      if Z % p = Y % p then
        u % p = 0 ∧ (∀ n : ℕ, fromEdwards (n • self.toPoint) = 0)
      else
        ((u * Z) % p = (u * Y + (Z + Y)) % p) ∧
        abs_montgomery (fromEdwards self.toPoint) = MontgomeryPoint.mkPoint mp ⦄

pub fn to_montgomery_batch(eds: &[Self]) -> Vec<MontgomeryPoint>

Available on crate feature alloc and non-verify only.

Converts a large batch of points to Edwards at once. This has the same behavior on identity elements as Self::to_montgomery.

pub fn compress(&self) -> CompressedEdwardsY

Compress this point to CompressedEdwardsY format.

✓✓ Lean specification

theorem compress_spec (self : EdwardsPoint) (hself : self.IsValid) :
    compress self ⦃ (result : CompressedEdwardsY) =>
      U8x32_as_Nat result = compress_edwards_pure self.toPoint ⦄

pub fn compress_batch(inputs: &[EdwardsPoint]) -> Vec<CompressedEdwardsY>

Available on crate feature alloc and non-verify only.

Compress several EdwardsPoints into CompressedEdwardsY format, using a batch inversion for a significant speedup.

impl EdwardsPoint

pub fn mul_base(scalar: &Scalar) -> Self

Fixed-base scalar multiplication by the Ed25519 base point.

Uses precomputed basepoint tables when the precomputed-tables feature is enabled, trading off increased code size for ~4x better performance.

✓✓ Lean specification

theorem mul_base_spec (scalar : scalar.Scalar)
    (h_s_canonical : U8x32_as_Nat scalar.bytes < 2 ^ 255) :
    mul_base scalar ⦃ (res : EdwardsPoint) =>
      EdwardsPoint.IsValid res ∧
      res.toPoint = (U8x32_as_Nat scalar.bytes) • _root_.Edwards.basepoint ⦄

pub fn mul_clamped(self, bytes: [u8; 32]) -> Self

Multiply this point by clamp_integer(bytes). For a description of clamping, see clamp_integer.

✓✓ Lean specification

theorem mul_clamped_spec (self : EdwardsPoint) (bytes : Array U8 32#usize)
    (h_self_valid : self.IsValid) :
    mul_clamped self bytes ⦃ (result : EdwardsPoint) =>
      result.IsValid ∧
      (∃ clamped_scalar,
        h ∣ U8x32_as_Nat clamped_scalar ∧
        U8x32_as_Nat clamped_scalar < 2 ^ 255 ∧
        2 ^ 254 ≤ U8x32_as_Nat clamped_scalar ∧
        result.toPoint = (U8x32_as_Nat clamped_scalar) • self.toPoint) ⦄

pub fn mul_base_clamped(bytes: [u8; 32]) -> Self

Multiply the basepoint by clamp_integer(bytes). For a description of clamping, see clamp_integer.

✓✓ Lean specification

theorem mul_base_clamped_spec (bytes : Array U8 32#usize) :
    mul_base_clamped bytes ⦃ (result : EdwardsPoint) =>
      EdwardsPoint.IsValid result ∧
      (∃ clamped_scalar,
        h ∣ U8x32_as_Nat clamped_scalar ∧
        U8x32_as_Nat clamped_scalar < 2 ^ 255 ∧
        2 ^ 254 ≤ U8x32_as_Nat clamped_scalar ∧
        result.toPoint = ((U8x32_as_Nat clamped_scalar) • _root_.Edwards.basepoint)) ⦄

impl EdwardsPoint

pub fn vartime_double_scalar_mul_basepoint( a: &Scalar, A: &EdwardsPoint, b: &Scalar, ) -> EdwardsPoint

Available on non-verify only.

Compute \(aA + bB\) in variable time, where \(B\) is the Ed25519 basepoint.

impl EdwardsPoint

pub fn mul_by_cofactor(&self) -> EdwardsPoint

Multiply by the cofactor: return \([8]P\).

✓✓ Lean specification

theorem mul_by_cofactor_spec (self : EdwardsPoint) (hself : self.IsValid) :
    mul_by_cofactor self ⦃ (result : EdwardsPoint) =>
      result.IsValid ∧
      result.toPoint = h • self.toPoint ⦄

pub fn is_small_order(&self) -> bool

Determine if this point is of small order.

Return

• true if self is in the torsion subgroup \( \mathcal E[8] \);
• false if self is not in the torsion subgroup \( \mathcal E[8] \).

Example

use curve25519_dalek::constants;

// Generator of the prime-order subgroup
let P = constants::ED25519_BASEPOINT_POINT;
// Generator of the torsion subgroup
let Q = constants::EIGHT_TORSION[1];

// P has large order
assert_eq!(P.is_small_order(), false);

// Q has small order
assert_eq!(Q.is_small_order(), true);

✓✓ Lean specification

theorem is_small_order_spec (self : EdwardsPoint) (hself : self.IsValid) :
    is_small_order self ⦃ (result : Bool) =>
      (result ↔ h • self.toPoint = 0) ⦄

pub fn is_torsion_free(&self) -> bool

Determine if this point is “torsion-free”, i.e., is contained in the prime-order subgroup.

Return

• true if self has zero torsion component and is in the prime-order subgroup;
• false if self has a nonzero torsion component and is not in the prime-order subgroup.

Example

use curve25519_dalek::constants;

// Generator of the prime-order subgroup
let P = constants::ED25519_BASEPOINT_POINT;
// Generator of the torsion subgroup
let Q = constants::EIGHT_TORSION[1];

// P is torsion-free
assert_eq!(P.is_torsion_free(), true);

// P + Q is not torsion-free
assert_eq!((P+Q).is_torsion_free(), false);

✓✓ Lean specification

theorem is_torsion_free_spec
    (self : EdwardsPoint) (hself : self.IsValid) :
    is_torsion_free self ⦃ (result : Bool) =>
      (result ↔ L • self.toPoint = 0) ⦄

Trait Implementations

impl<'a> Add<&'a AffineNielsPoint> for &EdwardsPoint

type Output = CompletedPoint

The resulting type after applying the + operator.

fn add(self, other: &'a AffineNielsPoint) -> CompletedPoint

Performs the + operation.

impl<'a> Add<&'a EdwardsPoint> for &EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the + operator.

fn add(self, other: &'a EdwardsPoint) -> EdwardsPoint

Performs the + operation.

✓✓ Lean specification

theorem add_spec
    (self : edwards.EdwardsPoint)
    (other : backend.serial.curve_models.AffineNielsPoint)
    (h_selfX_bounds : ∀ i, i < 5 → (self.X[i]!).val < 2 ^ 53)
    (h_selfY_bounds : ∀ i, i < 5 → (self.Y[i]!).val < 2 ^ 53)
    (h_selfZ_bounds : ∀ i, i < 5 → (self.Z[i]!).val < 2 ^ 53)
    (h_selfT_bounds : ∀ i, i < 5 → (self.T[i]!).val < 2 ^ 53)
    (h_otherYpX_bounds : ∀ i, i < 5 → (other.y_plus_x[i]!).val < 2 ^ 53)
    (h_otherYmX_bounds : ∀ i, i < 5 → (other.y_minus_x[i]!).val < 2 ^ 53)
    (h_otherXY2d_bounds : ∀ i, i < 5 → (other.xy2d[i]!).val < 2 ^ 53) :
    Shared0EdwardsPoint.Insts.CoreOpsArithAddSharedAAffineNielsPointCompletedPoint.add self other
      ⦃ (c : CompletedPoint) =>
      let X := Field51_as_Nat self.X
      let Y := Field51_as_Nat self.Y
      let Z := Field51_as_Nat self.Z
      let T := Field51_as_Nat self.T
      let YpX := Field51_as_Nat other.y_plus_x
      let YmX := Field51_as_Nat other.y_minus_x
      let XY2D := Field51_as_Nat other.xy2d
      let X' := Field51_as_Nat c.X
      let Y' := Field51_as_Nat c.Y
      let Z' := Field51_as_Nat c.Z
      let T' := Field51_as_Nat c.T
      (X' + Y * YmX) % p = (((Y + X) * YpX) + X * YmX) % p ∧
      (Y' + X * YmX) % p = (((Y + X) * YpX) + Y  * YmX) % p ∧
      Z' % p = ((2 * Z) + (T * XY2D)) % p ∧
      (T' + (T * XY2D)) % p = (2 * Z) % p ⦄

impl<'b> Add<&'b EdwardsPoint> for EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the + operator.

fn add(self, rhs: &'b EdwardsPoint) -> EdwardsPoint

Performs the + operation.

impl<'a> Add<&'a ProjectiveNielsPoint> for &EdwardsPoint

type Output = CompletedPoint

The resulting type after applying the + operator.

fn add(self, other: &'a ProjectiveNielsPoint) -> CompletedPoint

Performs the + operation.

impl<'a> Add<EdwardsPoint> for &'a EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the + operator.

fn add(self, rhs: EdwardsPoint) -> EdwardsPoint

Performs the + operation.

impl Add for EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the + operator.

fn add(self, rhs: EdwardsPoint) -> EdwardsPoint

Performs the + operation.

impl<'a> AddAssign<&'a EdwardsPoint> for EdwardsPoint

fn add_assign(&mut self, _rhs: &'a EdwardsPoint)

Performs the += operation.

impl AddAssign for EdwardsPoint

fn add_assign(&mut self, rhs: EdwardsPoint)

Performs the += operation.

impl Clone for EdwardsPoint

fn clone(&self) -> EdwardsPoint

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl ConditionallySelectable for EdwardsPoint

fn conditional_select( a: &EdwardsPoint, b: &EdwardsPoint, choice: Choice, ) -> EdwardsPoint

Select a or b according to choice.

✓✓ Lean specification

theorem conditional_select_spec (a b : EdwardsPoint) (choice : subtle.Choice) :
    conditional_select a b choice ⦃ (result : EdwardsPoint) =>
      result = if choice.val = 1#u8 then b else a ⦄

fn conditional_assign(&mut self, other: &Self, choice: Choice)

Conditionally assign other to self, according to choice.

fn conditional_swap(a: &mut Self, b: &mut Self, choice: Choice)

Conditionally swap self and other if choice == 1; otherwise, reassign both unto themselves.

impl ConstantTimeEq for EdwardsPoint

fn ct_eq(&self, other: &EdwardsPoint) -> Choice

Determine if two items are equal.

✓✓ Lean specification

theorem ct_eq_spec (self other : EdwardsPoint)
    (h_self_X : ∀ i, i < 5 → self.X.val[i]!.val ≤ 2 ^ 53)
    (h_self_Y : ∀ i, i < 5 → self.Y.val[i]!.val ≤ 2 ^ 53)
    (h_self_Z : ∀ i, i < 5 → self.Z.val[i]!.val ≤ 2 ^ 53)
    (h_other_X : ∀ i, i < 5 → other.X.val[i]!.val ≤ 2 ^ 53)
    (h_other_Y : ∀ i, i < 5 → other.Y.val[i]!.val ≤ 2 ^ 53)
    (h_other_Z : ∀ i, i < 5 → other.Z.val[i]!.val ≤ 2 ^ 53) :
    ct_eq self other ⦃ (c : subtle.Choice) =>
      (c = Choice.one ↔
        (Field51_as_Nat self.X * Field51_as_Nat other.Z)
          ≡ (Field51_as_Nat other.X * Field51_as_Nat self.Z) [MOD p] ∧
        (Field51_as_Nat self.Y * Field51_as_Nat other.Z)
          ≡ (Field51_as_Nat other.Y * Field51_as_Nat self.Z) [MOD p]) ∧
      (self.IsValid → other.IsValid → (c = Choice.one ↔ self.toPoint = other.toPoint)) ⦄

fn ct_ne(&self, other: &Self) -> Choice

Determine if two items are NOT equal.

impl Debug for EdwardsPoint

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for EdwardsPoint

fn default() -> EdwardsPoint

Returns the “default value” for a type.

impl Identity for EdwardsPoint

fn identity() -> EdwardsPoint

Returns the identity element of the curve. Can be used as a constructor.

✓✓ Lean specification

theorem identity_spec :
    identity ⦃ (result : EdwardsPoint) =>
      Field51_as_Nat result.X = 0 ∧
      Field51_as_Nat result.Y = 1 ∧
      Field51_as_Nat result.Z = 1 ∧
      Field51_as_Nat result.T = 0 ∧
      result.IsValid ∧
      result.toPoint = 0 ⦄

impl<'a> Mul<&'a EdwardsPoint> for &Scalar

fn mul(self, point: &'a EdwardsPoint) -> EdwardsPoint

Scalar multiplication: compute scalar * self.

For scalar multiplication of a basepoint, EdwardsBasepointTable is approximately 4x faster.

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'b> Mul<&'b EdwardsPoint> for Scalar

type Output = EdwardsPoint

The resulting type after applying the * operator.

fn mul(self, rhs: &'b EdwardsPoint) -> EdwardsPoint

Performs the * operation.

impl<'a> Mul<&'a Scalar> for &EdwardsPoint

fn mul(self, scalar: &'a Scalar) -> EdwardsPoint

Scalar multiplication: compute scalar * self.

For scalar multiplication of a basepoint, EdwardsBasepointTable is approximately 4x faster.

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'b> Mul<&'b Scalar> for EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the * operator.

fn mul(self, rhs: &'b Scalar) -> EdwardsPoint

Performs the * operation.

✓✓ Lean specification

theorem mul_spec
    (self : edwards.EdwardsPoint) (scalar : scalar.Scalar)
    (h_scalar_canonical : U8x32_as_Nat scalar.bytes < 2 ^ 255)
    (h_self_valid : self.IsValid) :
    mul self scalar ⦃ (result : edwards.EdwardsPoint) =>
      result.IsValid ∧
      result.toPoint = (U8x32_as_Nat scalar.bytes) • self.toPoint ⦄

impl<'a> Mul<EdwardsPoint> for &'a Scalar

type Output = EdwardsPoint

The resulting type after applying the * operator.

fn mul(self, rhs: EdwardsPoint) -> EdwardsPoint

Performs the * operation.

impl Mul<EdwardsPoint> for Scalar

type Output = EdwardsPoint

The resulting type after applying the * operator.

fn mul(self, rhs: EdwardsPoint) -> EdwardsPoint

Performs the * operation.

impl<'a> Mul<Scalar> for &'a EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the * operator.

fn mul(self, rhs: Scalar) -> EdwardsPoint

Performs the * operation.

impl Mul<Scalar> for EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the * operator.

fn mul(self, rhs: Scalar) -> EdwardsPoint

Performs the * operation.

impl<'a> MulAssign<&'a Scalar> for EdwardsPoint

fn mul_assign(&mut self, scalar: &'a Scalar)

Performs the *= operation.

impl MulAssign<Scalar> for EdwardsPoint

fn mul_assign(&mut self, rhs: Scalar)

Performs the *= operation.

impl MultiscalarMul for EdwardsPoint

Available on crate feature alloc only.

type Point = EdwardsPoint

The type of point being multiplied, e.g., RistrettoPoint.

fn multiscalar_mul<I, J>(scalars: I, points: J) -> EdwardsPoint

where I: IntoIterator, I::Item: Borrow<Scalar>, J: IntoIterator, J::Item: Borrow<EdwardsPoint>,

Given an iterator of (possibly secret) scalars and an iterator of public points, compute $$ Q = c_1 P_1 + \cdots + c_n P_n. $$

impl Neg for &EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the - operator.

fn neg(self) -> EdwardsPoint

Performs the unary - operation.

✓✓ Lean specification

theorem neg_spec
    (self : edwards.EdwardsPoint)
    (h_self_valid : self.IsValid) :
    neg self ⦃ (result : edwards.EdwardsPoint) =>
      result.IsValid ∧
      result.toPoint = -self.toPoint ⦄

impl Neg for EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the - operator.

fn neg(self) -> EdwardsPoint

Performs the unary - operation.

impl PartialEq for EdwardsPoint

fn eq(&self, other: &EdwardsPoint) -> bool

Tests for self and other values to be equal, and is used by ==.

✓✓ Lean specification

theorem eq_spec (self other : EdwardsPoint)
    (h_self_valid : self.IsValid) (h_other_valid : other.IsValid) :
    eq self other ⦃ (result : Bool) =>
      result = true ↔ self.toPoint = other.toPoint ⦄

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<'a> Sub<&'a AffineNielsPoint> for &EdwardsPoint

type Output = CompletedPoint

The resulting type after applying the - operator.

fn sub(self, other: &'a AffineNielsPoint) -> CompletedPoint

Performs the - operation.

impl<'a> Sub<&'a EdwardsPoint> for &EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the - operator.

fn sub(self, other: &'a EdwardsPoint) -> EdwardsPoint

Performs the - operation.

✓✓ Lean specification

theorem sub_spec
    (self : edwards.EdwardsPoint)
    (other : backend.serial.curve_models.AffineNielsPoint)
    (h_selfX_bounds : ∀ i, i < 5 → (self.X[i]!).val < 2 ^ 53)
    (h_selfY_bounds : ∀ i, i < 5 → (self.Y[i]!).val < 2 ^ 53)
    (h_selfZ_bounds : ∀ i, i < 5 → (self.Z[i]!).val < 2 ^ 53)
    (h_selfT_bounds : ∀ i, i < 5 → (self.T[i]!).val < 2 ^ 53)
    (h_otherYpX_bounds : ∀ i, i < 5 → (other.y_plus_x[i]!).val < 2 ^ 53)
    (h_otherYmX_bounds : ∀ i, i < 5 → (other.y_minus_x[i]!).val < 2 ^ 53)
    (h_otherXY2d_bounds : ∀ i, i < 5 → (other.xy2d[i]!).val < 2 ^ 53) :
    Shared0EdwardsPoint.Insts.CoreOpsArithSubSharedAAffineNielsPointCompletedPoint.sub self other
      ⦃ (c : CompletedPoint) =>
      let X := Field51_as_Nat self.X
      let Y := Field51_as_Nat self.Y
      let Z := Field51_as_Nat self.Z
      let T := Field51_as_Nat self.T
      let YpX := Field51_as_Nat other.y_plus_x
      let YmX := Field51_as_Nat other.y_minus_x
      let XY2D := Field51_as_Nat other.xy2d
      let X' := Field51_as_Nat c.X
      let Y' := Field51_as_Nat c.Y
      let Z' := Field51_as_Nat c.Z
      let T' := Field51_as_Nat c.T
      (X' + Y * YpX) % p = (((Y + X) * YmX) + X * YpX) % p ∧
      (Y' + X * YpX) % p = (((Y + X) * YmX) + Y  * YpX) % p ∧
      (Z' + (T * XY2D)) % p = (2 * Z) % p ∧
      T' % p = ((2 * Z) + (T * XY2D)) % p ⦄

impl<'b> Sub<&'b EdwardsPoint> for EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the - operator.

fn sub(self, rhs: &'b EdwardsPoint) -> EdwardsPoint

Performs the - operation.

impl<'a> Sub<&'a ProjectiveNielsPoint> for &EdwardsPoint

type Output = CompletedPoint

The resulting type after applying the - operator.

fn sub(self, other: &'a ProjectiveNielsPoint) -> CompletedPoint

Performs the - operation.

impl<'a> Sub<EdwardsPoint> for &'a EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the - operator.

fn sub(self, rhs: EdwardsPoint) -> EdwardsPoint

Performs the - operation.

impl Sub for EdwardsPoint

type Output = EdwardsPoint

The resulting type after applying the - operator.

fn sub(self, rhs: EdwardsPoint) -> EdwardsPoint

Performs the - operation.

impl<'a> SubAssign<&'a EdwardsPoint> for EdwardsPoint

fn sub_assign(&mut self, _rhs: &'a EdwardsPoint)

Performs the -= operation.

impl SubAssign for EdwardsPoint

fn sub_assign(&mut self, rhs: EdwardsPoint)

Performs the -= operation.

impl<T> Sum<T> for EdwardsPoint

where T: Borrow<EdwardsPoint>,

fn sum<I>(iter: I) -> Self

where I: Iterator<Item = T>,

Takes an iterator and generates Self from the elements by “summing up” the items.

impl VartimeMultiscalarMul for EdwardsPoint

Available on crate feature alloc only.

type Point = EdwardsPoint

The type of point being multiplied, e.g., RistrettoPoint.

fn optional_multiscalar_mul<I, J>(scalars: I, points: J) -> Option<EdwardsPoint>

where I: IntoIterator, I::Item: Borrow<Scalar>, J: IntoIterator<Item = Option<EdwardsPoint>>,

Given an iterator of public scalars and an iterator of Options of points, compute either Some(Q), where $$ Q = c_1 P_1 + \cdots + c_n P_n, $$ if all points were Some(P_i), or else return None.

fn vartime_multiscalar_mul<I, J>(scalars: I, points: J) -> Self::Point

where I: IntoIterator, I::Item: Borrow<Scalar>, J: IntoIterator, J::Item: Borrow<Self::Point>, Self::Point: Clone,

Given an iterator of public scalars and an iterator of public points, compute $$ Q = c_1 P_1 + \cdots + c_n P_n, $$ using variable-time operations.

impl Zeroize for EdwardsPoint

Available on crate feature zeroize only.

fn zeroize(&mut self)

Reset this EdwardsPoint to the identity element.

impl Copy for EdwardsPoint

impl Eq for EdwardsPoint