Finite fields with order in type

This then propagates to ECPoint to use those fields

Formatting is adjusted

Include some constants of ECC for bitcoin

1 files changed, 84 insertions, 56 deletions

diff --git a/ecc.hs b/ecc.hs
index 56a3067..e639e3a 100644
--- a/ecc.hs
+++ b/ecc.hs
@@ -1,48 +1,52 @@
-{-# LANGUAGE FlexibleInstances #-}
-
-data FieldElement a = FieldElement
-  { number :: a
-  , prime  :: a
-  }
-  deriving Eq
-
-instance (Num a, Show a) => Show (FieldElement a) where
-  show a = "FieldElement_" ++ show (prime a) ++ " " ++ show (number a)
-
-instance Integral a => Num (FieldElement a) where
-  (FieldElement a b) + (FieldElement c d)
-    | b /= d    = error "Distinct Fields"
-    | otherwise = FieldElement (mod (a + c) b) b
-  (FieldElement a b) * (FieldElement c d)
-    | b /= d    = error "Distinct Fields"
-    | otherwise = FieldElement (mod (a * c) b) b
-  abs a = a
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
+
+import           Data.Bits
+import           Data.Proxy
+import           Data.Ratio   (denominator, numerator)
+import           GHC.TypeLits
+import           Text.Printf  (PrintfArg, printf)
+
+-- FiniteFields
+--https://stackoverflow.com/questions/39823408/prime-finite-field-z-pz-in-haskell-with-operator-overloading
+newtype FieldElement (p :: Nat) = FieldElement Integer deriving Eq
+
+instance KnownNat n => Num (FieldElement n) where
+  FieldElement x + FieldElement y = fromInteger $ x + y
+  FieldElement x * FieldElement y = fromInteger $ x * y
+  abs x = x
   signum _ = 1
-  negate (FieldElement a b) = FieldElement (mod (b - a) b) b
-  fromInteger _ = error "can't transform"
+  negate (FieldElement x) = fromInteger $ negate x
+  fromInteger a = FieldElement (mod a n) where n = natVal (Proxy :: Proxy n)
+
+instance KnownNat n => Fractional (FieldElement n) where
+  recip a = a ^ (n - 2) where n = natVal (Proxy :: Proxy n)
+  fromRational r = fromInteger (numerator r) / fromInteger (denominator r)
+
+instance KnownNat n => Show (FieldElement n) where
+  show (FieldElement a) | n == (2 ^ 256 - 2 ^ 32 - 977) = printf "0x%064x" a
+                        | otherwise = "FieldElement_" ++ show n ++ " " ++ show a
+    where n = natVal (Proxy :: Proxy n)
 
-instance (Integral a) => Fractional (FieldElement a) where
-  recip a = a ^ (prime a - 2)
-  fromRational _ = error "can't transform"
 
 assert :: Bool -> Bool
 assert False = error "WRONG"
 assert x     = x
 
 aa =
-  let a = FieldElement 2 31
-      b = FieldElement 15 31
-  in  assert
-        (  (a + b == FieldElement 17 31)
-        && (a /= b)
-        && (a - b == FieldElement 18 31)
-        )
+  let a = FieldElement 2 :: FieldElement 31
+      b = FieldElement 15
+  in  (a + b == FieldElement 17, a /= b, a - b == FieldElement 18)
 
 bb =
-  let a = FieldElement 19 31
-      b = FieldElement 24 31
+  let a = FieldElement 19 :: FieldElement 31
+      b = FieldElement 24
   in  a * b
 
+-- Elliptic curve
 data ECPoint a
   = Infinity
   | ECPoint
@@ -51,41 +55,52 @@ data ECPoint a
       , a :: a
       , b :: a
       }
-  deriving (Eq )
-
-rmul :: Integral a => a -> FieldElement a -> FieldElement a
-a `rmul` (FieldElement v p) = FieldElement (mod (a * v) p) p
+  deriving (Eq)
 
-instance Show a => Show (ECPoint (FieldElement a)) where
+instance KnownNat n => Show (ECPoint (FieldElement n)) where
   show Infinity = "ECPoint(Infinity)"
