Required context to read this: FFMul RFC Given witnesses $a$, $b$, $q$, $r$ each represented as 3 limbs $(x_0, x_1, x_2)$ by $$x = x_0 + 2^\ell x_1 + 2^{2\ell} x_2,$$ we want to prove that, assuming a certain list of constraints, \begin{equation} a b = q f + r \qquad (1)

See soundness proof and existing FFmul RFC for relevant, but not required context. Recap: The original design could not be made sound because we are quite sure that individual range checks on all limbs $q_0$, $q_1$, $q_2$ are necessary, and the original design already uses all 7 x 2 = 14 permutable cells in the two rows available to the gate. Original design: //~ | col | `ForeignFieldMul` | `Zero` | //~ | --- | ---------------------------- | ------------------------- | //~ | 0 | `left_input0` (copy) | `remainder0` (copy) | //~ | 1 | `left_input1` (copy) | `remainder1` (copy) |

Pickles is Mina's library for creating recursive snark proofs. It's working well, but it's lacking documentation and a spec. While I'm at ETHAmsterdam, I'll try to understand the inner workings of Pickles share my findings and hopefully produce some useful resources for others start a JS implementation of Pickles, on top of snarkyjs The starting point is here - the OCaml entry point of Pickles' main function, Pickles.compile.