5 A rigorous treatment of knowledge soundness

Theorem 3.5 extracts from a tree of accepting transcripts with three children at every node and one level per round: $3^k$ leaves for $k={\log }_{2}d$ rounds, that is $d^{{\log }_{2}3}$ with ${\log }_{2}3=1.58496\mathrm{\dots }$, polynomial in $d$ though more than a binary tree would cost. At the deployed $d=2^{11}=2048$ the tree has $3^{11}=177147$ leaves against the $2^{11}=2048$ a binary tree would have; the extractor runs in expected polynomial time, the rewinding that assembles the tree being the Crypto Guide’s (§“Sigma-protocols”, the tree-extraction theorem cited there). Its knowledge error is the $O(\log d/|𝔽|)$ of Theorem 3.5, one $O(1/|𝔽|)$ term per round for the challenges the siblings must avoid. The scale of these terms is worth fixing once: the proof system’s own allowances are linear in $n=d$, the $18431/|𝔽|\approx 2^{-239.8}$ of the identity check (§2.4), whose difference polynomial $C-h{Z}_H$ has degree at most $d_{\max }n-1=18431$ at the deployed $d_{\max }=9$ ($\mathrm{deg}C\le d_{\max }(n-1)$ by the proof of Theorem 4.7, and the $d_{\max }-1$ committed chunks of the quotient have degree each, §4.5); the order-$n/|𝔽|$ term of the multipoint reduction (Lemma 4.5); and $d/|𝔽|=2^{11}/2^{254}=2^{-243}$ is that linear allowance for the opening. The opening’s proved error sits below it, and quoting the linear figure for the opening loses nothing in a system whose other terms are already linear in $d$, as the proof of Theorem 3.5 noted. Every one of these is a Schwartz–Zippel term, not a security level, in the sense fixed in §1.2.

The compiled argument of §4.7 was assembled in two layers, an information-theoretic polynomial IOP and a cryptographic commitment scheme, and its extractor is assembled in the same two layers, run backwards (Figure 15).

The lower layer recovers polynomials. The prover has sent commitments $C_{\nu }$ and, in phases 6 and 7, one opening of the combined $F^{\ast }=F+{\sum }_i[x_4^i]Q_i$ with $Q_i={\sum }_e[x_1^e]C_{{\nu }_{i,e}}$ (Construction 4.4). Phase 7 runs the deployed opening of §3.8, and the extractor of Corollary 3.13, the tree extraction of Theorem 3.5 with two further levels, $\xi$ and $\zeta$, the latter in the root role of the resampled $U$, returns the coefficient vector behind $F^{\ast }$, a representation of $F^{\ast }$ over $(𝐆,H)$, or a nontrivial discrete-logarithm relation among $𝐆$, $H$ and $U$. To reach the individual commitments the extractor rewinds over the combining challenges as well: the vectors behind $F^{\ast }$ for $m+1$ distinct values of $x_4$ are $m+1$ linear equations in the $m+1$ unknown vectors behind $F,Q_1,\mathrm{\dots },Q_m$, whose coefficient matrix has the rows $(1,x_4,\mathrm{\dots },x_4^m)$ and is invertible because a nonzero polynomial of degree at most $m$ has at most $m$ roots (Math Guide, §“Roots and the factor theorem”), the argument of the proof of Lemma 3.4; the vectors behind $Q_i$ for $|I_i|$ distinct values of $x_1$ likewise yield the vectors behind each $C_{\nu }$ in group $i$. One $C_{\nu }$ is the collapsed quotient ${\sum }_i[x^{ni}]\mathrm{𝖢𝗈𝗆𝗆𝗂𝗍}(h_i)$ of §4.5; its vectors for $d_{\max }-1$ values of $x$ with pairwise distinct $x^n$ yield the vectors behind the chunks $h_i$, by the same argument with $x^n$ in place of $x_4$. The output is one polynomial of degree per commitment the prover sent, and two different vectors extracted for one commitment would be a nontrivial discrete-logarithm relation among $𝐆$ and $H$, exactly as at the root of Theorem 3.5. This layer is the only place the discrete logarithm on Vesta enters, and it enters in only one way: the extractor either recovers the polynomials or exhibits a relation.

