first working (if not very efficient :) version of dynark-style dynamic proofs

This commit is contained in:
Balazs Komuves 2026-06-15 22:40:00 +02:00
parent 67d0126cf4
commit f3f8a0a82b
No known key found for this signature in database
GPG Key ID: F63B7AEF18435562
8 changed files with 250 additions and 75 deletions

View File

@ -55,7 +55,7 @@ func trueIndices*( bs: seq[bool] ): seq[int] =
idxs[j] = i
j += 1
return idxs
func falseIndices*( bs: seq[bool] ): seq[int] =
let k = countFalses(bs)
var idxs: seq[int] = newSeq[int]( k )
@ -66,6 +66,17 @@ func falseIndices*( bs: seq[bool] ): seq[int] =
j += 1
return idxs
func selectTrues*[T]( bs: seq[bool] , xs: seq[T] ): seq[T] =
assert( bs.len == xs.len )
let k = countTrues(bs)
var ys: seq[T] = newSeq[T]( k )
var j = 0
for (i,b) in bs.pairs:
if b:
ys[j] = xs[i]
j += 1
return ys
func notBoolSeq*( us: seq[bool]): seq[bool] =
let n = us.len
var ws: seq[bool] = newSeq[bool]( n )
@ -138,6 +149,33 @@ func sumSeqFr*(xs : seq[Fr[BN254_Snarks]]): Fr[BN254_Snarks] =
s += xs[i]
return s
func countNonZerosFr*( xs: seq[Fr[BN254_Snarks]] ): int =
var cnt = 0
for x in xs:
if not isZeroFr(x):
cnt += 1
return cnt
# returns a mask and a filtered vector
func selectNonZerosFr*( xs: seq[Fr[BN254_Snarks]] ): (seq[bool] , seq[Fr[BN254_Snarks]]) =
var cnt = 0
var mask: seq[bool] = newSeq[bool]( xs.len )
for (i,x) in xs.pairs:
if isZeroFr(x):
mask[i] = false
else:
mask[i] = true
cnt += 1
var k = 0
var short: seq[Fr[BN254_Snarks]] = newSeq[Fr[BN254_Snarks]]( cnt )
for (i,x) in xs.pairs:
if mask[i]:
short[k] = x
k += 1
return (mask,short)
#-------------------------------------------------------------------------------
# G1 arrays

View File

@ -13,18 +13,26 @@
import std/options
import taskpools
import constantine/math/arithmetic
import constantine/named/properties_fields
import groth16/bn128
import groth16/bn128/arrays
import groth16/misc
import groth16/zkey_types
import groth16/files/witness
import groth16/math/domain
import groth16/math/ntt
import groth16/math/poly
import groth16/prover/types
import groth16/prover/shared
import groth16/partial/finish
import groth16/dynamic/types
import groth16/dynamic/setup
import groth16/dynamic/shared
@ -94,3 +102,59 @@ proc testCrossTermCoeffs*(N : int): bool =
return (smart === reference)
#-------------------------------------------------------------------------------
proc finishDynaProofWithMaskV1*( zkey: ZKey, wtns: Witness, dynaPreProof: DynaPreProofV1, mask: Mask, pool: Taskpool, printTimings: bool): Proof =
let N = zkey.header.domainSize
let M = zkey.header.nvars
let D = createDomain( N )
let partialMask = dynaPreProof.partialProof.partial_mask
var deltaAB: OnlyAB
var witnessDelta: seq[Option[F]] = newSeq[Option[F]]( M )
withMeasureTime(printTimings,"building deltaAz, deltaBz"):
for j in 0..<M:
if partialMask[j]:
witnessDelta[j] = none(F)
else:
witnessDelta[j] = some(wtns.values[j])
deltaAB = buildOnlyAB( zkey , witnessDelta )
var proof: Proof
withMeasureTime(printTimings,"finishing the linear terms"):
proof = finishPartialProofWithMaskGeneric( false, zkey, wtns, dynaPreProof.partialProof, mask, pool, false )
var nonlin: G1
var cs: seq[F]
withMeasureTime(printTimings,"computing the nonlinear \"cross\" term"):
withMeasureTime(printTimings," - computing the cross coeffs took"):
cs = crossTermCoeffs(D , deltaAB.valuesAz , deltaAB.valuesBz )
withMeasureTime(printTimings," - computing the cross MSM took"):
nonlin = msmMultiThreadedG1( cs , dynaPreProof.dynaSetup.pointsDeltaLZ , pool )
echo " - nonzero coefficients in deltaA = " & $countNonZerosFr(deltaAB.valuesAz)
echo " - nonzero coefficients in deltaB = " & $countNonZerosFr(deltaAB.valuesBz)
echo " - nonzero coefficients in the cross-term = " & $countNonZerosFr(cs)
withMeasureTime(printTimings,"computing the nonlinear \"projection\" terms"):
let comprAz = selectTrues( dynaPreProof.deltaImages.imageA , deltaAB.valuesAz )
let comprBz = selectTrues( dynaPreProof.deltaImages.imageB , deltaAB.valuesBz )
# echo "comprAz.len = " & $comprAz.len
# echo "comprBz.len = " & $comprBz.len
# echo "projBA.len = " & $dynaPreProof.dynaPreprocess.projA0.len
# echo "projB0.len = " & $dynaPreProof.dynaPreprocess.projB0.len
nonlin += msmMultiThreadedG1( comprAz , dynaPreProof.dynaPreprocess.projB0 , pool )
nonlin += msmMultiThreadedG1( comprBz , dynaPreProof.dynaPreprocess.projA0 , pool )
proof.pi_c += nonlin
return proof
proc finishDynaProofV1*( zkey: ZKey, wtns: Witness, dynaPreProof: DynaPreProofV1 , pool: Taskpool, printTimings = false ): Proof =
let mask = randomMask()
return finishDynaProofWithMaskV1( zkey, wtns, dynaPreProof, mask, pool, printTimings )
#-------------------------------------------------------------------------------

