Skip to content

Commit 4f994ed

Browse files
Acentellessdiehl
Acentelles
authored and
sdiehl
committed
Implement proofs of arithmetic circuit computations (#7)
* Generalise over choice of field, use linear library where applicable * Implement proofs of arithmetic circuit computations * Fix random number generation for blinding factors * Make randomN return Integer * Handle arithmetic proof protocol errors * Merge circleCI changes from master * Less linear * Fix case when arithmetic circuit is empty * Pad circuit and assignment to accept circuits of any number of gates * Add test documentation * Derive Generic and NFData * Fq derives Generic and NFData * Derive Generic and NFData (#10) * Derive Generic and NFData * Fq derives Generic and NFData * Add haddock documentation * Update Readme with Arithmetic Circuits section * Add complete example to Readme
1 parent 62e8558 commit 4f994ed

File tree

14 files changed

+823
-96
lines changed

14 files changed

+823
-96
lines changed

‎Bulletproofs/ArithmeticCircuit.hs‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
module Bulletproofs.ArithmeticCircuit
2+
( generateProof
3+
, verifyProof
4+
5+
, ArithCircuitProof(..)
6+
, ArithCircuit(..)
7+
, ArithWitness(..)
8+
, GateWeights(..)
9+
, Assignment(..)
10+
) where
11+
12+
import Bulletproofs.ArithmeticCircuit.Internal
13+
import Bulletproofs.ArithmeticCircuit.Prover
14+
import Bulletproofs.ArithmeticCircuit.Verifier

‎Bulletproofs/ArithmeticCircuit/Internal.hs‎

Lines changed: 256 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,256 @@
1+
{-# LANGUAGE ViewPatterns, RecordWildCards, ScopedTypeVariables #-}
2+
{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-}
3+
4+
module Bulletproofs.ArithmeticCircuit.Internal where
5+
6+
import Protolude hiding (head)
7+
import Data.List (head)
8+
import qualified Data.List as List
9+
import qualified Data.Map as Map
10+
11+
import System.Random.Shuffle (shuffleM)
12+
import qualified Crypto.Random.Types as Crypto (MonadRandom(..))
13+
import Crypto.Number.Generate (generateMax, generateBetween)
14+
import Control.Monad.Random (MonadRandom)
15+
import qualified Crypto.PubKey.ECC.Types as Crypto
16+
import qualified Crypto.PubKey.ECC.Prim as Crypto
17+
18+
import Bulletproofs.Curve
19+
import Bulletproofs.Utils
20+
import Bulletproofs.RangeProof
21+
import qualified Bulletproofs.InnerProductProof as IPP
22+
23+
data ArithCircuitProofError
24+
= TooManyGates Integer -- ^ The number of gates is too high
25+
| NNotPowerOf2 Integer -- ^ The number of gates is not a power of 2
26+
deriving (Show, Eq)
27+
28+
data ArithCircuitProof f
29+
= ArithCircuitProof
30+
{ tBlinding :: f
31+
-- ^ Blinding factor of the T1 and T2 commitments,
32+
-- combined into the form required to make the committed version of the x-polynomial add up
33+
, mu :: f
34+
-- ^ Blinding factor required for the Verifier to verify commitments A, S
35+
, t :: f
36+
-- ^ Dot product of vectors l and r that prove knowledge of the value in range
37+
-- t = t(x) = l(x) · r(x)
38+
, aiCommit :: Crypto.Point
39+
-- ^ Commitment to vectors aL and aR
40+
, aoCommit :: Crypto.Point
41+
-- ^ Commitment to vectors aO
42+
, sCommit :: Crypto.Point
43+
-- ^ Commitment to new vectors sL, sR, created at random by the Prover
44+
, tCommits :: [Crypto.Point]
45+
-- ^ Commitments to t1, t3, t4, t5, t6
46+
, productProof :: IPP.InnerProductProof f
47+
} deriving (Show, Eq, Generic, NFData)
48+
49+
data ArithCircuit f
50+
= ArithCircuit
51+
{ weights :: GateWeights f
52+
-- ^ Weights for vectors of left and right inputs and for vector of outputs
53+
, commitmentWeights :: [[f]]
54+
-- ^ Weigths for a commitments V of rank m
55+
, cs :: [f]
56+
-- ^ Vector of constants of size Q
57+
} deriving (Show, Eq, Generic, NFData)
58+
59+
60+
data GateWeights f
61+
= GateWeights
62+
{ wL :: [[f]] -- ^ WL ∈ F^(Q x n)
63+
, wR :: [[f]] -- ^ WR ∈ F^(Q x n)
64+
, wO :: [[f]] -- ^ WO ∈ F^(Q x n)
65+
} deriving (Show, Eq, Generic, NFData)
66+
67+
data ArithWitness f
68+
= ArithWitness
69+
{ assignment :: Assignment f -- ^ Vectors of left and right inputs and vector of outputs
70+
, commitments :: [Crypto.Point] -- ^ Vector of commited input values ∈ F^m
71+
, commitBlinders :: [f] -- ^ Vector of blinding factors for input values ∈ F^m
72+
} deriving (Show, Eq, Generic, NFData)
73+
74+
data Assignment f
75+
= Assignment
76+
{ aL :: [f] -- ^ aL ∈ F^n. Vector of left inputs of each multiplication gate
77+
, aR :: [f] -- ^ aR ∈ F^n. Vector of right inputs of each multiplication gate
78+
, aO :: [f] -- ^ aO ∈ F^n. Vector of outputs of each multiplication gate
79+
} deriving (Show, Eq, Generic, NFData)
80+
81+
-- | Pad circuit weights to make n be a power of 2, which
82+
-- is required to compute the inner product proof
83+
padCircuit :: Num f => ArithCircuit f -> ArithCircuit f
84+
padCircuit ArithCircuit{..}
85+
= ArithCircuit
86+
{ weights = GateWeights wLNew wRNew wONew
87+
, commitmentWeights = commitmentWeights
88+
, cs = cs
89+
}
90+
where
91+
GateWeights{..} = weights
92+
wLNew = padToNearestPowerOfTwo <$> wL
93+
wRNew = padToNearestPowerOfTwo <$> wR
94+
wONew = padToNearestPowerOfTwo <$> wO
95+
96+
-- | Pad assignment vectors to make their length n be a power of 2, which
97+
-- is required to compute the inner product proof
98+
padAssignment :: Num f => Assignment f -> Assignment f
99+
padAssignment Assignment{..}
100+
= Assignment aLNew aRNew aONew
101+
where
102+
aLNew = padToNearestPowerOfTwo aL
103+
aRNew = padToNearestPowerOfTwo aR
104+
aONew = padToNearestPowerOfTwo aO
105+
106+
delta :: (Eq f, Field f) => Integer -> f -> [f] -> [f] -> f
107+
delta n y zwL zwR= (powerVector (recip y) n `hadamardp` zwR) `dot` zwL
108+
109+
commitBitVector :: (AsInteger f) => f -> [f] -> [f] -> Crypto.Point
110+
commitBitVector vBlinding vL vR = vLG `addP` vRH `addP` vBlindingH
111+
where
112+
vBlindingH = vBlinding `mulP` h
113+
vLG = foldl' addP Crypto.PointO ( zipWith mulP vL gs )
114+
vRH = foldl' addP Crypto.PointO ( zipWith mulP vR hs )
115+
116+
shamirGxGxG :: (Show f, Num f) => Crypto.Point -> Crypto.Point -> Crypto.Point -> f
117+
shamirGxGxG p1 p2 p3
118+
= fromInteger $ oracle $ show q <> pointToBS p1 <> pointToBS p2 <> pointToBS p3
119+
120+
shamirGs :: (Show f, Num f) => [Crypto.Point] -> f
121+
shamirGs ps = fromInteger $ oracle $ show q <> foldMap pointToBS ps
122+
123+
shamirZ :: (Show f, Num f) => f -> f
124+
shamirZ z = fromInteger $ oracle $ show q <> show z
125+
126+
---------------------------------------------
127+
-- Polynomials
128+
---------------------------------------------
129+
130+
evaluatePolynomial :: (Num f) => Integer -> [[f]] -> f -> [f]
131+
evaluatePolynomial (fromIntegral -> n) poly x
132+
= foldl'
133+
(\acc (idx, e) -> acc ^+^ ((*) (x ^ idx) <$> e))
134+
(replicate n 0)
135+
(zip [0..] poly)
136+
137+
multiplyPoly :: Num n => [[n]] -> [[n]] -> [n]
138+
multiplyPoly l r
139+
= snd <$> Map.toList (foldl' (\accL (i, li)
140+
-> foldl'
141+
(\accR (j, rj) -> case Map.lookup (i + j) accR of
142+
Just x -> Map.insert (i + j) (x + (li `dot` rj)) accR
143+
Nothing -> Map.insert (i + j) (li `dot` rj) accR
144+
) accL (zip [0..] r))
145+
(Map.empty :: Num n => Map.Map Int n)
146+
(zip [0..] l))
147+
148+
149+
---------------------------------------------
150+
-- Linear algebra
151+
---------------------------------------------
152+
153+
vectorMatrixProduct :: (Num f) => [f] -> [[f]] -> [f]
154+
vectorMatrixProduct v m
155+
= sum . zipWith (*) v <$> transpose m
156+
157+
vectorMatrixProductT :: (Num f) => [f] -> [[f]] -> [f]
158+
vectorMatrixProductT v m
159+
= sum . zipWith (*) v <$> m
160+
161+
matrixVectorProduct :: (Num f) => [[f]] -> [f] -> [f]
162+
matrixVectorProduct m v
163+
= head $ matrixProduct m [v]
164+
165+
powerMatrix :: (Num f) => [[f]] -> Integer -> [[f]]
166+
powerMatrix m 0 = m
167+
powerMatrix m n = matrixProduct m (powerMatrix m (n-1))
168+
169+
matrixProduct :: Num a => [[a]] -> [[a]] -> [[a]]
170+
matrixProduct a b = (\ar -> sum . zipWith (*) ar <$> transpose b) <$> a
171+
172+
insertAt :: Int -> a -> [a] -> [a]
173+
insertAt z y xs = as ++ (y : bs)
174+
where
175+
(as, bs) = splitAt z xs
176+
177+
genIdenMatrix :: (Num f) => Integer -> [[f]]
178+
genIdenMatrix size = (\x -> (\y -> fromIntegral (fromEnum (x == y))) <$> [1..size]) <$> [1..size]
179+
180+
genZeroMatrix :: (Num f) => Integer -> Integer -> [[f]]
181+
genZeroMatrix (fromIntegral -> n) (fromIntegral -> m) = replicate n (replicate m 0)
182+
183+
generateWv :: (Num f, MonadRandom m) => Integer -> Integer -> m [[f]]
184+
generateWv lConstraints m
185+
| lConstraints < m = panic "Number of constraints must be bigger than m"
186+
| otherwise = shuffleM (genIdenMatrix m ++ genZeroMatrix (lConstraints - m) m)
187+
188+
generateGateWeights :: (Crypto.MonadRandom m, Num f) => Integer -> Integer -> m (GateWeights f)
189+
generateGateWeights lConstraints n = do
190+
[wL, wR, wO] <- replicateM 3 ((\i -> insertAt (fromIntegral i) (oneVector n) (replicate (fromIntegral lConstraints - 1) (zeroVector n))) <$> generateMax (fromIntegral lConstraints))
191+
pure $ GateWeights wL wR wO
192+
where
193+
zeroVector x = replicate (fromIntegral x) 0
194+
oneVector x = replicate (fromIntegral x) 1
195+
196+
generateRandomAssignment :: forall f m . (Num f, AsInteger f, Crypto.MonadRandom m) => Integer -> m (Assignment f)
197+
generateRandomAssignment n = do
198+
aL <- replicateM (fromIntegral n) ((fromInteger :: Integer -> f) <$> generateMax (2^n))
199+
aR <- replicateM (fromIntegral n) ((fromInteger :: Integer -> f) <$> generateMax (2^n))
200+
let aO = aL `hadamardp` aR
201+
pure $ Assignment aL aR aO
202+
203+
computeInputValues :: (Field f, Eq f) => GateWeights f -> [[f]] -> Assignment f -> [f] -> [f]
204+
computeInputValues GateWeights{..} wV Assignment{..} cs
205+
= solveLinearSystem $ zipWith (\row s -> reverse $ s : row) wV solutions
206+
where
207+
solutions = vectorMatrixProductT aL wL
208+
^+^ vectorMatrixProductT aR wR
209+
^+^ vectorMatrixProductT aO wO
210+
^-^ cs
211+
212+
gaussianReduce :: (Field f, Eq f) => [[f]] -> [[f]]
213+
gaussianReduce matrix = fixlastrow $ foldl reduceRow matrix [0..length matrix-1]
214+
where
215+
-- Swaps element at position a with element at position b.
216+
swap xs a b
217+
| a > b = swap xs b a
218+
| a == b = xs
219+
| a < b = let (p1, p2) = splitAt a xs
220+
(p3, p4) = splitAt (b - a - 1) (List.tail p2)
221+
in p1 ++ [xs List.!! b] ++ p3 ++ [xs List.!! a] ++ List.tail p4
222+
223+
-- Concat the lists and repeat
224+
reduceRow matrix1 r = take r matrix2 ++ [row1] ++ nextrows
225+
where
226+
--First non-zero element on or below (r,r).
227+
firstnonzero = head $ filter (\x -> matrix1 List.!! x List.!! r /= 0) [r..length matrix1 - 1]
228+
--Matrix with row swapped (if needed)
229+
matrix2 = swap matrix1 r firstnonzero
230+
--Row we're working with
231+
row = matrix2 List.!! r
232+
--Make it have 1 as the leading coefficient
233+
row1 = (\x -> x * recip (row List.!! r)) <$> row
234+
--Subtract nr from row1 while multiplying
235+
subrow nr = let k = nr List.!! r in zipWith (\a b -> k*a - b) row1 nr
236+
--Apply subrow to all rows below
237+
nextrows = subrow <$> drop (r + 1) matrix2
238+
239+
240+
fixlastrow matrix' = a ++ [List.init (List.init row) ++ [1, z * recip nz]]
241+
where
242+
a = List.init matrix'; row = List.last matrix'
243+
z = List.last row
244+
nz = List.last (List.init row)
245+
246+
-- Solve a matrix (must already be in REF form) by back substitution.
247+
substituteMatrix :: (Field f, Eq f) => [[f]] -> [f]
248+
substituteMatrix matrix = foldr next [List.last (List.last matrix)] (List.init matrix)
249+
where
250+
next row found = let
251+
subpart = List.init $ drop (length matrix - length found) row
252+
solution = List.last row - sum (zipWith (*) found subpart)
253+
in solution : found
254+
255+
solveLinearSystem :: (Field f, Eq f) => [[f]] -> [f]
256+
solveLinearSystem = reverse . substituteMatrix . gaussianReduce

‎Bulletproofs/ArithmeticCircuit/Prover.hs‎

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
{-# LANGUAGE RecordWildCards, ScopedTypeVariables, ViewPatterns #-}
2+
module Bulletproofs.ArithmeticCircuit.Prover where
3+
4+
import Protolude
5+
6+
import Crypto.Random.Types (MonadRandom(..))
7+
import Crypto.Number.Generate (generateMax)
8+
import qualified Crypto.PubKey.ECC.Prim as Crypto
9+
import qualified Crypto.PubKey.ECC.Types as Crypto
10+
11+
import Bulletproofs.Curve
12+
import Bulletproofs.Utils hiding (shamirZ)
13+
import qualified Bulletproofs.InnerProductProof as IPP
14+
import Bulletproofs.ArithmeticCircuit.Internal
15+
16+
-- | Generate a zero-knowledge proof of computation
17+
-- for an arithmetic circuit with a valid witness
18+
generateProof
19+
:: forall f m
20+
. (MonadRandom m, AsInteger f, Field f, Show f, Eq f)
21+
=> ArithCircuit f
22+
-> ArithWitness f
23+
-> m (ArithCircuitProof f)
24+
generateProof (padCircuit -> ArithCircuit{..}) ArithWitness{..} = do
25+
let GateWeights{..} = weights
26+
let Assignment{..} = padAssignment assignment
27+
[aiBlinding, aoBlinding, sBlinding] <- replicateM 3 ((fromInteger :: Integer -> f) <$> generateMax q)
28+
let n = fromIntegral $ length aL
29+
aiCommit = commitBitVector aiBlinding aL aR -- commitment to aL, aR
30+
aoCommit = commitBitVector aoBlinding aO [] -- commitment to aO
31+
32+
(sL, sR) <- chooseBlindingVectors n -- choose blinding vectors sL, sR
33+
let sCommit = commitBitVector sBlinding sL sR -- commitment to sL, sR
34+
35+
let y = shamirGxGxG aiCommit aoCommit sCommit
36+
z = shamirZ y
37+
ys = powerVector y n
38+
zs = drop 1 (powerVector z (qLen + 1))
39+
40+
zwL = zs `vectorMatrixProduct` wL
41+
zwR = zs `vectorMatrixProduct` wR
42+
zwO = zs `vectorMatrixProduct` wO
43+
44+
-- Polynomials
45+
[lPoly, rPoly] = computePolynomials n aL aR aO sL sR y zwL zwR zwO
46+
tPoly = multiplyPoly lPoly rPoly
47+
48+
w = (aL `vectorMatrixProductT` wL)
49+
^+^ (aR `vectorMatrixProductT` wR)
50+
^+^ (aO `vectorMatrixProductT` wO)
51+
52+
t2 = (aL `dot` (aR `hadamardp` ys))
53+
- (aO `dot` ys)
54+
+ (zs `dot` w)
55+
+ delta n y zwL zwR
56+
57+
tBlindings <- insertAt 2 0 . (:) 0 <$> replicateM 5 ((fromInteger :: Integer -> f) <$> generateMax q)
58+
let tCommits = zipWith commit tPoly tBlindings
59+
60+
let x = shamirGs tCommits
61+
evalTCommit = foldl' addP Crypto.PointO (zipWith mulP (powerVector x 7) tCommits)
62+
63+
let ls = evaluatePolynomial n lPoly x
64+
rs = evaluatePolynomial n rPoly x
65+
t = ls `dot` rs
66+
67+
commitTimesWeigths = commitBlinders `vectorMatrixProductT` commitmentWeights
68+
zGamma = zs `dot` commitTimesWeigths
69+
tBlinding = sum (zipWith (\i blinding -> blinding * (x ^ i)) [0..] tBlindings)
70+
+ (fSquare x * zGamma)
71+
72+
mu = aiBlinding * x + aoBlinding * fSquare x + sBlinding * (x ^ 3)
73+
74+
let uChallenge = shamirU tBlinding mu t
75+
u = uChallenge `mulP` g
76+
hs' = zipWith mulP (powerVector (recip y) n) hs
77+
gExp = (*) x <$> (powerVector (recip y) n `hadamardp` zwR)
78+
hExp = (((*) x <$> zwL) ^+^ zwO) ^-^ ys
79+
commitmentLR = (x `mulP` aiCommit)
80+
`addP` (fSquare x `mulP` aoCommit)
81+
`addP` ((x ^ 3)`mulP` sCommit)
82+
`addP` foldl' addP Crypto.PointO (zipWith mulP gExp gs)
83+
`addP` foldl' addP Crypto.PointO (zipWith mulP hExp hs')
84+
`addP` Crypto.pointNegate curve (mu `mulP` h)
85+
`addP` (t `mulP` u)
86+
87+
let productProof = IPP.generateProof
88+
IPP.InnerProductBase { bGs = gs, bHs = hs', bH = u }
89+
commitmentLR
90+
IPP.InnerProductWitness { ls = ls, rs = rs }
91+
92+
pure ArithCircuitProof
93+
{ tBlinding = tBlinding
94+
, mu = mu
95+
, t = t
96+
, aiCommit = aiCommit
97+
, aoCommit = aoCommit
98+
, sCommit = sCommit
99+
, tCommits = tCommits
100+
, productProof = productProof
101+
}
102+
where
103+
qLen = fromIntegral $ length commitmentWeights
104+
computePolynomials n aL aR aO sL sR y zwL zwR zwO
105+
= [ [l0, l1, l2, l3]
106+
, [r0, r1, r2, r3]
107+
]
108+
where
109+
l0 = replicate (fromIntegral n) 0
110+
l1 = aL ^+^ (powerVector (recip y) n `hadamardp` zwR)
111+
l2 = aO
112+
l3 = sL
113+
114+
r0 = zwO ^-^ powerVector y n
115+
r1 = (powerVector y n `hadamardp` aR) ^+^ zwL
116+
r2 = replicate (fromIntegral n) 0
117+
r3 = powerVector y n `hadamardp` sR
118+

0 commit comments

Comments
 (0)