EIP-0045: Native STARK Proof Verification Opcode

eip-0045-cryptographic-rationale.md

@@ -0,0 +1,235 @@
+# EIP-0045: Cryptographic Rationale & Formal Security Analysis
+
+**Status:** Draft  
+**Authors:** A. Shannon  
+**EIP:** [ergoplatform/eips#103](https://github.com/ergoplatform/eips/pull/103)  
+**Implementation:** [sigmastate-interpreter#1116](https://github.com/ergoplatform/sigmastate-interpreter/pull/1116)  
+
+---
+
+## Abstract
+
+This document provides the formal cryptographic backing for EIP-0045, a native STARK verification opcode (`VerifyStark`) for the Ergo eUTXO protocol. We establish three results:
+
+1. **Physical necessity** — ErgoScript's JIT interpreter cannot execute STARK verification within the per-block computational budget, making a native JVM opcode the only viable path for on-chain zero-knowledge proof verification.
+2. **Protocol specification** — We define the algebraic tower (BabyBear Ext16), the DEEP-FRI verification scheme, and the concrete cryptographic instantiation (Poseidon1, Blake2b-256, Q=35, B=2048).
+3. **Formal soundness** — We prove the verifier is sound against both classical PPT and quantum-bounded adversaries at security level λ = 128 bits, using game-based reductions.
+
+---
+
+## 1. Motivation: The JIT Complexity Barrier
+
+Ergo's block validation cost is capped by the `maxBlockCost` consensus parameter, currently approximately **7,030,268 JIT units** on mainnet (adjustable via miner voting). This budget is shared across all transactions in a single block. Attempting to verify a STARK proof via interpreted ErgoScript hits a hard complexity wall on two fronts.
+
+### 1.1 Hashing Cost
+
+A single `blake2b256` invocation inside an ErgoScript `.fold()` loop costs **~1,400 JIT units**. A standard STARK verification with Q = 35 FRI queries and Merkle depth D = 16 requires:
+
+- **Per query:** D sibling hashes for the Trace tree + D for the Quotient tree + D for each FRI layer
+- **Conservative estimate:** 35 × 16 = 560 hash verifications per Merkle tree, across Trace, Quotient, and FRI rounds
+
+Hashing alone consumes **≥ 784,000 JIT units** — approximately **10% of the entire mainnet block budget** — leaving insufficient room for the contract's actual business logic (nullifier set membership checks, AVL+ tree insertions, state transition validation).
+
+### 1.2 Algebraic Cost
+
+STARK verification requires extension field arithmetic over F_{p^16}. Simulating these operations in ErgoScript requires:
+
+- **Multiplication:** Karatsuba polynomial multiplication across nested `Coll[Long]` tuples — each F_{p^16} multiply expands to ~120 base-field multiplications in the AST evaluator
+- **Inversion:** Extended Euclidean algorithm or Fermat's little theorem, both requiring iterative loops over the interpreter
+- **FRI folding:** Each Radix-8 iFFT step requires 7 F_{p^16} multiplications and 12 additions per query
+
+The interpreter overhead (AST node allocation, type checking, cost accumulation per node) amplifies the raw arithmetic cost by an estimated **10–100×** compared to native JVM execution.
+
+### 1.3 Conclusion
+
+A native `VerifyStark` opcode eliminates interpretation overhead entirely. The cryptographic computation runs at raw JVM speed, and the cost is collapsed into a **single O(1) AOT-calculated JIT charge** — the same architectural pattern used by Ergo's existing `proveDlog` and `proveDHTuple` sigma-protocol primitives. This is not an optimization; it is a physical requirement.
+
+---
+
+## 2. Algebraic Foundations & Cryptographic Instantiation
+
+To achieve 128-bit Post-Quantum (PQ) security within the execution constraints of the Ergo JVM, EIP-0045 specifies a highly optimized algebraic tower and a conservatively parameterized symmetric cryptographic stack.
+
+### 2.1 The Base Field and Quadratic Extension Tower
+
+**Base Field.** The protocol operates over the **BabyBear** prime field F_p, where:
+
+    p = 15 · 2^27 + 1
+
+Its 31-bit size allows field operations to stay comfortably within standard 32-bit CPU registers, avoiding multi-limb `BigInteger` allocation overhead on the JVM and enabling extremely fast modular arithmetic.
+
+**Extension Tower.** A 31-bit field provides insufficient collision resistance for cryptographic commitments and interactive challenges. To satisfy the 128-bit security target against Schwartz-Zippel algebraic forgery, polynomials are evaluated over a **Quadratic Extension Tower** of degree 16 (F_{p^16}).
+
+- The tower is constructed sequentially (F_{p^2} → F_{p^4} → F_{p^8} → F_{p^16}) using the quadratic non-residue x² − 11 at each level.
+- *Implementation rationale:* Using a power-of-2 tower (Ext16) rather than a prime extension (e.g., Ext13) enables recursive Karatsuba multiplication at each tower level. This binary decomposition maps directly to the JVM's arithmetic pipeline and to Ergo's AST Evaluator execution model.
+- *Algebraic capacity:* The Ext16 tower provides an algebraic collision space of 16 × 31 = 496 bits, completely overwhelming the 128-bit security target required to rule out algebraic forgery via the Schwartz-Zippel lemma.
+
+### 2.2 Symmetric Cryptography
+
+The STARK protocol requires two distinct types of hash functions: one for Merkle commitments (algebraic, field-native) and one for the Fiat-Shamir transcript (byte-oriented).
+
+**1. Merkle Commitments: Poseidon1 over BabyBear**
+
+- **Parameters:** Width T = 24, Capacity C = 13, Rate R = 11. The round structure consists of 8 full rounds + 22 partial rounds = 30 total rounds, following the Poseidon1 specification for conservative security margin.
+- **MDS Matrix:** Dense Cauchy Maximum Distance Separable (MDS) matrix, guaranteeing maximal branch number.
+- **Role:** Poseidon1 is used for **all Merkle tree hashing** — leaf construction (absorbing BabyBear trace row elements) and internal node hashing (tweakable: `Poseidon1(seed ‖ layer ‖ nodeIndex ‖ left ‖ right)`).
+- **Digest size:** 13 BabyBear elements = 52 bytes serialized as little-endian u32.
+- **Rationale (Poseidon1 vs. Poseidon2):** While Poseidon2 offers better off-chain prover performance via sparse internal matrices, recent literature (Grassi et al., 2025 — subspace-trail cryptanalysis over small prime fields) has raised concerns about the safety margin of its sparse matrices when instantiated over fields as small as BabyBear. EIP-0045 strictly enforces **Poseidon1** with a dense Cauchy MDS matrix to prioritize conservative L1 security. The 13-element capacity (≈ 403 bits) provides strong resistance against known algebraic and statistical attacks.
+
+**2. Fiat-Shamir Transcript: Native Blake2b-256**
+
+To transform the Interactive Oracle Proof (IOP) into a Non-Interactive argument (NIOP), we use Ergo's native `Blake2b-256` as the Random Oracle for Fiat-Shamir challenge generation. Merkle roots (52 bytes each, serialized as LE-u32 BabyBear elements) are committed into the Blake2b-256 transcript.
+
+- **The Formal vs. Pragmatic Tension (C1/C2).** We explicitly acknowledge the current academic tension regarding hash capacity in the Quantum Random Oracle Model (QROM). Under strict formal bounds, absorbing the extraction loss of the BCS theorem (Ben-Sasson, Chiesa, Spooner, 2016) theoretically requires a ≥ 384-bit hash function to maintain a gapless 128-bit PQ security parameter without relying on conjectures.
+- **Our Position.** EIP-0045 adopts the **pragmatic industrial standard** utilized by production STARK implementations (StarkWare, RISC Zero, Polygon Miden). We conjecture that a 256-bit state is practically sufficient, as actual quantum preimage attacks (Grover's algorithm) against a 256-bit chaotic state are strictly bounded at 2^128 quantum operations. Reusing Ergo's highly optimized, consensus-hardened `Blake2b-256` avoids introducing a new hash primitive to the protocol layer, saving JIT overhead while maintaining conjectured PQ security. All challenges are squeezed using strict **rejection sampling** (mask MSB, reject values ≥ p) to eliminate modular bias entirely.
+
+### 2.3 Protocol Parameters
+
+To compress the proof while maintaining the 128-bit soundness target against quantum adversaries, the FRI protocol is parameterized as follows:
+
+| Parameter | Value | Rationale |
+|-----------|-------|-----------|
+| Queries (Q) | 35 | Independent Merkle path queries per FRI round |
+| Blowup Factor (B) | 2048 | Code rate ρ = 1/B = 2^{-11} |
+| Folding Factor | Radix-8 | Folds 8 evaluations → 1 per round (unrolled iFFT-8) |
+
+**Why B = 2048?** The blowup factor is deliberately extreme compared to off-chain STARK systems (which typically use B ∈ {4, 16, 64}). On-chain, every Merkle hash costs ~1,400 JIT units, making Q (the query count) the dominant cost variable. By increasing B, we maximize the proximity gap per query, allowing us to reduce Q to the minimum required for 128-bit PQ soundness — thereby minimizing the on-chain verification cost. The tradeoff (larger proof size) is absorbed off-chain by the prover.
+
+The formal derivation connecting B, Q, ρ, and the 128-bit PQ security target under the QROM Fiat-Shamir transformation is presented in Section 4 (Adversary Games).
+
+---
+
+## 3. DEEP-FRI Protocol Scheme & Verification Mechanics
+
+The `VerifyStark` opcode verifies the transition integrity of an Algebraic Intermediate Representation (AIR). Let T_i(X) be the algebraic execution trace polynomials for the zkVM registers, and H(X) be the quotient polynomial evaluating the AIR constraints.
+
+### 3.1 DEEP-ALI Composition
+
+The Fiat-Shamir transcript challenges the Prover with a uniformly random Out-Of-Domain (OOD) point z ← F_{p^16}. The Prover provides the evaluations T_i(z), the next-row transitions T_i(z · g), and the quotient evaluation H(z).
+
+The `AirRegistry` subsystem inside the opcode executes the physical transition constraints over F_{p^16} and verifies the fundamental AIR relation against the vanishing polynomial Z_H(X):
+
+    C(z) = H(z) · Z_H(z)
+
+To mathematically bind these proven OOD evaluations to the committed Merkle roots without querying the trace at z (which is off-domain), the Verifier constructs the DEEP composition polynomial evaluations E(x_q) for each of the Q query points x_q:
+
+    E(x_q) = Σᵢ αᵢ · (Tᵢ(x_q) - Tᵢ(z)) / (x_q - z)
+           + Σᵢ βᵢ · (Tᵢ(x_q) - Tᵢ(z·g)) / (x_q - z·g)
+           + γ  · (H(x_q) - H(z)) / (x_q - z)
+
+**L1 JVM Optimization (Montgomery Batch Inversion).**
+Evaluating this formula naively requires 2Q heavy F_{p^16} inversions. For Q = 35, 70 inversions would severely tax the AST evaluator. EIP-0045 deploys a Montgomery Batch Inversion over the extension field. This reduces the algebraic cost to a **single true F_{p^16} inversion** combined with a linear sweep of lightweight multiplications, saving tens of thousands of AST allocation cycles.
+
+### 3.2 Radix-8 FRI Folding & Interpolation
+
+The evaluations E(x_q) serve as the inputs to the FRI protocol, which iteratively proves that the committed data belongs to a low-degree polynomial.
+
+To compress the proof and minimize on-chain operations, EIP-0045 utilizes a **Radix-8** folding factor. At each round r:
+
+1. The evaluation domain is collapsed by a factor of 8 (N → N/8).
+2. For each query, the Prover provides the 7 missing siblings forming a multiplicative coset C = {x_0, x_1, ..., x_7}.
+3. The Verifier interpolates the unique polynomial P(X) of degree < 8 over the coset, and evaluates it at the transcript challenge α_r.
+
+**L1 JVM Optimization (Unrolled iFFT-8).**
+Standard Lagrange interpolation over a coset requires O(N²) heavy F_{p^16} operations. EIP-0045 replaces this with an unrolled Inverse Fast Fourier Transform (iFFT-8). Because the coset roots are primitive 8th roots of unity residing entirely in the base field F_p, the "butterflies" of the iFFT require only scalar multiplications (F_{p^16} × F_p). The JVM executes this interpolation with **zero F_{p^16} inversions** and zero complex cross-multiplications, culminating in a simple Horner's method evaluation.
+
+---
+
+## 4. Formal Security Analysis (Adversary Games)
+
+We model the security of the EIP-0045 verification scheme using standard cryptographic games. Let λ_PQ = 128 be the target Post-Quantum security parameter. Let A be a quantum-bounded Probabilistic Polynomial-Time (PPT) adversary capable of querying the random oracle q_H times, and C be the Challenger (the L1 Ergo Verifier).
+
+### Game 1: Algebraic Soundness (Schwartz-Zippel)
+
+**Goal:** A attempts to pass the OOD check with a fraudulent state transition (i.e., C(X) ≠ H(X) · Z_H(X)).
+
+**Analysis:** By the Schwartz-Zippel lemma, two distinct polynomials of degree at most d evaluated at a random point z ∈ F_{p^16} agree with probability bounded by:
+
+    ε_SZ ≤ d / |F_{p^16}|
+
+Given the algebraic capacity of Ext16 (|F_{p^16}| = p^16 ≈ 2^496) and a maximum constraint degree d ≪ 2^32, the probability of an algebraic forgery is bounded by ε_SZ ≈ 2^{-464}. This provides **unconditional, information-theoretic security** against both classical and quantum adversaries. No computational assumption is required.
+
+### Game 2: IOP Proximity Soundness (FRI)
+
+**Goal:** A attempts to pass the interactive FRI query phase while providing a function that is δ-far from any valid Reed-Solomon codeword.
+
+**Analysis:** In the Interactive Oracle Proof (IOP) setting, each independent random query catches a cheating prover (whose committed function deviates from the code) with probability at least (1 − ρ), where ρ = B^{-1} is the code rate. Over Q independent queries, the interactive soundness error is bounded by the standard upper bound:
+
+    ε_IOP ≤ ρ^Q
+
+With our extreme blowup factor B = 2048, the code rate is ρ = 2^{-11}. Given Q = 35 queries:
+
+    ε_IOP ≤ (2^{-11})^35 = 2^{-385}
+
+This baseline interactive soundness is deliberately over-parameterized. The 385-bit interactive margin is the mathematical prerequisite required to absorb the extraction loss introduced by the QROM transformation analyzed in Game 3.
+
+### Game 3: Non-Interactive Forgery in the QROM (BCS Reduction)
+
+**Goal:** Since the protocol is Non-Interactive (NIOP), A controls the local generation of the proof and utilizes quantum oracle access to `Blake2b-256` to grind for favorable Fiat-Shamir challenges, attempting to bypass the soundness limits of Game 2.
+
+**Analysis:** Under the Ben-Sasson, Chiesa, Spooner (BCS) transformation bound for the Quantum Random Oracle Model (QROM), A's ability to grind the random oracle imposes a strict quadratic penalty on the interactive soundness:
+
+    ε_QROM ≤ q_H² · ε_IOP + ε_extract
+
+where q_H is the number of quantum hashing operations performed by A (the Grover search limit), and ε_extract is the extraction error of the IOP, which is negligible for algebraically structured IOPs and is hereafter omitted.
+
+For a 256-bit hash function targeted at 128-bit PQ security, the maximum number of effective quantum queries is q_H = 2^128. Substituting our interactive bound from Game 2:
+
+    q_H² · ε_IOP = (2^128)² · 2^{-385}
+                  = 2^256 · 2^{-385}
+                  = 2^{-129}
+
+**Under the standard QROM modeling assumption (Blake2b-256 as a random oracle), the parameter configuration (Q = 35, B = 2048) absorbs the quadratic extraction penalty, satisfying λ_PQ ≥ 128 with 1 bit of margin (2^{-129} ≤ 2^{-128}).**
+
+This tight parameterization is intentional: it minimizes Q (and therefore on-chain JIT cost) while meeting the security target under the same QROM assumptions used by all production STARK systems. Furthermore, the `FiatShamirTranscript` strictly enforces **rejection sampling** (mask MSB, reject values ≥ p), denying A any modular bias exploitation during challenge derivation.
+
+> **Note on formal rigor:** The security claim above is conditional on modeling Blake2b-256 as a quantum random oracle — a standard but unproven cryptographic assumption. This is the same assumption made by every production STARK system (StarkWare, RISC Zero, Polygon Miden). If this assumption is invalidated by future cryptanalysis, a new vmType profile with Blake2b-384 can be activated via the consensus process without modifying the opcode.
+
+### Game 4: Tweakable Merkle Collision Resistance
+
+**Goal:** A attempts to construct a Merkle commitment that can be opened to inconsistent evaluations at queried positions, or to reuse a valid Merkle subtree at a different depth or index to substitute invalid evaluations during the query phase.
+
+**Analysis:** In the STARK threat model, the prover is adversarial and chooses the Merkle tree contents. The binding property therefore depends on **collision resistance** of the Merkle hash — a malicious prover who can find a collision could potentially prepare inconsistent openings under the same committed root.
+
+EIP-0045 mitigates topological attacks by enforcing **Tweakable Hashing** (conforming to NIST FIPS 205 / SPHINCS+ standards). Every Merkle node is hashed with Poseidon1 and explicit domain separation:
+
+    Poseidon1(PublicSeed ‖ Layer ‖ NodeIndex ‖ Left ‖ Right)
+
+Because every node's hash is geometrically bound to its exact topological position, A cannot reuse paths across layers or indices. A is forced to find a direct collision in the Poseidon1 sponge state. The collision resistance of Poseidon1 is bounded by its capacity: C = 13 BabyBear elements ≈ 403 bits. Finding a collision requires:
+
+- **Classical:** O(2^201) operations (birthday bound on 403-bit capacity)
+- **Quantum:** O(2^134) operations (Brassard-Høyer-Tapp / BHT)
+
+Since 134 > 128, the Poseidon1 Merkle binding safely exceeds the λ_PQ = 128 requirement.
+
+**Note on hash function separation:** The Merkle hash (Poseidon1, ≥134-bit PQ collision) and Fiat-Shamir hash (Blake2b-256, conjectured ≥128-bit PQ under QROM) are distinct cryptographic components with independent security analyses. Game 4 (collision) and Game 3 (grinding) are separate attack surfaces — combining them in a single analysis would be a formal error.
+
+---
+
+## 5. Node Exhaustion & DoS Shield (The AOT Guarantee)
+
+If A cannot break the cryptography mathematically, they may attempt to halt the Ergo network by submitting a structurally valid but computationally massive proof (e.g., Q = 100,000, D = 30) to force the SigmaState JVM to exhaust memory or CPU time during block validation.
+
+**Mitigation.** The `VerifyStark` AST node executes an O(1) Ahead-Of-Time (AOT) defense shield *before any cryptographic operation begins*. Note that the transaction (including proof bytes) has already been deserialized from the P2P network at this point — the AOT shield prevents expensive crypto execution, not initial TX parsing:
+
+1. The node extracts Q (queries) and D (Merkle depth) as scalar values from the `costParams` argument.
+2. It computes the absolute JIT ceiling based on calibrated cost constants:
+
+        Cost_AOT = Cost_Base + (Q · Cost_FRI) + (Q · D · Cost_Merkle)
+
+3. The node invokes `ErgoTreeEvaluator.addCost(JitCost(Cost_AOT))`.
+
+**Result.** If Cost_AOT > MaxBlockCost, a `CostLimitException` is instantly thrown. A is forced to pay the mathematically derived computational cost upfront. The transaction is rejected without executing a single cryptographic operation or array allocation, completely neutralizing the L1 DoS vector in O(1) time and guaranteeing consensus liveness.
+
+**Critical implementation note.** The `CostLimitException` is explicitly re-thrown through the `catch` block — without this, the generic `catch(_: Throwable)` pattern in the SigmaState evaluator would silently swallow the cost exception, defeating the AOT fail-fast guarantee entirely.
+
+---
+
+## References
+
+1. Ben-Sasson, E., Bentov, I., Horesh, Y., Riabzev, M. (2018). "Scalable, transparent, and post-quantum secure computational integrity." IACR Cryptology ePrint Archive, 2018/046.
+2. Ben-Sasson, E., Chiesa, A., Spooner, N. (2016). "Interactive Oracle Proofs." TCC 2016.
+3. Grassi, L., et al. (2025). "Subspace Trail Cryptanalysis of Poseidon2 over Small Prime Fields."
+4. NIST FIPS 205 (2024). "Stateless Hash-Based Digital Signature Standard (SPHINCS+)."
+5. Brassard, G., Høyer, P., Tapp, A. (1998). "Quantum Cryptanalysis of Hash and Claw-Free Functions."
+6. Ergo Foundation. "ErgoScript Language Specification." https://ergoplatform.org