View File

@ -12,11 +12,14 @@
import std/options
import taskpools
import constantine/math/arithmetic
import constantine/named/properties_fields
import groth16/bn128
import groth16/bn128/arrays
import groth16/misc
import groth16/zkey_types
@ -24,9 +27,13 @@ import groth16/math/domain
import groth16/math/convolution
import groth16/math/poly
import groth16/partial/precalc
import groth16/dynamic/types
import groth16/dynamic/setup
import groth16/dynamic/shared
import groth16/dynamic/finish
#-------------------------------------------------------------------------------
@ -51,7 +58,7 @@ func projectionElementsV1*(setup: DynaSetupV1, D: Domain, As: seq[F], complImage
let cf : F = WBarStarA[k] - As[k] * sumW
Us[k] = ALstarW[k] - (As[k] ** setup.wConvDeltaLZ[k]) + (cf ** setup.pointsDeltaLZ[k])
return Us
return selectTrues( complImage , Us )
#---------------------------------------
@ -64,8 +71,8 @@ func simulateProjectionElementsV1*( D: Domain, tau: F, delta: F, As: seq[F], com
let deltaInv : F = invFr(delta)
# reverse indexed wvec: wvecBar[i] = wvec[-i]
let wvecBar: seq[F] = fftReverseVec( setup.weightVec )
# # reverse indexed wvec: wvecBar[i] = wvec[-i]
# let wvecBar: seq[F] = fftReverseVec( calculateWVec( D ) )
# sum_i A[i]*L_i(tau)
var asLTau: F = zeroFr
@ -94,7 +101,7 @@ func simulateProjectionElementsV1*( D: Domain, tau: F, delta: F, As: seq[F], com
let corr : F = deltaInv * As[k] * Lk_tau
Us[k] = (y - corr) ** gen1
return Us
return selectTrues( complImage , Us )
#---------------------------------------
@ -115,22 +122,53 @@ proc testProjectionElementsV1*(N: int, tau: F, delta: F ): bool =
#---------------------------------------
func dynaPreprocessV1*(zkey: ZKey, setup: DynaSetupV1, partialWitness: PartialWitness): DynaPreprocessV1 =
func dynaPreprocessV1*(zkey: ZKey, setup: DynaSetupV1, partialAB: PartialAB): DynaPreprocessV1 =
let N = zkey.header.domainSize
let D = createDomain(N)
# let wtnsMask = partialWitnessMask(partialWitness)
let partialAB = buildPartialAB( zkey, partialWitness.values )
let projA = projectionElementsV1( setup , D , partialAB.valuesAz , partialAB.complImageA )
let projB = projectionElementsV1( setup , D , partialAB.valuesBz , partialAB.complImageB )
# note: as we want to compute A0(x)*B'(x), the image masks should be the other ones!!
let projA = projectionElementsV1( setup , D , partialAB.valuesAz , partialAB.complImageB )
let projB = projectionElementsV1( setup , D , partialAB.valuesBz , partialAB.complImageA )
return DynaPreprocessV1( projA0: projA, projB0: projB )
#-------------------------------------------------------------------------------
proc dynaPreProofV1*(zkey: ZKey, setup: DynaSetupV1, partialWitness: PartialWitness, pool: Taskpool, printTimings: bool): DynaPreProofV1 =
let N = zkey.header.domainSize
let D = createDomain(N)
var partialAB : PartialAB
withMeasureTime(printTimings,"build partial AB"):
partialAB = buildPartialAB( zkey, partialWitness.values )
let imageAB = orBoolSeqs( partialAB.complImageA , partialAB.complImageB )
let deltaImages = DeltaImages( imageA : partialAB.complImageA ,
imageB : partialAB.complImageB ,
imageAB : imageAB )
var partialProof : PartialProof
withMeasureTime(printTimings,"precomputing the linear terms"):
partialProof = generatePartialProof( zkey, partialWitness, pool, false )
var nonlin: G1
withMeasureTime(printTimings,"precomputing the nonlinear term `A0(tau)*B0(tau)` "):
let cs = crossTermCoeffs(D , partialAB.valuesAz , partialAB.valuesBz )
nonlin = msmMultiThreadedG1( cs , setup.pointsDeltaLZ , pool )
partialProof.partial_pi_c += nonlin
var preprocess : DynaPreprocessV1
withMeasureTime(printTimings,"precomputing the \"projection\" points"):
preprocess = dynaPreprocessV1( zkey, setup, partialAB )
return DynaPreProofV1( partialProof : partialProof ,
deltaImages : deltaImages ,
dynaSetup : setup ,
dynaPreprocess : preprocess )
#-------------------------------------------------------------------------------

View File

@ -4,12 +4,13 @@
# import constantine/named/properties_fields
import groth16/bn128
import groth16/misc
import groth16/math/domain
import groth16/math/group_fft
import groth16/math/poly
import groth16/math/convolution
# import groth16/math/convert
import groth16/math/convert
# import groth16/math/ntt
import groth16/zkey_types
@ -26,19 +27,29 @@ import groth16/dynamic/shared
#-------------------------------------------------------------------------------
# does the setup from the ZKey (prover key)
func dynaSetupV1FromZKey*(zkey: Zkey): DynaSetupV1 =
assert( zkey.header.flavour == JensGroth , "DynaSetupV1 requires classic (quotient) flavour, not Jordi's one!" )
proc dynaSetupV1FromZKey*(zkey: Zkey): DynaSetupV1 =
let N = zkey.header.domainSize
let D = createDomain(N)
# assert( zkey.header.flavour == JensGroth , "DynaSetupV1 requires classic (quotient) flavour, not Jordi's one!" )
var deltaZTau : seq[G1] # the points `delta^-1 * (tau^N-1) * tau^i * g1`
case zkey.header.flavour
of JensGroth:
deltaZTau = zkey.pPoints.pointsH1
of Snarkjs:
echo "Jordi-style .zkey detected; converting points! (slow...)"
withMeasureTime(true,"Jordi-to-Jens conversion"):
deltaZTau = convertPointsFromJordi(D , zkey.pPoints.pointsH1)
let deltaLZ = inverseGroupFFT( zkey.pPoints.pointsH1 , D )
let wvec = calculateWVec( D )
let deltaLZ = inverseGroupFFT( deltaZTau , D )
let conv = groupConvolution( wvec , deltaLZ )
return DynaSetupV1( pointsDeltaLZ : deltaLZ ,
weightVec : wvec ,
wConvDeltaLZ : conv )
#---------------------------------------
@ -60,8 +71,7 @@ func simulateDynaSetupV1*( D: Domain, tau: F, delta: F ): DynaSetupV1 =
let wvec = calculateWVec( D )
let conv = groupConvolution( wvec , deltaLZ )
return DynaSetupV1( weightVec : wvec ,
pointsDeltaLZ : deltaLZ ,
return DynaSetupV1( pointsDeltaLZ : deltaLZ ,
wConvDeltaLZ : conv )
#-------------------------------------------------------------------------------

View File

@ -1,6 +1,8 @@
import std/options
import taskpools
import constantine/math/arithmetic
import constantine/named/properties_fields
@ -138,20 +140,21 @@ func buildOnlyAB*( zkey: ZKey, pwitness: seq[Option[F]] ): OnlyAB =
var valuesBz = newSeq[F](domSize)
for entry in zkey.coeffs:
case entry.matrix
if not isZeroFr(entry.coeff):
case entry.matrix
of MatrixA:
if isSome(pwitness[entry.col]):
valuesAz[entry.row] += entry.coeff * pwitness[entry.col].unsafeGet()
of MatrixB:
if isSome(pwitness[entry.col]):
valuesBz[entry.row] += entry.coeff * pwitness[entry.col].unsafeGet()
else: raise newException(AssertionDefect, "fatal error")
of MatrixA:
if isSome(pwitness[entry.col]):
valuesAz[entry.row] += entry.coeff * pwitness[entry.col].unsafeGet()
of MatrixB:
if isSome(pwitness[entry.col]):
valuesBz[entry.row] += entry.coeff * pwitness[entry.col].unsafeGet()
else: raise newException(AssertionDefect, "fatal error")
return OnlyAB( valuesAz:valuesAz ,
valuesBz:valuesBz )
return OnlyAB( valuesAz: valuesAz ,
valuesBz: valuesBz )
#---------------------------------------
@ -171,26 +174,27 @@ func buildPartialAB*( zkey: ZKey, pwitness: seq[Option[F]] ): PartialAB =
complImageB[i] = false
for entry in zkey.coeffs:
case entry.matrix
if not isZeroFr(entry.coeff):
case entry.matrix
of MatrixA:
if isSome(pwitness[entry.col]):
valuesAz[entry.row] += entry.coeff * pwitness[entry.col].unsafeGet()
else:
complImageA[entry.row] = true
of MatrixB:
if isSome(pwitness[entry.col]):
valuesBz[entry.row] += entry.coeff * pwitness[entry.col].unsafeGet()
else:
complImageB[entry.row] = true
else: raise newException(AssertionDefect, "fatal error")
of MatrixA:
if isSome(pwitness[entry.col]):
valuesAz[entry.row] += entry.coeff * pwitness[entry.col].unsafeGet()
else:
complImageA[entry.row] = true
of MatrixB:
if isSome(pwitness[entry.col]):
valuesBz[entry.row] += entry.coeff * pwitness[entry.col].unsafeGet()
else:
complImageB[entry.row] = true
else: raise newException(AssertionDefect, "fatal error")
return PartialAB( valuesAz:valuesAz,
valuesBz:valuesBz,
complImageA:complImageA,
complImageB:complImageB )
return PartialAB( valuesAz: valuesAz,
valuesBz: valuesBz,
complImageA: complImageA,
complImageB: complImageB )
#-------------------------------------------------------------------------------
# the phi(x) polynomials and Lagrange product decomposition (for testing purposes)

View File

@ -29,9 +29,13 @@ type
type
DeltaImages* = object
imageA* : seq[bool] # image of the witness update space under A
imageB* : seq[bool] # image of the witness update space under B
imageAB* : seq[bool] # union of the previous two
# things we can compute at circuit setup time
DynaSetupV1* = object
weightVec* : seq[F] # the weights `W_k = 1/N/(omega^-k - 1)`
pointsDeltaLZ* : seq[G1] # the points `delta^-1 * L_i(tau) * Z(tau) * g1` where `Z(x) = x^N-1`
wConvDeltaLZ* : seq[G1] # the convolution of `W` and `pointsDeltaLZ`
@ -41,8 +45,10 @@ type
projB0* : seq[G1] # the same for B0
DynaPreProofV1* = object
partialProof* : PartialProof
dyanPreprocess* : DynaPreprocessV1
partialProof* : PartialProof # linear part of the partial proof
deltaImages* : DeltaImages # image of the witness delta under A and B (where can update happen)
dynaSetup* : DynaSetupV1 # circuit-setup time calculations
dynaPreprocess* : DynaPreprocessV1 # "Dynark"-style preprocessing
# this is used in the "cross-term"
OnlyAB* = object

View File

@ -14,7 +14,6 @@ import constantine/named/properties_fields
import groth16/bn128
import groth16/math/domain
import groth16/math/poly
import groth16/math/matrix
import groth16/zkey_types
import groth16/files/witness
import groth16/misc
@ -27,7 +26,8 @@ import groth16/prover/shared
# the finishing prover
#
proc finishPartialProofWithMask*( zkey: ZKey, wtns: Witness, partialProof: PartialProof, mask: Mask, pool: Taskpool, printTimings: bool): Proof =
# you can turn on/off the computation of the nonlinear term (useful for the "dynark" version)
proc finishPartialProofWithMaskGeneric*( nonlinear_term: bool, zkey: ZKey, wtns: Witness, partialProof: PartialProof, mask: Mask, pool: Taskpool, printTimings: bool): Proof =
# if (zkey.header.curve != wtns.curve):
# echo( "zkey.header.curve = " & ($zkey.header.curve) )
@ -87,22 +87,26 @@ proc finishPartialProofWithMask*( zkey: ZKey, wtns: Witness, partialProof: Parti
k += 1
var abc : ABC
withMeasureTime(printTimings,"building 'ABC'"):
abc = buildABC( zkey, witness )
var qs : seq[Fr[BN254_Snarks]]
withMeasureTime(printTimings,"computing the quotient (FFTs)"):
case zkey.header.flavour
if nonlinear_term:
# the points H are [delta^-1 * tau^i * Z(tau)]
of JensGroth:
let polyQ = computeQuotientPointwise( abc, pool )
qs = polyQ.coeffs
withMeasureTime(printTimings,"building 'ABC'"):
abc = buildABC( zkey, witness )
withMeasureTime(printTimings,"computing the quotient (FFTs)"):
case zkey.header.flavour
# the points H are `[delta^-1 * L_{2i+1}(tau)]_1`
# where L_i are Lagrange basis polynomials on the double-sized domain
of Snarkjs:
qs = computeSnarkjsScalarCoeffs( abc, pool )
# the points H are [delta^-1 * tau^i * Z(tau)]
of JensGroth:
let polyQ = computeQuotientPointwise( abc, pool )
qs = polyQ.coeffs
# the points H are `[delta^-1 * L_{2i+1}(tau)]_1`
# where L_i are Lagrange basis polynomials on the double-sized domain
of Snarkjs:
qs = computeSnarkjsScalarCoeffs( abc, pool )
assert( hdr.domainSize == qs.len )
# masking coeffs
let r = mask.r
@ -111,7 +115,6 @@ proc finishPartialProofWithMask*( zkey: ZKey, wtns: Witness, partialProof: Parti
assert( witness.len == pts.pointsA1.len )
assert( witness.len == pts.pointsB1.len )
assert( witness.len == pts.pointsB2.len )
assert( hdr.domainSize == qs.len )
assert( hdr.domainSize == pts.pointsH1.len )
assert( nvars - npubs - 1 == pts.pointsC1.len )
@ -131,22 +134,28 @@ proc finishPartialProofWithMask*( zkey: ZKey, wtns: Witness, partialProof: Parti
pi_b += msmMultiThreadedG2( compact_witness , compact_pointsB2, pool )
var pi_c : G1 = partialProof.partial_pi_c
withMeasureTime(printTimings,"computing pi_C (2x G1 MSM)"):
withMeasureTime(printTimings,"computing pi_C linear part (G1 MSM)"):
pi_c += s ** pi_a
pi_c += r ** rho
pi_c += negFr(r*s) ** spec.delta1
pi_c += msmMultiThreadedG1( qs , pts.pointsH1, pool )
pi_c += msmMultiThreadedG1( compact_zs , compact_pointsC1, pool )
withMeasureTime(printTimings,"computing pi_C nonlinear part (large G1 MSM)"):
if nonlinear_term:
pi_c += msmMultiThreadedG1( qs , pts.pointsH1, pool )
return Proof( curve:"bn128", publicIO:pubIO, pi_a:pi_a, pi_b:pi_b, pi_c:pi_c )
#-------------------------------------------------------------------------------
proc finishPartialProofWithMask*( zkey: ZKey, wtns: Witness, partial: PartialProof, mask: Mask, pool: Taskpool, printTimings: bool): Proof =
return finishPartialProofWithMaskGeneric( true, zkey, wtns, partial, mask, pool, printTimings )
proc finishPartialProofWithTrivialMask*( zkey: ZKey, wtns: Witness, partial: PartialProof, pool: Taskpool, printTimings: bool ): Proof =
let mask = Mask( r: zeroFr , s: zeroFr )
return finishPartialProofWithMask( zkey, wtns, partial, mask, pool, printTimings )
proc finishPartialProof*( zkey: ZKey, wtns: Witness, partial: PartialProof, pool: Taskpool, printTimings = false ): Proof =
proc finishPartialProof*( zkey: ZKey, wtns: Witness, partial: PartialProof, pool: Taskpool, printTimings = false): Proof =
let mask = randomMask()
return finishPartialProofWithMask( zkey, wtns, partial, mask, pool, printTimings )

View File

@ -4,6 +4,7 @@
import constantine/named/properties_fields
import groth16/bn128
import groth16/bn128/debug
#-------------------------------------------------------------------------------
@ -28,6 +29,11 @@ func isEqualProof*(prf1, prf2: Proof): bool =
(prf1.pi_b === prf2.pi_b) and
(prf1.pi_c === prf2.pi_c)
proc debugPrintProof*(prf: Proof) =
debugPrintG1( "pi_A:" , prf.pi_a )
debugPrintG2( "pi_B:" , prf.pi_b )
debugPrintG1( "pi_C:" , prf.pi_c )
#-------------------------------------------------------------------------------
# Az, Bz, Cz column vectors
#