content: {-# LANGUAGE RecordWildCards, ViewPatterns #-}
  module Bulletproofs.ArithmeticCircuit.Verifier where
  
  import Protolude hiding (head)
  import Data.List (head)
  
  import Data.Curve.Weierstrass.SECP256K1 (PA, Fr, mul, inv, gen)
  
  import Bulletproofs.Utils hiding (shamirZ)
  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
    :: [PA]
    -> ArithCircuitProof Fr PA
    -> ArithCircuit Fr
    -> 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 mul hs (powerVector (recip y) n)
  
      uChallenge = shamirU tBlinding mu t
      u = gen `mul` uChallenge
  
      verifyTPoly = lhs == rhs
        where
          lhs = commit t tBlinding
          rhs = (gen `mul` gExp)
              <> tCommitsExpSum
              <> 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 `hadamard` zwR)
          hExp = (((*) x <$> zwL) ^+^ zwO) ^-^ ys
          commitmentLR = (aiCommit `mul` x)
                       <> (aoCommit `mul` (x ^ 2))
                       <> (sCommit `mul` (x ^ 3))
                       <> sumExps gExp gs
                       <> sumExps hExp hs'
                       <> (inv (h `mul` mu))
                       <> (u `mul` t)
  