bug: Race condition on Hint

[niconiconi]

We found a race condition on SolveWithHint function, we provide a minimal example to reproduce the bug.

Description

package gnarktest

import (
	"fmt"
	"math/big"
	"testing"

	"github.com/consensys/gnark-crypto/ecc"
	"github.com/consensys/gnark/backend/groth16"
	"github.com/consensys/gnark/constraint/solver"
	"github.com/consensys/gnark/frontend"
	"github.com/consensys/gnark/frontend/cs/r1cs"
)

func idivFunc(mod *big.Int, inputs []*big.Int, outputs []*big.Int) error {
	zero := big.NewInt(0)
	if inputs[0].Cmp(zero) == 0 && inputs[1].Cmp(zero) == 0 {
		outputs[0] = big.NewInt(1)
		outputs[1] = big.NewInt(0)
		return nil
	} else if inputs[1].Cmp(zero) == 0 {
		outputs[0] = big.NewInt(0)
		outputs[1] = inputs[0]
		return nil
	}
	outputs[0], outputs[1] = new(big.Int).DivMod(inputs[0], inputs[1], outputs[1])
	return nil
}

func Permute(_ *big.Int, inputs []*big.Int, outputs []*big.Int) error {
	if len(inputs) != len(outputs) {
		panic("Input and Output length should be the same")
	}
	var newOdd []*big.Int = make([]*big.Int, 0)
	var newEnd []*big.Int = make([]*big.Int, 0)

	for i := 0; i < len(inputs); i++ {
		if inputs[i].Cmp(big.NewInt(1<<21)) == 1 {
			newEnd = append(newEnd, inputs[i])
		} else {
			newOdd = append(newOdd, inputs[i])
		}
	}
	for i := 0; i < len(newOdd); i++ {
		outputs[i] = newOdd[i]
	}
	for i := 0; i < len(newEnd); i++ {
		outputs[len(newOdd)+i] = newEnd[i]
	}
	return nil
}

type test_circuit struct {
	A frontend.Variable
	B frontend.Variable
	C frontend.Variable
}

func (c *test_circuit) Define(api frontend.API) error {
	testvariablet0 := api.Add(1, 254)
	testvariablet1 := api.Add(1, 2)
	testvariablet2 := api.Add(1, 5)
	testvariablet3 := api.Add(1, 6)
	testvariable1 := api.Add(1, 7)
	testvariable2 := api.Add(2, 99)
	testvariable3 := api.Add(3, 77)
	variablelist := []frontend.Variable{testvariablet0, testvariablet1, testvariablet2, testvariablet3, testvariable1, testvariable2, testvariable3}
	NewSort(api, variablelist)
	return nil
}
func IDivMod(api frontend.API, a frontend.Variable, b frontend.Variable) (frontend.Variable, frontend.Variable) {
	api.Println("a", a)
	api.Println("b", b)
	rets, err := api.NewHint(idivFunc, 2, a, b)
	if err != nil {
		panic("i_div_mod error: " + err.Error())
	} else {
		quotient := rets[0]
		remainder := rets[1]
		api.Println("quotient", quotient)
		api.Println("remainder", remainder)
		api.AssertIsEqual(api.Add(api.Mul(b, quotient), remainder), a)
		return quotient, remainder
	}
}
func NewSort(api frontend.API, x []frontend.Variable) []frontend.Variable {
	sortX, _ := api.NewHint(Permute, len(x), x...)
	oneByte := frontend.Variable(1 << 8)
	oneByte2 := frontend.Variable(1 << 8)
	for i := 0; i < len(x); i++ {
		_, r := IDivMod(api, sortX[i], oneByte)
		res := api.Cmp(r, oneByte2)
		api.Println("res", res)
	}
	return x
}
func TestHint(t *testing.T) {
	solver.RegisterHint(Permute)
	solver.RegisterHint(idivFunc)
	var circuit test_circuit
	r1cs, _ := frontend.Compile(ecc.BN254.ScalarField(), r1cs.NewBuilder, &circuit)
	pk, _, _ := groth16.Setup(r1cs)
	var assignment test_circuit
	assignment.A = big.NewInt(1)
	assignment.B = big.NewInt(2)
	assignment.C = big.NewInt(3)
	witness, _ := frontend.NewWitness(&assignment, ecc.BN254.ScalarField())
	proof, _ := groth16.Prove(r1cs, pk, witness)
	fmt.Printf("proof %v\n", proof)
}

