I would like to know the feasibility of implementing this to understand if we wait for it, or we try to find some other workaround. @ivokub @gbotrel Thanks.

I'm thinking that instead of returning a flag, it could simply return an assert error (but do no actually Assert).

That is very interesting proposal, and I think it would be worth it. It could actually enable a few use-cases for making rollups more gas-efficient using "optimistic zk-rollup" approach where the PLONK/Groth16 proofs are not always verified on-chain but the challengers could post proof-of-invalidity for some posted proofs. I recall someone has proposed the idea, but I cannot find it now.

The issue is however, that the proof can fail in several places, so we would need to account for that. And for example when the proof verification fails early, then we need to swap the rest of proof checking to work on dummy variables so that we would have a solvable witness to be able to complete the circuit. I haven't checked the proposed change in detail, but just keep in mind.

Another idea - you can provide the expected verification result (succcess/failure) as an argument, as it should be part of the witness anyway imo. And then inside the assertion method you use a hint to deduce what is the actual failure reason, and then implement the corresponding cases. We have done something very similar in ECRecover precompile for Linea, see https://github.com/Consensys/gnark/blob/master/std/evmprecompiles/01-ecrecover.go as we also need to prove ECRecover calls with invalid inputs (in which case the transaction is reverted, but we need to prove the revert). It actually required quite a lot of thinking to handle all the failure cases properly. I think in general for Groth16 it should be straightforward as we only do a pairing check essentially, but for PLONK we actually have several asserts inside the recursive verifier.

In the example you have, in cases:

_, err := something()
if err != nil {
    valid = v.api.Mul(valid, 0)
}

you don't have to add the assertions - such errors are circuit compile time errors (a la input length mismatch etc.), not solving time errors. So it is safe to do instead

go
_, err := something()
if err != nil {
    return err
}

In the example you have, in cases:

_, err := something()
if err != nil {
valid = v.api.Mul(valid, 0)
}
you don't have to add the assertions - such errors are circuit compile time errors (a la input length mismatch etc.), not solving time errors. So it is safe to do instead

go
_, err := something()
if err != nil {
    return err
}

Right! Well, that was only a very quick&dirty example to provide better understanding of the proposal.

I do believe the big challenge is what you mention of when the proof verification fails early, then we need to swap the rest of proof checking to work on dummy variables so that we would have a solvable witness to be able to complete the circuit.

And one more thing - essentially when doing a PairingCheck, then we compute the pairing result and compare it against 1 in the target group. It is just that when we call PairingCheck, then we don't do the full finalexp, but only part of it, saving a lot of constraints for the full successful recursive verifier. But I think something similar could be done when we only want to check if the pairing corresponds to 1 or not.

Pinging @yelhousni to loop in.

So, I definitely recommend posting as a PR and then we could start working from that. And for simplicity I think Groth16 at first and later can figure out PLONK.

In general, not having direct Assertions within the Gnark standard library would improve control-flow on the final circuit design. I.e, Circom uses this approach, and they do have control-flow with if/else statements and so on, which is quite useful.
https://docs.circom.io/circom-language/control-flow/

Of course, this is a big change to the design of the framework, so it's maybe something that can be worked slowly with time.

Related #81

In general, not having direct Assertions within the Gnark standard library would improve control-flow on the final circuit design. I.e, Circom uses this approach, and they do have control-flow with if/else statements and so on, which is quite useful. https://docs.circom.io/circom-language/control-flow/

Of course, this is a big change to the design of the framework, so it's maybe something that can be worked slowly with time.

Related #81

Indeed, it would be a big change. Our problem is that gnark is essentially Go API, but for such control flow changes we would have to have a DSL or do source code processing from AST etc.

So, I definitely recommend posting as a PR and then we could start working from that. And for simplicity I think Groth16 at first and later can figure out PLONK.

I'm not sure if I can do that. I can work at the Circuit API level, but modifying the Pairing Check requires some understanding that I might not have. Furthermore, I'm a bit lost on what part of the Gnark code is built with a Generator and which is manually coded, tbh. Are the algebra/pairing functions autogenerated somehow? Where is the source?

I think for the in-circuit implementation we don't use autogenerated code. The interfaces and implementations are defined in https://github.com/Consensys/gnark/blob/master/std/algebra/interfaces.go and https://github.com/Consensys/gnark/tree/master/std/algebra (see native for 2-chain implementation and emulated for emulated implementations).

For out-circuit computation it is good enough to compute Pair of the inputs, initialize target group 1 with https://pkg.go.dev/github.com/consensys/gnark-crypto@v0.16.0/ecc/bls12-377/internal/fptower#E12.SetOne and then https://pkg.go.dev/github.com/consensys/gnark-crypto@v0.16.0/ecc/bls12-377/internal/fptower#E12.Equal for checking if the pairing check succeeded.

Pinging @yelhousni to loop in.

Indeed PairingCheck computes the final exp only once and shares the squares of all the Miller loops à la 'FE((f_1 * ... *f_n)^2).