curve25519_dalek::constants

Constant RISTRETTO_BASEPOINT_POINT

✓✓ Lean specification
theorem RISTRETTO_BASEPOINT_POINT_spec :
    RISTRETTO_BASEPOINT_POINT ⦃ (result : RistrettoPoint) =>
      result.IsValid ∧ _root_.L • result.toPoint = 0 ∧
      result.toPoint ≠ 0 ∧ 4 • result.toPoint ≠ 0 ∧
      result.toPoint = _root_.Edwards.basepoint ⦄
Source 
pub const RISTRETTO_BASEPOINT_POINT: RistrettoPoint;
Expand description

The Ristretto basepoint, as a RistrettoPoint.

This is called _POINT to distinguish it from _TABLE, which provides fast scalar multiplication.