Stellar Soroban UltraHonk verifier #8560
Replies: 2 comments 4 replies
-
Hi @qpzm, I'm Jay from the core team at Stellar. Thanks for the proposal and detailed methodology description.
Happy to answer any questions! |
Beta Was this translation helpful? Give feedback.
-
@Savio-Sou There is a question reviewing the barrentenberg code. In |
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
-
Summary
We aims to bring Aztec's UltraHonk verifier to the Stellar ecosystem by:
We implemented a POC with basic elliptic curve operations using arkworks.
https://github.com/ModoriLabs/soroban-ultrahonk-verifier
Motivation
We considered building Honk with BLS12-381, but Honk requires a cycle of curves: BN254 and Grumpkin.
https://github.com/AztecProtocol/barretenberg/blob/master/cpp/src/barretenberg/stdlib/honk_verifier/ultra_recursive_verifier.cpp#L63
BLS12-381 does not have a well-known cycle of curves, so we have decided to implement non-native BN254 and pairing operations to test the UltraHonk prover on Soroban's local network.
Our strategy has two phases:
Methodology
1. Theoretical research
UltraHonk is a combination of sumcheck and shplemini, and shplemini consists of Gemini and Shplonk.
SHPLONK is a more effective Plonk where k constraints at multiple points can be verified with just 2 pairings. It uses a variant of KZG commitment. This is unoptimized check of SHPLONK. I will explain the optimized process below.
Example of SHPLONK Section 4 ("Reducing Verifier Operations at the Expense of Proof Length")
Let's walk through a concrete example using the Section 4 scheme from the SHPLONK paper. This scheme reduces verifier operations (pairings) to only 2 pairings by adding an extra (G_1) element to the proof.
Problem Setup
Polynomials:
Evaluation points:
Prover's Steps
1. Commit
Let$\tau = 9$ . $cm_1= [82]_1, cm_2 = [21]_1$ .
2. Open
(a) Verifier sends random challenge$\gamma \in \mathbb{F}_p$
Let$\gamma = 3$
(b) Prover computes the combined polynomial
Let the evaluation set:
The Lagrange denominators:
The combined polynomial:
Substituting$\gamma = 3$ ,
Compute:
(c) Sample a random evaluation point$z \in \mathbb{F}_p$
Let$z = 4$ $W = [h(x)]_1 = [15]_1$
Prover sends
(d) Prover computes the quotient polynomial
In our example,$L(X) = −3X^2 −9X + 84$ .
Prover sends:
Verify (only 2 pairings)
Verifier computes:
Verifier checks the pairing equation:
This is an optimization of this equation to fix the trusted setup of$\mathbb{F}_2$ .
In our example, the left hand side is the equation of these three: (1) - (2) - (3).
The sum over commitments:$\sum_{i=1}^{2} \gamma^{i-1} Z_{T \setminus S_i}(z) \cdot \text{cm}_i$
In our example, the calculation goes as below:
The sum over claimed evaluations:
The right hand side is
Because$\tau$ = 9, it is $e([-240]_1, [1]_2)$ equal to the left hand side.
https://eprint.iacr.org/2020/081.pdf
https://hackmd.io/@walpo/shplonk
Gemini is a zero-knowledge proof system that is:
Especially, UltraHonk uses the method to convert a multivariate PCS to a univariate PCS. This is useful when we can random linearly combine the KZG proof with other KZG proofs.
Let$f: {0,1}^n \rightarrow \mathbb{F}$ be a multilinear polynomial over n variables.$\mathcal{U}_n$ sends f to a univariate polynomial $\hat f(X) \in \mathbb{F}[X]$ of degree < $2^n$ , defined as:
The univariatization map
where:
Here is an example.
Suppose
I want to prove that$g(\rho) = 1 \cdot (1-5) \cdot (1-6) + 2 \cdot 5 \cdot (1-6) + 3 \cdot (1-5) \cdot 6 + 4 \cdot 5 \cdot 6 = 20 - 50 - 72 + 120 = 18$ $f(x) := \mathcal{U}_n(g)(x) = 1 + 2x + 3x^2 + 4x^3$
Let
Through 2 foldings with$\rho_0, \rho_1$ ,
$f^{(i)}(x^2) = (1- \rho_{i-1})f_{even}(x) + \rho_{i-1} \cdot f_{odd}(x) = (1- \rho_{i-1})\frac{f^{(i-1)}(x) - f^{(i-1)}(-x)}{2} + \rho_{i-1} \cdot \frac{f^{(i-1)}(x) - f^{(i-1)}(x)}{2x}$
This matches with the$g(\rho)$ .
https://eprint.iacr.org/2022/420
https://github.com/arkworks-rs/gemini
2. Code review
Before adopting the codebase, we review each repo to ensure it has implemented the paper correctly.
Let's grasp the prover logic to make a safe verifier. In this explanation, I will skip zero-knowledgeness.
gemini_prove
transforms the multilinear function evaluation check to a batch evaluation check of univariate functions.shplonk_prove
proves it withk+1
pairings. In our code, k = 1.https://github.com/TaceoLabs/co-snarks/blob/main/co-noir/ultrahonk/src/decider/shplemini/prover.rs#L419
Sumcheck
Notation
GS(x)
: gate separators for an input x.R_j
: the j-th relation polyanoimalPurpose
Relation separator$\alpha$
$\alpha$ prevents relation R_1 errors from cancelling R_2 errors.
Gate separators$u_i$ .$1 + u_i * (\beta_i - 1) = (1 - u_i) + u_i * \beta_i$ .$\prod_\limits{i={0\ldots d-1}} (1-u_i) + u_i \cdot \beta_i$ as its
In round i, let the round challenge of sum-check
The code is
F::ONE + (round_challenge * (self.betas[self.current_element_idx] - F::ONE))
equal toEvery input gate has
gate_separator
.Example
Every input gate has a different$GS(x)$ prevents input (0,0) errors from cancelling input (0,1) errors.
gate_separator
.gemini_prove
compute_fold_polynomials
performs polynomial folding to create multiple fold polynomialsfold(A_l)[j] = (1-u_l) * even(A_l)[j] + u_l * odd(A_l)[j]
construct_univariate_opening_claims
evaluates polynomials at specific challenge points:shplonk_prove
compute_gemini_fold_pos_evaluations
.u
from the sumcheck.l = CONST_PROOF_SIZE_LOG_N to 1
, calculate3-1. Implement UltraHonk verifier: Sumcheck and shplemini
There are many implementations of UltraHonk. Follow this with no_std.
verifySumcheck
proof.sumcheckUnivariates[round][0]
is the value evaluated at x=0.proof.sumcheckUnivariates[round][1]
is the value evaluated at x=1.roundTarget == proof.sumcheckUnivariates[round][0] + proof.sumcheckUnivariates[round][1]
.roundTarget
must be equal tograndHonkRelationSum
which a verifier can calculate.u_i
is a sumcheck challenge.B_j
is a gate challenge.alpha
is a random value to random-linearly combine the constraints of the gates.R_i
is a gate constraint.Reference: https://github.com/AztecProtocol/barretenberg/blob/master/sol/src/honk/BaseHonkVerifier.sol#L124
function computeNextTargetSum
Say the round univariate as p(x).
$w_j = \frac{1}{\displaystyle\prod_{k \ne j} (x_j - x_k)}, \quad j = 0, \ldots, n$ $w_j$ .
We set the evaluation domain as {0,1,2,3,4,5,6,7}.
Therefore, it is pre-calculated as [-5040, 720, -240, 144, -144, 240, -720, 5040].
This is the inverse of
For example
w_0 = 1/(0-1)(0-2)...(0-7) = -1/5040
.We put
x = round_challenge
in the p(x) below to calculate the target sum.This function returns$B(x) = \displaystyle\sum_{j=0}^{n} \frac{w_j}{x - x_j}$ .
p(roundChallenge) * B(roundChallenge)
whereIt is a modified Barycentric intepolation to avoid division.
3-2. Implement UltraHonk verifier: Custom gates
UltraHonk consists of the following custom gates:
This is a part of our ongoing review of custom gates.
AllEntities
witness
is the current row entities.shifted_witness
is the next row entities.https://github.com/TaceoLabs/co-snarks/blob/main/co-noir/ultrahonk/src/types.rs#L45-L49
There are precomputed columns which depend only on the circuit structure, not on the inputs.
id_i
: uniquely identifies each "location" in the constraint system.sigma_i
: for copy constraintslagrange_first
: A polynomial that equals 1 at the first row and 0 elsewhere.lagrange_last
: A polynomial that equals 1 at the last row and 0 elsewhere.q_m, q_l, q_r, q_o, q_c
: coefficients for the arithmetic gatesq_lookup
: a selector for lookup gates.table_i
: precomputed lookup tablesarithmetic constraints
$w_{1\omega},w_{4\omega}$ mean the next row entities. It is shifted_witness in co-snarks implementation.
$$q_{arith} \cdot \left( \left( \frac{-1}{2} \cdot (q_{arith} - 3) \cdot q_m \cdot w_1 \cdot w_2 + q_1 \cdot w_1 + q_2 \cdot w_2 + q_3 \cdot w_3 + q_4 \cdot w_4 + q_c \right) + (q_{arith} - 1) \cdot \left( \alpha \cdot (q_{arith} - 2) \cdot (w_1 + w_4 - w_{1\omega} + q_m) + w_{4\omega} \right) \right) = 0$$
q_arith = 0
: Entire gate is disabled.We can split the two halves.
The first half
q_arith = 1
:q_arith = 2
: The multiplication term is scaled by -1/2.q_arith = 3
: The multiplication term is completely disabled.q_arith > 3
: The Multiplication term is scaled by $-1/2 \cdot (q_{arith} - 3)$.The second half
https://github.com/TaceoLabs/co-snarks/blob/main/co-noir/ultrahonk/src/decider/relations/ultra_arithmetic_relation.rs
permutation relations
Our barycentric interpolation does not use FFT, so the domain for interpolation is
[0..domain_size]
. It means the next row is accessible byz_perm(X+1)
in the constraints.delta range relations
This gate checks the difference between two wires are in
[0,1,2,3]
.We will continue reviewing other constraint gates.
4. Implement BN254 with no_std (Optional)
Integrate BN254 as a host-native functions in rs-soroban-sdk using the arkworks bn254 implementation. This is a brief overview of the necessary functions.
BN curve is an elliptic curve of the form$y^2 = x^3 + b$ over $F_p$ where
Elliptic curve operations
Finite field operations
Subgroup check$Z_r × Z_r$ , so there are (r+1) subgroups of size r. Among them, we choose:
If p does not divide r, then E[r] has the structure of
G_1 subgroup check
G_2 subgroup check is to confirm$P \in E(F_p^k)$ is in the r-torsion group, so $r[P] = O$ . Instead of calculating $r[P]$ , we will check $\psi(P) = [6x^2]P$ .
Proof of the equivalence.
Suppose$[r]P = O$ .
r = p - t + 1
, soSuppose$\psi(P) = [t-1]P$ holds.
Pairing
The optimal Ate pairing e: G_1 × G_2 → G_T over the BN254 curve
Soroban
u128
andu64
in Stellar.#![no_std]
. The size of Rust standard library is too big to put in a contract.Timelines and Deliverables
bb prove
, and verifyTeam
ModoriLabs has developed semaphore.nr and integrated noir circuits in Pluto’s Web prover based on Supernova folding scheme. qpzm and teddav are also zk auditors in Electisec.
Start Date
June 2025
Reference
Beta Was this translation helpful? Give feedback.
All reactions