Expected Behavior

Pass the test

Actual Behavior

sometimes it's div by zero, sometimes it's unsatisfied constraint.

Possible Fix

Either fix the race condition, or just specify the following in your documentation:
In a hint function, you cannot directly copy the input to the output (or even in a permuted way).

Steps to Reproduce

1. Run the test provided above

Your Environment

• gnark version used: v0.9.1
• gnark-crypto version used: v0.12.2-0.20231013160410-1f65e75b6dfb
• go version (e.g. 1.20.6): 1.21
• Operating System and version: macOS, Linux, Windows

Cause of the problem:

In this file:
https://github.com/Consensys/gnark/blob/5f1643d98071aabc5abbe89573e4c153cd1c6b0e/constraint/bn254/solver.go#L240C10-L240C10

this part:

There is a race condition if output is a copy of input. For example:

1. Assign output[1] = input[0]
2. Thread 1 do: put(output[1])
3. Thread 2 do: q := pool.BigInt.Get() but unfortunately it got the output[1] from the pool (same memory address)
4. Thread 1 do: put(input[0])

Then in this case, thread 2 will be in trouble because q is recycled by Thread 1 and may be later used by other processes causing a race condition.

[niconiconi]

BTW, the fix from client's code:

package gnarktest

import (
	"fmt"
	"math/big"
	"testing"

	"github.com/consensys/gnark-crypto/ecc"
	"github.com/consensys/gnark/backend/groth16"
	"github.com/consensys/gnark/constraint/solver"
	"github.com/consensys/gnark/frontend"
	"github.com/consensys/gnark/frontend/cs/r1cs"
)

func idivFunc(mod *big.Int, inputs []*big.Int, outputs []*big.Int) error {
	zero := big.NewInt(0)
	if inputs[0].Cmp(zero) == 0 && inputs[1].Cmp(zero) == 0 {
		outputs[0] = big.NewInt(1)
		outputs[1] = big.NewInt(0)
		return nil
	} else if inputs[1].Cmp(zero) == 0 {
		outputs[0] = big.NewInt(0)
		outputs[1] = inputs[0]
		return nil
	}
	outputs[0], outputs[1] = new(big.Int).DivMod(inputs[0], inputs[1], outputs[1])
	return nil
}

func Permute(_ *big.Int, inputs []*big.Int, outputs []*big.Int) error {
	if len(inputs) != len(outputs) {
		panic("Input and Output length should be the same")
	}
	var newOdd []*big.Int = make([]*big.Int, 0)
	var newEnd []*big.Int = make([]*big.Int, 0)

	for i := 0; i < len(inputs); i++ {
		if inputs[i].Cmp(big.NewInt(1<<21)) == 1 {
			newEnd = append(newEnd, inputs[i])
		} else {
			newOdd = append(newOdd, inputs[i])
		}
	}
	for i := 0; i < len(newOdd); i++ {
                 // here if you make a new big.Int instead of directly copy from the input, you will be fine
		outputs[i] = new(big.Int).Set(newOdd[i]) 
	}
	for i := 0; i < len(newEnd); i++ {
                 // here if you make a new big.Int instead of directly copy from the input, you will be fine
		outputs[len(newOdd)+i] = new(big.Int).Set(newEnd[i]) 
	}
	return nil
}

type test_circuit struct {
	A frontend.Variable
	B frontend.Variable
	C frontend.Variable
}