The upper layer recovers the witness. With the polynomials in hand, the prover’s claimed evaluations are the true evaluations of fixed polynomials except with the Schwartz–Zippel allowance of Lemma 4.5, since a claimed value that differs from the extracted polynomial’s value survives the reduction only with that probability; and “the true evaluations of fixed polynomials” is precisely the hypothesis under which §2 proved its theorems. Theorem 2.5 turns the accepted identity $C(x)=h(x)Z_H(x)$ into divisibility of $C$, Lemma 4.6 splits it into the vanishing of every constraint polynomial on the rows, Theorem 2.11 with Corollary 2.12 turns the running products into the wiring, and Theorem 2.15 with Proposition 2.16 turns the lookup identities into table membership, each with its stated term over $|𝔽|$; Theorem 2.2 reads gate satisfaction off divisibility. The witness is then read off directly: the advice columns are the values of the extracted advice polynomials on the rows. Nothing in this layer uses an assumption; the IOP’s extractor outputs the oracles, which the layer below supplies. The consequence runs both ways. A break of the discrete logarithm on Vesta breaks the lower layer and nothing else, in the way §3.5 described, one commitment opening to any vector; and no assumption can rescue an identity that the upper layer does not actually enforce, because the upper layer’s errors are counting statements about polynomials.

What is proved and what is described. In the interactive setting the composed extractor is a tree extractor in the sense of the Crypto Guide with a wider tree: three children at each of the $k$ inner-product levels, two at the $\zeta$ level and two at the $\xi$ level, $m+1$ at the $x_4$ level, ${\max }_i|I_i|$ at the $x_1$ level, one $x_1$ serving every group, and, at the $x$ level, $(d_{\max }-2)n+1=14337$ children: each value of $x^n$ has at most $n$ preimages, so only that many distinct challenges guarantee the $d_{\max }-1$ pairwise distinct $x^n$ the quotient step needs, as Theorem 3.5 took five children for three distinct squares. The two $\zeta$ children must moreover be nonzero, as in Corollary 3.13. Each polynomial the upper layer consumes is fixed by a binding commitment sent before every challenge that tests it: the advice before $\theta$, the permuted lookup columns $A^{\prime }$ and $S^{\prime }$ before $\beta$ and $\gamma$, the running products and the random polynomial before $y$, the quotient chunks before $x$ (§4.5); the polynomial behind $F$ and the mask behind $S$, committed after $x$, serve only inside the lower layer; and all of the consumed ones precede $x$, the first challenge at which the tree branches, so the upper layer’s Schwartz–Zippel arguments apply on every branch without further rewinding. The inner-product part of that tree is Corollary 3.13, proved; the theorems of the upper layer are proved in §2; the accounting that joins them into one tree-extraction statement with one knowledge error is the compilation principle of Remark 4.11, whose hypotheses this volume names and does not discharge. In particular the compiled error is not asserted to be the sum of the layers’ errors.

