There should be some way for flagging the output of a hint as a constant when needed

[aybehrouz]

When a hint is called on constant inputs the return value should be considered to be constant. This can greatly help in detecting constant wires and performing optimizations. Currently it seems that the output of a hint is always flagged as a non constant:

bits, _ := api.Compiler().NewHint(NBits, 5, 17)
_, isConstant := api.Compiler().ConstantValue(bits[0])
print(isConstant)

output:

false

[ivokub]

Hmm, I'm not sure this may always be true. We could also use hints for obtaining randomness or potentially I/O.

For example lets say we have a hint which returns randomness from some trustworthy random beacon. As an input the hint takes how many bytes of output we want and it is a constant input. However, the output is a variable and we have to check in-circuit that it is correct (e.h. assert is correctly signed and is VRF output etc.)

[ivokub]

(but the use case is cool! I think we should implement it :)

[gbotrel]

mmhh yes we don't have such use cases yet (ie a hint w/ constant as place holder).

But an alternative, is to replace bits, _ := api.Compiler().NewHint(NBits, 5, 17) by NBits(5,17) directly no? If it's a constant in the circuit, then, why bother going through the hint mechanism?

[aybehrouz]

Hmm, I'm not sure this may always be true. We could also use hints for obtaining randomness or potentially I/O.

Can't we possibly say that in those cases actually the hint is accepting a private non-constant input? (I mean the beacon is actually giving a private input to us) Maybe I'm wrong, but I personally see hints solely as a way for helping the solver, so constant inputs should give constant outputs.

mmhh yes we don't have such use cases yet (ie a hint w/ constant as place holder).

The thing is, I've realized that almost any function that uses hints can not benefit from automatic optimizations for constants. You'll have to handle constants explicitly, which is really cumbersome. Do you remember we removed the constant path of ToBinary in a PR? Now I've realized that ToBinary(api, constant) can generate undesirable constraints! 😅 The reason that those constraints are generated is that the function uses a hint and that hint doesn't allow removing constraints.

[aybehrouz]

For example bits.ToBinary(api, 14, bits.WithNbDigits(4)) currently generates 5 constraints. I changed the code of toBinary to this:

func toBinary(api frontend.API, v frontend.Variable, opts ...BaseConversionOption) []frontend.Variable {
	// parse options
	cfg := baseConversionConfig{
		NbDigits:             api.Compiler().FieldBitLen(),
		UnconstrainedOutputs: false,
	}

	for _, o := range opts {
		if err := o(&cfg); err != nil {
			panic(err)
		}
	}

	c := big.NewInt(1)
	/*
		bits, err := api.Compiler().NewHint(NBits, cfg.NbDigits, v)
		if err != nil {
			panic(err)
		}
	*/
// instead of using the hint, we use a constant array. We see
// that no redundant constraint is generated.
	bits := []frontend.Variable{0, 1, 1, 1}

	var Σbi frontend.Variable
	Σbi = 0
	for i := 0; i < cfg.NbDigits; i++ {
		Σbi = api.Add(Σbi, api.Mul(bits[i], c))
		c.Lsh(c, 1)
		if !cfg.UnconstrainedOutputs {
			api.AssertIsBoolean(bits[i])
		}
	}

	// record the constraint Σ (2**i * b[i]) == a
	api.AssertIsEqual(Σbi, v)

	return bits
}

This generates only 1 constraint. That single constraint is generated because api.AssertIsEqual does not properly handle constants and api.AssertIsEqual(14,14) generates one unnecessary constraint. If we fix that then constants can be fully optimized automatically if we fix the hint problem.

And something like toBinary(api, 14) happens when you use something like AssertIsLess(x, 14).

[ivokub]

In my view, a hint is non-deterministic computation by the prover. So if we say that if the input are constant then also outputs are, then we break the assumption that hint can be any computation.

Rather, it is a bug if AssertIsLess(x, 14) generates redundant constraints. We should fix that instead of redefining hints. As you said, we need to add cases where either of the inputs to the assertion is a constant and handle those separately.

[aybehrouz]

The thing is, if the constant property gets propagated correctly, in most cases we won't need to handle constants by defining a lot of if-else clauses. Assume I'm writing a function like this:

func f(x, y frontend.Variable) frontend.Variable {
    return g(api.Add(x, y))
}

Let's say that g will not generate any constraints when its input is a constant. We want to make sure that no constraints are generated when both x and y are constants. Fortunately, because api.Add returns a constant when both of its inputs are constants (i.e. it propagates the constant property) here we don't need to handle constants by if-else. If api.Add always returned a non-constant, then we would need an ugly code.

Hints are a problem, because they never propagate the constant property. They always return a non-constant. That's the only reason the current implementation of ToBinary is unable to handle constants.

Automatically Inferring that the output of a hint is a constant could be a solution that makes development easier. However, I did not consider hints that produce private inputs by computation. So, if that doesn't work, we can give a programmer a way to define that the output of a hint function is a constant. There should be some way for propagating the constant property.

[ivokub]

Automatically Inferring that the output of a hint is a constant could be a solution that makes development easier. However, I did not consider hints that produce private inputs by computation. So, if that doesn't work, we can give a programmer a way to define that the output of a hint function is a constant. There should be some way for propagating the constant property.

Hint functions are not uniquely determined! This means that the prover/solver can swap hint functions at runtime. But the circuit definition happens at compile time. So if in circuit we somehow assume that an output of a hint is constant, we compile it into a constraint system without some assertions. However, the prover can simply replace the hint function which returns either different variable (which may or may not be a constant). This leads to unsound proofs.

I still think that the only problem is that binary decomposition has a bug and we need to fix it.

In general I think that using hints is really dangerous and mostly leads to unsound proofs. In latest gadgets I usually try to avoid exposing the hint functions at all to prevent users using them directly (a la https://github.com/ConsenSys/gnark/blob/develop/std/algebra/emulated/fields_bls12381/hints.go#L17).

[ivokub]

But I do get that differentiating between variables and constants right now in gnark is not perfect.

I think long-term better approach would be to have different types and prevent using frontend.API for all-constant operations. For variable-constant operations I think it would be better to have either separate methods or we should use type parameters. But this would be a breaking change and we are not planning it right now.

[aybehrouz]

Hint functions are not uniquely determined! This means that the prover/solver can swap hint functions at runtime.

Here we are replacing the output of the hint with a constant wire, so the hint function is actually "optimized-out" and removed from the final circuit. There will be no issues regarding malicious provers.

Think of it like this: the user defines a circuit using the gnark API. When we are compiling the circuit, we can detect that some defined gates are actually redundant and we can remove them. For example the user has defined a multiplication gate that has two constant inputs 3, 6. We can simply replace this gate with the constant wire 18. For hints a similar thing happens. A hint is like a private input in the view of the circuit/constraint system. When we realize that the output of the hint is a constant, we can replace it with a constant wire.

As an example assume we have a division gadget Div. If the user, in his code, has used something like Div(6,3), we can simply replace this gadget with the constant wire 2. Now let's take a look at a possible implementation (the code may have errors):

func Div(api frontend.API, x, y frontend.Variable) frontend.Variable {
    q, _ := api.Compiler().NewHint(divHint, 1, x, y)
    api.AssertIsEqual(x, api.Mul(y, q))
    return q
}

Here, the optimizer knows that x and y are constants 6 and 3. But it thinks that q is a variable so it can not optimize api.Mul and api.AssertIsEqual. However, q actually is 2 and is a constant.

Interestingly I've checked several examples of this type, and it seems gnark is already able to perform most of this sort of optimizations. You just need to fix hints.

[ivokub]

func Div(api frontend.API, x, y frontend.Variable) frontend.Variable {
    q, _ := api.Compiler().NewHint(divHint, 1, x, y)
    api.AssertIsEqual(x, api.Mul(y, q))
    return q
}

Here, the optimizer knows that x and y are constants 6 and 3. But it thinks that q is a variable so it can not optimize api.Mul and api.AssertIsEqual. However, q actually is 2 and is a constant.

Interestingly I've checked several examples of this type, and it seems gnark is already able to perform most of this sort of optimizations. You just need to fix hints.

Optimizer(compiler) cannot know that q = 2 as it doesn't know what is divHint. Right now it is only for simplicity that we provide the function pointer to NewHint (and use it to compute a unique tag), but we do not store the implementation. Actually, we only store a unique tag in this location and later solver is asked to provide some value for two inputs and this tag.

If the example would be

func Div(api frontend.API, x, y frontend.Variable) frontend.Variable {
    q, _ := api.Compiler().NewHint("fn1", 1, x, y) // tag "fn1" indicates the location
    api.AssertIsEqual(x, api.Mul(y, q))
    return q
}

Then the solver is later just asked: "given tag fn1, inputs 6, 3, give me one output". There is no indication that the operation is division etc etc.

[aybehrouz]

Optimizer(compiler) cannot know that q = 2 as it doesn't know what is divHint. Right now it is only for simplicity that we provide the function pointer to NewHint

The compiler could have access to the implementation of the hint anyway. For the moment let's assume all hints are stateless as my initial assumption. If all hints are stateless, when the compiler sees that all inputs to the hint are constants, it can simply execute the hint function on those constant values (constant values are available at compile time) and record the output as a constant wire which replaces the hint output.

Actually I think you can implement a new function: Compiler.NewStateLessHint and implement that logic. That way stateful hints, like those examples you mentioned, will not become problematic because they can use the old Compiler.NewHint.

[hussein-aitlahcen]

Optimizer(compiler) cannot know that q = 2 as it doesn't know what is divHint. Right now it is only for simplicity that we provide the function pointer to NewHint

The compiler could have access to the implementation of the hint anyway. For the moment let's assume all hints are stateless as my initial assumption. If all hints are stateless, when the compiler sees that all inputs to the hint are constants, it can simply execute the hint function on those constant values (constant values are available at compile time) and record the output as a constant wire which replaces the hint output.

Actually I think you can implement a new function: Compiler.NewStateLessHint and implement that logic. That way stateful hints, like those examples you mentioned, will not become problematic because they can use the old Compiler.NewHint.

Definitely makes sense to me, you want to inline the hint function if it is pure and applied to constants. Nifty optimization for ToBits/FromBits indeed. Would be interested to check your branch and tell if my circuit is simplified (~60M constraints with many constants).

[aybehrouz]

Would be interested to check your branch and tell if my circuit is simplified

I'd be more than happy if that could be useful for you.