{-# 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 PrimeField (PrimeField(..), toInt)
import Bulletproofs.Curve
import Bulletproofs.Utils hiding (shamirZ)
import Bulletproofs.RangeProof.Internal hiding (delta)
import qualified Bulletproofs.InnerProductProof as IPP
import Bulletproofs.ArithmeticCircuit.Internal
verifyProof
:: (KnownNat p)
=> [Crypto.Point]
-> ArithCircuitProof (PrimeField p)
-> ArithCircuit (PrimeField p)
-> 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 = sumExps (zs `vectorMatrixProduct` wL) hs'
wRCommit = sumExps wRExp gs
wOCommit = sumExps (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` sumExps vExp vCommits
gExp = (x ^ 2) * (k + cQ)
cQ = zs `dot` cs
vExp = (*) (x ^ 2) <$> (zs `vectorMatrixProduct` commitmentWeights)
k = delta n y zwL zwR
xs = 0 : x : 0 : (((^) x) <$> [3..6])
tCommitsExpSum = sumExps 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` ((x ^ 2) `mulP` aoCommit)
`addP` ((x ^ 3) `mulP` sCommit)
`addP` sumExps gExp gs
`addP` sumExps hExp hs'
`addP` Crypto.pointNegate curve (mu `mulP` h)
`addP` (t `mulP` u)