Everything above is interactive: the extractor chose the challenges it fed the prover. In the deployed argument the challenges are hashes, and the extractor of the Crypto Guide’s Fiat–Shamir theorem obtains its second transcript by forking: it finds, among the prover’s at most $Q$ hash queries, the critical one whose answer became the challenge, rewinds to it, and answers it afresh, succeeding with probability about $\epsilon (\epsilon /Q-1/|𝔽|)$, so that the extractor’s success is the prover’s squared and divided by $Q$ (§“The Fiat–Shamir transform: from interactive to non-interactive”, the knowledge-soundness clause of its theorem). That theorem covers one challenge. The tree of Theorem 3.5 needs three siblings at each of $k$ levels, and a sibling at level $j$ must share the transcript prefix through level $j-1$, which in the hashed setting means agreeing with the prover’s prefix and its earlier hash answers: in a transcript hash, changing one message redraws all later challenges, so siblings at round $j$ can be found only among the prover’s own queries. Let $\mu$ be the number of verifier challenges of the protocol being lifted. The simplest lifting guesses, among the at most $Q$ queries, the $\mu$ that answered them, and runs the interactive extractor against the interactive prover that the guess defines; the guess is right with probability at least $Q^{-\mu }$, so the knowledge error is multiplied by $Q^{\mu }$. Attema, Fehr and Klooß (Fiat–Shamir Transformation of Multi-Round Interactive Proofs) record this $Q^{\mu }$ as the loss for a general $(2\mu +1)$-move protocol; nesting the one-round forking level by level fares worse, since each level squares the success probability before dividing by $Q$. For the opening alone $\mu$ exceeds $k={\log }_{2}d$, the choice of $U$ (in the deployed opening, $\xi$ and $\zeta$) being a challenge too, and $\mu$ grows once the proof system’s own challenges are counted. The loss belongs to this analysis. For $(k_1,\mathrm{\dots },k_{\mu })$-special-sound protocols (Crypto Guide, §“Sigma-protocols”, the definition of tree special soundness) the same authors prove, in the random oracle model and with no idealisation of the group, a knowledge error that grows only linearly in $Q$. The rounds of the opening’s extraction tree have that shape, but its root step, which rewinds the choice of $U$ (in the deployed opening, $\xi$ and $\zeta$), and its alternative output, a discrete-logarithm relation, are not checked here against that theorem’s hypotheses, and this volume does not assess that route.

With the deployed $k={\log }_{2}d=11$, so $\mu >11$ for the opening alone, and a query budget of $Q=2^{80}$ hash evaluations, the factor $Q^{\mu }$ exceeds $Q^{11}=2^{880}$; multiplied by the linear allowance $d/|𝔽|=2^{-243}$ it exceeds $2^{637}$, a bound above $1$, which is no bound at all. Nor does the proved $O(\log d/|𝔽|)$ help: the challenge space is a $255$-bit field with fewer than $2^{255}$ elements, so $2^{880}$ exceeds $|𝔽|$ itself, and a factor larger than $|𝔽|$ turns every term of the form $c/|𝔽|$ with $c\ge 1$ into a number above $1$. Asymptotically the loss falls elsewhere. With $Q$ and $d$ polynomial in the security parameter $\lambda$ (Crypto Guide, §“Adversaries and the security parameter”) and $|𝔽|=2^{\mathrm{\Theta }(\lambda )}$, the factor $Q^{\mu }=2^{O({\log }^2\lambda )}$ is super-polynomial and sub-exponential in the Math Guide’s classification (§“Polynomial, exponential, and negligible functions”). The Schwartz–Zippel terms survive it: $Q^{\mu }O(\log d)/|𝔽|=2^{O({\log }^2\lambda )-\mathrm{\Theta }(\lambda )}$ is negligible. The reduction does not survive it: the guessing extractor succeeds only with probability reduced by $Q^{\mu }$, or runs $Q^{\mu }$ times longer to compensate, and so is not $\mathrm{𝖯𝖯𝖳}$, and the prover’s success is then bounded only by $Q^{\mu }$ times the discrete-logarithm advantage, which need not be negligible when that advantage is merely negligible. The interactive extractor is polynomial, $d^{{\log }_{2}3}$ transcripts in expected polynomial time; the looseness arises in the naive analysis of the passage to the non-interactive argument.

Remark 4.11 named the two notions built to avoid this: round-by-round knowledge soundness, which labels partial transcripts as doomed and bounds the probability that one verifier challenge lifts the doom, and state-restoration soundness, which lets the prover restore an earlier verifier state and redraw its challenge, precisely the freedom a prover attacking a transcript hash has. Each exists to obtain a bound on the compiled argument that loses a factor linear in $Q$ rather than $Q^{\mu }$; no equivalence between them is asserted here, as none was there. Claiming a single factor $Q$ for a compiled protocol nevertheless requires the precise theorem’s state-restoration, transcript, challenge and extraction hypotheses to hold of that protocol, and this volume does not assert a factor-$Q$ bound for Halo 2’s compiled protocol. The next subsection names the model in which the halo2 book proves such a bound, in the state-restoration form, for its abstract interactive protocol, what that analysis assumes, and why its instantiation to the deployed transcript remains unwritten.

