Struct CompletedPoint

pub struct CompletedPoint {
    pub X: FieldElement51,
    pub Y: FieldElement51,
    pub Z: FieldElement51,
    pub T: FieldElement51,
}

A CompletedPoint is a point \(((X:Z), (Y:T))\) on the \(\mathbb P^1 \times \mathbb P^1 \) model of the curve. A point (x,y) in the affine model corresponds to \( ((x:1),(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

T: FieldElement51

Implementations

impl CompletedPoint

pub fn as_projective(&self) -> ProjectivePoint

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

This costs \(3 \mathrm M \).

✓✓ Lean specification

theorem as_projective_spec
    (q : CompletedPoint) (hq_valid : q.IsValid) :
    as_projective q ⦃ (proj : ProjectivePoint) =>
      proj.IsValid ∧ proj.toPoint = q.toPoint ⦄

pub fn as_extended(&self) -> EdwardsPoint

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

This costs \(4 \mathrm M \).

✓✓ Lean specification

theorem as_extended_spec (q : CompletedPoint)
    (h_q_Valid : q.IsValid) :
    as_extended q ⦃ (e : edwards.EdwardsPoint) =>
      let X := Field51_as_Nat q.X
      let Y := Field51_as_Nat q.Y
      let Z := Field51_as_Nat q.Z
      let T := Field51_as_Nat q.T
      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 * T) % p ∧
      Y' % p = (Y * Z) % p ∧
      Z' % p = (Z * T) % p ∧
      T' % p = (X * Y) % p ∧
      (∀ i < 5, e.X[i]!.val < 2 ^ 52) ∧
      (∀ i < 5, e.Y[i]!.val < 2 ^ 52) ∧
      (∀ i < 5, e.Z[i]!.val < 2 ^ 52) ∧
      (∀ i < 5, e.T[i]!.val < 2 ^ 52) ∧
      e.IsValid ∧
      e.toPoint = q.toPoint ⦄

Trait Implementations

impl Clone for CompletedPoint

fn clone(&self) -> CompletedPoint

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CompletedPoint

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

Formats the value using the given formatter.

impl Copy for CompletedPoint