func (c *test_circuit) Define(api frontend.API) error {
	testvariablet0 := api.Add(1, 254)
	testvariablet1 := api.Add(1, 2)
	testvariablet2 := api.Add(1, 5)
	testvariablet3 := api.Add(1, 6)
	testvariable1 := api.Add(1, 7)
	testvariable2 := api.Add(2, 99)
	testvariable3 := api.Add(3, 77)
	variablelist := []frontend.Variable{testvariablet0, testvariablet1, testvariablet2, testvariablet3, testvariable1, testvariable2, testvariable3}
	NewSort(api, variablelist)
	return nil
}
func IDivMod(api frontend.API, a frontend.Variable, b frontend.Variable) (frontend.Variable, frontend.Variable) {
	api.Println("a", a)
	api.Println("b", b)
	rets, err := api.NewHint(idivFunc, 2, a, b)
	if err != nil {
		panic("i_div_mod error: " + err.Error())
	} else {
		quotient := rets[0]
		remainder := rets[1]
		api.Println("quotient", quotient)
		api.Println("remainder", remainder)
		api.AssertIsEqual(api.Add(api.Mul(b, quotient), remainder), a)
		return quotient, remainder
	}
}
func NewSort(api frontend.API, x []frontend.Variable) []frontend.Variable {
	sortX, _ := api.NewHint(Permute, len(x), x...)
	oneByte := frontend.Variable(1 << 8)
	oneByte2 := frontend.Variable(1 << 8)
	for i := 0; i < len(x); i++ {
		_, r := IDivMod(api, sortX[i], oneByte)
		res := api.Cmp(r, oneByte2)
		api.Println("res", res)
	}
	return x
}
func TestHint(t *testing.T) {
	solver.RegisterHint(Permute)
	solver.RegisterHint(idivFunc)
	var circuit test_circuit
	r1cs, _ := frontend.Compile(ecc.BN254.ScalarField(), r1cs.NewBuilder, &circuit)
	pk, _, _ := groth16.Setup(r1cs)
	var assignment test_circuit
	assignment.A = big.NewInt(1)
	assignment.B = big.NewInt(2)
	assignment.C = big.NewInt(3)
	witness, _ := frontend.NewWitness(&assignment, ecc.BN254.ScalarField())
	proof, _ := groth16.Prove(r1cs, pk, witness)
	fmt.Printf("proof %v\n", proof)
}

[niconiconi]

but I do think it's an easy fix from the library's code, just de-dup the duplicated memory address

[ivokub]

As far as I recall, we use a pool to reuse the inputs and outputs from the hint. So it would be correct to instead assign to output value using Set(*big.Int) method. This is indeed not documented imo.

Could you try that in the hint you would do:

func idivFunc(mod *big.Int, inputs []*big.Int, outputs []*big.Int) error {
	zero := big.NewInt(0)
	if inputs[0].Cmp(zero) == 0 && inputs[1].Cmp(zero) == 0 {
		outputs[0].Set(big.NewInt(1))
		outputs[1].Set(big.NewInt(0))
		return nil
	} else if inputs[1].Cmp(zero) == 0 {
		outputs[0].Set(big.NewInt(0))
		outputs[1].Set(inputs[0])
		return nil
	}
	q, r = new(big.Int).DivMod(inputs[0], inputs[1], outputs[1])
        outputs[0].Set(q)
        outputs[1].Set(r)
	return nil
}

func Permute(_ *big.Int, inputs []*big.Int, outputs []*big.Int) error {
	if len(inputs) != len(outputs) {
		panic("Input and Output length should be the same")
	}
	var newOdd []*big.Int = make([]*big.Int, 0)
	var newEnd []*big.Int = make([]*big.Int, 0)

	for i := 0; i < len(inputs); i++ {
		if inputs[i].Cmp(big.NewInt(1<<21)) == 1 {
			newEnd = append(newEnd, inputs[i])
		} else {
			newOdd = append(newOdd, inputs[i])
		}
	}
	for i := 0; i < len(newOdd); i++ {
		outputs[i].Set(newOdd[i])
	}
	for i := 0; i < len(newEnd); i++ {
		outputs[len(newOdd)+i].Set(newEnd[i])
	}
	return nil
}

[niconiconi]

The doc should also clarify following code is not allowed:

func Permute(_ *big.Int, inputs []*big.Int, outputs []*big.Int) error {
	if len(inputs) != len(outputs) {
		panic("Input and Output length should be the same")
	}
	var newOdd []*big.Int = make([]*big.Int, 0)
	var newEnd []*big.Int = make([]*big.Int, 0)

	for i := 0; i < len(inputs); i++ {
		if inputs[i].Cmp(big.NewInt(1<<21)) == 1 {
			newEnd = append(newEnd, inputs[i])
		} else {
			newOdd = append(newOdd, inputs[i])
		}
	}
	for i := 0; i < len(newOdd); i++ {
		outputs[i] = newOdd[i]
	}
	for i := 0; i < len(newEnd); i++ {
		outputs[len(newOdd)+i] = newEnd[i]
	}
	return nil
}

This can cause race condition. It should emphiaze that user can ONLY "Set" the output value, and users cannot assign any other new/old pointer to the output.