The algebraic group model sits between the standard model, in which the adversary is any $\mathrm{𝖯𝖯𝖳}$ algorithm and every primitive is concrete code it may inspect (Crypto Guide, §“The standard model and the random oracle model”), and the generic group model, in which the adversary may perform group operations only through an oracle on opaque handles and never exploits the representation of an element (the same section, the remark on the generic and algebraic group models). An algebraic adversary is less restricted than a generic one, since it may compute on the bit representation of group elements however it likes; it must only be able to explain each element it outputs as a combination of elements it has seen. The model is an idealisation (the same remark): a proof in it says nothing about an adversary that outputs a group element it cannot explain. Figure 16 draws the three models as nested restrictions on the adversary and places this section’s analyses on them; the random oracle model, which idealises the hash rather than the group, is an independent axis, and an analysis may combine either group model with it.

In this model the prover outputs every group element with its representation, and the extractor reads the witness off the representations of a single accepting transcript instead of assembling it from rewound ones; no rewinding occurs, and the price is the assumption that the prover is algebraic. For the deployed opening, equation (29), the halo2 book’s Protocol Description chapter carries this out (“Witness-extended Emulation”, the definition of the bad-challenge sets): comparing the two sides of the accepting equation coordinate by coordinate either exhibits a nontrivial discrete-logarithm relation among the generators or, unless some challenge falls in a set of bad challenges fixed by the messages before it, forces the representation of $P$ to open to the claimed value. The analysed protocol draws every challenge from one space $𝒞$ of field elements, none zero or a row, and each round challenge $u_j$ further so that its factor $1+u_j{x}_3^{2^{j-1}}$ of $g_{\mathrm{dep}}(x_3)$ in (26) is nonzero. Each round challenge $u_j$ has at most $4n$ bad values in $𝒞$, and $\zeta$ and $\xi$ have one each; the book bounds the bad sets of the proof system’s other challenges, $x_1,\mathrm{\dots },x_4$, $x$ and those of the committed rounds, by the degrees of the identities they test, the largest being $n_g(n-1)$, the bound on the constraint polynomial’s degree in each indeterminate, provided $n_g(n-1)\ge 4n$, as at the deployed $n_g=9$, where $18423>4n=8192$; the book admits $n_g\ge 4$, for which this can fail.

Ghoshal and Tessaro (Tight State-Restoration Soundness in the Algebraic Group Model) carry this analysis out for Bulletproofs-style inner-product arguments: they prove tight state-restoration soundness in the algebraic group model and derive Fiat–Shamir security bounds from it under their stated hypotheses, the transfer from the state-restoration game to the compiled argument being their theorem. The deployed analysis follows them. The protocol specification defines the proving system by reference to the halo2 book (protocol specification, § 5.4.10.3, “Halo 2”), and the book’s Protocol Description chapter fixes the framework: it adopts state-restoration soundness because the concrete protocol is realised through the Fiat–Shamir transformation and a cheating prover can fork the transcript at will, and it invokes Ghoshal and Tessaro’s theorem for the passage from that game to soundness of the compiled argument. Its abstract interactive protocol is stated for a relation of the form “a fixed multivariate constraint polynomial in the column polynomials and the challenges vanishes on the rows”, with the column polynomials as the witness, over public parameters of $n+2$ group elements, $𝐆$, $U$ and the blinding generator $H$ (written $W$ there).

