Let and be the two fields, with , for Elliptic curves and . Assume . We have a proof system (Kimchi) over and , where commitments to public inputs are:
Respectively. See Pasta Curves for more details.
When referring to the -side we mean the proof system for circuit over the field .
In pickles-rs we have the notion of “passing” a variable (including the transcript) from one side to the other. e.g. when a field element needs to be used as a scalar on .
This document explains what goes on “under the hood”. Let us start by understanding why:
Let be a scalar which we want to use to do both:
- Field arithmetic in
- Scalar operations on
In order to do so efficiently, we need to split these operations across two circuits (and therefore proofs) because:
- Emulating arithmetic in is very expensive, e.g. computing requires multiplications over : 100’s of gates for a single multiplication.
- Since we cannot compute over efficiently, because, like before, emulating arithmetic in is very expensive…
The solution is to “pass” a value between the two proofs, in other words to have two values and which are equal as integers i.e. : they represent “the same number”. A naive first attempt would be to simply add to the witness on the -side, however this has two problems:
Insufficient Field Size: hence cannot fit in .
No Binding: More concerning, there is no binding between the in the -witness and the in the -witness: a malicious prover could choose completely unreleated values. This violates soundness of the overall -relation being proved.
The solution to the first problem is simple:
In the -side decompose with (high bits) and (low bit). Note since ; always the case for any cycle of curves, is only smaller than , by Hasse. Now “” is “represented” by the two values .
Note that no decomposition is nessary if the “original value” was in , since is big enough to hold the lift of any element in .
To solve the binding issue we will add to the public inputs on the -side, for simplicity we will describe the case where are the only public inputs in the -side, which means that the commitment to the public inputs on the side is:
At this point it is important to note that is defined over !
Which means that we can compute efficiently on the -side!
Therefore to enforce the binding, we:
- Add a sub-circuit which checks:
- Add to the public input on the -side.
At this point the statement of the proof in -side is: the -proof is sound, condition on providing an opening of that satisifies the -relation.
At this point you can stop and verify the proof (in the case of a “step proof” you would), by recomputing outside the circuit while checking the -relation manually “in the clear”.
However, when recursing (e.g. wrapping in a “wrap proof”) we need to “ingest” this public input ; after all, to avoid blowup in the proof size everything (proofs/accumulators/public inputs etc.) must eventually become part of the witness and every computation covered by a circuit…
To this end, the wrap proof is a proof for the -relation with the public input which additionally verifies the -proof.
The next “step” proof then verifies this wrap proof which means that then becomes part of the witness!
We can arbitrarily choose which side should compute the public input of the other, in pickles we let “wrap” compute the commitment to the public input.
Enforces that the public input of the proof verified on the Fr side is equal to the Fp input computed on Fr side.