Skip to content

Conversation

@Vindaar
Copy link
Collaborator

@Vindaar Vindaar commented Aug 22, 2024

Edit: The PR previously contained a long description of my debugging of the Groth16 prover implementation. For anyone interested, it can still be found here.

This PR implements a Groth16 prover and verifier, which requires SnarkJS produced .wtns, .zkey and .r1cs binary files.

  • Implement verifier

@Vindaar
Copy link
Collaborator Author

Vindaar commented Jan 12, 2025

I just had another look at SnarkJS to see if I can figure out the double Montgomery encoding situation.

As it turns out at least I could identify the SnarkJS code that writes the coefficients as doubly Montgomery encoded. This happens here:

const nR2 = curve.Fr.mul(n, R2r);
curve.Fr.toRprLE(buffCoeff, 12, nR2);

where R2r is:

const R2r = curve.Fr.e(Scalar.mod(Scalar.mul(Rr,Rr), primeR));

Which at the very least finally ends the question of whether I'm imagining things or not.

I still have no clue why this is done to be honest. The commits touching these lines are not very illuminating either.

@Vindaar Vindaar changed the title Groth16 prover buggy draft Groth16 prover Jan 25, 2025
@Vindaar Vindaar marked this pull request as ready for review January 25, 2025 17:51
Previously these were generated from the wrong branch of the
`{.booldefine.}` variables we had in the code when the PR was still a
draft. Instead of parsing the data as doubly Montgomery encoded as
they actually are, we parsed them as regular Montgomery encoded
resulting in wrong test vectors.
@Vindaar
Copy link
Collaborator Author

Vindaar commented Sep 10, 2025

I guess the code at the moment only works on the 64-bit backend. That rings a bell, it was probably due to the parsing of the binary files. Need to check.

Copy link
Owner

@mratsim mratsim left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

I have added several notes for further refactoring and will follow-up with an issue once that is merged. I think the PR is too big at the moment to add further non-critical fix.

Critical if possible would be to fix the 32-bit tests.

The FFT part is not worth changing at the moment but is important to merge now because the following future work use FFT:

  • FRI for zkVM acceleration
  • Whir for Lean Ethereum
  • PeerDAS. Ethereum 2D KZG commitments with Error Correcting Codes

result &= "\n" & sp & ")"

func toDecimal*[EC: EC_ShortW_Prj or EC_ShortW_Jac or EC_ShortW_Aff or EC_ShortW_JacExt](P: EC, indent: static int = 0): string =
## Stringify an elliptic curve point to Hex
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
## Stringify an elliptic curve point to Hex
## Stringify an elliptic curve point to decimal

## Note. Leading zeros are not removed.
## Output as decimal.
##
## WARNING: NOT constant time!
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually it is constant-time see low-level impl:

func toDecimal*(a: BigInt): string =
## Convert to a decimal string.
##
## This procedure is intended for configuration, prototyping, research and debugging purposes.
## You MUST NOT use it for production.
##
## This function is constant-time.
## This function does heap-allocation.
const len = decimalLength(BigInt.bits)
result = newString(len)
var a = a
for i in countdown(len-1, 0):
let c = ord('0') + a.div10().int
result[i] = char(c)

The mid-level impl is wrong:

func toDecimal*(f: FF): string =
## Convert to a decimal string.
##
## It is intended for configuration, prototyping, research and debugging purposes.
## You MUST NOT use it for production.
##
## This function is NOT constant-time at the moment.
f.toBig().toDecimal()

But it's fine, afaik, it's only used for debugging purposes.

accum.add toDecimal(f)

func appendDecimal*(accum: var string, f: ExtensionField, indent = 0, order: static Endianness = bigEndian) =
## Stringify a tower field element to hex.
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
## Stringify a tower field element to hex.
## Stringify a tower field element to decimal.

