Specify Groth16 adapted to RelaxedR1CS and fork arkworks Groth16 adapting it into that design

[arnaucube]

@levs57 has suggested modifying Groth16 to adapt it to RelaxedR1CS, which not only would have less overhead than the current approach, but also seems to have benefits regarding the commitment openings of cm(E), cm(W).

Not for the milestone https://github.com/privacy-scaling-explorations/folding-schemes/milestone/1 , but for those usecases where Decider's proving time is crucial, @levs57's approach will perform much better than the in-circuit RelaxedR1CS checker approach (but the latter is more modular in terms of being able to use any R1CS-based proving scheme for the Decider without needing to adapt each one, but has the ~3x overhead).

The idea of this issue is to track progress on the specification of Groth16 adapted to RelaxedR1CS and it's implementation, which probably would be a fork of arkworks Groth16 repo, which @levs57 already sketched. Once ready, we would need to fork arkworks Groth16 implementation to addapt it to @levs57's design.

[pnyda]

@levs57 Could you post somewhere the sketch of how we can modify Groth16 to support a relaxed R1CS? There was a discussion going on at PSE ZK Summer Program on how Nova on Groth16 would look like. I'm really curious!

[levs57]

Hi!! The solution is the following. Given claimed relaxed instance [w], [E] that allegedly satisfies Aw * Bw - u Cw = E, we rescale commitments as follows: [w'] = u^(-1) [w], [E'] = u^(-2) E. // here, I do treat u as external value not included in [w], and all other public inputs should be treated as if they are part of [w], hope it is clear. Then, substituting this into the equation, we get Aw' * Bw' - Cw' = E' This is a non-relaxed R1CS on the vector w'|E', with new matrices A, B, C having the following block forms: A B C 0 0 Id Best wishes, Lev.