Struct CompressedEdwardsY

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

In “Edwards y” / “Ed25519” format, the curve point \((x,y)\) is determined by the \(y\)-coordinate and the sign of \(x\).

The first 255 bits of a CompressedEdwardsY represent the \(y\)-coordinate. The high bit of the 32nd byte gives the sign of \(x\).

Tuple Fields

0: [u8; 32]

Implementations

impl CompressedEdwardsY

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

View this CompressedEdwardsY as an array of bytes.

✓✓ Lean specification

theorem as_bytes_spec (self : CompressedEdwardsY) :
    as_bytes self ⦃ (result : Array U8 32#usize) =>
      result = self ⦄

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

Copy this CompressedEdwardsY to an array of bytes.

pub fn decompress(&self) -> Option<EdwardsPoint>

Attempt to decompress to an EdwardsPoint.

Returns None if the input is not the \(y\)-coordinate of a curve point.

✓✓ Lean specification

theorem decompress_spec (self : CompressedEdwardsY) :
    decompress self ⦃ (result : Option EdwardsPoint) =>
      let y : CurveField := ((U8x32_as_Nat self % 2 ^ 255 : Nat) : CurveField)
      let x_sign_bit := self[31]!.val.testBit 7
      (result.isSome ↔ ∃ pt : Point Ed25519, pt.y = y) ∧
      (∀ ep, result = some ep →
        ep.IsValid ∧
        ep.Y.toField = y ∧
        Field51_as_Nat ep.Y ≡ (U8x32_as_Nat self % 2 ^ 255) [MOD p] ∧
        ep.Z.toField = 1 ∧
        Field51_as_Nat ep.Z % p = 1 ∧
        (y ^ 2 ≠ 1 →
          (x_sign_bit ↔ (Field51_as_Nat ep.X % p) % 2 = 1))) ⦄

impl CompressedEdwardsY

pub fn from_slice(bytes: &[u8]) -> Result<CompressedEdwardsY, TryFromSliceError>

Construct a CompressedEdwardsY from a slice of bytes.

Errors

Returns TryFromSliceError if the input bytes slice does not have a length of 32.

✓✓ Lean specification

theorem from_slice_spec
    (bytes : Slice U8) :
    from_slice bytes ⦃
      (result : core.result.Result CompressedEdwardsY core.array.TryFromSliceError) =>
      (bytes.length = 32 → ∃ cey : CompressedEdwardsY, result = .Ok cey ∧ cey.val = bytes.val) ∧
      (bytes.length ≠ 32 → result = .Err ()) ⦄

Trait Implementations

impl Clone for CompressedEdwardsY

fn clone(&self) -> CompressedEdwardsY

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl ConstantTimeEq for CompressedEdwardsY

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

Determine if two items are equal.

✓✓ Lean specification

theorem ct_eq_spec
    (self other : CompressedEdwardsY) :
    ct_eq self other ⦃ (result : subtle.Choice) =>
      result = Choice.one ↔ self = other ⦄

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

Determine if two items are NOT equal.

impl Debug for CompressedEdwardsY

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

Formats the value using the given formatter.

impl Default for CompressedEdwardsY

fn default() -> CompressedEdwardsY

Returns the “default value” for a type.

impl Hash for CompressedEdwardsY

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 CompressedEdwardsY

fn identity() -> CompressedEdwardsY

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

✓✓ Lean specification

theorem identity_spec :
    identity ⦃ (result : CompressedEdwardsY) =>
      U8x32_as_Nat result = 1 ⦄

impl PartialEq for CompressedEdwardsY

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

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

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 TryFrom<&[u8]> for CompressedEdwardsY

type Error = TryFromSliceError

The type returned in the event of a conversion error.

fn try_from(slice: &[u8]) -> Result<CompressedEdwardsY, TryFromSliceError>

Performs the conversion.

impl Zeroize for CompressedEdwardsY

Available on crate feature zeroize only.

fn zeroize(&mut self)

Reset this CompressedEdwardsY to the compressed form of the identity element.

impl Copy for CompressedEdwardsY

impl Eq for CompressedEdwardsY

impl StructuralPartialEq for CompressedEdwardsY