Considerations when implementing zk proofs of crystals-dilithium signatures.

We’ll consider only the simplified scheme as described above. Discussion should be applicable to the full scheme.

Proving signature

With crystals-dilithium we must contend with a variable length signing procedure. Specifically we have to rejection sample based on the value of $y$, and generate a ball polynomial $c$ based on a hash. Both of these operations are non-deterministic. e.g. it’s expected that they must be retried (specifically the authors target 4-7 iterations).

Inside a zk circuit we can avoid variable length execution by doing the rejection sampling at witness generation time and providing a suitable $y$ as an input. The circuit does not need to range check the $z$ value inside the proof. Outputting a value outside the range leaks the secret key, so it’s important that the witness calculation function operates correctly. In fact, we don’t need to constrain the calculation of the $c$ value either.

The verification procedure is robust and allows us to constrain relatively little of the signing procedure. Specifically we can take $c$, $y$, and $s_1$ as inputs directly.

We must constrain only the following:

• $z=y+c{s}_1$ ($\ell$ polynomial additions and $\ell$ polynomial multiplications) ($\ell \approx 5$)

unconstrained $w_1$ and $c$ calculation

The verifier calculates $Az-ct$. We can substitute $z$ and $t$ in this equation to get

$A(y+c{s}_1)-c(A{s}_1+s_2)=Ay+Ac{s}_1-Ac{s}_1-c{s}_2$

The middle terms cancel leaving $Ay-c{s}_2$

$c$ and $s_2$ are both of small norm and are filtered out by decomposing into the high bits of the coefficients yielding ${w^{\prime }}_1$. Because the verifier calculates the ${w^{\prime }}_1$ value, it’s able to ensure that $c$ was hashed appropriately even without explicit constraints in the zk circuit.

misc notes

Polynomials are in a ring with modulus $X^{256}+1$ with coefficients in a field with scalar modulus $\approx 2^{23}$.

Depending on the architecture of the execution system we can do lazy reduction for the scalar operations. This is a compiler level optimization that is particularly relevant in systems with large native types (e.g. $\approx 2^{256}$) that can’t efficiently support montgomery/crt representation.