Struct ProjectivePoint

pub struct ProjectivePoint {
    pub X: FieldElement51,
    pub Y: FieldElement51,
    pub Z: FieldElement51,
}

A ProjectivePoint is a point \((X:Y:Z)\) on the \(\mathbb P^2\) model of the curve. A point \((x,y)\) in the affine model corresponds to \((x:y:1)\).

More details on the relationships between the different curve models can be found in the module-level documentation.

Fields

X: FieldElement51

Y: FieldElement51

Z: FieldElement51

Implementations

impl ProjectivePoint

pub fn as_extended(&self) -> EdwardsPoint

Convert this point from the \( \mathbb P^2 \) model to the \( \mathbb P^3 \) model.

This costs \(3 \mathrm M + 1 \mathrm S\).

✓✓ Lean specification

theorem as_extended_spec
    (q : ProjectivePoint)
    (h_qX_bounds : ∀ i, i < 5 → (q.X[i]!).val < 2 ^ 54)
    (h_qY_bounds : ∀ i, i < 5 → (q.Y[i]!).val < 2 ^ 54)
    (h_qZ_bounds : ∀ i, i < 5 → (q.Z[i]!).val < 2 ^ 54) :
    as_extended q ⦃ (e : curve25519_dalek.edwards.EdwardsPoint) =>
      let X := Field51_as_Nat q.X
      let Y := Field51_as_Nat q.Y
      let Z := Field51_as_Nat q.Z
      let X' := Field51_as_Nat e.X
      let Y' := Field51_as_Nat e.Y
      let Z' := Field51_as_Nat e.Z
      let T' := Field51_as_Nat e.T
      X' % p = (X * Z) % p ∧
      Y' % p = (Y * Z) % p ∧
      Z' % p = (Z^2) % p ∧
      T' % p = (X * Y) % p ⦄

impl ProjectivePoint

pub fn double(&self) -> CompletedPoint

Double this point: return self + self

✓✓ Lean specification

theorem double_spec
    (q : ProjectivePoint) (hq_valid : q.IsValid) :
    ProjectivePoint.double q ⦃ (c : CompletedPoint) =>
      c.IsValid ∧ c.toPoint = q.toPoint + q.toPoint ⦄

Trait Implementations

impl Clone for ProjectivePoint

fn clone(&self) -> ProjectivePoint

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProjectivePoint

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

Formats the value using the given formatter.

impl Identity for ProjectivePoint

fn identity() -> ProjectivePoint

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

✓✓ Lean specification

theorem identity_spec :
    identity ⦃ (result : backend.serial.curve_models.ProjectivePoint) =>
      Field51_as_Nat result.X = 0 ∧
      Field51_as_Nat result.Y = 1 ∧
      Field51_as_Nat result.Z = 1 ⦄

impl Copy for ProjectivePoint