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.