-  show p        = "ECPoint_" ++ show (prime (x p)) ++ points ++ params
+  show p
+    | n == (2 ^ 256 - 2 ^ 32 - 977) = "S256Point" ++ points
+    | otherwise  = "ECPoint_" ++ show n ++ points ++ params
    where
-    points = "(" ++ show (number (x p)) ++ ", " ++ show (number (y p)) ++ ")"
-    params = "a_" ++ show (number (a p)) ++ "|b_" ++ show (number (b p))
-
+    n      = natVal (Proxy :: Proxy n)
+    points = "(" ++ si (x p) ++ ", " ++ si (y p) ++ ")"
+    params = "a_" ++ si (a p) ++ "|b_" ++ si (b p)
+    si (FieldElement r) | n == (2 ^ 256 - 2 ^ 32 - 977) = printf "0x%064x" r
+                        | otherwise                     = show r
 
 validECPoint :: (Eq a, Num a) => ECPoint a -> Bool
-validECPoint Infinity = True
-validECPoint p        = y p ^ 2 == x p ^ 3 + a p * x p + b p
+validECPoint Infinity          = True
+validECPoint (ECPoint x y a b) = y ^ 2 == x ^ 3 + a * x + b
 
 add :: (Eq a, Fractional a) => ECPoint a -> ECPoint a -> ECPoint a
 add Infinity p        = p
 add p        Infinity = p
-add p q | a p /= a q || b p /= b q = error "point not on same curve"
-        | x p == x q && y p /= y q = Infinity
-        | x p /= x q               = new_point $ (y q - y p) / (x q - x p)
-        | x p == x q && y p == 0   = Infinity
-        | p == q                   = new_point $ (3 * x p ^ 2 + a p) / (2 * y p)
-        | otherwise                = error "Unexpected case of points"
+add p q
+  | a p /= a q || b p /= b q = error "point not on same curve"
+  | x p == x q && y p /= y q = Infinity
+  | x p /= x q               = new_point $ (y q - y p) / (x q - x p)
+  | x p == x q && y p == 0   = Infinity
+  | p == q                   = new_point $ (3 * x p ^ 2 + a p) / (2 * y p)
+  | otherwise                = error "Unexpected case of points"
  where
   new_point slope =
     let new_x = slope ^ 2 - x p - x q
         new_y = slope * (x p - new_x) - y p
     in  ECPoint new_x new_y (a p) (b p)
 
+binex :: (Eq a, Fractional a) => Integer -> ECPoint a -> ECPoint a -> ECPoint a
+binex m value result | m == 0       = result
+                     | m .&. 1 == 1 = loop (add result value)
+                     | otherwise    = loop result
+  where loop = binex (m `shiftR` 1) (add value value)
+
+crmul :: (Eq a, Fractional a) => Integer -> ECPoint a -> ECPoint a
+crmul m ec = binex m ec Infinity
 
+tre = FieldElement 3 :: FieldElement 31
 cc =
-  let a = ECPoint 3 (-7) 5 7
+  let a = ECPoint tre (-7) 5 7
       b = ECPoint 18 77 5 7
       c = ECPoint (-1) (-1) 5 7
   in  ( validECPoint a
@@ -101,9 +116,22 @@ cc =
 
 dd =
   let prime = 223
-      a     = FieldElement 0 prime
-      b     = FieldElement 7 prime
-      x     = FieldElement 192 prime
-      y     = FieldElement 105 prime
+      a     = FieldElement 0 :: FieldElement prime
+      b     = FieldElement 7
+      x     = FieldElement 192
+      y     = FieldElement 105
       point = ECPoint x y a b
-  in  validECPoint point
+  in  point
+
+
+type S256Field = FieldElement (2 ^ 256- 2^ 32 - 977)
+type S256Point = ECPoint S256Field
+s256point :: S256Field -> S256Field -> S256Point
+s256point x y = ECPoint x y 0 7
+li :: S256Field
+li = 12
+ri= ECPoint 3 7 5 7 :: S256Point
+
+
+ncons = 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141
+gcons = s256point 0x79be667ef9dcbbac55a06295ce870b07029bfcdb2dce28d959f2815b16f81798 0x483ada7726a3c4655da4fbfc0e1108a8fd17b448a68554199c47d08ffb10d4b8