Idris2Doc : Crypto.Curve.Weierstrass

Crypto.Curve.Weierstrass

(source)
Definitions
interface WeierstrassPoint : Type -> Type
  Parameters: p
Methods:
  
a_coefficent : Integer
  
b_coefficent : Integer
  
prime : Integer
  
to_jacobian : p -> (Integer, (Integer, Integer))
  
from_jacobian : (Integer, (Integer, Integer)) -> p
  
g : p
  
to_from_jacobian : (x : (Integer, (Integer, Integer))) -> to_jacobian (from_jacobian x) = x
  
bits' : Nat
  
curve_n : Integer

Implementations:
  
WeierstrassPoint P256
  
WeierstrassPoint P384
  
WeierstrassPoint P521
a_coefficent : WeierstrassPoint p => Integer
  Visibility: public export
b_coefficent : WeierstrassPoint p => Integer
  Visibility: public export
prime : WeierstrassPoint p => Integer
  Visibility: public export
to_jacobian : WeierstrassPoint p => p -> (Integer, (Integer, Integer))
  Visibility: public export
from_jacobian : WeierstrassPoint p => (Integer, (Integer, Integer)) -> p
  Visibility: public export
g : WeierstrassPoint p => p
  Visibility: public export
to_from_jacobian : {auto __con : WeierstrassPoint p} -> (x : (Integer, (Integer, Integer))) -> to_jacobian (from_jacobian x) = x
  Visibility: public export
bits' : WeierstrassPoint p => Nat
  Visibility: public export
curve_n : WeierstrassPoint p => Integer
  Visibility: public export
data P256 : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkP256 : (Integer, (Integer, Integer)) -> P256

  Hint: 
WeierstrassPoint P256
data P384 : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkP384 : (Integer, (Integer, Integer)) -> P384

  Hint: 
WeierstrassPoint P384
data P521 : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkP521 : (Integer, (Integer, Integer)) -> P521

  Hint: 
WeierstrassPoint P521