From 8d1554b1eb97d4456fa4d042327ac3829c9e27ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=93scar=20N=C3=A1jera?= Date: Sun, 4 Jul 2021 15:40:34 +0200 Subject: 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 --- ecc.hs | 140 +++++++++++++++++++++++++++++++++++++++-------------------------- 1 file 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 -- cgit v1.2.3