bug: Proving Failed if builder.config.CompressThreshold is modified

[ZhmYe]

Hello!
I am a beginner trying to use gnark as a zero knowledge proof framework.
I have implemented two types of circuits here. The first circuit is used to prove the last two terms of a fixed length Fibonacci sequence, and the second circuit is used to recursively verify the proof.At the beginning, the latter could run normally, but the former encountered some problems.
Firstly, let me explain the problems encountered in the former. The circuit I have written is as follows:

type FibonacciCircuit struct {
	X1 frontend.Variable `gnark:",public"`
	X2 frontend.Variable `gnark:",public"`
	V1 frontend.Variable `gnark:"v1"`
	V2 frontend.Variable `gnark:"v2"`
}

func (c *FibonacciCircuit) Define(api frontend.API) error {
	for i := 0; i < 1000000; i++ {
		c.X1 = api.Add(c.X1, c.X2)
		c.X2 = api.Add(c.X1, c.X2)
	}
	api.AssertIsEqual(c.V1, c.X1)
	api.AssertIsEqual(c.V2, c.X2)
	return nil
}

After compilation, I found that the number of wires obtained was only 5, including the public input "1" that r1cs already has, as well as the 2 public inputs and 2 private inputs I declared in the circuit.But the effect I hope to present is to have 100000 internal variables, because in the Define function, I wrote 1000000 loops.

After investigation, I found that if I comment out the judgment conditions in the following code in frontend/cs/r1cs/builder.go.

func (builder *builder) compress(le expr.LinearExpression) expr.LinearExpression {
	// here comment
	if builder.config.CompressThreshold <= 0 || len(le) < builder.config.CompressThreshold {
		return le
	}
    
 
    
	one := builder.cstOne()
	t := builder.newInternalVariable()
	builder.cs.AddR1C(builder.newR1C(le, one, t), builder.genericGate)
	return t
}

Then the result I want will appear.Based on the commented out judgment criteria, I attempted to modify CompressThreshold to 2, in other words, almost all equations will be compressed.But in this way, my second circuit will report an error.

The secondcircuit is the recursive verification circuit.This is an official sample provided by gnark.

type InnerCircuit struct {
	P, Q frontend.Variable
	N    frontend.Variable `gnark:",public"`
}

func (c *InnerCircuit) Define(api frontend.API) error {
	res := api.Mul(c.P, c.Q)
	api.AssertIsEqual(res, c.N)
	return nil
}

func GetInner(field *big.Int) (constraint.ConstraintSystem, groth16.VerifyingKey, witness.Witness, groth16.Proof) {
	// compiles our circuit into a R1CS
	innerCcs, err := frontend.Compile(field, r1cs.NewBuilder, &InnerCircuit{})
	if err != nil {
		panic(err)
	}

	// groth16 zkSNARK: Setup
	innerPK, innerVK, err := groth16.Setup(innerCcs)
	if err != nil {
		panic(err)
	}

	// inner witness definition
	innerAssignment := InnerCircuit{
		P: 3,
		Q: 5,
		N: 15,
	}
	innerWitness, err := frontend.NewWitness(&innerAssignment, field)
	if err != nil {
		panic(err)
	}
	innerPubWitness, err := innerWitness.Public()
	if err != nil {
		panic(err)
	}

	// inner groth16: Prove & Verify
	innerProof, err := groth16.Prove(innerCcs, innerPK, innerWitness)
	if err != nil {
		panic(err)
	}
	err = groth16.Verify(innerProof, innerVK, innerPubWitness)
	if err != nil {
		panic(err)
	}
	return innerCcs, innerVK, innerPubWitness, innerProof
}
type MiddleCircuit[FR emulated.FieldParams, G1El algebra.G1ElementT, G2El algebra.G2ElementT, GtEl algebra.GtElementT] struct {
	Proof        Proof[G1El, G2El]
	VerifyingKey VerifyingKey[G1El, G2El, GtEl]
	InnerWitness Witness[FR]
}

func (c *MiddleCircuit[FR, G1El, G2El, GtEl]) Define(api frontend.API) error {
	curve, err := algebra.GetCurve[FR, G1El](api)
	if err != nil {
		return fmt.Errorf("new curve: %w", err)
	}
	pairing, err := algebra.GetPairing[G1El, G2El, GtEl](api)
	if err != nil {
		return fmt.Errorf("get pairing: %w", err)
	}
	verifier := NewVerifier(curve, pairing)
	err = verifier.AssertProof(c.VerifyingKey, c.Proof, c.InnerWitness)
	return err
}

After modifying the above configuration, I encountered an error when attempting to prove the circuit:

panic: found more than one wire to instantiate

I really hope to know a way to balance the above two issues, Looking forward to your answer very much, thank you!

[ivokub]

It seems that you are rewriting the circuit variables:

	for i := 0; i < 1000000; i++ {
		c.X1 = api.Add(c.X1, c.X2)
		c.X2 = api.Add(c.X1, c.X2)
	}

Could you instead try something like:

res1 = api.Add(c.X1, c.X2)
res2 = api.Add(c.X2, res1)
for i := 0; i < 100000; i++ {
    res := api.Add(res1, res2)
    res1, res2 = res2, tmp
}

[ivokub]

See the written Fibonacci example: http://play.gnark.io/?id=_wmhuc14gg

What happens in R1CS is that the gnark compiler essentially computes the Fibonacci sequence value at runtime as it can replace recursively the additions when computing the sequence. So there is no need to create any new variables as the result depends solely on F0 and F1.

[ZhmYe]

Thanks for your answer. For some purposes, I hope that the Fibonacci sequence circuit can have enough internal variables during the proof period (such as 100000 in the above circuit). But as far as I know, in gnark, "api.add()" only generates a new constraint when the length of the linear expression exceeds a certain number (CompressThreshold), which results in the aforementioned circuit not generating any constraints at all, which is not in line with my requirements. So I tried to modify the CompressThreshold, but it caused an error in the other circuit in my problem at the top.

[ivokub]

I see, you want to force creation of constraints for Fibonacci example. Modifying CompressThreshold can be done using a circuit compile time option frontend.WithCompressThreshold. So, what would happen if you call:

ccs, err := frontend.Compile(field, r1cs.NewBuilder, &InnerCircuit{}, frontend.WithCompressThreshold(1))

For the background why we have this option is that there is a folklore knowledge that additions in R1CS are "free" (as in, doesn't create new constraints), but in practice the circuit compiler becomes very memory-hungry when working with very large linear expressions (lengths of thousands+), so when compressing circuits by enforcing bigLE * 1 = newVar now and then only adds a few percent of constraints, but makes compiler several magnitudes faster and memory efficient.

[ivokub]

NB! I think I haven't personally tried out frontend.WithCompressThreshold(1) myself, only other small values e.g. 5 etc. It would be useful if you let us know how it would work :)