Struct MontgomeryPoint

pub struct MontgomeryPoint(pub [u8; 32]);

Holds the \(u\)-coordinate of a point on the Montgomery form of Curve25519 or its twist.

Tuple Fields

0: [u8; 32]

Implementations

impl MontgomeryPoint

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

Fixed-base scalar multiplication (i.e. multiplication by the base point).

✓✓ Lean specification

theorem mul_base_spec (scalar : scalar.Scalar)
    (h_s_canonical : U8x32_as_Nat scalar.bytes < 2 ^ 255) :
    mul_base scalar ⦃ (result : MontgomeryPoint) =>
      let ep := (U8x32_as_Nat scalar.bytes) • _root_.Edwards.basepoint
      if ep.y = 1 then
        MontgomeryPoint.mkPoint result = T_point
      else
        MontgomeryPoint.mkPoint result = abs_montgomery
          ((U8x32_as_Nat scalar.bytes) • (fromEdwards _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 (P : MontgomeryPoint) (bytes : Array U8 32#usize)
    (hP_bound : U8x32_as_Nat P < 2 ^ 255) :
    mul_clamped P bytes ⦃ (result : MontgomeryPoint) =>
      (∃ clamped_scalar,
      h ∣ U8x32_as_Nat clamped_scalar ∧
      U8x32_as_Nat clamped_scalar < 2 ^ 255 ∧
      2 ^ 254 ≤ U8x32_as_Nat clamped_scalar ∧
      let m := (U8x32_as_Nat clamped_scalar)
      MontgomeryPoint.mkPoint result = m • (MontgomeryPoint.mkPoint P)) ⦄

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 : MontgomeryPoint) =>
      (∃ clamped_scalar_nat,
      h ∣ clamped_scalar_nat ∧
      clamped_scalar_nat < 2 ^ 255 ∧
      2 ^ 254 ≤ clamped_scalar_nat ∧
      (if (clamped_scalar_nat • Edwards.basepoint).y = 1 then
          MontgomeryPoint.mkPoint result = T_point
        else MontgomeryPoint.mkPoint result =
          abs_montgomery (clamped_scalar_nat • fromEdwards _root_.Edwards.basepoint))) ⦄

pub fn mul_bits_be(&self, bits: impl Iterator<Item = bool>) -> MontgomeryPoint

Available on non-verify only.

Given self \( = u_0(P) \), and a big-endian bit representation of an integer \(n\), return \( u_0([n]P) \). This is constant time in the length of bits.

NOTE: You probably do not want to use this function. Almost every protocol built on Curve25519 uses clamped multiplication, explained here. When in doubt, use Self::mul_clamped.

pub const fn as_bytes(&self) -> &[u8; 32]

View this MontgomeryPoint as an array of bytes.

✓✓ Lean specification

theorem as_bytes_spec (self : MontgomeryPoint) :
    as_bytes self ⦃ (result : MontgomeryPoint) =>
      result = self ⦄

pub const fn to_bytes(&self) -> [u8; 32]

Convert this MontgomeryPoint to an array of bytes.

✓✓ Lean specification

theorem to_bytes_spec (self : MontgomeryPoint) :
    to_bytes self ⦃ (result : MontgomeryPoint) =>
      result = self ⦄

pub fn to_edwards(&self, sign: u8) -> Option<EdwardsPoint>

Attempt to convert to an EdwardsPoint, using the supplied choice of sign for the EdwardsPoint.

Inputs

• sign: a u8 donating the desired sign of the resulting EdwardsPoint. 0 denotes positive and 1 negative.

Return

• Some(EdwardsPoint) if self is the \(u\)-coordinate of a point on (the Montgomery form of) Curve25519;

• None if self is the \(u\)-coordinate of a point on the twist of (the Montgomery form of) Curve25519;

✓✓ Lean specification

theorem to_edwards_spec (mp : MontgomeryPoint) (sign : U8) :
    to_edwards mp sign ⦃ (result : Option edwards.EdwardsPoint) =>
      (∀ ep, result = some ep →
        ∃ Z_inv,
          field.FieldElement51.invert ep.Z = ok Z_inv ∧
          let u := U8x32_as_Nat mp % 2^255
          let y := Field51_as_Nat ep.Y * Field51_as_Nat Z_inv % p
          (y * ((u + 1) % p)) % p = ((u + p - 1) % p) % p ∧
          ep.IsValid ) ⦄

Trait Implementations

impl Clone for MontgomeryPoint

fn clone(&self) -> MontgomeryPoint

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl ConditionallySelectable for MontgomeryPoint

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

Select a or b according to choice.

✓✓ Lean specification

theorem conditional_select_spec (a b : MontgomeryPoint) (choice : subtle.Choice) :
    conditional_select a b choice ⦃ (result : MontgomeryPoint) =>
      ∀ i < 32,
        result[i]! = (if choice.val = 1#u8 then b[i]! else a[i]!) ⦄

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 MontgomeryPoint

Equality of MontgomeryPoints is defined mod p.

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

Determine if two items are equal.

✓✓ Lean specification

theorem ct_eq_spec (self other : MontgomeryPoint) :
    ct_eq self other ⦃ (c : subtle.Choice) =>
      (c = Choice.one ↔
        (U8x32_as_Nat self % 2 ^ 255) ≡ (U8x32_as_Nat other % 2 ^ 255) [MOD p]) ⦄

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

Determine if two items are NOT equal.

impl Debug for MontgomeryPoint

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

Formats the value using the given formatter.

impl Default for MontgomeryPoint

fn default() -> MontgomeryPoint

Returns the “default value” for a type.

impl Hash for MontgomeryPoint

fn hash<H: Hasher>(&self, state: &mut H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Identity for MontgomeryPoint

fn identity() -> MontgomeryPoint

Return the group identity element, which has order 4.

✓✓ Lean specification

theorem identity_spec :
    identity ⦃ (result : MontgomeryPoint) =>
      (∀ i : Fin 32, result[i]! = 0#u8) ∧
      U8x32_as_Nat result = 0 ⦄

impl Mul<&MontgomeryPoint> for &Scalar

type Output = MontgomeryPoint

The resulting type after applying the * operator.

fn mul(self, point: &MontgomeryPoint) -> MontgomeryPoint

Performs the * operation.

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

type Output = MontgomeryPoint

The resulting type after applying the * operator.

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

Performs the * operation.

impl Mul<&Scalar> for &MontgomeryPoint

Multiply this MontgomeryPoint by a Scalar.

NOTE: This implementation avoids using Scalar::bits_le() and iterator adapters (.rev(), .skip()) because Charon/Aeneas cannot extract the Iterator trait machinery. Instead, we inline the bit iteration using a while loop.

fn mul(self, scalar: &Scalar) -> MontgomeryPoint

Given self \( = u_0(P) \), and a Scalar \(n\), return \( u_0([n]P) \)

type Output = MontgomeryPoint

The resulting type after applying the * operator.

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

type Output = MontgomeryPoint

The resulting type after applying the * operator.

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

Performs the * operation.

✓✓ Lean specification

theorem mul_loop_spec
    (affine_u : backend.serial.u64.field.FieldElement51)
    (x0 x1 : montgomery.ProjectivePoint)
    (scalar_bytes : Array U8 32#usize)
    (prev_bit : Bool)
    (i : Isize)
    (idx0W : Field51_as_Nat x0.W = 0)
    (idx1W : Field51_as_Nat x1.W = 1)
    (idx0U : Field51_as_Nat x0.U = 1) :
    mul_loop affine_u x0 x1 scalar_bytes prev_bit i
    ⦃ (result : montgomery.ProjectivePoint × montgomery.ProjectivePoint × Bool) =>
      (result.2.2 = true →
        let q := (i.val / 8).toNat
        let r := (i.val % 8).toNat
        let m := ∑ i ∈ Finset.range q, 2^(8 * i) * (scalar_bytes[i]!).val
          + 2^(8 * q) * ((scalar_bytes[q]!).val % 2^(r+1))
          + 2^(8 * q + r) * prev_bit.toNat
        let u := x1.U.toField
        let u_out := result.2.1.U.toField
        let w_out := result.2.1.W.toField
        let u_ord := u_out/w_out
        result.2.1.U.IsValid ∧
        result.2.1.W.IsValid ∧
        result.1.U.IsValid ∧
        result.1.W.IsValid ∧
        w_out ≠ 0 ∧
        MontgomeryPoint.u_affine_toPoint u_ord = m • (MontgomeryPoint.u_affine_toPoint u)) ∧
      (result.2.2 = false →
        let q := (i.val / 8).toNat
        let r := (i.val % 8).toNat
        let m := ∑ i ∈ Finset.range q, 2^(8 * i) * (scalar_bytes[i]!).val
        + 2^(8 * q) * ((scalar_bytes[q]!).val % 2^(r+1))
        + 2^(8 * q + r) * prev_bit.toNat
        let u := x1.U.toField
        let u_out := result.1.U.toField
        let w_out := result.1.W.toField
        let u_ord := u_out/w_out
        result.2.1.U.IsValid ∧
        result.2.1.W.IsValid ∧
        result.1.U.IsValid ∧
        result.1.W.IsValid ∧
        w_out ≠ 0 ∧
        MontgomeryPoint.u_affine_toPoint u_ord = m • (MontgomeryPoint.u_affine_toPoint u)) ⦄

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

type Output = MontgomeryPoint

The resulting type after applying the * operator.

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

Performs the * operation.

impl Mul<MontgomeryPoint> for Scalar

type Output = MontgomeryPoint

The resulting type after applying the * operator.

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

Performs the * operation.

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

type Output = MontgomeryPoint

The resulting type after applying the * operator.

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

Performs the * operation.

impl Mul<Scalar> for MontgomeryPoint

type Output = MontgomeryPoint

The resulting type after applying the * operator.

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

Performs the * operation.

impl MulAssign<&Scalar> for MontgomeryPoint

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

Performs the *= operation.

impl MulAssign<Scalar> for MontgomeryPoint

fn mul_assign(&mut self, rhs: Scalar)

Performs the *= operation.

✓✓ Lean specification

theorem mul_assign_spec (self : MontgomeryPoint) (scalar : scalar.Scalar)
    (hself_bound : U8x32_as_Nat self < 2 ^ 255) :
    mul_assign self scalar ⦃ (result : MontgomeryPoint) =>
      let m := (U8x32_as_Nat scalar.bytes) % 2^255
      MontgomeryPoint.mkPoint result = m • (MontgomeryPoint.mkPoint self) ⦄

impl PartialEq for MontgomeryPoint

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

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

✓✓ Lean specification

theorem eq_spec (self other : MontgomeryPoint) :
    eq self other ⦃ (b : Bool) =>
      (b = true ↔
        (U8x32_as_Nat self % 2 ^ 255) ≡ (U8x32_as_Nat other % 2 ^ 255) [MOD p]) ⦄

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 Zeroize for MontgomeryPoint

Available on crate feature zeroize only.

fn zeroize(&mut self)

Zero out this object from memory using Rust intrinsics which ensure the zeroization operation is not “optimized away” by the compiler.

impl Copy for MontgomeryPoint

impl Eq for MontgomeryPoint