Struct Scalar

pub struct Scalar { /* private fields */ }

The Scalar struct holds an element of \(\mathbb Z / \ell\mathbb Z \).

Implementations

impl Scalar

pub fn from_bytes_mod_order(bytes: [u8; 32]) -> Scalar

Construct a Scalar by reducing a 256-bit little-endian integer modulo the group order \( \ell \).

✓✓ Lean specification

theorem from_bytes_mod_order_spec (bytes : Array U8 32#usize) :
    from_bytes_mod_order bytes ⦃ (s : Scalar) =>
      U8x32_as_Nat s.bytes ≡ U8x32_as_Nat bytes [MOD L] ∧
      U8x32_as_Nat s.bytes < L ⦄

pub fn from_bytes_mod_order_wide(input: &[u8; 64]) -> Scalar

Construct a Scalar by reducing a 512-bit little-endian integer modulo the group order \( \ell \).

✓✓ Lean specification

theorem from_bytes_mod_order_wide_spec (input : Array U8 64#usize) :
    from_bytes_mod_order_wide input ⦃ (result : Scalar) =>
      U8x32_as_Nat result.bytes ≡ U8x64_as_Nat input [MOD L] ∧
      U8x32_as_Nat result.bytes < L ⦄

pub fn from_canonical_bytes(bytes: [u8; 32]) -> CtOption<Scalar>

Attempt to construct a Scalar from a canonical byte representation.

Return

• Some(s), where s is the Scalar corresponding to bytes, if bytes is a canonical byte representation modulo the group order \( \ell \);
• None if bytes is not a canonical byte representation.

✓✓ Lean specification

theorem from_canonical_bytes_spec (bytes : Array U8 32#usize) :
    from_canonical_bytes bytes ⦃ (s : subtle.CtOption Scalar) =>
      (U8x32_as_Nat bytes < L → s.is_some = Choice.one ∧ s.value.bytes = bytes) ∧
      (L ≤ U8x32_as_Nat bytes → s.is_some = Choice.zero) ⦄

impl Scalar

pub const ZERO: Self

The scalar \( 0 \).

pub const ONE: Self

The scalar \( 1 \).

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

Convert this Scalar to its underlying sequence of bytes.

Example

use curve25519_dalek::scalar::Scalar;

let s: Scalar = Scalar::ZERO;

assert!(s.to_bytes() == [0u8; 32]);

✓✓ Lean specification

theorem to_bytes_spec (s : Scalar) :
    to_bytes s ⦃ (a : Array U8 32#usize) =>
      a = s.bytes ∧
      mk a = s ⦄

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

View the little-endian byte encoding of the integer representing this Scalar.

Example

use curve25519_dalek::scalar::Scalar;

let s: Scalar = Scalar::ZERO;

assert!(s.as_bytes() == &[0u8; 32]);

✓✓ Lean specification

theorem as_bytes_spec (s : Scalar) :
    as_bytes s ⦃ (result : Array U8 32#usize) =>
      result = s.bytes ∧
      mk result = s ⦄

pub fn invert(&self) -> Scalar

Given a nonzero Scalar, compute its multiplicative inverse.

Warning

self MUST be nonzero. If you cannot prove that this is the case, you SHOULD NOT USE THIS FUNCTION.

Returns

The multiplicative inverse of the this Scalar.

Example

use curve25519_dalek::scalar::Scalar;

// x = 2238329342913194256032495932344128051776374960164957527413114840482143558222
let X: Scalar = Scalar::from_bytes_mod_order([
        0x4e, 0x5a, 0xb4, 0x34, 0x5d, 0x47, 0x08, 0x84,
        0x59, 0x13, 0xb4, 0x64, 0x1b, 0xc2, 0x7d, 0x52,
        0x52, 0xa5, 0x85, 0x10, 0x1b, 0xcc, 0x42, 0x44,
        0xd4, 0x49, 0xf4, 0xa8, 0x79, 0xd9, 0xf2, 0x04,
    ]);
// 1/x = 6859937278830797291664592131120606308688036382723378951768035303146619657244
let XINV: Scalar = Scalar::from_bytes_mod_order([
        0x1c, 0xdc, 0x17, 0xfc, 0xe0, 0xe9, 0xa5, 0xbb,
        0xd9, 0x24, 0x7e, 0x56, 0xbb, 0x01, 0x63, 0x47,
        0xbb, 0xba, 0x31, 0xed, 0xd5, 0xa9, 0xbb, 0x96,
        0xd5, 0x0b, 0xcd, 0x7a, 0x3f, 0x96, 0x2a, 0x0f,
    ]);

let inv_X: Scalar = X.invert();
assert!(XINV == inv_X);
let should_be_one: Scalar = &inv_X * &X;
assert!(should_be_one == Scalar::ONE);

✓✓ Lean specification

theorem invert_spec (self : Scalar) (h : U8x32_as_Nat self.bytes % L ≠ 0) :
    invert self ⦃ (result : Scalar) =>
      U8x32_as_Nat self.bytes * U8x32_as_Nat result.bytes ≡ 1 [MOD L] ⦄

pub fn batch_invert(inputs: &mut [Scalar]) -> Scalar

Available on crate feature alloc only.

Given a slice of nonzero (possibly secret) Scalars, compute their inverses in a batch.

Return

Each element of inputs is replaced by its inverse.

The product of all inverses is returned.

Warning

All input Scalars MUST be nonzero. If you cannot prove that this is the case, you SHOULD NOT USE THIS FUNCTION.

Example

let mut scalars = [
    Scalar::from(3u64),
    Scalar::from(5u64),
    Scalar::from(7u64),
    Scalar::from(11u64),
];

let allinv = Scalar::batch_invert(&mut scalars);

assert_eq!(allinv, Scalar::from(3*5*7*11u64).invert());
assert_eq!(scalars[0], Scalar::from(3u64).invert());
assert_eq!(scalars[1], Scalar::from(5u64).invert());
assert_eq!(scalars[2], Scalar::from(7u64).invert());
assert_eq!(scalars[3], Scalar::from(11u64).invert());

✓✓ Lean specification

theorem batch_invert_spec
    (inputs : Slice scalar.Scalar)
    (vals : ℕ → ℕ)
    (h_vals_lt : ∀ j < inputs.val.length, vals j < L)
    (h_vals_nz : ∀ j < inputs.val.length, vals j % L ≠ 0)
    (h_vals_def : ∀ j < inputs.val.length,
        SliceScalarAt inputs j (fun b => U8x32_as_Nat b = vals j)) :
    batch_invert inputs ⦃ (result : scalar.Scalar × Slice scalar.Scalar) =>
      U8x32_as_Nat result.1.bytes * PrefixProd vals inputs.val.length ≡ 1 [MOD L] ∧
      ∀ j < inputs.val.length,
          SliceScalarAt result.2 j
            (fun b => U8x32_as_Nat b * vals j ≡ 1 [MOD L]) ⦄

Trait Implementations

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

type Output = Scalar

The resulting type after applying the + operator.

fn add(self, _rhs: &'a Scalar) -> Scalar

Performs the + operation.

✓✓ Lean specification

theorem add_spec (self _rhs : scalar.Scalar)
    (h_self : U8x32_as_Nat self.bytes < L)
    (h_rhs : U8x32_as_Nat _rhs.bytes < L) :
    add self _rhs ⦃ (result : scalar.Scalar) =>
      U8x32_as_Nat result.bytes ≡ U8x32_as_Nat self.bytes + U8x32_as_Nat _rhs.bytes [MOD L] ∧
      U8x32_as_Nat result.bytes < L ⦄

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

type Output = Scalar

The resulting type after applying the + operator.

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

Performs the + operation.

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

type Output = Scalar

The resulting type after applying the + operator.

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

Performs the + operation.

impl Add for Scalar

type Output = Scalar

The resulting type after applying the + operator.

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

Performs the + operation.

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

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

Performs the += operation.

impl AddAssign for Scalar

fn add_assign(&mut self, rhs: Scalar)

Performs the += operation.

impl Clone for Scalar

fn clone(&self) -> Scalar

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl ConditionallySelectable for Scalar

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 : scalar.Scalar)
    (choice : subtle.Choice) :
    conditional_select a b choice ⦃ (result : scalar.Scalar) =>
      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 Scalar

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

Determine if two items are equal.

✓✓ Lean specification

theorem ct_eq_spec (self other : scalar.Scalar) :
    ct_eq self other ⦃ (c : subtle.Choice) =>
      c = Choice.one ↔ self.bytes = other.bytes ⦄

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

Determine if two items are NOT equal.

impl Debug for Scalar

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

Formats the value using the given formatter.

impl Default for Scalar

fn default() -> Scalar

Returns the “default value” for a type.

impl From<u128> for Scalar

fn from(x: u128) -> Scalar

Converts to this type from the input type.

impl From<u16> for Scalar

fn from(x: u16) -> Scalar

Converts to this type from the input type.

impl From<u32> for Scalar

fn from(x: u32) -> Scalar

Converts to this type from the input type.

impl From<u64> for Scalar

fn from(x: u64) -> Scalar

Construct a scalar from the given u64.

Inputs

An u64 to convert to a Scalar.

Returns

A Scalar corresponding to the input u64.

Example

use curve25519_dalek::scalar::Scalar;

let fourtytwo = Scalar::from(42u64);
let six = Scalar::from(6u64);
let seven = Scalar::from(7u64);

assert!(fourtytwo == six * seven);

impl From<u8> for Scalar

fn from(x: u8) -> Scalar

Converts to this type from the input type.

✓✓ Lean specification

theorem from_spec (x : Std.U128) :
    «from» x ⦃ (result : Scalar) =>
      U8x32_as_Nat result.bytes = x.val ⦄

impl Hash for Scalar

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 Index<usize> for Scalar

fn index(&self, _index: usize) -> &u8

Index the bytes of the representative for this Scalar. Mutation is not permitted.

type Output = u8

The returned type after indexing.

impl<'a, 'b> Mul<&'a EdwardsBasepointTable> for &'b Scalar

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'a, 'b> Mul<&'a EdwardsBasepointTableRadix128> for &'b Scalar

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'a, 'b> Mul<&'a EdwardsBasepointTableRadix256> for &'b Scalar

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'a, 'b> Mul<&'a EdwardsBasepointTableRadix32> for &'b Scalar

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'a, 'b> Mul<&'a EdwardsBasepointTableRadix64> for &'b Scalar

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

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 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<'a> Mul<&'a RistrettoBasepointTable> for &Scalar

Available on crate feature precomputed-tables only.

type Output = RistrettoPoint

The resulting type after applying the * operator.

fn mul(self, basepoint_table: &'a RistrettoBasepointTable) -> RistrettoPoint

Performs the * operation.

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

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

Scalar multiplication: compute self * scalar.

type Output = RistrettoPoint

The resulting type after applying the * operator.

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

type Output = RistrettoPoint

The resulting type after applying the * operator.

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

Performs the * operation.

impl<'a, 'b> Mul<&'b Scalar> for &'a EdwardsBasepointTable

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'a, 'b> Mul<&'b Scalar> for &'a EdwardsBasepointTableRadix128

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'a, 'b> Mul<&'b Scalar> for &'a EdwardsBasepointTableRadix256

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'a, 'b> Mul<&'b Scalar> for &'a EdwardsBasepointTableRadix32

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

impl<'a, 'b> Mul<&'b Scalar> for &'a EdwardsBasepointTableRadix64

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

Construct an EdwardsPoint from a Scalar \(a\) by computing the multiple \(aB\) of this basepoint \(B\).

type Output = EdwardsPoint

The resulting type after applying the * operator.

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 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 &RistrettoBasepointTable

Available on crate feature precomputed-tables only.

type Output = RistrettoPoint

The resulting type after applying the * operator.

fn mul(self, scalar: &'b Scalar) -> RistrettoPoint

Performs the * operation.

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

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

Scalar multiplication: compute scalar * self.

type Output = RistrettoPoint

The resulting type after applying the * operator.

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

type Output = Scalar

The resulting type after applying the * operator.

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

Performs the * operation.

✓✓ Lean specification

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

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.

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.

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

type Output = RistrettoPoint

The resulting type after applying the * operator.

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

Performs the * operation.

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

type Output = Scalar

The resulting type after applying the * operator.

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

Performs the * operation.

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<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<RistrettoPoint> for &'a Scalar

type Output = RistrettoPoint

The resulting type after applying the * operator.

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

Performs the * operation.

impl Mul<RistrettoPoint> for Scalar

type Output = RistrettoPoint

The resulting type after applying the * operator.

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

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<'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<'a> Mul<Scalar> for &'a RistrettoPoint

type Output = RistrettoPoint

The resulting type after applying the * operator.

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

Performs the * operation.

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

type Output = Scalar

The resulting type after applying the * operator.

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

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 Mul<Scalar> for MontgomeryPoint

type Output = MontgomeryPoint

The resulting type after applying the * operator.

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

Performs the * operation.

impl Mul<Scalar> for RistrettoPoint

type Output = RistrettoPoint

The resulting type after applying the * operator.

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

Performs the * operation.

impl Mul for Scalar

type Output = Scalar

The resulting type after applying the * operator.

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

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 MontgomeryPoint

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

Performs the *= operation.

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

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

Performs the *= operation.

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

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

Performs the *= operation.

✓✓ Lean specification

theorem mul_assign_spec (self _rhs : Scalar)
    (h_self : U8x32_as_Nat self.bytes < L)
    (h_rhs : U8x32_as_Nat _rhs.bytes < L) :
    mul_assign self _rhs ⦃ (result : Scalar) =>
      U8x32_as_Nat result.bytes ≡ U8x32_as_Nat self.bytes * U8x32_as_Nat _rhs.bytes [MOD L] ∧
      U8x32_as_Nat result.bytes < L ⦄

impl MulAssign<Scalar> for EdwardsPoint

fn mul_assign(&mut self, rhs: Scalar)

Performs the *= operation.

impl MulAssign<Scalar> for MontgomeryPoint

fn mul_assign(&mut self, rhs: Scalar)

Performs the *= operation.

impl MulAssign<Scalar> for RistrettoPoint

fn mul_assign(&mut self, rhs: Scalar)

Performs the *= operation.

impl MulAssign for Scalar

fn mul_assign(&mut self, rhs: Scalar)

Performs the *= operation.

impl Neg for &Scalar

type Output = Scalar

The resulting type after applying the - operator.

fn neg(self) -> Scalar

Performs the unary - operation.

✓✓ Lean specification

theorem neg_spec (self : scalar.Scalar)
    (h_self : U8x32_as_Nat self.bytes < L) :
    neg self ⦃ (result : scalar.Scalar) =>
      U8x32_as_Nat result.bytes + U8x32_as_Nat self.bytes ≡ 0 [MOD L] ∧
      U8x32_as_Nat result.bytes < L ⦄

impl Neg for Scalar

type Output = Scalar

The resulting type after applying the - operator.

fn neg(self) -> Scalar

Performs the unary - operation.

impl PartialEq for Scalar

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

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

✓✓ Lean specification

theorem eq_spec (self other : Scalar) :
    eq self other ⦃ (result : Bool) =>
      result = true ↔ self.bytes = other.bytes ⦄

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<T> Product<T> for Scalar

where T: Borrow<Scalar>,

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

where I: Iterator<Item = T>,

Takes an iterator and generates Self from the elements by multiplying the items.

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

type Output = Scalar

The resulting type after applying the - operator.

fn sub(self, rhs: &'a Scalar) -> Scalar

Performs the - operation.

✓✓ Lean specification

theorem sub_spec (self rhs : scalar.Scalar)
    (h_self : U8x32_as_Nat self.bytes < L)
    (h_rhs : U8x32_as_Nat rhs.bytes < L) :
    sub self rhs ⦃ (result : scalar.Scalar) =>
      U8x32_as_Nat result.bytes + U8x32_as_Nat rhs.bytes ≡
        U8x32_as_Nat self.bytes [MOD L] ∧
      U8x32_as_Nat result.bytes < L ⦄

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

type Output = Scalar

The resulting type after applying the - operator.

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

Performs the - operation.

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

type Output = Scalar

The resulting type after applying the - operator.

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

Performs the - operation.

impl Sub for Scalar

type Output = Scalar

The resulting type after applying the - operator.

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

Performs the - operation.

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

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

Performs the -= operation.

impl SubAssign for Scalar

fn sub_assign(&mut self, rhs: Scalar)

Performs the -= operation.

impl<T> Sum<T> for Scalar

where T: Borrow<Scalar>,

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

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 Scalar

impl Eq for Scalar