Naive attempt at a simple implementation of secp256k1 in Idris

EllipticCurve.idr

module EllipticCurve
%default total

-- Resources:
-- Bitcoin secp256k1 https://en.bitcoin.it/wiki/Secp256k1
-- SafeCurves: https://safecurves.cr.yp.to/base.html
-- https://github.com/iCHAIT/Elliptical-Curve-Cryptography
-- https://github.com/mfourne/eccrypto/
-- secp256k1 can't ladder? https://safecurves.cr.yp.to/ladder.html


data ECPoint : Type where
  MkECPoint : (x: Nat) -> (y: Nat) -> ECPoint
  ECPointInf : ECPoint


-- EllipticCurve values for the secp256k1 curve
-- ====================================================================
p : Nat
p = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC2F

a : Nat
a = 0x0000000000000000000000000000000000000000000000000000000000000000

b : Nat
b = 0x0000000000000000000000000000000000000000000000000000000000000007

G : ECPoint
G = MkECPoint
    0x79BE667EF9DCBBAC55A06295CE870B07029BFCDB2DCE28D959F2815B16F81798
    0x483ADA7726A3C4655DA4FBFC0E1108A8FD17B448A68554199C47D08FFB10D4B8

-- `n` is the "order" of the curve
-- All private keys must be < the order `n`
n : Nat
n = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364141

h : Nat
h = 0x01



-- representation of a function: y^2 = x^3 + ax + b
-- p is the size of the finite field for the curve
-- G is the base point for the curve
-- n is the order of the curve
-- h is the cofactor of the curve
data EllipticCurve : Type where
  MkEC : (p: Nat)
      -> (a: Nat)
      -> (b: Nat)
      -> (G: ECPoint)
      -> (n: Nat)
      -> (h: Nat)
      -> {auto ppr : GT p 0 }
      -> {auto npr : GT n 0 }
      -> {auto hpr : GT h 0 }
      -> EllipticCurve

-- Modulus that always returns a positive number by adding the modulus if negative
ecMod : (a: Integer) -> (q: Nat) -> {auto pr: GT q 0} -> Nat
ecMod a q =
  let qi = toIntegerNat q
      --  We assert_total b/c we have a proof that `q` (and thus `qi`) is > 0
      m = assert_total (a `mod` qi) in
  if(m < 0)
  then toNat (m + qi)
  else toNat m

-- Compute the additive inverse of a point on a given curve
neg : EllipticCurve -> ECPoint -> ECPoint
neg _ ECPointInf = ECPointInf
neg (MkEC p _ _ _ _ _) (MkECPoint x y) =
  let nyi = (-(toIntegerNat y)) in
    MkECPoint x $ ecMod nyi p

-- Compute the multiplicative inverse of a point on a given a curve
inv : EllipticCurve -> Integer -> Nat
inv (MkEC p a b G n h) x =  subInv p x where
  subInv : Nat -> Integer -> Nat
  subInv Z _ =  0 -- TODO: How to better handle / avoid this case
  subInv i@(S k) n =
    if (((n * (toIntegerNat i)) `ecMod` p) == 1)
    then i
    else subInv k n

-- Implemented from: http://www.secg.org/sec1-v2.pdf pg. 8
add : EllipticCurve -> ECPoint -> ECPoint -> ECPoint
add _ p1 ECPointInf = p1
add _ ECPointInf p2 = p2
add c@(MkEC p _ _ _ _ _) p1@(MkECPoint x1 y1) p2@(MkECPoint x2 y2) =
  case ( (x1 == x2) && (y1 /= y2 || y1 == 0) ) of
    True => ECPointInf
    False => case (x1 /= x2) of
      True =>
        let y1i = toIntegerNat y1
            y2i = toIntegerNat y2
            x1i = toIntegerNat x1
            x2i = toIntegerNat x2
            l   = (y2i - y1i) * (toIntegerNat (inv c (x2i - x1i))) `ecMod` p
            li  = toIntegerNat l
            x3  = ((pow li 2) - (2 * x1i)) `ecMod` p
            x3i = toIntegerNat x3
            y3  = ((li * (x1i - x3i)) - y1i) `ecMod` p
        in
          MkECPoint x3 y3
      False =>
        let y1i = toIntegerNat y1
            y2i = toIntegerNat y2
            x1i = toIntegerNat x1
            x2i = toIntegerNat x2
            2y1inv = inv c (y1i * 2)
            -- l   = (((3 * (pow x1i 2)) + (toIntegerNat a)) * 2y1inv) `ecMod` p
        in
          -- MkECPoint l l
          ?hole

-- TODO: Implement an efficient version of `double`
double : EllipticCurve -> ECPoint -> ECPoint
double c p = add c p p

-- TODO: Implement an efficient version of `mult`
mult : EllipticCurve -> ECPoint -> Nat -> ECPoint
mult _ _ Z = ECPointInf
mult c p (S k) = subMult p p k where
  subMult : ECPoint -> ECPoint -> Nat -> ECPoint
  subMult _ p1 Z     = p
  subMult orig p1 (S k1) = subMult orig (add c p1 orig) k1