diff --git a/Bulletproofs/ArithmeticCircuit.hs b/Bulletproofs/ArithmeticCircuit.hs new file mode 100644 --- /dev/null +++ b/Bulletproofs/ArithmeticCircuit.hs @@ -0,0 +1,14 @@ +module Bulletproofs.ArithmeticCircuit +( generateProof +, verifyProof + +, ArithCircuitProof(..) +, ArithCircuit(..) +, ArithWitness(..) +, GateWeights(..) +, Assignment(..) +) where + +import Bulletproofs.ArithmeticCircuit.Internal +import Bulletproofs.ArithmeticCircuit.Prover +import Bulletproofs.ArithmeticCircuit.Verifier diff --git a/Bulletproofs/ArithmeticCircuit/Internal.hs b/Bulletproofs/ArithmeticCircuit/Internal.hs new file mode 100644 --- /dev/null +++ b/Bulletproofs/ArithmeticCircuit/Internal.hs @@ -0,0 +1,257 @@ +{-# LANGUAGE ViewPatterns, RecordWildCards, ScopedTypeVariables #-} +{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-} + +module Bulletproofs.ArithmeticCircuit.Internal where + +import Protolude hiding (head) +import Control.Monad.Fail +import Data.List (head) +import qualified Data.List as List +import qualified Data.Map as Map + +import System.Random.Shuffle (shuffleM) +import qualified Crypto.Random.Types as Crypto (MonadRandom(..)) +import Crypto.Number.Generate (generateMax, generateBetween) +import Control.Monad.Random (MonadRandom) +import qualified Crypto.PubKey.ECC.Types as Crypto +import qualified Crypto.PubKey.ECC.Prim as Crypto + +import Bulletproofs.Curve +import Bulletproofs.Utils +import Bulletproofs.RangeProof +import qualified Bulletproofs.InnerProductProof as IPP + +data ArithCircuitProofError + = TooManyGates Integer -- ^ The number of gates is too high + | NNotPowerOf2 Integer -- ^ The number of gates is not a power of 2 + deriving (Show, Eq) + +data ArithCircuitProof f + = ArithCircuitProof + { tBlinding :: f + -- ^ Blinding factor of the T1 and T2 commitments, + -- combined into the form required to make the committed version of the x-polynomial add up + , mu :: f + -- ^ Blinding factor required for the Verifier to verify commitments A, S + , t :: f + -- ^ Dot product of vectors l and r that prove knowledge of the value in range + -- t = t(x) = l(x) · r(x) + , aiCommit :: Crypto.Point + -- ^ Commitment to vectors aL and aR + , aoCommit :: Crypto.Point + -- ^ Commitment to vectors aO + , sCommit :: Crypto.Point + -- ^ Commitment to new vectors sL, sR, created at random by the Prover + , tCommits :: [Crypto.Point] + -- ^ Commitments to t1, t3, t4, t5, t6 + , productProof :: IPP.InnerProductProof f + } deriving (Show, Eq, Generic, NFData) + +data ArithCircuit f + = ArithCircuit + { weights :: GateWeights f + -- ^ Weights for vectors of left and right inputs and for vector of outputs + , commitmentWeights :: [[f]] + -- ^ Weigths for a commitments V of rank m + , cs :: [f] + -- ^ Vector of constants of size Q + } deriving (Show, Eq, Generic, NFData) + + +data GateWeights f + = GateWeights + { wL :: [[f]] -- ^ WL ∈ F^(Q x n) + , wR :: [[f]] -- ^ WR ∈ F^(Q x n) + , wO :: [[f]] -- ^ WO ∈ F^(Q x n) + } deriving (Show, Eq, Generic, NFData) + +data ArithWitness f + = ArithWitness + { assignment :: Assignment f -- ^ Vectors of left and right inputs and vector of outputs + , commitments :: [Crypto.Point] -- ^ Vector of commited input values ∈ F^m + , commitBlinders :: [f] -- ^ Vector of blinding factors for input values ∈ F^m + } deriving (Show, Eq, Generic, NFData) + +data Assignment f + = Assignment + { aL :: [f] -- ^ aL ∈ F^n. Vector of left inputs of each multiplication gate + , aR :: [f] -- ^ aR ∈ F^n. Vector of right inputs of each multiplication gate + , aO :: [f] -- ^ aO ∈ F^n. Vector of outputs of each multiplication gate + } deriving (Show, Eq, Generic, NFData) + +-- | Pad circuit weights to make n be a power of 2, which +-- is required to compute the inner product proof +padCircuit :: Num f => ArithCircuit f -> ArithCircuit f +padCircuit ArithCircuit{..} + = ArithCircuit + { weights = GateWeights wLNew wRNew wONew + , commitmentWeights = commitmentWeights + , cs = cs + } + where + GateWeights{..} = weights + wLNew = padToNearestPowerOfTwo <$> wL + wRNew = padToNearestPowerOfTwo <$> wR + wONew = padToNearestPowerOfTwo <$> wO + +-- | Pad assignment vectors to make their length n be a power of 2, which +-- is required to compute the inner product proof +padAssignment :: Num f => Assignment f -> Assignment f +padAssignment Assignment{..} + = Assignment aLNew aRNew aONew + where + aLNew = padToNearestPowerOfTwo aL + aRNew = padToNearestPowerOfTwo aR + aONew = padToNearestPowerOfTwo aO + +delta :: (Eq f, Field f) => Integer -> f -> [f] -> [f] -> f +delta n y zwL zwR= (powerVector (recip y) n `hadamardp` zwR) `dot` zwL + +commitBitVector :: (AsInteger f) => f -> [f] -> [f] -> Crypto.Point +commitBitVector vBlinding vL vR = vLG `addP` vRH `addP` vBlindingH + where + vBlindingH = vBlinding `mulP` h + vLG = foldl' addP Crypto.PointO ( zipWith mulP vL gs ) + vRH = foldl' addP Crypto.PointO ( zipWith mulP vR hs ) + +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 + +shamirGs :: (Show f, Num f) => [Crypto.Point] -> f +shamirGs ps = fromInteger $ oracle $ show q <> foldMap pointToBS ps + +shamirZ :: (Show f, Num f) => f -> f +shamirZ z = fromInteger $ oracle $ show q <> show z + +--------------------------------------------- +-- Polynomials +--------------------------------------------- + +evaluatePolynomial :: (Num f) => Integer -> [[f]] -> f -> [f] +evaluatePolynomial (fromIntegral -> n) poly x + = foldl' + (\acc (idx, e) -> acc ^+^ ((*) (x ^ idx) <$> e)) + (replicate n 0) + (zip [0..] poly) + +multiplyPoly :: Num n => [[n]] -> [[n]] -> [n] +multiplyPoly l r + = snd <$> Map.toList (foldl' (\accL (i, li) + -> foldl' + (\accR (j, rj) -> case Map.lookup (i + j) accR of + Just x -> Map.insert (i + j) (x + (li `dot` rj)) accR + Nothing -> Map.insert (i + j) (li `dot` rj) accR + ) accL (zip [0..] r)) + (Map.empty :: Num n => Map.Map Int n) + (zip [0..] l)) + + +--------------------------------------------- +-- Linear algebra +--------------------------------------------- + +vectorMatrixProduct :: (Num f) => [f] -> [[f]] -> [f] +vectorMatrixProduct v m + = sum . zipWith (*) v <$> transpose m + +vectorMatrixProductT :: (Num f) => [f] -> [[f]] -> [f] +vectorMatrixProductT v m + = sum . zipWith (*) v <$> m + +matrixVectorProduct :: (Num f) => [[f]] -> [f] -> [f] +matrixVectorProduct m v + = head $ matrixProduct m [v] + +powerMatrix :: (Num f) => [[f]] -> Integer -> [[f]] +powerMatrix m 0 = m +powerMatrix m n = matrixProduct m (powerMatrix m (n-1)) + +matrixProduct :: Num a => [[a]] -> [[a]] -> [[a]] +matrixProduct a b = (\ar -> sum . zipWith (*) ar <$> transpose b) <$> a + +insertAt :: Int -> a -> [a] -> [a] +insertAt z y xs = as ++ (y : bs) + where + (as, bs) = splitAt z xs + +genIdenMatrix :: (Num f) => Integer -> [[f]] +genIdenMatrix size = (\x -> (\y -> fromIntegral (fromEnum (x == y))) <$> [1..size]) <$> [1..size] + +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, MonadFail m) => Integer -> Integer -> m (GateWeights f) +generateGateWeights lConstraints n = do + [wL, wR, wO] <- replicateM 3 ((\i -> insertAt (fromIntegral i) (oneVector n) (replicate (fromIntegral lConstraints - 1) (zeroVector n))) <$> generateMax (fromIntegral lConstraints)) + 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 GateWeights{..} wV Assignment{..} cs + = solveLinearSystem $ zipWith (\row s -> reverse $ s : row) wV solutions + where + solutions = vectorMatrixProductT aL wL + ^+^ vectorMatrixProductT aR wR + ^+^ vectorMatrixProductT aO wO + ^-^ cs + +gaussianReduce :: (Field f, Eq f) => [[f]] -> [[f]] +gaussianReduce matrix = fixlastrow $ foldl reduceRow matrix [0..length matrix-1] + where + -- Swaps element at position a with element at position b. + swap xs a b + | a > b = swap xs b a + | a == b = xs + | a < b = let (p1, p2) = splitAt a xs + (p3, p4) = splitAt (b - a - 1) (List.tail p2) + in p1 ++ [xs List.!! b] ++ p3 ++ [xs List.!! a] ++ List.tail p4 + + -- Concat the lists and repeat + reduceRow matrix1 r = take r matrix2 ++ [row1] ++ nextrows + where + --First non-zero element on or below (r,r). + firstnonzero = head $ filter (\x -> matrix1 List.!! x List.!! r /= 0) [r..length matrix1 - 1] + --Matrix with row swapped (if needed) + matrix2 = swap matrix1 r firstnonzero + --Row we're working with + row = matrix2 List.!! r + --Make it have 1 as the leading coefficient + row1 = (\x -> x * recip (row List.!! r)) <$> row + --Subtract nr from row1 while multiplying + subrow nr = let k = nr List.!! r in zipWith (\a b -> k*a - b) row1 nr + --Apply subrow to all rows below + nextrows = subrow <$> drop (r + 1) matrix2 + + + fixlastrow matrix' = a ++ [List.init (List.init row) ++ [1, z * recip nz]] + where + a = List.init matrix'; row = List.last matrix' + z = List.last row + 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 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 = reverse . substituteMatrix . gaussianReduce diff --git a/Bulletproofs/ArithmeticCircuit/Prover.hs b/Bulletproofs/ArithmeticCircuit/Prover.hs new file mode 100644 --- /dev/null +++ b/Bulletproofs/ArithmeticCircuit/Prover.hs @@ -0,0 +1,119 @@ +{-# LANGUAGE RecordWildCards, ScopedTypeVariables, ViewPatterns #-} +module Bulletproofs.ArithmeticCircuit.Prover where + +import Protolude + +import Control.Monad.Fail +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 Bulletproofs.Curve +import Bulletproofs.Utils hiding (shamirZ) +import qualified Bulletproofs.InnerProductProof as IPP +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, MonadFail m, AsInteger f, Field f, Show f, Eq f) + => ArithCircuit f + -> ArithWitness f + -> m (ArithCircuitProof f) +generateProof (padCircuit -> ArithCircuit{..}) ArithWitness{..} = do + let GateWeights{..} = weights + let Assignment{..} = padAssignment assignment + [aiBlinding, aoBlinding, sBlinding] <- replicateM 3 ((fromInteger :: Integer -> f) <$> generateMax q) + let n = fromIntegral $ length aL + aiCommit = commitBitVector aiBlinding aL aR -- commitment to aL, aR + aoCommit = commitBitVector aoBlinding aO [] -- commitment to aO + + (sL, sR) <- chooseBlindingVectors n -- choose blinding vectors sL, sR + let sCommit = commitBitVector sBlinding sL sR -- commitment to sL, sR + + let y = shamirGxGxG aiCommit aoCommit sCommit + z = shamirZ y + ys = powerVector y n + zs = drop 1 (powerVector z (qLen + 1)) + + zwL = zs `vectorMatrixProduct` wL + zwR = zs `vectorMatrixProduct` wR + zwO = zs `vectorMatrixProduct` wO + + -- Polynomials + [lPoly, rPoly] = computePolynomials n aL aR aO sL sR y zwL zwR zwO + tPoly = multiplyPoly lPoly rPoly + + w = (aL `vectorMatrixProductT` wL) + ^+^ (aR `vectorMatrixProductT` wR) + ^+^ (aO `vectorMatrixProductT` wO) + + t2 = (aL `dot` (aR `hadamardp` ys)) + - (aO `dot` ys) + + (zs `dot` w) + + delta n y zwL zwR + + tBlindings <- insertAt 2 0 . (:) 0 <$> replicateM 5 ((fromInteger :: Integer -> f) <$> generateMax q) + let tCommits = zipWith commit tPoly tBlindings + + let x = shamirGs tCommits + evalTCommit = foldl' addP Crypto.PointO (zipWith mulP (powerVector x 7) tCommits) + + let ls = evaluatePolynomial n lPoly x + rs = evaluatePolynomial n rPoly x + t = ls `dot` rs + + commitTimesWeigths = commitBlinders `vectorMatrixProductT` commitmentWeights + zGamma = zs `dot` commitTimesWeigths + tBlinding = sum (zipWith (\i blinding -> blinding * (x ^ i)) [0..] tBlindings) + + (fSquare x * zGamma) + + mu = aiBlinding * x + aoBlinding * fSquare x + 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 ^ 3)`mulP` sCommit) + `addP` foldl' addP Crypto.PointO (zipWith mulP gExp gs) + `addP` foldl' addP Crypto.PointO (zipWith mulP hExp hs') + `addP` Crypto.pointNegate curve (mu `mulP` h) + `addP` (t `mulP` u) + + let productProof = IPP.generateProof + IPP.InnerProductBase { bGs = gs, bHs = hs', bH = u } + commitmentLR + IPP.InnerProductWitness { ls = ls, rs = rs } + + pure ArithCircuitProof + { tBlinding = tBlinding + , mu = mu + , t = t + , aiCommit = aiCommit + , aoCommit = aoCommit + , sCommit = sCommit + , tCommits = tCommits + , productProof = productProof + } + where + qLen = fromIntegral $ length commitmentWeights + computePolynomials n aL aR aO sL sR y zwL zwR zwO + = [ [l0, l1, l2, l3] + , [r0, r1, r2, r3] + ] + where + l0 = replicate (fromIntegral n) 0 + l1 = aL ^+^ (powerVector (recip y) n `hadamardp` zwR) + l2 = aO + l3 = sL + + r0 = zwO ^-^ powerVector y n + r1 = (powerVector y n `hadamardp` aR) ^+^ zwL + r2 = replicate (fromIntegral n) 0 + r3 = powerVector y n `hadamardp` sR + diff --git a/Bulletproofs/ArithmeticCircuit/Verifier.hs b/Bulletproofs/ArithmeticCircuit/Verifier.hs new file mode 100644 --- /dev/null +++ b/Bulletproofs/ArithmeticCircuit/Verifier.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE RecordWildCards, ViewPatterns #-} +module Bulletproofs.ArithmeticCircuit.Verifier where + +import Protolude hiding (head) +import Data.List (head) + +import qualified Crypto.PubKey.ECC.Prim as Crypto +import qualified Crypto.PubKey.ECC.Types as Crypto + +import Bulletproofs.Curve +import Bulletproofs.Utils hiding (shamirZ) +import Bulletproofs.RangeProof.Internal hiding (delta) +import qualified Bulletproofs.InnerProductProof as IPP + +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) + => [Crypto.Point] + -> ArithCircuitProof f + -> ArithCircuit f + -> Bool +verifyProof vCommits proof@ArithCircuitProof{..} (padCircuit -> ArithCircuit{..}) + = verifyLRCommitment && verifyTPoly + where + GateWeights{..} = weights + n = fromIntegral $ length $ head wL + qLen = fromIntegral $ length wL + + x = shamirGs tCommits + y = shamirGxGxG aiCommit aoCommit sCommit + z = shamirZ y + + ys = powerVector y n + zs = drop 1 (powerVector z (qLen + 1)) + zwL = zs `vectorMatrixProduct` wL + zwR = zs `vectorMatrixProduct` wR + zwO = zs `vectorMatrixProduct` wO + + hs' = zipWith mulP (powerVector (recip y) n) hs + + wLCommit = foldl' addP Crypto.PointO (zipWith mulP (zs `vectorMatrixProduct` wL) hs') + wRCommit = foldl' addP Crypto.PointO (zipWith mulP wRExp gs) + wOCommit = foldl' addP Crypto.PointO (zipWith mulP (zs `vectorMatrixProduct` wO) hs') + wRExp = powerVector (recip y) n `hadamardp` (zs `vectorMatrixProduct` wL) + + uChallenge = shamirU tBlinding mu t + u = uChallenge `mulP` g + + verifyTPoly = lhs == rhs + where + lhs = commit t tBlinding + rhs = (gExp `mulP` g) + `addP` tCommitsExpSum + `addP` foldl' addP Crypto.PointO ( zipWith mulP vExp vCommits ) + gExp = fSquare x * (k + cQ) + cQ = zs `dot` cs + vExp = (*) (fSquare x) <$> (zs `vectorMatrixProduct` commitmentWeights) + k = delta n y zwL zwR + xs = 0 : x : 0 : (((^) x) <$> [3..6]) + tCommitsExpSum = foldl' addP Crypto.PointO (zipWith mulP xs tCommits) + + verifyLRCommitment + = IPP.verifyProof + n + IPP.InnerProductBase { bGs = gs, bHs = hs', bH = u } + commitmentLR + productProof + where + gExp = (*) x <$> (powerVector (recip y) n `hadamardp` zwR) + hExp = (((*) x <$> zwL) ^+^ zwO) ^-^ ys + commitmentLR = (x `mulP` aiCommit) + `addP` (fSquare x `mulP` aoCommit) + `addP` ((x ^ 3) `mulP` sCommit) + `addP` foldl' addP Crypto.PointO (zipWith mulP gExp gs) + `addP` foldl' addP Crypto.PointO (zipWith mulP hExp hs') + `addP` Crypto.pointNegate curve (mu `mulP` h) + `addP` (t `mulP` u) diff --git a/Bulletproofs/Fq.hs b/Bulletproofs/Fq.hs --- a/Bulletproofs/Fq.hs +++ b/Bulletproofs/Fq.hs @@ -1,19 +1,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE DeriveGeneric #-} -module Bulletproofs.Fq ( - Fq(..), - new, - inv, - fqInv, - fqZero, - fqOne, - fqSquare, - fqCube, - fqSubV, - fqAddV, - euclidean, - random -) where +module Bulletproofs.Fq where import Protolude @@ -28,7 +16,7 @@ -- | Prime field with characteristic @_q@ newtype Fq = Fq Integer -- ^ Use @new@ instead of this constructor - deriving (Show, Eq, Bits, Ord) + deriving (Show, Eq, Bits, Ord, Generic, NFData) instance Num Fq where (+) = fqAdd @@ -88,6 +76,13 @@ fqCube :: Fq -> Fq fqCube x = fqMul x (fqMul x x) +fqPower :: Fq -> Integer -> Fq +fqPower base exp = fqPower' base exp (Fq 1) + +fqPower' :: Fq -> Integer -> Fq -> Fq +fqPower' base 0 acc = acc +fqPower' base exp acc = fqPower' base (exp - 1) (fqMul base acc) + inv :: Fq -> Fq inv (Fq a) = Fq $ euclidean a q `mod` q @@ -109,15 +104,5 @@ where c = a `div` b d = a `mod` b -random :: MonadRandom m => Integer -> m Fq -random n = Fq <$> generateMax (2^n) - -fqAddV :: [Fq] -> [Fq] -> [Fq] -fqAddV = zipWith (+) - -fqSubV :: [Fq] -> [Fq] -> [Fq] -fqSubV = zipWith (-) - -fqMulV :: [Fq] -> [Fq] -> [Fq] -fqMulV = zipWith (*) - +random :: MonadRandom m => m Fq +random = Fq <$> generateMax q diff --git a/Bulletproofs/InnerProductProof/Internal.hs b/Bulletproofs/InnerProductProof/Internal.hs --- a/Bulletproofs/InnerProductProof/Internal.hs +++ b/Bulletproofs/InnerProductProof/Internal.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-} module Bulletproofs.InnerProductProof.Internal ( InnerProductProof(..), InnerProductWitness(..), @@ -7,9 +8,8 @@ import Protolude import qualified Crypto.PubKey.ECC.Types as Crypto -import Bulletproofs.Fq -data InnerProductProof +data InnerProductProof f = InnerProductProof { lCommits :: [Crypto.Point] -- ^ Vector of commitments of the elements in the original vector l @@ -17,20 +17,20 @@ , rCommits :: [Crypto.Point] -- ^ Vector of commitments of the elements in the original vector r -- whose size is the logarithm of base 2 of the size of vector r - , l :: Fq + , l :: f -- ^ Remaining element of vector l at the end of -- the recursive algorithm that generates the inner-product proof - , r :: Fq + , r :: f -- ^ Remaining element of vector r at the end of -- the recursive algorithm that generates the inner-product proof - } deriving (Show, Eq) + } deriving (Show, Eq, Generic, NFData) -data InnerProductWitness +data InnerProductWitness f = InnerProductWitness - { ls :: [Fq] + { ls :: [f] -- ^ Vector of values l that the prover uses to compute lCommits -- in the recursive inner product algorithm - , rs :: [Fq] + , rs :: [f] -- ^ Vector of values r that the prover uses to compute rCommits -- in the recursive inner product algorithm } deriving (Show, Eq) diff --git a/Bulletproofs/InnerProductProof/Prover.hs b/Bulletproofs/InnerProductProof/Prover.hs --- a/Bulletproofs/InnerProductProof/Prover.hs +++ b/Bulletproofs/InnerProductProof/Prover.hs @@ -1,6 +1,6 @@ {-# LANGUAGE NamedFieldPuns, MultiWayIf #-} -module Bulletproofs.InnerProductProof.Prover ( +module Bulletproofs.InnerProductProof.Prover ( generateProof, ) where @@ -13,30 +13,31 @@ import Bulletproofs.Curve import Bulletproofs.Utils -import Bulletproofs.Fq as Fq import Bulletproofs.InnerProductProof.Internal -- | Generate proof that a witness l, r satisfies the inner product relation -- on public input (Gs, Hs, h) generateProof - :: InnerProductBase -- ^ Generators Gs, Hs, h + :: (AsInteger f, Eq f, Field f) + => InnerProductBase -- ^ Generators Gs, Hs, h -> Crypto.Point -- ^ Commitment P = A + xS − zG + (z*y^n + z^2 * 2^n) * hs' of vectors l and r -- whose inner product is t - -> InnerProductWitness + -> InnerProductWitness f -- ^ Vectors l and r that hide bit vectors aL and aR, respectively - -> InnerProductProof + -> InnerProductProof f generateProof productBase commitmentLR witness = generateProof' productBase commitmentLR witness [] [] generateProof' - :: InnerProductBase + :: (AsInteger f, Eq f, Field f) + => InnerProductBase -> Crypto.Point - -> InnerProductWitness + -> InnerProductWitness f -> [Crypto.Point] -> [Crypto.Point] - -> InnerProductProof + -> InnerProductProof f generateProof' InnerProductBase{ bGs, bHs, bH } commitmentLR @@ -44,6 +45,7 @@ lCommits rCommits = case (ls, rs) of + ([], []) -> InnerProductProof [] [] 0 0 ([l], [r]) -> InnerProductProof (reverse lCommits) (reverse rCommits) l r _ -> if | not checkLGs -> panic "Error in: l' * Gs' == l * Gs + x^2 * A_L + x^(-2) * A_R" | not checkRHs -> panic "Error in: r' * Hs' == r * Hs + x^2 * B_L + x^(-2) * B_R" @@ -65,8 +67,8 @@ (gsLeft, gsRight) = splitAt nPrime bGs (hsLeft, hsRight) = splitAt nPrime bHs - cL = dotp lsLeft rsRight - cR = dotp lsRight rsLeft + cL = dot lsLeft rsRight + cR = dot lsRight rsLeft lCommit = foldl' addP Crypto.PointO (zipWith mulP lsLeft gsRight) `addP` @@ -82,20 +84,20 @@ x = shamirX' commitmentLR lCommit rCommit - xInv = inv x + xInv = recip x xs = replicate nPrime x xsInv = replicate nPrime xInv gs'' = zipWith addP (zipWith mulP xsInv gsLeft) (zipWith mulP xs gsRight) hs'' = zipWith addP (zipWith mulP xs hsLeft) (zipWith mulP xsInv hsRight) - ls' = ((*) x <$> lsLeft) `fqAddV` ((*) xInv <$> lsRight) - rs' = ((*) xInv <$> rsLeft) `fqAddV` ((*) x <$> rsRight) + ls' = ((*) x <$> lsLeft) ^+^ ((*) xInv <$> lsRight) + rs' = ((*) xInv <$> rsLeft) ^+^ ((*) x <$> rsRight) commitmentLR' - = (fqSquare x `mulP` lCommit) + = (fSquare x `mulP` lCommit) `addP` - (fqSquare xInv `mulP` rCommit) + (fSquare xInv `mulP` rCommit) `addP` commitmentLR @@ -109,8 +111,8 @@ bL' = foldl' addP Crypto.PointO (zipWith mulP rsLeft hsRight) bR' = foldl' addP Crypto.PointO (zipWith mulP rsRight hsLeft) - z = dotp ls rs - z' = dotp ls' rs' + z = dot ls rs + z' = dot ls' rs' lGs = foldl' addP Crypto.PointO (zipWith mulP ls bGs) rHs = foldl' addP Crypto.PointO (zipWith mulP rs bHs) @@ -123,23 +125,23 @@ == foldl' addP Crypto.PointO (zipWith mulP ls bGs) `addP` - (fqSquare x `mulP` aL') + (fSquare x `mulP` aL') `addP` - (fqSquare xInv `mulP` aR') + (fSquare xInv `mulP` aR') checkRHs = rHs' == foldl' addP Crypto.PointO (zipWith mulP rs bHs) `addP` - (fqSquare x `mulP` bR') + (fSquare x `mulP` bR') `addP` - (fqSquare xInv `mulP` bL') + (fSquare xInv `mulP` bL') checkLBs - = dotp ls' rs' + = dot ls' rs' == - dotp ls rs + fqSquare x * cL + fqSquare xInv * cR + dot ls rs + fSquare x * cL + fSquare xInv * cR checkC = commitmentLR diff --git a/Bulletproofs/InnerProductProof/Verifier.hs b/Bulletproofs/InnerProductProof/Verifier.hs --- a/Bulletproofs/InnerProductProof/Verifier.hs +++ b/Bulletproofs/InnerProductProof/Verifier.hs @@ -1,6 +1,6 @@ -{-# LANGUAGE RecordWildCards, NamedFieldPuns, MultiWayIf #-} +{-# LANGUAGE RecordWildCards, NamedFieldPuns, MultiWayIf, ScopedTypeVariables #-} -module Bulletproofs.InnerProductProof.Verifier ( +module Bulletproofs.InnerProductProof.Verifier ( verifyProof, ) where @@ -13,17 +13,16 @@ import Bulletproofs.Curve import Bulletproofs.Utils -import Bulletproofs.Fq as Fq -import Bulletproofs.RangeProof.Internal import Bulletproofs.InnerProductProof.Internal -- | Optimized non-interactive verifier using multi-exponentiation and batch verification verifyProof - :: Integer -- ^ Range upper bound + :: (AsInteger f, Field f) + => Integer -- ^ Range upper bound -> InnerProductBase -- ^ Generators Gs, Hs, h -> Crypto.Point -- ^ Commitment P - -> InnerProductProof + -> InnerProductProof f -- ^ Proof that a secret committed value lies in a certain interval -> Bool verifyProof n productBase@InnerProductBase{..} commitmentLR productProof@InnerProductProof{ l, r } @@ -41,35 +40,36 @@ gsCommit = foldl' addP Crypto.PointO (zipWith mulP otherExponents bGs) hsCommit = foldl' addP Crypto.PointO (zipWith mulP (reverse otherExponents) bHs) -mkChallenges :: InnerProductProof -> Crypto.Point -> ([Fq], [Fq], Crypto.Point) +mkChallenges :: (AsInteger f, Field f) => InnerProductProof f -> Crypto.Point -> ([f], [f], Crypto.Point) mkChallenges InnerProductProof{ lCommits, rCommits } commitmentLR = foldl' (\(xs, xsInv, accC) (li, ri) -> let x = shamirX' accC li ri - xInv = inv x - c = (fqSquare x `mulP` li) `addP` (fqSquare xInv `mulP` ri) `addP` accC + xInv = recip x + c = (fSquare x `mulP` li) `addP` (fSquare xInv `mulP` ri) `addP` accC in (x:xs, xInv:xsInv, c) ) ([], [], commitmentLR) (zip lCommits rCommits) -mkOtherExponents :: Integer -> [Fq] -> [Fq] +mkOtherExponents :: forall f . (AsInteger f, Field f) => Integer -> [f] -> [f] mkOtherExponents n challenges = Map.elems $ foldl' f - (Map.fromList [(0, Fq.inv $ product challenges)]) + (Map.fromList [(0, recip $ product challenges)]) [0..n'-1] where n' = n `div` 2 f acc i = foldl' (f' i) acc [0..logBase2 n-1] - f' :: Integer -> Map.Map Integer Fq -> Integer -> Map.Map Integer Fq + + f' :: Integer -> Map.Map Integer f -> Integer -> Map.Map Integer f f' i acc' j = let i1 = (2^j) + i in if | i1 >= n -> acc' | Map.member i1 acc' -> acc' | otherwise -> Map.insert i1 - (acc' Map.! i * fqSquare (challenges L.!! fromIntegral j)) + (acc' Map.! i * fSquare (challenges L.!! fromIntegral j)) acc' diff --git a/Bulletproofs/MultiRangeProof.hs b/Bulletproofs/MultiRangeProof.hs new file mode 100644 --- /dev/null +++ b/Bulletproofs/MultiRangeProof.hs @@ -0,0 +1,12 @@ +module Bulletproofs.MultiRangeProof ( + RangeProof(..) + , RangeProofError(..) + + , generateProof + , generateProofUnsafe + , verifyProof +) where + +import Bulletproofs.RangeProof.Internal +import Bulletproofs.MultiRangeProof.Prover +import Bulletproofs.MultiRangeProof.Verifier diff --git a/Bulletproofs/MultiRangeProof/Prover.hs b/Bulletproofs/MultiRangeProof/Prover.hs new file mode 100644 --- /dev/null +++ b/Bulletproofs/MultiRangeProof/Prover.hs @@ -0,0 +1,183 @@ +{-# LANGUAGE RecordWildCards, MultiWayIf, ScopedTypeVariables #-} + +module Bulletproofs.MultiRangeProof.Prover ( + generateProof, + generateProofUnsafe, +) where + +import Protolude + +import Control.Monad.Fail +import Crypto.Random.Types (MonadRandom(..)) +import Crypto.Number.Generate (generateMax) +import qualified Crypto.PubKey.ECC.Generate as Crypto +import qualified Crypto.PubKey.ECC.Prim as Crypto +import qualified Crypto.PubKey.ECC.Types as Crypto + +import Bulletproofs.Curve +import Bulletproofs.Utils +import Bulletproofs.RangeProof.Internal + +import Bulletproofs.InnerProductProof as IPP hiding (generateProof) +import qualified Bulletproofs.InnerProductProof as IPP + +-- | Prove that a list of values lies in a specific range +generateProof + :: (AsInteger f, Eq f, Field f, Show f, MonadRandom m, MonadFail m) + => Integer -- ^ Upper bound of the range we want to prove + -> [(Integer, Integer)] + -- ^ Values we want to prove in range and their blinding factors + -> ExceptT RangeProofError m (RangeProof f) +generateProof upperBound vsAndvBlindings = do + unless (upperBound < q) $ throwE $ UpperBoundTooLarge upperBound + + case doubleLogM of + Nothing -> throwE $ NNotPowerOf2 upperBound + Just n -> do + unless (checkRanges n vs) $ throwE $ ValuesNotInRange vs + + lift $ generateProofUnsafe upperBound vsAndvBlindingsExp2 + + where + doubleLogM :: Maybe Integer + doubleLogM = do + x <- logBase2M upperBound + logBase2M x + pure x + vs = fst <$> vsAndvBlindings + m = length vsAndvBlindings + residue = replicate (2 ^ log2Ceil m - m) (0, 0) + -- Vector of values passed must be of length 2^x + vsAndvBlindingsExp2 = vsAndvBlindings ++ residue + + +-- | Generate range proof from valid inputs +generateProofUnsafe + :: forall f m + . (AsInteger f, Eq f, Field f, Show f, MonadRandom m, MonadFail m) + => Integer -- ^ Upper bound of the range we want to prove + -> [(Integer, Integer)] + -- ^ Values we want to prove in range and their blinding factors + -> m (RangeProof f) +generateProofUnsafe upperBound vsAndvBlindings = do + let n = logBase2 upperBound + m = fromIntegral $ length vsAndvBlindings + nm = n * m + + vsF :: [f] + vsF = (fromInteger . fst) <$> vsAndvBlindings + + vBlindingsF :: [f] + vBlindingsF = (fromInteger . snd) <$> vsAndvBlindings + + let aL = reversedEncodeBitMulti n vsF + aR = complementaryVector aL + + (sL, sR) <- chooseBlindingVectors nm + + [aBlinding, sBlinding] + <- replicateM 2 ((fromInteger :: Integer -> f) <$> generateMax q) + + (aCommit, sCommit) <- commitBitVectors aBlinding sBlinding aL aR sL sR + + -- Oracle generates y, z from a, c + let y = shamirY aCommit sCommit + z = shamirZ aCommit sCommit y + + let lrPoly@LRPolys{..} = computeLRPolys n m aL aR sL sR y z + tPoly@TPoly{..} = computeTPoly lrPoly + + [t1Blinding, t2Blinding] + <- replicateM 2 ((fromInteger :: Integer -> f) <$> generateMax q) + + + let t1Commit = commit t1 t1Blinding + t2Commit = commit t2 t2Blinding + + -- Oracle generates x from previous data in transcript + let x = shamirX aCommit sCommit t1Commit t2Commit y z + + let ls = l0 ^+^ ((*) x <$> l1) + rs = r0 ^+^ ((*) x <$> r1) + t = t0 + (t1 * x) + (t2 * fSquare x) + + unless (t == dot ls rs) $ + panic "Error on: t = dot l r" + + unless (t1 == dot l1 r0 + dot l0 r1) $ + panic "Error on: t1 = dot l1 r0 + dot l0 r1" + + let tBlinding = sum (zipWith (\vBlindingF j -> (z ^ (j + 1)) * vBlindingF) vBlindingsF [1..m]) + + (t2Blinding * fSquare x) + + (t1Blinding * x) + mu = aBlinding + (sBlinding * x) + + let uChallenge = shamirU tBlinding mu t + u = uChallenge `mulP` g + hs' = zipWith (\yi hi-> recip yi `mulP` hi) (powerVector y nm) hs + commitmentLR = computeLRCommitment n m aCommit sCommit t tBlinding mu x y z hs' + productProof = IPP.generateProof + InnerProductBase { bGs = gs, bHs = hs', bH = u } + commitmentLR + InnerProductWitness { ls = ls, rs = rs } + + pure RangeProof + { tBlinding = tBlinding + , mu = mu + , t = t + , aCommit = aCommit + , sCommit = sCommit + , t1Commit = t1Commit + , t2Commit = t2Commit + , productProof = productProof + } + + +-- | Compute l and r polynomials to prove knowledge of aL, aR without revealing them. +-- We achieve it by transferring the vectors l, r. +-- The two terms of the dot product above are set as the constant term, +-- while sL, sR are the coefficient of x^1 , in the following two linear polynomials, +-- which are combined into a quadratic in x: +-- l(x) = (a L − z1 n ) + s L x +-- r(x) = y^n ◦ (aR + z * 1^n + sR * x) + z^2 * 2^n +computeLRPolys + :: (Eq f, Num f) + => Integer + -> Integer + -> [f] + -> [f] + -> [f] + -> [f] + -> f + -> f + -> LRPolys f +computeLRPolys n m aL aR sL sR y z + = LRPolys + { l0 = aL ^-^ ((*) z <$> powerVector 1 nm) + , l1 = sL + , r0 = (powerVector y nm `hadamardp` (aR ^+^ z1nm)) + ^+^ foldl' (\acc j -> iter j ^+^ acc) (replicate (fromIntegral nm) 0) [1..m] + , r1 = hadamardp (powerVector y nm) sR + } + where + z1nm = (*) z <$> powerVector 1 nm + nm = n * m + iter j = (*) (z ^ (j + 1)) <$> (powerVector 0 ((j - 1) * n) ++ powerVector 2 n ++ powerVector 0 ((m - j) * n)) + + + +-- | Compute polynomial t from polynomial r +-- t(x) = l(x) · r(x) = t0 + t1 * x + t2 * x^2 +computeTPoly :: Num f => LRPolys f -> TPoly f +computeTPoly lrPoly@LRPolys{..} + = TPoly + { t0 = t0 + , t1 = (dot (l0 ^+^ l1) (r0 ^+^ r1) - t0) - t2 + , t2 = t2 + } + where + t0 = dot l0 r0 + t2 = dot l1 r1 + + + diff --git a/Bulletproofs/MultiRangeProof/Verifier.hs b/Bulletproofs/MultiRangeProof/Verifier.hs new file mode 100644 --- /dev/null +++ b/Bulletproofs/MultiRangeProof/Verifier.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE RecordWildCards, MultiWayIf, NamedFieldPuns #-} + +module Bulletproofs.MultiRangeProof.Verifier ( + verifyProof, + verifyTPoly, + verifyLRCommitment, +) where + +import Protolude +import Prelude (zipWith3) + +import qualified Crypto.PubKey.ECC.Generate as Crypto +import qualified Crypto.PubKey.ECC.Prim as Crypto +import qualified Crypto.PubKey.ECC.Types as Crypto + +import Bulletproofs.RangeProof.Internal +import Bulletproofs.Curve +import Bulletproofs.Utils + +import Bulletproofs.InnerProductProof as IPP hiding (verifyProof) +import qualified Bulletproofs.InnerProductProof as IPP + +-- | Verify that a commitment was computed from a value in a given range +verifyProof + :: (AsInteger f, Eq f, Field f, Show f) + => Integer -- ^ Range upper bound + -> [Crypto.Point] -- ^ Commitments of in-range values + -> RangeProof f + -- ^ Proof that a secret committed value lies in a certain interval + -> Bool +verifyProof upperBound vCommits proof@RangeProof{..} + = and + [ verifyTPoly n vCommitsExp2 proof x y z + , verifyLRCommitment n mExp2 proof x y z + ] + where + x = shamirX aCommit sCommit t1Commit t2Commit y z + y = shamirY aCommit sCommit + z = shamirZ aCommit sCommit y + n = logBase2 upperBound + m = length vCommits + -- Vector of values passed must be of length 2^x + vCommitsExp2 = vCommits ++ residueCommits + residueCommits = replicate (2 ^ log2Ceil m - m) Crypto.PointO + mExp2 = fromIntegral $ length vCommitsExp2 + +-- | Verify the constant term of the polynomial t +-- t = t(x) = t0 + t1*x + t2*x^2 +-- This is what binds the proof to the actual original Pedersen commitment V to the actual value +verifyTPoly + :: (AsInteger f, Eq f, Field f) + => Integer -- ^ Dimension n of the vectors + -> [Crypto.Point] -- ^ Commitments of in-range values + -> RangeProof f + -- ^ Proof that a secret committed value lies in a certain interval + -> f -- ^ Challenge x + -> f -- ^ Challenge y + -> f -- ^ Challenge z + -> Bool +verifyTPoly n vCommits proof@RangeProof{..} x y z + = lhs == rhs + where + m = fromIntegral $ length vCommits + lhs = commit t tBlinding + rhs = + foldl' addP Crypto.PointO ( zipWith mulP ((*) (fSquare z) <$> powerVector z m) vCommits ) + `addP` + (delta n m y z `mulP` g) + `addP` + (x `mulP` t1Commit) + `addP` + (fSquare x `mulP` t2Commit) + +-- | Verify the inner product argument for the vectors l and r that form t +verifyLRCommitment + :: (AsInteger f, Eq f, Field f, Show f) + => Integer -- ^ Dimension n of the vectors + -> Integer + -> RangeProof f + -- ^ Proof that a secret committed value lies in a certain interval + -> f -- ^ Challenge x + -> f -- ^ Challenge y + -> f -- ^ Challenge z + -> Bool +verifyLRCommitment n m proof@RangeProof{..} x y z + = IPP.verifyProof + nm + IPP.InnerProductBase { bGs = gs, bHs = hs', bH = u } + commitmentLR + productProof + where + commitmentLR = computeLRCommitment n m aCommit sCommit t tBlinding mu x y z hs' + hs' = zipWith (\yi hi-> recip yi `mulP` hi) (powerVector y nm) hs + uChallenge = shamirU tBlinding mu t + u = uChallenge `mulP` g + nm = n * m diff --git a/Bulletproofs/RangeProof/Internal.hs b/Bulletproofs/RangeProof/Internal.hs --- a/Bulletproofs/RangeProof/Internal.hs +++ b/Bulletproofs/RangeProof/Internal.hs @@ -1,42 +1,27 @@ -module Bulletproofs.RangeProof.Internal ( - RangeProof(..), - RangeProofError(..), - LRPolys(..), - TPoly(..), - delta, - checkRange, - reversedEncodeBit, - complementaryVector, - chooseBlindingVectors, - commitBitVectors, - computeLRCommitment, - obfuscateEncodedBits, - obfuscateEncodedBitsSingle, -) where +module Bulletproofs.RangeProof.Internal where import Protolude import Numeric (showIntAtBase) import Data.Char (intToDigit, digitToInt) +import Crypto.Number.Generate (generateMax) import Crypto.Random.Types (MonadRandom(..)) -import qualified Crypto.PubKey.ECC.Generate as Crypto import qualified Crypto.PubKey.ECC.Prim as Crypto import qualified Crypto.PubKey.ECC.Types as Crypto import Bulletproofs.Utils import Bulletproofs.Curve -import Bulletproofs.Fq as Fq import Bulletproofs.InnerProductProof.Internal -data RangeProof +data RangeProof f = RangeProof - { tBlinding :: Fq + { tBlinding :: f -- ^ Blinding factor of the T1 and T2 commitments, -- combined into the form required to make the committed version of the x-polynomial add up - , mu :: Fq + , mu :: f -- ^ Blinding factor required for the Verifier to verify commitments A, S - , t :: Fq + , t :: f -- ^ Dot product of vectors l and r that prove knowledge of the value in range -- t = t(x) = l(x) · r(x) , aCommit :: Crypto.Point @@ -49,7 +34,7 @@ -- ^ Pedersen commitment to coefficient t1 , t2Commit :: Crypto.Point -- ^ Pedersen commitment to coefficient t2 - , productProof :: InnerProductProof + , productProof :: InnerProductProof f -- ^ Inner product argument to prove that a commitment P -- has vectors l, r ∈ Z^n for which P = l · G + r · H + ( l, r ) · U } deriving (Show, Eq) @@ -57,78 +42,83 @@ data RangeProofError = UpperBoundTooLarge Integer -- ^ The upper bound of the range is too large | ValueNotInRange Integer -- ^ Value is not within the range required + | ValuesNotInRange [Integer] -- ^ Values are not within the range required | NNotPowerOf2 Integer -- ^ Dimension n is required to be a power of 2 - deriving (Show) + deriving (Show, Eq) ----------------------------- -- Polynomials ----------------------------- -data LRPolys +data LRPolys f = LRPolys - { l0 :: [Fq] - , l1 :: [Fq] - , r0 :: [Fq] - , r1 :: [Fq] + { l0 :: [f] + , l1 :: [f] + , r0 :: [f] + , r1 :: [f] } -data TPoly +data TPoly f = TPoly - { t0 :: Fq - , t1 :: Fq - , t2 :: Fq + { t0 :: f + , t1 :: f + , t2 :: f } ----------------------------- -- Internal functions ----------------------------- - -- | Encode the value v into a bit representation. Let aL be a vector -- of bits such that = v (put more simply, the components of a L are the -- binary digits of v). -encodeBit :: Integer -> Fq -> [Fq] -encodeBit n (Fq v) = fillWithZeros n $ Fq.new . fromIntegral . digitToInt <$> showIntAtBase 2 intToDigit v "" +encodeBit :: (AsInteger f, Num f) => Integer -> f -> [f] +encodeBit n v = fillWithZeros n $ fromIntegral . digitToInt <$> showIntAtBase 2 intToDigit (asInteger v) "" -- | Bits of v reversed. -- v = = a_0 * 2^0 + ... + a_n-1 * 2^(n-1) -reversedEncodeBit :: Integer -> Fq -> [Fq] +reversedEncodeBit :: (AsInteger f, Num f) => Integer -> f -> [f] reversedEncodeBit n = reverse . encodeBit n +-- TODO: Test it +reversedEncodeBitMulti :: (AsInteger f, Num f) => Integer -> [f] -> [f] +reversedEncodeBitMulti n = foldl' (\acc v -> acc ++ reversedEncodeBit n v) [] + -- | In order to prove that v is in range, each element of aL is either 0 or 1. -- We construct a “complementary” vector aR = aL − 1^n and require that -- aL ◦ aR = 0 hold. complementaryVector :: Num a => [a] -> [a] complementaryVector aL = (\vi -> vi - 1) <$> aL + -- | Add non-relevant zeros to a vector to match the size -- of the other vectors used in the protocol -fillWithZeros :: Integer -> [Fq] -> [Fq] +fillWithZeros :: Num f => Integer -> [f] -> [f] fillWithZeros n aL = zeros ++ aL where - zeros = replicate (fromInteger n - length aL) (Fq 0) + zeros = replicate (fromInteger n - length aL) 0 -- | Obfuscate encoded bits with challenges y and z. -- z^2 * + z * + = (z^2) * v -- The property holds because = 0 and = 0 -obfuscateEncodedBits :: Integer -> [Fq] -> [Fq] -> Fq -> Fq -> Fq +obfuscateEncodedBits :: (Eq f, Field f) => Integer -> [f] -> [f] -> f -> f -> f obfuscateEncodedBits n aL aR y z - = (fqSquare z * dotp aL (powerVector 2 n)) - + (z * dotp ((aL `fqSubV` powerVector 1 n) `fqSubV` aR) yN) - + dotp (hadamardp aL aR) yN + = (fSquare z * dot aL (powerVector 2 n)) + + (z * dot ((aL ^-^ powerVector 1 n) ^-^ aR) yN) + + dot (hadamardp aL aR) yN where yN = powerVector y n --- Convert obfuscateEncodedBits into aCommit sCommitingle inner product. +-- Convert obfuscateEncodedBits into a single inner product. -- We can afford for this factorization to leave terms “dangling”, but -- what’s important is that the aL , aR terms be kept inside -- (since they can’t be shared with the Verifier): -- = z 2 v + δ(y, z) -obfuscateEncodedBitsSingle :: Integer -> [Fq] -> [Fq] -> Fq -> Fq -> Fq +obfuscateEncodedBitsSingle :: (Eq f, Field f) => Integer -> [f] -> [f] -> f -> f -> f obfuscateEncodedBitsSingle n aL aR y z - = dotp - (aL `fqSubV` z1n) - (hadamardp (powerVector y n) (aR `fqAddV` z1n) `fqAddV` ((*) (fqSquare z) <$> powerVector 2 n)) + = dot + (aL ^-^ z1n) + (hadamardp (powerVector y n) (aR ^+^ z1n) ^+^ ((*) (fSquare z) <$> powerVector 2 n)) where z1n = (*) z <$> powerVector 1 n @@ -137,13 +127,13 @@ -- Prover can send commitments to these vectors; -- these are properly blinded vector Pedersen commitments: commitBitVectors - :: MonadRandom m - => Fq - -> Fq - -> [Fq] - -> [Fq] - -> [Fq] - -> [Fq] + :: (MonadRandom m, AsInteger f) + => f + -> f + -> [f] + -> [f] + -> [f] + -> [f] -> m (Crypto.Point, Crypto.Point) commitBitVectors aBlinding sBlinding aL aR sL sR = do let aLG = foldl' addP Crypto.PointO ( zipWith mulP aL gs ) @@ -161,50 +151,60 @@ pure (aCommit, sCommit) -chooseBlindingVectors :: MonadRandom m => Integer -> m ([Fq], [Fq]) -chooseBlindingVectors n = do - sL <- replicateM (fromInteger n) (Fq.random n) - sR <- replicateM (fromInteger n) (Fq.random n) - pure (sL, sR) - -- | (z − z^2) * <1^n, y^n> − z^3 * <1^n, 2^n> -delta :: Integer -> Fq -> Fq -> Fq -delta n y z - = ((z - Fq.fqSquare z) * dotp (powerVector 1 n) (powerVector y n)) - - (Fq.fqCube z * dotp (powerVector 1 n) (powerVector 2 n)) +delta :: (Eq f, Field f) => Integer -> Integer -> f -> f -> f +delta n m y z + = ((z - fSquare z) * dot (powerVector 1 nm) (powerVector y nm)) + - foldl' (\acc j -> acc + ((z ^ (j + 2)) * dot (powerVector 1 n) (powerVector 2 n))) 0 [1..m] + where + nm = n * m --- | Check that a value is in aCommit sCommitpecific range +-- | Check that a value is in a specific range checkRange :: Integer -> Integer -> Bool checkRange n v = v >= 0 && v < 2 ^ n +-- | Check that a value is in a specific range +checkRanges :: Integer -> [Integer] -> Bool +checkRanges n vs = and $ fmap (\v -> v >= 0 && v < 2 ^ n) vs + -- | Compute commitment of linear vector polynomials l and r -- P = A + xS − zG + (z*y^n + z^2 * 2^n) * hs' computeLRCommitment - :: Integer + :: (AsInteger f, Eq f, Num f, Show f) + => Integer + -> Integer -> Crypto.Point -> Crypto.Point - -> Fq - -> Fq - -> Fq - -> Fq - -> Fq - -> Fq + -> f + -> f + -> f + -> f + -> f + -> f -> [Crypto.Point] -> Crypto.Point -computeLRCommitment n aCommit sCommit t tBlinding mu x y z hs' - = aCommit +computeLRCommitment n m aCommit sCommit t tBlinding mu x y z hs' + = aCommit -- A `addP` - (x `mulP` sCommit) + (x `mulP` sCommit) -- xS `addP` - Crypto.pointNegate curve (z `mulP` gsSum) + Crypto.pointNegate curve (z `mulP` gsSum) -- (- zG) `addP` - foldl' addP Crypto.PointO (zipWith mulP hExp hs') + foldl' addP Crypto.PointO (zipWith mulP hExp hs') -- (hExp Hs') `addP` + foldl' + (\acc j -> acc `addP` foldl' addP Crypto.PointO (zipWith mulP (hExp' j) (sliceHs' j))) + Crypto.PointO + [1..m] + `addP` Crypto.pointNegate curve (mu `mulP` h) `addP` (t `mulP` u) where - gsSum = foldl' addP Crypto.PointO (take (fromIntegral n) gs) - hExp = ((*) z <$> powerVector y n) `fqAddV` ((*) (fqSquare z) <$> powerVector 2 n) + gsSum = foldl' addP Crypto.PointO (take (fromIntegral nm) gs) + hExp = (*) z <$> powerVector y nm + hExp' j = (*) (z ^ (j+1)) <$> powerVector 2 n + sliceHs' j = slice n j hs' uChallenge = shamirU tBlinding mu t u = uChallenge `mulP` g + nm = n * m diff --git a/Bulletproofs/RangeProof/Prover.hs b/Bulletproofs/RangeProof/Prover.hs --- a/Bulletproofs/RangeProof/Prover.hs +++ b/Bulletproofs/RangeProof/Prover.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE RecordWildCards, MultiWayIf #-} - module Bulletproofs.RangeProof.Prover ( generateProof, generateProofUnsafe, @@ -7,157 +5,30 @@ import Protolude +import Control.Monad.Fail import Crypto.Random.Types (MonadRandom(..)) -import qualified Crypto.PubKey.ECC.Generate as Crypto -import qualified Crypto.PubKey.ECC.Prim as Crypto -import qualified Crypto.PubKey.ECC.Types as Crypto -import Bulletproofs.Curve -import Bulletproofs.Utils -import Bulletproofs.Fq as Fq +import Bulletproofs.Utils (AsInteger, Field) import Bulletproofs.RangeProof.Internal - -import Bulletproofs.InnerProductProof as IPP hiding (generateProof) -import qualified Bulletproofs.InnerProductProof as IPP +import qualified Bulletproofs.MultiRangeProof.Prover as MRP -- | Prove that a value lies in a specific range generateProof - :: MonadRandom m - => Integer -- ^ Upper bound of the range we want to prove - -> Integer -- ^ Value we want to prove in range - -> Integer -- ^ Blinding factor - -> ExceptT RangeProofError m RangeProof -generateProof upperBound v vBlinding = do - unless (upperBound < q) $ throwE $ UpperBoundTooLarge upperBound - - case doubleLogM of - Nothing -> throwE $ NNotPowerOf2 upperBound - Just n -> do - unless (checkRange n v) $ throwE $ ValueNotInRange v - lift $ generateProofUnsafe upperBound v vBlinding - - where - doubleLogM :: Maybe Integer - doubleLogM = do - x <- logBase2M upperBound - logBase2M x - pure x - + :: (AsInteger f, Eq f, Field f, Show f, MonadRandom m, MonadFail m) + => Integer -- ^ Upper bound of the range we want to prove + -> (Integer, Integer) + -- ^ Values we want to prove in range and their blinding factors + -> ExceptT RangeProofError m (RangeProof f) +generateProof upperBound (v, vBlinding) = + MRP.generateProof upperBound [(v, vBlinding)] -- | Generate range proof from valid inputs generateProofUnsafe - :: MonadRandom m - => Integer -- ^ Upper bound of the range we want to prove - -> Integer -- ^ Value we want to prove in range - -> Integer -- ^ Blinding factor - -> m RangeProof -generateProofUnsafe upperBound v vBlinding = do - let n = logBase2 upperBound - vFq = Fq.new v - vBlindingFq = Fq.new vBlinding - - let aL = reversedEncodeBit n vFq - aR = complementaryVector aL - - (sL, sR) <- chooseBlindingVectors n - - [aBlinding, sBlinding] <- replicateM 2 (Fq.random n) - - (aCommit, sCommit) <- commitBitVectors aBlinding sBlinding aL aR sL sR - - -- Oracle generates y, z from a, c - let y = shamirY aCommit sCommit - z = shamirZ aCommit sCommit y - - let lrPoly@LRPolys{..} = computeLRPolys n aL aR sL sR y z - tPoly@TPoly{..} = computeTPoly lrPoly - - [t1Blinding, t2Blinding] <- replicateM 2 (Fq.random n) - - let t1Commit = commit t1 t1Blinding - t2Commit = commit t2 t2Blinding - - -- Oracle generates x from previous data in transcript - let x = shamirX aCommit sCommit t1Commit t2Commit y z - - let ls = l0 `fqAddV` ((*) x <$> l1) - rs = r0 `fqAddV` ((*) x <$> r1) - t = t0 + (t1 * x) + (t2 * fqSquare x) - - unless (t == dotp ls rs) $ - panic "Error on: t = dotp l r" - - unless (t1 == dotp l1 r0 + dotp l0 r1) $ - panic "Error on: t1 = dotp l1 r0 + dotp l0 r1" - - unless (t0 == (vFq * fqSquare z) + delta n y z) $ - panic "Error on: t0 = v * z^2 + delta(y, z)" - - let tBlinding = (fqSquare z * vBlindingFq) + (t2Blinding * fqSquare x) + (t1Blinding * x) - mu = aBlinding + (sBlinding * x) - - let uChallenge = shamirU tBlinding mu t - u = uChallenge `mulP` g - hs' = zipWith (\yi hi-> inv yi `mulP` hi) (powerVector y n) hs - commitmentLR = computeLRCommitment n aCommit sCommit t tBlinding mu x y z hs' - productProof = IPP.generateProof - InnerProductBase { bGs = gs, bHs = hs', bH = u } - commitmentLR - InnerProductWitness { ls = ls, rs = rs } - - pure RangeProof - { tBlinding = tBlinding - , mu = mu - , t = t - , aCommit = aCommit - , sCommit = sCommit - , t1Commit = t1Commit - , t2Commit = t2Commit - , productProof = productProof - } - - --- | Compute l and r polynomials to prove knowledge of aL, aR without revealing them. --- We achieve it by transferring the vectors l, r. --- The two terms of the dot product above are set as the constant term, --- while sL, sR are the coefficient of x^1 , in the following two linear polynomials, --- which are combined into a quadratic in x: --- l(x) = (a L − z1 n ) + s L x --- r(x) = y^n ◦ (aR + z * 1^n + sR * x) + z^2 * 2^n -computeLRPolys - :: Integer - -> [Fq] - -> [Fq] - -> [Fq] - -> [Fq] - -> Fq - -> Fq - -> LRPolys -computeLRPolys n aL aR sL sR y z - = LRPolys - { l0 = aL `fqSubV` ((*) z <$> powerVector 1 n) - , l1 = sL - , r0 = (powerVector y n `hadamardp` (aR `fqAddV` z1n)) - `fqAddV` - ((*) (fqSquare z) <$> powerVector 2 n) - , r1 = hadamardp (powerVector y n) sR - } - where - z1n = (*) z <$> powerVector 1 n - - --- | Compute polynomial t from polynomial r --- t(x) = l(x) · r(x) = t0 + t1 * x + t2 * x^2 -computeTPoly :: LRPolys -> TPoly -computeTPoly lrPoly@LRPolys{..} - = TPoly - { t0 = t0 - , t1 = (dotp (l0 `fqAddV` l1) (r0 `fqAddV` r1) - t0) - t2 - , t2 = t2 - } - where - t0 = dotp l0 r0 - t2 = dotp l1 r1 - - + :: (AsInteger f, Eq f, Field f, Show f, MonadRandom m, MonadFail m) + => Integer -- ^ Upper bound of the range we want to prove + -> (Integer, Integer) + -- ^ Values we want to prove in range and their blinding factors + -> m (RangeProof f) +generateProofUnsafe upperBound (v, vBlinding) = + MRP.generateProofUnsafe upperBound [(v, vBlinding)] diff --git a/Bulletproofs/RangeProof/Verifier.hs b/Bulletproofs/RangeProof/Verifier.hs --- a/Bulletproofs/RangeProof/Verifier.hs +++ b/Bulletproofs/RangeProof/Verifier.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RecordWildCards, MultiWayIf, NamedFieldPuns, ViewPatterns #-} +{-# LANGUAGE RecordWildCards, MultiWayIf, NamedFieldPuns #-} module Bulletproofs.RangeProof.Verifier ( verifyProof, @@ -7,82 +7,51 @@ ) where import Protolude -import Prelude (zipWith3) -import qualified Crypto.PubKey.ECC.Generate as Crypto -import qualified Crypto.PubKey.ECC.Prim as Crypto import qualified Crypto.PubKey.ECC.Types as Crypto import Bulletproofs.RangeProof.Internal import Bulletproofs.Curve import Bulletproofs.Utils -import Bulletproofs.Fq as Fq -import Bulletproofs.InnerProductProof as IPP hiding (verifyProof) -import qualified Bulletproofs.InnerProductProof as IPP +import qualified Bulletproofs.MultiRangeProof.Verifier as MRP -- | Verify that a commitment was computed from a value in a given range verifyProof - :: Integer -- ^ Range upper bound - -> Crypto.Point -- ^ Commitment of an in-range value - -> RangeProof + :: (AsInteger f, Eq f, Field f, Show f) + => Integer -- ^ Range upper bound + -> Crypto.Point -- ^ Commitments of in-range values + -> RangeProof f -- ^ Proof that a secret committed value lies in a certain interval -> Bool verifyProof upperBound vCommit proof@RangeProof{..} - = and - [ verifyTPoly n vCommit proof x y z - , verifyLRCommitment n proof x y z - ] - where - x = shamirX aCommit sCommit t1Commit t2Commit y z - y = shamirY aCommit sCommit - z = shamirZ aCommit sCommit y - hs' = zipWith (\yi hi-> inv yi `mulP` hi) (powerVector y n) hs - n = logBase2 upperBound + = MRP.verifyProof upperBound [vCommit] proof -- | Verify the constant term of the polynomial t -- t = t(x) = t0 + t1*x + t2*x^2 -- This is what binds the proof to the actual original Pedersen commitment V to the actual value verifyTPoly - :: Integer -- ^ Dimension n of the vectors - -> Crypto.Point -- ^ Commitment of an in-range value - -> RangeProof + :: (AsInteger f, Eq f, Field f, Show f) + => Integer -- ^ Dimension n of the vectors + -> Crypto.Point -- ^ Commitment of in-range value + -> RangeProof f -- ^ Proof that a secret committed value lies in a certain interval - -> Fq -- ^ Challenge x - -> Fq -- ^ Challenge y - -> Fq -- ^ Challenge z + -> f -- ^ Challenge x + -> f -- ^ Challenge y + -> f -- ^ Challenge z -> Bool -verifyTPoly n vCommit proof@RangeProof{..} x y z - = lhs == rhs - where - lhs = commit t tBlinding - rhs = (fqSquare z `mulP` vCommit) - `addP` - (delta n y z `mulP` g) - `addP` - (x `mulP` t1Commit) - `addP` - (fqSquare x `mulP` t2Commit) +verifyTPoly n vCommit + = MRP.verifyTPoly n [vCommit] -- | Verify the inner product argument for the vectors l and r that form t verifyLRCommitment - :: Integer -- ^ Dimension n of the vectors - -> RangeProof + :: (AsInteger f, Eq f, Field f, Show f) + => Integer -- ^ Dimension n of the vectors + -> RangeProof f -- ^ Proof that a secret committed value lies in a certain interval - -> Fq -- ^ Challenge x - -> Fq -- ^ Challenge y - -> Fq -- ^ Challenge z + -> f -- ^ Challenge x + -> f -- ^ Challenge y + -> f -- ^ Challenge z -> Bool -verifyLRCommitment n proof@RangeProof{..} x y z - = IPP.verifyProof - n - IPP.InnerProductBase { bGs = gs, bHs = hs', bH = u } - commitmentLR - productProof - where - commitmentLR = computeLRCommitment n aCommit sCommit t tBlinding mu x y z hs' - hs' = zipWith (\yi hi-> inv yi `mulP` hi) (powerVector y n) hs - uChallenge = shamirU tBlinding mu t - u = uChallenge `mulP` g - - +verifyLRCommitment n + = MRP.verifyLRCommitment n 1 diff --git a/Bulletproofs/Utils.hs b/Bulletproofs/Utils.hs --- a/Bulletproofs/Utils.hs +++ b/Bulletproofs/Utils.hs @@ -1,41 +1,51 @@ -module Bulletproofs.Utils ( - dotp, - addP, - subP, - mulP, - shamirU, - shamirX, - shamirX', - shamirY, - shamirZ, - commit, - hadamardp, - powerVector, - logBase2, - logBase2M, -) where +module Bulletproofs.Utils where import Protolude import qualified Crypto.PubKey.ECC.Prim as Crypto import qualified Crypto.PubKey.ECC.Types as Crypto +import Crypto.Random (MonadRandom) +import Crypto.Number.Generate (generateMax) -import Bulletproofs.Fq as Fq +import Bulletproofs.Fq as Fq hiding (asInteger) import Bulletproofs.Curve --- | Return a vector containing the first n powers of a -powerVector :: Fq -> Integer -> [Fq] -powerVector (Fq a) x = (\i -> Fq.new (a ^ i)) <$> [0..x-1] +class AsInteger a where + asInteger :: a -> Integer --- | Inner product between two vector polynomials -dotp :: Num a => [a] -> [a] -> a -dotp a b = foldl' (+) 0 (hadamardp a b) +instance AsInteger Fq where + asInteger (Fq x) = x +instance AsInteger Integer where + asInteger x = x + +-- Class for specialisations of field operations that may have +-- optimised implementations. +class (Num f, Fractional f) => Field f where + fSquare :: f -> f + +instance Field Fq where + fSquare = Fq.fqSquare + +-- | Return a vector containing the first n powers of a +powerVector :: (Eq f, Num f) => f -> Integer -> [f] +powerVector a x + = (\i -> if i == 0 && a == 0 then 0 else a ^ i) <$> [0..x-1] + -- | Hadamard product or entry wise multiplication of two vectors hadamardp :: Num a => [a] -> [a] -> [a] hadamardp a b | length a == length b = zipWith (*) a b | otherwise = panic "Vector sizes must match" +dot :: Num a => [a] -> [a] -> a +dot xs ys = sum $ hadamardp xs ys + +(^+^) :: Num a => [a] -> [a] -> [a] +(^+^) = zipWith (+) + +(^-^) :: Num a => [a] -> [a] -> [a] +(^-^) = zipWith (-) + -- | Add two points of the same curve addP :: Crypto.Point -> Crypto.Point -> Crypto.Point addP = Crypto.pointAdd curve @@ -45,12 +55,12 @@ subP x y = Crypto.pointAdd curve x (Crypto.pointNegate curve y) -- | Multiply a scalar and a point in an elliptic curve -mulP :: Fq -> Crypto.Point -> Crypto.Point -mulP (Fq x) = Crypto.pointMul curve x +mulP :: AsInteger f => f -> Crypto.Point -> Crypto.Point +mulP x = Crypto.pointMul curve (asInteger x) -- | Create a Pedersen commitment to a value given -- a value and a blinding factor -commit :: Fq -> Fq -> Crypto.Point +commit :: AsInteger f => f -> f -> Crypto.Point commit x r = (x `mulP` g) `addP` (r `mulP` h) isLogBase2 :: Integer -> Bool @@ -68,42 +78,83 @@ then Just (logBase2 x) else Nothing +slice :: Integer -> Integer -> [a] -> [a] +slice n j vs = take (fromIntegral $ j * n - (j - 1)*n) (drop (fromIntegral $ (j - 1) * n) vs) + +-- | Append minimal amount of zeroes until the list has a length which +-- is a power of two. +padToNearestPowerOfTwo + :: Num f => [f] -> [f] +padToNearestPowerOfTwo [] = [] +padToNearestPowerOfTwo xs = padToNearestPowerOfTwoOf (length xs) xs + +-- | Given n, append zeroes until the list has length 2^n. +padToNearestPowerOfTwoOf + :: Num f + => Int -- ^ n + -> [f] -- ^ list which should have length <= 2^n + -> [f] -- ^ list which will have length 2^n +padToNearestPowerOfTwoOf i xs = xs ++ replicate padLength 0 + where + padLength = nearestPowerOfTwo - length xs + nearestPowerOfTwo = 2 ^ log2Ceil i + +-- | Calculate ceiling of log base 2 of an integer. +log2Ceil :: Int -> Int +log2Ceil x = floorLog + correction + where + floorLog = finiteBitSize x - 1 - countLeadingZeros x + correction = if countTrailingZeros x < floorLog + then 1 + else 0 + +randomN :: MonadRandom m => Integer -> m Integer +randomN n = generateMax (2^n) + +chooseBlindingVectors :: (Num f, MonadRandom m) => Integer -> m ([f], [f]) +chooseBlindingVectors n = do + sL <- replicateM (fromInteger n) (fromInteger <$> generateMax (2^n)) + sR <- replicateM (fromInteger n) (fromInteger <$> generateMax (2^n)) + pure (sL, sR) + -------------------------------------------------- -- Fiat-Shamir transformations -------------------------------------------------- -shamirY :: Crypto.Point -> Crypto.Point -> Fq +shamirY :: Num f => Crypto.Point -> Crypto.Point -> f shamirY aCommit sCommit - = Fq.new $ oracle $ + = fromInteger $ oracle $ show q <> pointToBS aCommit <> pointToBS sCommit -shamirZ :: Crypto.Point -> Crypto.Point -> Fq -> Fq +shamirZ :: (Show f, Num f) => Crypto.Point -> Crypto.Point -> f -> f shamirZ aCommit sCommit y - = Fq.new $ oracle $ + = fromInteger $ oracle $ show q <> pointToBS aCommit <> pointToBS sCommit <> show y shamirX - :: Crypto.Point + :: (Show f, Num f) + => Crypto.Point -> Crypto.Point -> Crypto.Point -> Crypto.Point - -> Fq - -> Fq - -> Fq + -> f + -> f + -> f shamirX aCommit sCommit t1Commit t2Commit y z - = Fq.new $ oracle $ + = fromInteger $ oracle $ show q <> pointToBS aCommit <> pointToBS sCommit <> pointToBS t1Commit <> pointToBS t2Commit <> show y <> show z shamirX' - :: Crypto.Point + :: Num f + => Crypto.Point -> Crypto.Point -> Crypto.Point - -> Fq + -> f shamirX' commitmentLR l' r' - = Fq.new $ oracle $ + = fromInteger $ oracle $ show q <> pointToBS l' <> pointToBS r' <> pointToBS commitmentLR -shamirU :: Fq -> Fq -> Fq -> Fq +shamirU :: (Show f, Num f) => f -> f -> f -> f shamirU tBlinding mu t - = Fq.new $ oracle $ + = fromInteger $ oracle $ show q <> show tBlinding <> show mu <> show t diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -80,33 +80,144 @@ argument transmits only 2 [log2] + 2 elements. In total, the prover sends only 2 [log2(n)] + 4 group elements and 5 elements in _Z_p +Aggregating Logarithmic Proofs +============================== + +We can construct a single proof of range of multiple values, while only incurring an additional space cost of 2 log2(m) for +_m_ additional values _v_, as opposed to a multiplicative factor of _m_ when creating _m_ independent range proofs. + +The aggregate range proof makes use of the inner product argument. It uses 2 [log2 (n * m)] + 4 group elements and 5 elements in Zp. + +See [Multi range proof example](https://github.com/adjoint-io/bulletproofs/tree/master#multi-range-proof) + + Usage ===== +Single range proof: +------------------- + ```haskell -import Bulletproofs.RangeProof +import qualified Bulletproofs.RangeProof as RP -testProtocol :: Integer -> Integer -> IO Bool -testProtocol v vBlinding = do +testSingleRangeProof :: (Integer, Integer) -> IO Bool +testSingleRangeProof (v, vBlinding) = do let vCommit = commit v vBlinding -- n needs to be a power of 2 n = 2 ^ 8 upperBound = 2 ^ n -- Prover - proofE <- generateProof upperBound v vBlinding + proofE <- runExceptT $ RP.generateProof upperBound (v, vBlinding) + -- Verifier case proofE of Left err -> panic $ show err Right (proof@RangeProof{..}) - -> pure $ verifyProof upperBound vCommit proof + -> pure $ RP.verifyProof upperBound vCommit proof ``` +Multi range proof: +------------------ + +```haskell +import qualified Bulletproofs.MultiRangeProof as MRP + +testMultiRangeProof :: [(Integer, Integer)] -> IO Bool +testMultiRangeProof vsAndvBlindings = do + let vCommits = fmap (uncurry commit) vsAndvBlindings + -- n needs to be a power of 2 + n = 2 ^ 8 + upperBound = 2 ^ n + + -- Prover + proofE <- runExceptT $ MRP.generateProof upperBound vsAndvBlindings + + -- Verifier + case proofE of + Left err -> panic $ show err + Right (proof@RangeProof{..}) + -> pure $ MRP.verifyProof upperBound vCommits proof +``` + + The dimension _n_ needs to be a power of 2. -This implementation offers support for the SECp256k1 curve, a Koblitz curve. +This implementation offers support for SECp256k1, a Koblitz curve. Further information about this curve can be found in the Uplink docs: [SECp256k1 curve](https://www.adjoint.io/docs/cryptography.html#id1 "SECp256k1 curve") + +Zero-knowledge proof for Arithmetic Circuits +============================================ + +An arithmetic circuit over a field and variables (a1, ..., an) is a directed acyclic graph whose vertices are called gates. + +Arithmetic circuit can be described alternatively as a list of multiplication gates with a collection of linear consistency equations +relating the inputs and outputs of the gates. Any circuit described as an acyclic graph can be efficiently converted into this alternative description. + +Bulletproofs present a protocol to generate zero-knowledge argument for arithmetic circuits using the inner product argument, +which allows to get a proof of size 2 log2(n) + 13 elements and include committed values as inputs to the arithmetic circuit. + +In the protocol, the Prover proves that the hadamard product of _aL_ and _aR_ and a set of linear constraints hold. +The input values _v_ used to generate the proof are then committed and shared with the Verifier. + +```haskell +import qualified Bulletproofs.ArithmeticCircuit + +-- Example: +-- 2 linear constraints (q = 2): +-- aL[0] + aL[1] + aL[2] + aL[3] = v[0] +-- aR[0] + aR[1] + aR[2] + aR[3] = v[1] +-- +-- 4 multiplication constraints (implicit) (n = 4): +-- aL[0] * aR[0] = aO[0] +-- aL[1] * aR[1] = aO[1] +-- aL[2] * aR[2] = aO[2] +-- aL[3] * aR[3] = aO[3] +-- +-- 2 input values (m = 2) + +arithCircuitExample :: ArithCircuit Fq +arithCircuitExample = ArithCircuit + { weights = GateWeights + { wL = [[1, 1, 1, 1] + ,[0, 0, 0, 0]] + , wR = [[0, 0, 0, 0] + ,[1, 1, 1, 1]] + , wO = [[0, 0, 0, 0] + ,[0, 0, 0, 0]] + } + , commitmentWeights = [[1, 0] + ,[0, 1]] + , cs = [0, 0] + } + +testArithCircuitProof :: ([Fq], [Fq]) -> ArithCircuit Fq -> IO Bool +testArithCircuitProof (aL, aR) arithCircuit = do + let n = 4 + m = 2 + q = 2 + + -- Multiplication constraints + let aO = aL `hadamardp` aR + + -- Linear constraints + v0 = sum aL + v1 = sum aR + + commitBlinders <- replicateM m Fq.random + let commitments = zipWith commit [v0, v1] commitBlinders + + let arithWitness = ArithWitness + { assignment = Assignment aL aR aO + , commitments = commitments + , commitBlinders = commitBlinders + } + + proof <- generateProof arithCircuit arithWitness + + pure $ verifyProof commitments proof arithCircuit +``` **References**: diff --git a/bulletproofs.cabal b/bulletproofs.cabal --- a/bulletproofs.cabal +++ b/bulletproofs.cabal @@ -2,11 +2,11 @@ -- -- see: https://github.com/sol/hpack -- --- hash: b1527afdaf3310a51701ef0c756ab6e3cd6ed3606bc52e74b6a0a744bbbf5426 +-- hash: 001d69dda0cfa16ecf909cb395bf12816dd1e053a263be2983d7dbe569e9a5a0 name: bulletproofs -version: 0.2.0 -description: Please see the README on GitHub at +version: 0.2.1 +description: Please see the README on GitHub at category: Cryptography homepage: https://github.com/adjoint-io/bulletproofs#readme bug-reports: https://github.com/adjoint-io/bulletproofs/issues @@ -31,10 +31,17 @@ Bulletproofs.RangeProof.Internal Bulletproofs.RangeProof.Prover Bulletproofs.RangeProof.Verifier + Bulletproofs.MultiRangeProof + Bulletproofs.MultiRangeProof.Prover + Bulletproofs.MultiRangeProof.Verifier Bulletproofs.InnerProductProof Bulletproofs.InnerProductProof.Internal Bulletproofs.InnerProductProof.Prover Bulletproofs.InnerProductProof.Verifier + Bulletproofs.ArithmeticCircuit + Bulletproofs.ArithmeticCircuit.Internal + Bulletproofs.ArithmeticCircuit.Prover + Bulletproofs.ArithmeticCircuit.Verifier Bulletproofs.Utils other-modules: Paths_bulletproofs @@ -42,12 +49,14 @@ ./. default-extensions: OverloadedStrings NoImplicitPrelude build-depends: - arithmoi + MonadRandom + , arithmoi , base >=4.7 && <5 , containers , cryptonite , memory , protolude >=0.2 + , random-shuffle , text default-language: Haskell2010 @@ -55,6 +64,7 @@ type: exitcode-stdio-1.0 main-is: TestDriver.hs other-modules: + TestArithCircuitProtocol TestCommon TestField TestProtocol @@ -63,7 +73,8 @@ tests default-extensions: OverloadedStrings NoImplicitPrelude build-depends: - QuickCheck + MonadRandom + , QuickCheck , arithmoi , base , bulletproofs @@ -71,6 +82,7 @@ , cryptonite , memory , protolude >=0.2 + , random-shuffle , tasty , tasty-discover , tasty-hunit diff --git a/tests/TestArithCircuitProtocol.hs b/tests/TestArithCircuitProtocol.hs new file mode 100644 --- /dev/null +++ b/tests/TestArithCircuitProtocol.hs @@ -0,0 +1,230 @@ +{-# LANGUAGE ViewPatterns, RecordWildCards #-} + +module TestArithCircuitProtocol where + +import Protolude + +import qualified Data.Map as Map +import qualified Data.List as List + +import Test.Tasty +import Test.Tasty.QuickCheck +import Test.QuickCheck +import qualified Test.QuickCheck.Monadic as QCM + +import Crypto.Number.Generate (generateMax, generateBetween) +import Control.Monad.Random (MonadRandom) + +import qualified Bulletproofs.InnerProductProof as IPP +import qualified Bulletproofs.Fq as Fq +import Bulletproofs.Utils +import Bulletproofs.Curve +import Bulletproofs.Fq +import Bulletproofs.ArithmeticCircuit +import Bulletproofs.ArithmeticCircuit.Internal + +-- | Test an arbitrary circuit +-- Construction: +-- 1. aL, aR, aO; wL, wR, wO; c +-- such that wL * aL + wR * aR + wO * aO = c +-- +-- 2. Create wV and v to +-- - reduce the size of the prove (m <= n) +-- - hide assignment +-- wL * aL + wR * aR + wO * aO - c = wV * v +test_arithCircuitProof_arbitrary :: TestTree +test_arithCircuitProof_arbitrary = localOption (QuickCheckTests 10) $ + testProperty "Arbitrary arithmetic circuit proof" $ QCM.monadicIO $ do + n <- QCM.run $ generateBetween 1 100 + m <- QCM.run $ generateBetween 1 n + let lConstraints = m + + weights@GateWeights{..} <- QCM.run $ generateGateWeights lConstraints n + commitmentWeights <- QCM.run $ generateWv lConstraints m + Assignment{..} <- QCM.run $ generateRandomAssignment n + + cs <- QCM.run $ replicateM (fromIntegral m) Fq.random + commitBlinders <- QCM.run $ replicateM (fromIntegral m) Fq.random + + let gateWeights = GateWeights wL wR wO + gateInputs = Assignment aL aR aO + vs = computeInputValues weights commitmentWeights gateInputs cs + commitments = zipWith commit vs commitBlinders + arithCircuit = ArithCircuit gateWeights commitmentWeights cs + arithWitness = ArithWitness gateInputs commitments commitBlinders + + proof <- QCM.run $ generateProof arithCircuit arithWitness + + QCM.assert $ verifyProof commitments proof arithCircuit + +-- | Test hadamard product relation +-- 2 linear constraints (q = 2): +-- aL[0] + aL[1] + ... + aL[15] = v[0] +-- aR[0] + aR[1] + ... + aR[15] = v[1] +-- +-- 16 multiplication constraints (implicit) (n = 16): +-- +-- 2 input values (m = 2) +test_arithCircuitProof_hadamardp :: TestTree +test_arithCircuitProof_hadamardp = localOption (QuickCheckTests 20) $ + testProperty "Arithmetic circuit proof. Hadamard product relation" $ QCM.monadicIO $ do + + let n = 16 + aL <- QCM.run $ replicateM (fromIntegral n) Fq.random + aR <- QCM.run $ replicateM (fromIntegral n) Fq.random + let aO = aL `hadamardp` aR + + r <- QCM.run Fq.random + s <- QCM.run Fq.random + let v0 = sum aL + v1 = sum aR + + let v0Commit = commit v0 r + v1Commit = commit v1 s + + let zeroVector = replicate (fromIntegral n) 0 + oneVector = replicate (fromIntegral n) 1 + + let wL = [oneVector, zeroVector] + wR = [zeroVector, oneVector] + wO = [zeroVector, zeroVector] + + commitmentWeights = [[1, 0], [0, 1]] + cs = [0, 0] + commitments = [v0Commit, v1Commit] + commitBlinders = [r, s] + gateWeights = GateWeights wL wR wO + gateInputs = Assignment aL aR aO + arithCircuit = ArithCircuit gateWeights commitmentWeights cs + arithWitness = ArithWitness gateInputs commitments commitBlinders + + proof <- QCM.run $ generateProof arithCircuit arithWitness + + QCM.assert $ verifyProof commitments proof arithCircuit + +-- | Test that an addition circuit without multiplication gates succeeds +-- 1 linear constraints (q = 1): +-- v[0] + v[1] = v[2] +-- +-- 0 multiplication constraints (implicit) (n = 0): +-- +-- 3 input values (m = 3) +test_arithCircuitProof_no_mult_gates :: TestTree +test_arithCircuitProof_no_mult_gates = localOption (QuickCheckTests 20) $ + testProperty "Arithmetic circuit proof. n = 0, m = 3, q = 1" + $ QCM.monadicIO $ do + let n = 0 + m = 3 + + commitBlinders <- QCM.run $ replicateM m Fq.random + let wL = [[]] + wR = [[]] + wO = [[]] + cs = [0] + aL = [] + aR = [] + aO = [] + commitmentWeights = [[1, 1, -1]] + vs = [2, 5, 7] + commitments = zipWith commit vs commitBlinders + gateWeights = GateWeights wL wR wO + gateInputs = Assignment aL aR aO + arithCircuit = ArithCircuit gateWeights commitmentWeights cs + arithWitness = ArithWitness gateInputs commitments commitBlinders + + proof <- QCM.run $ generateProof arithCircuit arithWitness + + QCM.assert $ verifyProof commitments proof arithCircuit + +-- | Test that a circuit with a single multiplication gate +-- with linear contraints and not committed values succeeds +-- 3 linear constraints (q = 3): +-- aL[0] = 3 +-- aR[0] = 4 +-- aO[0] = 9 +-- +-- 1 multiplication constraint (implicit) (n = 1): +-- aL[0] * aR[0] = aO[0] +-- +-- 0 input values (m = 0) +test_arithCircuitProof_no_input_values :: TestTree +test_arithCircuitProof_no_input_values = localOption (QuickCheckTests 20) $ + testProperty "Arithmetic circuit proof. n = 1, m = 0, q = 3" + $ QCM.monadicIO $ do + let n = 1 + m = 0 + + commitBlinders <- QCM.run $ replicateM m Fq.random + let wL = [[0], [0], [1]] + wR = [[0], [1], [0]] + wO = [[1], [0], [0]] + cs = [35, 5, 7] + aL = [7] + aR = [5] + aO = [35] + commitmentWeights = [[], [], []] + vs = [] + commitments = zipWith commit vs commitBlinders + gateWeights = GateWeights wL wR wO + gateInputs = Assignment aL aR aO + arithCircuit = ArithCircuit gateWeights commitmentWeights cs + arithWitness = ArithWitness gateInputs commitments commitBlinders + + proof <- QCM.run $ generateProof arithCircuit arithWitness + + QCM.assert $ verifyProof commitments proof arithCircuit + + +-- 5 linear constraints (q = 5): +-- aO[0] = aO[1] +-- aL[0] = V[0] - z +-- aL[1] = V[2] - z +-- aR[0] = V[1] - z +-- aR[1] = V[3] - z +-- +-- 2 multiplication constraint (implicit) (n = 2): +-- aL[0] * aR[0] = aO[0] +-- aL[1] * aR[1] = aO[1] +-- +-- 4 input values (m = 4) +test_arithCircuitProof_shuffle_circuit :: TestTree +test_arithCircuitProof_shuffle_circuit = localOption (QuickCheckTests 20) $ + testProperty "Arithmetic circuit proof. n = 2, m = 4, q = 5" $ QCM.monadicIO $ do + z <- QCM.run Fq.random + commitBlinders <- QCM.run $ replicateM 4 Fq.random + + let wL = [[0, 0] + ,[1, 0] + ,[0, 1] + ,[0, 0] + ,[0, 0]] + wR = [[0, 0] + ,[0, 0] + ,[0, 0] + ,[1, 0] + ,[0, 1]] + wO = [[1, -1] + ,[0, 0] + ,[0, 0] + ,[0, 0] + ,[0, 0]] + wV = [[0, 0, 0, 0] + ,[1, 0, 0, 0] + ,[0, 0, 1, 0] + ,[0, 1, 0 ,0] + ,[0, 0, 0, 1]] + cs = [0, -z, -z, -z, -z] + aL = [4 - z, 9 - z] + aR = [9 - z, 4 - z] + aO = aL `hadamardp` aR + vs = [4, 9, 9, 4] + commitments = zipWith commit vs commitBlinders + gateWeights = GateWeights wL wR wO + gateInputs = Assignment aL aR aO + arithCircuit = ArithCircuit gateWeights wV cs + arithWitness = ArithWitness gateInputs commitments commitBlinders + + proof <- QCM.run $ generateProof arithCircuit arithWitness + + QCM.assert $ verifyProof commitments proof arithCircuit + diff --git a/tests/TestProtocol.hs b/tests/TestProtocol.hs --- a/tests/TestProtocol.hs +++ b/tests/TestProtocol.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE ViewPatterns, RecordWildCards #-} +{-# LANGUAGE ViewPatterns, RecordWildCards, TypeApplications #-} module TestProtocol where @@ -10,7 +10,7 @@ import qualified Test.QuickCheck.Monadic as QCM import Crypto.Random.Types (MonadRandom(..)) -import Crypto.Number.Generate (generateMax) +import Crypto.Number.Generate (generateMax, generateBetween) import qualified Crypto.PubKey.ECC.Generate as Crypto import qualified Crypto.PubKey.ECC.Prim as Crypto import qualified Crypto.PubKey.ECC.Types as Crypto @@ -19,6 +19,10 @@ import qualified Bulletproofs.RangeProof as RP import qualified Bulletproofs.RangeProof.Internal as RP import qualified Bulletproofs.RangeProof.Verifier as RP + +import qualified Bulletproofs.MultiRangeProof as MRP +import qualified Bulletproofs.MultiRangeProof.Verifier as MRP + import Bulletproofs.Utils import Bulletproofs.Fq as Fq @@ -32,34 +36,55 @@ getUpperBound :: Integer -> Integer getUpperBound n = 2 ^ n -prop_complementaryVector_dotp :: [Bin] -> Property -prop_complementaryVector_dotp ((unbin <$>) -> xs) - = dotp xs (RP.complementaryVector xs) === 0 +prop_complementaryVector_dot :: [Bin] -> Property +prop_complementaryVector_dot ((unbin <$>) -> xs) + = dot xs (RP.complementaryVector xs) === 0 prop_complementaryVector_hadamard :: [Bin] -> Property prop_complementaryVector_hadamard ((toInteger . unbin <$>) -> xs) = hadamardp xs (RP.complementaryVector xs) === replicate (length xs) 0 -prop_dotp_aL2n :: Property -prop_dotp_aL2n = QCM.monadicIO $ do +prop_dot_aL2n :: Property +prop_dot_aL2n = QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - v <- QCM.run $ Fq.random n - QCM.assert $ RP.reversedEncodeBit n v `dotp` powerVector (Fq.new 2) n == v + v <- QCM.run $ randomN n + QCM.assert $ RP.reversedEncodeBit n v `dot` powerVector 2 n == v prop_challengeComplementaryVector :: Property prop_challengeComplementaryVector = QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - v <- QCM.run $ Fq.random n + v <- QCM.run $ randomN n let aL = RP.reversedEncodeBit n v aR = RP.complementaryVector aL - y <- QCM.run $ Fq.random n + y <- QCM.run $ randomN n QCM.assert - $ dotp - ((aL `fqSubV` powerVector 1 n) `fqSubV` aR) + $ dot + ((aL ^-^ powerVector 1 n) ^-^ aR) (powerVector y n) == 0 +prop_reversedEncodeBitAggr :: Int -> Property +prop_reversedEncodeBitAggr x = QCM.monadicIO $ do + n <- QCM.run $ (2 ^) <$> generateMax 8 + vs <- QCM.run $ replicateM x $ randomN n + let m = fromIntegral $ length vs + reversed = RP.reversedEncodeBitMulti n vs + QCM.assert $ vs == fmap (\j -> dot (slice n j reversed) (powerVector 2 n)) [1..m] + +prop_challengeComplementaryVectorAggr :: Int -> Property +prop_challengeComplementaryVectorAggr x = QCM.monadicIO $ do + n <- QCM.run $ (2 ^) <$> generateMax 8 + vs <- QCM.run $ replicateM 3 $ randomN n + let aL = RP.reversedEncodeBitMulti n vs + aR = RP.complementaryVector aL + m = length vs + y <- QCM.run $ randomN n + QCM.assert $ + replicate m 0 + == + fmap (\j -> dot ((slice n j aL ^-^ powerVector 1 n) ^-^ slice n j aR) (powerVector y n)) [1..fromIntegral m] + prop_obfuscateEncodedBits :: Fq -> Fq @@ -67,11 +92,11 @@ prop_obfuscateEncodedBits y z = QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - v <- QCM.run $ Fq.random n + v <- QCM.run $ Fq.new <$> randomN n let aL = RP.reversedEncodeBit n v aR = RP.complementaryVector aL - QCM.assert $ RP.obfuscateEncodedBits n aL aR y z == fqSquare z * v + QCM.assert $ RP.obfuscateEncodedBits n aL aR y z == fSquare z * v prop_singleInnerProduct :: Fq @@ -80,107 +105,129 @@ prop_singleInnerProduct y z = QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - v <- QCM.run $ Fq.random n + v <- QCM.run $ Fq.new <$> randomN n let aL = RP.reversedEncodeBit n v aR = RP.complementaryVector aL - QCM.assert $ RP.obfuscateEncodedBitsSingle n aL aR y z == (fqSquare z * v) + RP.delta n y z + QCM.assert $ RP.obfuscateEncodedBitsSingle n aL aR y z == (fSquare z * v) + RP.delta n 1 y z -setupV :: MonadRandom m => Integer -> m (Integer, Integer, Crypto.Point) +setupV :: MonadRandom m => Integer -> m ((Integer, Integer), Crypto.Point) setupV n = do v <- generateMax (2^n) vBlinding <- Crypto.scalarGenerate curve let vCommit = commit (Fq.new v) (Fq.new vBlinding) - pure (v, vBlinding, vCommit) + pure ((v, vBlinding), vCommit) test_verifyTPolynomial :: TestTree -test_verifyTPolynomial = localOption (QuickCheckTests 50) $ +test_verifyTPolynomial = localOption (QuickCheckTests 5) $ testProperty "Verify T polynomial" $ QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - (v, vBlinding, vCommit) <- QCM.run $ setupV n + m <- QCM.run $ (2 ^) <$> generateMax 3 + ctx <- QCM.run $ replicateM m (setupV n) - proofE <- QCM.run $ runExceptT $ RP.generateProof (getUpperBound n) v vBlinding + proofE <- QCM.run $ runExceptT $ MRP.generateProof (getUpperBound n) (fst <$> ctx) case proofE of Left err -> panic $ show err Right (proof@RP.RangeProof{..}) -> do - let x = shamirX aCommit sCommit t1Commit t2Commit y z + let x, y, z :: Fq + x = shamirX aCommit sCommit t1Commit t2Commit y z y = shamirY aCommit sCommit z = shamirZ aCommit sCommit y - QCM.assert $ RP.verifyTPoly n vCommit proof x y z + QCM.assert $ MRP.verifyTPoly n (snd <$> ctx) proof x y z test_verifyLRCommitments :: TestTree -test_verifyLRCommitments = localOption (QuickCheckTests 20) $ +test_verifyLRCommitments = localOption (QuickCheckTests 5) $ testProperty "Verify LR commitments" $ QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - (v, vBlinding, vCommit) <- QCM.run $ setupV n + m <- QCM.run $ (2 ^) <$> generateMax 3 + ctx <- QCM.run $ replicateM (fromIntegral m) (setupV n) - proofE <- QCM.run $ runExceptT $ RP.generateProof (getUpperBound n) v vBlinding + proofE <- QCM.run $ runExceptT $ MRP.generateProof (getUpperBound n) (fst <$> ctx) case proofE of Left err -> panic $ show err Right (proof@RP.RangeProof{..}) -> do - let x = shamirX aCommit sCommit t1Commit t2Commit y z + let x, y, z :: Fq + x = shamirX aCommit sCommit t1Commit t2Commit y z y = shamirY aCommit sCommit z = shamirZ aCommit sCommit y - QCM.assert $ RP.verifyLRCommitment n proof x y z + QCM.assert $ MRP.verifyLRCommitment n m proof x y z prop_valueNotInRange :: Property -prop_valueNotInRange = expectFailure . QCM.monadicIO $ do +prop_valueNotInRange = QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - (v, vBlinding, vCommit) <- QCM.run $ setupV n + ((v, vBlinding), vCommit) <- QCM.run $ setupV n let upperBound = getUpperBound n vNotInRange = v + upperBound - proofE <- QCM.run $ runExceptT $ RP.generateProof upperBound vNotInRange vBlinding + proofE <- QCM.run $ runExceptT $ MRP.generateProof @Fq upperBound [(vNotInRange, vBlinding)] case proofE of - Left err -> panic $ show err + Left err -> + QCM.assert $ RP.ValuesNotInRange [vNotInRange] == err Right (proof@RP.RangeProof{..}) -> - QCM.assert $ RP.verifyProof upperBound vCommit proof + QCM.assert $ MRP.verifyProof upperBound [vCommit] proof prop_invalidUpperBound :: Property -prop_invalidUpperBound = expectFailure . QCM.monadicIO $ do +prop_invalidUpperBound = QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - (v, vBlinding, vCommit) <- QCM.run $ setupV n + ((v, vBlinding), vCommit) <- QCM.run $ setupV n let invalidUpperBound = q + 1 - proofE <- QCM.run $ runExceptT $ RP.generateProof invalidUpperBound v vBlinding + proofE <- QCM.run $ runExceptT $ MRP.generateProof @Fq invalidUpperBound [(v, vBlinding)] case proofE of - Left err -> panic $ show err + Left err -> + QCM.assert $ RP.UpperBoundTooLarge invalidUpperBound == err Right (proof@RP.RangeProof{..}) -> - QCM.assert $ RP.verifyProof invalidUpperBound vCommit proof + QCM.assert $ MRP.verifyProof invalidUpperBound [vCommit] proof prop_differentUpperBound :: Positive Integer -> Property prop_differentUpperBound (Positive upperBound') = expectFailure . QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - (v, vBlinding, vCommit) <- QCM.run $ setupV n - proofE <- QCM.run $ runExceptT $ RP.generateProof (getUpperBound n) v vBlinding + ((v, vBlinding), vCommit) <- QCM.run $ setupV n + proofE <- QCM.run $ runExceptT $ MRP.generateProof @Fq (getUpperBound n) [(v, vBlinding)] case proofE of Left err -> panic $ show err Right (proof@RP.RangeProof{..}) -> - QCM.assert $ RP.verifyProof upperBound' vCommit proof + QCM.assert $ MRP.verifyProof upperBound' [vCommit] proof test_invalidCommitment :: TestTree test_invalidCommitment = localOption (QuickCheckTests 20) $ testProperty "Check invalid commitment" $ QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - (v, vBlinding, vCommit) <- QCM.run $ setupV n + ((v, vBlinding), vCommit) <- QCM.run $ setupV n let invalidVCommit = commit (Fq.new $ v + 1) (Fq.new vBlinding) upperBound = getUpperBound n - proofE <- QCM.run $ runExceptT $ RP.generateProof upperBound v vBlinding + proofE <- QCM.run $ runExceptT $ MRP.generateProof @Fq upperBound [(v, vBlinding)] case proofE of Left err -> panic $ show err Right (proof@RP.RangeProof{..}) -> - QCM.assert $ not $ RP.verifyProof upperBound invalidVCommit proof + QCM.assert $ not $ MRP.verifyProof upperBound [invalidVCommit] proof -test_completeness :: TestTree -test_completeness = localOption (QuickCheckTests 20) $ - testProperty "Test range proof completeness" $ QCM.monadicIO $ do +test_multiRangeProof_completeness :: TestTree +test_multiRangeProof_completeness = localOption (QuickCheckTests 5) $ + testProperty "Test multi range proof completeness" $ QCM.monadicIO $ do n <- QCM.run $ (2 ^) <$> generateMax 8 - (v, vBlinding, vCommit) <- QCM.run $ setupV n + m <- QCM.run $ generateBetween 1 10 + ctx <- QCM.run $ replicateM (fromIntegral m) (setupV n) let upperBound = getUpperBound n - proofE <- QCM.run $ runExceptT $ RP.generateProof upperBound v vBlinding + + proofE <- QCM.run $ runExceptT $ MRP.generateProof @Fq (getUpperBound n) (fst <$> ctx) case proofE of Left err -> panic $ show err Right (proof@RP.RangeProof{..}) -> + QCM.assert $ MRP.verifyProof upperBound (snd <$> ctx) proof + +test_singleRangeProof_completeness :: TestTree +test_singleRangeProof_completeness = localOption (QuickCheckTests 20) $ + testProperty "Test single range proof completeness" $ QCM.monadicIO $ do + n <- QCM.run $ (2 ^) <$> generateMax 8 + ((v, vBlinding), vCommit) <- QCM.run $ setupV n + let upperBound = getUpperBound n + + proofE <- QCM.run $ runExceptT $ RP.generateProof @Fq (getUpperBound n) (v, vBlinding) + case proofE of + Left err -> panic $ show err + Right (proof@RP.RangeProof{..}) -> QCM.assert $ RP.verifyProof upperBound vCommit proof +