Integration with Galois field library (#15)

* Use galois-field library

* Pass tests

* Use Gen monad and create arbitrary instances for arithmetic circuits

* Remove Fractional constraints in favor of PrimeField

* Upgrade CircleCI

* Remove redundant Fq type signatures

* Ensure prime fields are used in range proofs

* Update README

* Update changelog

Author: Acentelles

.circleci/config.yml

@@ -0,0 +1,22 @@
+version: 2
+jobs:
+  build:
+    docker:
+      - image: fpco/stack-build:lts
+    steps:
+      - checkout
+      - restore_cache:
+          name: Restore Cached Dependencies
+          keys:
+            - pairing-{{ checksum "package.yaml" }}
+      - run:
+          name: Resolve/Update Dependencies
+          command: stack setup
+      - run:
+          name: Run tests
+          command: stack test
+      - save_cache:
+          name: Cache Dependencies
+          key: pairing-{{ checksum "package.yaml" }}
+          paths:
+            - ".stack-work"

Bulletproofs/ArithmeticCircuit/Internal.hs

@@ -7,6 +7,8 @@ import Protolude hiding (head)
 import Data.List (head)
 import qualified Data.List as List
 import qualified Data.Map as Map
+import Test.QuickCheck
+import PrimeField (PrimeField(..), toInt)
 
 import System.Random.Shuffle (shuffleM)
 import qualified Crypto.Random.Types as Crypto (MonadRandom(..))
@@ -103,10 +105,10 @@ padAssignment Assignment{..}
     aRNew = padToNearestPowerOfTwo aR
     aONew = padToNearestPowerOfTwo aO
 
-delta :: (Eq f, Field f) => Integer -> f -> [f] -> [f] -> f
+delta :: (KnownNat p) => Integer -> PrimeField p -> [PrimeField p] -> [PrimeField p] -> PrimeField p
 delta n y zwL zwR= (powerVector (recip y) n `hadamardp` zwR) `dot` zwL
 
-commitBitVector :: (AsInteger f) => f -> [f] -> [f] -> Crypto.Point
+commitBitVector :: (KnownNat p) => PrimeField p -> [PrimeField p] -> [PrimeField p] -> Crypto.Point
 commitBitVector vBlinding vL vR = vLG `addP` vRH `addP` vBlindingH
   where
     vBlindingH = vBlinding `mulP` h
@@ -115,13 +117,13 @@ commitBitVector vBlinding vL vR = vLG `addP` vRH `addP` vBlindingH
 
 shamirGxGxG :: (Show f, Num f) => Crypto.Point -> Crypto.Point -> Crypto.Point -> f
 shamirGxGxG p1 p2 p3
-  = fromInteger $ oracle $ show q <> pointToBS p1 <> pointToBS p2 <> pointToBS p3
+  = fromInteger $ oracle $ show _q <> pointToBS p1 <> pointToBS p2 <> pointToBS p3
 
 shamirGs :: (Show f, Num f) => [Crypto.Point] -> f
-shamirGs ps = fromInteger $ oracle $ show q <> foldMap pointToBS ps
+shamirGs ps = fromInteger $ oracle $ show _q <> foldMap pointToBS ps
 
 shamirZ :: (Show f, Num f) => f -> f
-shamirZ z = fromInteger $ oracle $ show q <> show z
+shamirZ z = fromInteger $ oracle $ show _q <> show z
 
 ---------------------------------------------
 -- Polynomials
@@ -180,30 +182,7 @@ genIdenMatrix size = (\x -> (\y -> fromIntegral (fromEnum (x == y))) <$> [1..siz
 genZeroMatrix :: (Num f) => Integer -> Integer -> [[f]]
 genZeroMatrix (fromIntegral -> n) (fromIntegral -> m) = replicate n (replicate m 0)
 
-generateWv :: (Num f, MonadRandom m) => Integer -> Integer -> m [[f]]
-generateWv lConstraints m
-  | lConstraints < m = panic "Number of constraints must be bigger than m"
-  | otherwise = shuffleM (genIdenMatrix m ++ genZeroMatrix (lConstraints - m) m)
-
-generateGateWeights :: (Crypto.MonadRandom m, Num f) => Integer -> Integer -> m (GateWeights f)
-generateGateWeights lConstraints n = do
-  let genVec = ((\i -> insertAt (fromIntegral i) (oneVector n) (replicate (fromIntegral lConstraints - 1) (zeroVector n))) <$> generateMax (fromIntegral lConstraints))
-  wL <- genVec
-  wR <- genVec
-  wO <- genVec
-  pure $ GateWeights wL wR wO
-  where
-    zeroVector x = replicate (fromIntegral x) 0
-    oneVector x = replicate (fromIntegral x) 1
-
-generateRandomAssignment :: forall f m . (Num f, AsInteger f, Crypto.MonadRandom m) => Integer -> m (Assignment f)
-generateRandomAssignment n = do
-  aL <- replicateM (fromIntegral n) ((fromInteger :: Integer -> f) <$> generateMax (2^n))
-  aR <- replicateM (fromIntegral n) ((fromInteger :: Integer -> f) <$> generateMax (2^n))
-  let aO = aL `hadamardp` aR
-  pure $ Assignment aL aR aO
-
-computeInputValues :: (Field f, Eq f) => GateWeights f -> [[f]] -> Assignment f -> [f] -> [f]
+computeInputValues :: (KnownNat p) => GateWeights (PrimeField p) -> [[PrimeField p]] -> Assignment (PrimeField p) -> [PrimeField p] -> [PrimeField p]
 computeInputValues GateWeights{..} wV Assignment{..} cs
   = solveLinearSystem $ zipWith (\row s -> reverse $ s : row) wV solutions
   where
@@ -212,7 +191,7 @@ computeInputValues GateWeights{..} wV Assignment{..} cs
         ^+^ vectorMatrixProductT aO wO
         ^-^ cs
 
-gaussianReduce :: (Field f, Eq f) => [[f]] -> [[f]]
+gaussianReduce :: (KnownNat p) => [[PrimeField p]] -> [[PrimeField p]]
 gaussianReduce matrix = fixlastrow $ foldl reduceRow matrix [0..length matrix-1]
   where
     -- Swaps element at position a with element at position b.
@@ -247,13 +226,80 @@ gaussianReduce matrix = fixlastrow $ foldl reduceRow matrix [0..length matrix-1]
         nz = List.last (List.init row)
 
 -- Solve a matrix (must already be in REF form) by back substitution.
-substituteMatrix :: (Field f, Eq f) => [[f]] -> [f]
+substituteMatrix :: (KnownNat p) => [[PrimeField p]] -> [PrimeField p]
 substituteMatrix matrix = foldr next [List.last (List.last matrix)] (List.init matrix)
   where
     next row found = let
       subpart = List.init $ drop (length matrix - length found) row
       solution = List.last row - sum (zipWith (*) found subpart)
       in solution : found
 
-solveLinearSystem :: (Field f, Eq f) => [[f]] -> [f]
+solveLinearSystem :: (KnownNat p) => [[PrimeField p]] -> [PrimeField p]
 solveLinearSystem = reverse . substituteMatrix . gaussianReduce
+
+-------------------------
+-- Arbitrary instances --
+-------------------------
+
+instance (KnownNat p) => Arbitrary (ArithCircuit (PrimeField p)) where
+  arbitrary = do
+    n <- choose (1, 100)
+    m <- choose (1, n)
+    arithCircuitGen n m
+
+arithCircuitGen :: forall p. (KnownNat p) => Integer -> Integer -> Gen (ArithCircuit (PrimeField p))
+arithCircuitGen n m = do
+    -- TODO: Can lConstraints be a different value?
+    let lConstraints = m
+
+    cs <- vectorOf (fromIntegral m) arbitrary
+
+    weights@GateWeights{..} <- gateWeightsGen lConstraints n
+    let gateWeights = GateWeights wL wR wO
+
+    commitmentWeights <- wvGen lConstraints m
+    pure $ ArithCircuit gateWeights commitmentWeights cs
+      where
+        gateWeightsGen :: Integer -> Integer -> Gen (GateWeights (PrimeField p))
+        gateWeightsGen lConstraints n = do
+          let genVec = ((\i -> insertAt i (oneVector n) (replicate (fromIntegral lConstraints - 1) (zeroVector n))) <$> choose (0, fromIntegral lConstraints))
+          wL <- genVec
+          wR <- genVec
+          wO <- genVec
+          pure $ GateWeights wL wR wO
+
+        wvGen :: Integer -> Integer -> Gen [[PrimeField p]]
+        wvGen lConstraints m
+          | lConstraints < m = panic "Number of constraints must be bigger than m"
+          | otherwise = shuffle (genIdenMatrix m ++ genZeroMatrix (lConstraints - m) m)
+        zeroVector x = replicate (fromIntegral x) 0
+        oneVector x = replicate (fromIntegral x) 1
+
+
+instance (KnownNat p) => Arbitrary (Assignment (PrimeField p)) where
+  arbitrary = do
+    n <- (arbitrary :: Gen Integer)
+    arithAssignmentGen n
+
+arithAssignmentGen :: (KnownNat p) => Integer -> Gen (Assignment (PrimeField p))
+arithAssignmentGen n = do
+    aL <- vectorOf (fromIntegral n) (fromInteger <$> choose (0, 2^n))
+    aR <- vectorOf (fromIntegral n) (fromInteger <$> choose (0, 2^n))
+    let aO = aL `hadamardp` aR
+    pure $ Assignment aL aR aO
+
+instance (KnownNat p) => Arbitrary (ArithWitness (PrimeField p)) where
+  arbitrary = do
+    n <- choose (1, 100)
+    m <- choose (1, n)
+    arithCircuit <- arithCircuitGen n m
+    assignment <- arithAssignmentGen n
+    arithWitnessGen assignment arithCircuit m
+
+arithWitnessGen :: (KnownNat p) => Assignment (PrimeField p) -> ArithCircuit (PrimeField p) -> Integer -> Gen (ArithWitness (PrimeField p))
+arithWitnessGen assignment arith@ArithCircuit{..} m = do
+  commitBlinders <- vectorOf (fromIntegral m) arbitrary
+  let vs = computeInputValues weights commitmentWeights assignment cs
+      commitments = zipWith commit vs commitBlinders
+  pure $ ArithWitness assignment commitments commitBlinders
+

Bulletproofs/ArithmeticCircuit/Prover.hs

@@ -7,6 +7,7 @@ import Crypto.Random.Types (MonadRandom(..))
 import Crypto.Number.Generate (generateMax)
 import qualified Crypto.PubKey.ECC.Prim as Crypto
 import qualified Crypto.PubKey.ECC.Types as Crypto
+import PrimeField (PrimeField(..), toInt)
 
 import Bulletproofs.Curve
 import Bulletproofs.Utils hiding (shamirZ)
@@ -16,15 +17,15 @@ import Bulletproofs.ArithmeticCircuit.Internal
 -- | Generate a zero-knowledge proof of computation
 -- for an arithmetic circuit with a valid witness
 generateProof
-  :: forall f m
-   . (MonadRandom m, AsInteger f, Field f, Show f, Eq f)
-  => ArithCircuit f
-  -> ArithWitness f
-  -> m (ArithCircuitProof f)
+  :: forall p m
+   . (MonadRandom m, KnownNat p)
+  => ArithCircuit (PrimeField p)
+  -> ArithWitness (PrimeField p)
+  -> m (ArithCircuitProof (PrimeField p))
 generateProof (padCircuit -> ArithCircuit{..}) ArithWitness{..} = do
   let GateWeights{..} = weights
       Assignment{..} = padAssignment assignment
-      genBlinding = (fromInteger :: Integer -> f) <$> generateMax q
+      genBlinding = (fromInteger :: Integer -> PrimeField p) <$> generateMax _q
   aiBlinding <- genBlinding
   aoBlinding <- genBlinding
   sBlinding <- genBlinding
@@ -57,7 +58,7 @@ generateProof (padCircuit -> ArithCircuit{..}) ArithWitness{..} = do
          + (zs `dot` w)
          + delta n y zwL zwR
 
-  tBlindings <- insertAt 2 0 . (:) 0 <$> replicateM 5 ((fromInteger :: Integer -> f) <$> generateMax q)
+  tBlindings <- insertAt 2 0 . (:) 0 <$> replicateM 5 ((fromInteger :: Integer -> PrimeField p) <$> generateMax _q)
   let tCommits = zipWith commit tPoly tBlindings
 
   let x = shamirGs tCommits
@@ -70,17 +71,17 @@ generateProof (padCircuit -> ArithCircuit{..}) ArithWitness{..} = do
       commitTimesWeigths = commitBlinders `vectorMatrixProductT` commitmentWeights
       zGamma = zs `dot` commitTimesWeigths
       tBlinding = sum (zipWith (\i blinding -> blinding * (x ^ i)) [0..] tBlindings)
-                + (fSquare x * zGamma)
+                + ((x ^ 2) * zGamma)
 
-      mu = aiBlinding * x + aoBlinding * fSquare x + sBlinding * (x ^ 3)
+      mu = aiBlinding * x + aoBlinding * (x ^ 2) + sBlinding * (x ^ 3)
 
   let uChallenge = shamirU tBlinding mu t
       u = uChallenge `mulP` g
       hs' = zipWith mulP (powerVector (recip y) n) hs
       gExp = (*) x <$> (powerVector (recip y) n `hadamardp` zwR)
       hExp = (((*) x <$> zwL) ^+^ zwO) ^-^ ys
       commitmentLR = (x `mulP` aiCommit)
-                   `addP` (fSquare x `mulP` aoCommit)
+                   `addP` ((x ^ 2) `mulP` aoCommit)
                    `addP` ((x ^ 3)`mulP` sCommit)
                    `addP` sumExps gExp gs
                    `addP` sumExps hExp hs'

Bulletproofs/ArithmeticCircuit/Verifier.hs

@@ -6,6 +6,7 @@ import Data.List (head)
 
 import qualified Crypto.PubKey.ECC.Prim as Crypto
 import qualified Crypto.PubKey.ECC.Types as Crypto
+import PrimeField (PrimeField(..), toInt)
 
 import Bulletproofs.Curve
 import Bulletproofs.Utils hiding (shamirZ)
@@ -17,10 +18,10 @@ import Bulletproofs.ArithmeticCircuit.Internal
 -- | Verify that a zero-knowledge proof holds
 -- for an arithmetic circuit given committed input values
 verifyProof
-  :: (AsInteger f, Field f, Eq f, Show f)
+  :: (KnownNat p)
   => [Crypto.Point]
-  -> ArithCircuitProof f
-  -> ArithCircuit f
+  -> ArithCircuitProof (PrimeField p)
+  -> ArithCircuit (PrimeField p)
   -> Bool
 verifyProof vCommits proof@ArithCircuitProof{..} (padCircuit -> ArithCircuit{..})
   = verifyLRCommitment && verifyTPoly
@@ -55,9 +56,9 @@ verifyProof vCommits proof@ArithCircuitProof{..} (padCircuit -> ArithCircuit{..}
         rhs = (gExp `mulP` g)
             `addP` tCommitsExpSum
             `addP` sumExps vExp vCommits
-        gExp = fSquare x * (k + cQ)
+        gExp = (x ^ 2) * (k + cQ)
         cQ = zs `dot` cs
-        vExp = (*) (fSquare x) <$> (zs `vectorMatrixProduct` commitmentWeights)
+        vExp = (*) (x ^ 2) <$> (zs `vectorMatrixProduct` commitmentWeights)
         k = delta n y zwL zwR
         xs = 0 : x : 0 : (((^) x) <$> [3..6])
         tCommitsExpSum = sumExps xs tCommits
@@ -72,7 +73,7 @@ verifyProof vCommits proof@ArithCircuitProof{..} (padCircuit -> ArithCircuit{..}
         gExp = (*) x <$> (powerVector (recip y) n `hadamardp` zwR)
         hExp = (((*) x <$> zwL) ^+^ zwO) ^-^ ys
         commitmentLR = (x `mulP` aiCommit)
-                     `addP` (fSquare x `mulP` aoCommit)
+                     `addP` ((x ^ 2) `mulP` aoCommit)
                      `addP` ((x ^ 3) `mulP` sCommit)
                      `addP` sumExps gExp gs
                      `addP` sumExps hExp hs'

Bulletproofs/Curve.hs

@@ -1,5 +1,7 @@
 module Bulletproofs.Curve (
-  q,
+  _q,
+  _a,
+  _b,
   g,
   h,
   gs,
@@ -23,15 +25,34 @@ import Math.NumberTheory.Moduli.Sqrt (sqrtModP)
 import Numeric
 import qualified Data.List as L
 
+-- Implementation using the elliptic curve secp256k12
+-- which has 128 bit security.
+-- Parameters as in Cryptonite:
+-- SEC_p256k1 = CurveFP  $ CurvePrime
+--     0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f
+--     (CurveCommon
+--         { ecc_a = 0x0000000000000000000000000000000000000000000000000000000000000000
+--         , ecc_b = 0x0000000000000000000000000000000000000000000000000000000000000007
+--         , ecc_g = Point 0x79be667ef9dcbbac55a06295ce870b07029bfcdb2dce28d959f2815b16f81798
+--                         0x483ada7726a3c4655da4fbfc0e1108a8fd17b448a68554199c47d08ffb10d4b8
+--         , ecc_n = 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141
+--         , ecc_h = 1
+--         })
 curveName :: Crypto.CurveName
 curveName = Crypto.SEC_p256k1
 
 curve :: Crypto.Curve
 curve = Crypto.getCurveByName curveName
 
 -- | Order of the curve
-q :: Integer
-q = Crypto.ecc_n . Crypto.common_curve $ curve
+_q :: Integer
+_q = Crypto.ecc_n . Crypto.common_curve $ curve
+
+_b :: Integer
+_b = Crypto.ecc_b . Crypto.common_curve $ curve
+
+_a :: Integer
+_a = Crypto.ecc_a . Crypto.common_curve $ curve
 
 -- | Generator of the curve
 g :: Crypto.Point
@@ -64,8 +85,8 @@ pointToBS Crypto.PointO      = ""
 pointToBS (Crypto.Point x y) = show x <> show y
 
 -- | Characteristic of the underlying finite field of the elliptic curve
-p :: Integer
-p = Crypto.ecc_p cp
+_p :: Integer
+_p = Crypto.ecc_p cp
   where
     cp = case curve of
       Crypto.CurveFP c -> c
@@ -82,6 +103,6 @@ generateH basePoint extra =
       then Crypto.Point x y
       else generateH basePoint (toS $ '1':extra)
   where
-    x = oracle (pointToBS basePoint <> toS extra) `mod` p
-    yM = sqrtModP (x ^ 3 + 7) p
+    x = oracle (pointToBS basePoint <> toS extra) `mod` _p
+    yM = sqrtModP (x ^ 3 + 7) _p