The theorem is quoted as an interface and not proved in this volume: it is the halo2 book’s (Protocol Description, “Witness-extended Emulation”), proved there by instantiating Theorem 1 of Ghoshal and Tessaro with the bad-challenge sets described above. Its extractor works online, from the representations of a single transcript, and never rewinds. At the deployed $n_g=d_{\max }=9$ and $n=2^{11}$, ${\epsilon }_{\mathrm{bad}}\le 18423/|𝒞|\approx 2^{-239.8}$, and $Q{\epsilon }_{\mathrm{bad}}\approx 2^{-159.8}$ at $Q=2^{80}$ queries.

Applying those bounds to the deployed Halo 2 transcript requires matching the precise folding, masking, challenge distribution and composition assumptions of the analysed protocol to the deployed one, and this volume does not prove that instantiation theorem. Four mismatches are visible from the earlier sections. The book’s abstract relation sees the permutation and lookup arguments of §2 only through the constraint polynomial and its committed columns; the Orchard circuit’s actual gates and table columns (§4.1) and its chunked running products (“The deployed chunking” in §2.6) instantiate that abstraction and must be checked against its degree hypotheses. The book’s challenges exclude zero, the rows and, for each $u_j$, the value that zeroes its factor of $g_{\mathrm{dep}}(x_3)$, while the deployed transcript squeezes full field elements with no rejection (§3.8), so the deployed challenge distribution differs from the analysed one by the excluded events. The analysed folding is the deployed normalisation of Remark 3.9, and the masking is the deployed mask of §3.8, so those two match; the hash, however, is BLAKE2b (§4.3), and the transfer theorem’s random oracle must be instantiated by it. And the book’s theorem is for the interactive argument against a state-restoration prover, the compiled bound following by the transfer theorem under its hypotheses. In the classification of §1.2, the status of the transfer is designed-but-unspecified: the bounds exist for the analysed protocol and the design intends them for the deployed one, but the theorem that carries them across is not written, here or in the specification.

The naive Fiat–Shamir knowledge-soundness analysis of the opening loses the factor $Q^{\mu }>Q^{\log d}$ of §5.1, exponential in the round count $\log d$ with base the query count $Q$: above $2^{880}$ at the deployed size for a $2^{80}$-query prover, against a challenge space of fewer than $2^{255}$ elements. The interactive extraction itself is polynomial, $d^{{\log }_{2}3}=177147$ transcripts at $d=2048$ in expected polynomial time, with the proved knowledge error $O(\log d/|𝔽|)$ of Theorem 3.5. The gap lies in the naive analysis of the lifting, and the notions of §5.1 and the model of §5.2 exist to close it.

Each analysis cited in this section that avoids the naive loss relies on an idealisation: the halo2 book’s extraction theorem (Theorem 5.3) on the algebraic group model, and its passage to the compiled argument on the random oracle model as well; the special-soundness analysis of Attema, Fehr and Klooß on the random oracle model alone. No standard-model tight bound is claimed for the deployment, by this volume or by the analyses it cites; this is a statement about the design’s analyses, not a specification claim, and the specification makes none. Read against the bit-security budget, the consequence is concrete. The discrete-logarithm layer offers about $2^{126}$ operations of classical security (§3.5; Crypto Guide, §“Standing assumptions”); a reduction tight in $Q$ lets the argument inherit that strength, less the algebraic term $Q{\epsilon }_{\mathrm{bad}}$ of Theorem 5.3, about $2^{-159.8}$ at $2^{80}$ queries, which is not the bottleneck; a reduction losing $2^{880}$ lets it inherit nothing. For the analysed protocol the number is therefore the assumption’s, in the algebraic group and random oracle models; for the deployed argument it is so only through the instantiation that §5.2 classifies designed-but-unspecified.

Proved without idealisation of the adversary or of the transcript hash are the interactive statement, Theorem 3.5, for uniform generators (the deployed hashed generators add its hypothesis that hash-to-curve is a random oracle), and the information-theoretic layer of §2; described, with the hypotheses named, are the layered extraction that joins them and the naive lifting’s loss; cited, with its instantiation to the deployed transcript classified designed-but-unspecified, is the halo2 book’s bound in the algebraic group model.