for i in 0 ..< half:
# FFT Butterfly
y_times_root .scalarMul_vartime(output[i+half], rootsOfUnity[i])
y_times_root .scalarMul_vartime(rootsOfUnity[i], output[i+half])
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Curious the PR that introduced scalarMul_vartime also rewrote this part of the FFT and the argument order should be scalarMul_vartime(EC, scalar).

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah my mistake, the argument order when out-of-place is correct. (EC out, scalar, EC in)

FFTS_SizeNotPowerOfTwo = "Input must be of a power of 2 length"

FFT_Descriptor*[F] = object # `F` is either `Fp[Name]` or `Fr[Name]`
## Metadata for FFT on Elliptic Curve
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

on fields.

Note that there was an implementation here: https://github.com/mratsim/constantine/blob/v0.2.0/research/kzg/fft_fr.nim

beta2*: EC_ShortW_Aff[Fp2[Name], G2] ## g₂^β
gamma2*: EC_ShortW_Aff[Fp2[Name], G2] ## g₂^γ
delta2*: EC_ShortW_Aff[Fp2[Name], G2] ## g₂^δ
gamma_abc*: seq[EC_ShortW_Aff[Fp[Name], G1]] ## == `zkey.ic` == `[g₁^{ \frac{β·A_i(τ) + α·B_i(τ) + C_0(τ)}{ γ }}]`
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TODO: we will probably want to remove all seqs here in the future to unify with GPU impl.

Also we just don't use seq in Constantine except at the very edge for easy integration with Nim

r1cs: r1cs
)

proc calcAp[Name: static Algebra](ctx: Groth16Prover[Name], wt: seq[Fr[Name]]): EC_ShortW_Jac[Fp[Name], G1] {.noinit.} =
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

All non-var parameters should be openArray instead of seq

result = B1_p


proc buildABC[Name: static Algebra](ctx: Groth16Prover[Name], wt: seq[Fr[Name]]): tuple[A, B, C: seq[Fr[Name]]] =
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TODO: remove seq creation and prefer the caller to pass allocated buffers if possible

Comment on lines +153 to +165
proc transform[Name: static Algebra](args: seq[Fr[Name]], inc: Fr[Name]): seq[Fr[Name]] =
## Applies (multiplies) increasing powers of `inc` to each element
## of `args`, i.e.
##
## `{ a[0], a[1]·inc, a[2]·inc², a[3]·inc³, ... }`.
##
## In our case `inc` is usually a root of unity of the power given by
## `log2( FFT order ) + 1`.
result = newSeq[Fr[Name]](args.len)
var cur = Fr[Name].fromUint(1.uint64)
for i in 0 ..< args.len:
result[i].prod(args[i], cur)
cur *= inc
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note: This patterns also exist in KZG and IPA and other commitments:

See

func ipaEvaluate* [Fr] (res: var Fr, poly: openArray[Fr], point: Fr, n: static int) =
var powers {.noInit.}: array[n,Fr]
powers.asUnchecked().computePowers(point, poly.len)
res.setZero()
for i in 0 ..< poly.len:
var tmp: Fr
tmp.prod(powers[i], poly[i])
res.sum(res,tmp)
res.setZero()
for i in 0 ..< poly.len:
var tmp {.noInit.}: Fr
tmp.prod(powers[i], poly[i])
res.sum(res,tmp)

So there is a computePowers proc, though it does allocate more.

func computePowers*[Name](dst: ptr UncheckedArray[FF[Name]], base: FF[Name], len: int) =
## We need linearly independent random numbers
## for batch proof sampling.
## Powers are linearly independent.
## It's also likely faster than calling a fast RNG + modular reduction
## to be in 0 < number < curve_order
## since modular reduction needs modular multiplication or a division anyway.
let N = len
if N >= 1:
dst[0].setOne()
if N >= 2:
dst[1] = base
for i in 2 ..< N:
dst[i].prod(dst[i-1], base)

pairing(proof.C, vk.delta2)

# 4. Check pairing equality
result = bool(lhs == rhs)
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TODO: This can be rewritten by negating either proof.A or proof.B then use multipairing and check that the result is the pairing group neutral element (i.e. 1 in GT/Fp12)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants