How can I write tests that use wrong hint functions?

[aybehrouz]

When we use hint functions, it's important that the written constraints be able to detect wrong hints. How can I write tests that use some fake and invalid hint functions to test this? Ideally I wouldn't want to pass the hint function as a parameter to my functions.

[ivokub]

Even though a malicious prover could replace hint functions, then I think gnark doesn't provide directly a way to provide incorrect hint function to the prover. We distinguish between hint functions based on id = Hash(Name(hintFn)) where hintFn is a function reference, Name returns fully qualified function name and Hash is some checksum function. So the id of the prover provided hint must be same what compiler has stored for solving some wires.

I think the most fastest option would be to separate hint function behaviour based on some (global) variable. But I think a cleaner solution would be to provide a prover option which allows to provide a hint function with some particular ID.

A hint function can be called several times in a circuit. Would you see a need for having different hint replacements during different calls? It would be more difficult, but still doable (we export a map of wire IDs->hint Fns and allow individual replacement etc.).

And just to add, anonymous functions do not work really well with hint functions. The main idea is that the prover can be a standalone process from the compiler. And then if the package containing anonymous function is not imported, then prover also cannot use the hint function.

[aybehrouz]

We just need to give a good name to any wire that receives a hint, so that the user can refer to it and set a costume value for it.

[gbotrel]

taking as example:

	bits, err := api.Compiler().NewHint(NBits, cfg.NbDigits, v)
	if err != nil {
		panic(err)
	}

	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)

if we replace the hint outputs by a user input (ie circuit.Bits), then you can do some "unit tests" to validate that the hint is correct?
Probably is a bit verbose on the code duplication side.

The option to add a "hook" to tell the solver how to set a particular hint value could also work, but it's ... also going to end up being "verbose" / force the need to have a map of correspondance, etc.

[aybehrouz]

Indeed, it's going to be a bit verbose....
unit tests are usually verbose anyways.

[gbotrel]

heh, some work in progress could enable what you want for "cheap" ; am looking at moving the backend options to constraint (or constraint/solver) package where they belong. And adding an option to "override" a hint could help package organization (cc @Tabaie )
ccs.Solve(witness, solver.OverrideHint(hintID, F))

Still early, might land on develop in the next couple of days.

[aybehrouz]

That's great. 😄

[gbotrel]

it's important that the written constraints be able to detect wrong hints.

Is it ? Technically, the output of the hint functions can be seen as witness (user input); the constraints should hold no matter what the hint outputs;

The hints are really a "convenience" at the constraint system level (it helps the solver assign a value to some wires because solving it "automatically" would be too compute intensive), but from a prover perspective, the actual soundness of constraints don't depend on the actual hint.

[aybehrouz]

That is absolutely correct.

I was trying to summarize the post, but I think actually I've not explained my point very well. I mean, the defined constraint system must make sure that the prover will fail if it uses wrong hint (i.e witness, as you correctly mentioned). For example, in the binary conversion example we need to add a constraint to check that the hint is binary. If we forget to do so, then the prover would be able to prove wrong statements.

I want to be able to test this in my automatic unit tests. For that, I'd need to somehow override the hint used in a function with a wrong one. For example in a binary convertor I should change the internal hint function with a bad one that returns non binary values and see if the prover fails or not.

[gbotrel]

👍
That may be a "better than nothing" solution, but still won't guarantee the soundness of the constraints using the hint output. (ie you can have a bad hint that makes the following constraint fail, and a "bad hint" that makes them "pass").

(on a side note; what we really want to do is check that a block of constraint is sound, has a unique solution and match a "spec". Have a local branch using cvc solver with the recently added FF theory, but did hit couple of perf bottlenecks along the way.. I'ld love to add some kind of "annotations" in gnark API that could guarantee certain properties of pieces of circuits).

[aybehrouz]

This is just something for writing better unit tests. It is not so sophisticated. 😅 Something like this:

hint.Override(NBits, BadHint)
assert.ProverFailed(....)

(on a side note; what we really want to do is check that a block of constraint is sound, has a unique solution and match a "spec". Have a local branch using cvc solver with the recently added FF theory, but did hit couple of perf bottlenecks along the way.. I'ld love to add some kind of "annotations" in gnark API that could guarantee certain properties of pieces of circuits).

That's very interesting.... maybe we can remove hints and consider them as witness, then try to find two different solutions for the constraint system. If two solutions were found we can give a warning or something....

[ivokub]

This is just something for writing better unit tests. It is not so sophisticated. 😅 Something like this:

hint.Override(NBits, BadHint)
assert.ProverFailed(....)

(on a side note; what we really want to do is check that a block of constraint is sound, has a unique solution and match a "spec". Have a local branch using cvc solver with the recently added FF theory, but did hit couple of perf bottlenecks along the way.. I'ld love to add some kind of "annotations" in gnark API that could guarantee certain properties of pieces of circuits).

That's very interesting.... maybe we can remove hints and consider them as witness, then try to find two different solutions for the constraint system. If two solutions were found we can give a warning or something....

So, actually there is something. We have the tinyfield field which is relatively small and allows enumerating all possible witness values (for small vectors): https://github.com/ConsenSys/gnark/tree/develop/internal/tinyfield.

You can see it testing example circuits here https://github.com/ConsenSys/gnark/blob/develop/test/solver_test.go#L28.

But as @gbotrel mentioned, some additional heuristics are needed to annotate parts of the circuit to avoid the possible solution space to explode (preventing checking any useful circuits).