source: https://aszepieniec.github.io/stark-anatomy/overview

• 互動式證明系統
• STARK概述
  • Computation
  • Arithmetization and Arithmetic Constraint System
  • Interpolation and Polynomial IOPs
  • Cryptographic Compilation with FRI

STARK 是一類互動式證明系統，但本教程將它們視為 SNARK 的一個特例，其中

• 雜湊函式是唯一的加密成分，
• 算術化基於 AIR（algebraic intermediate representation,代數中間表示），並將關於計算完整性的宣告轉化為關於某些多項式的低次數(low degree)的宣告
• 使用 FRI 作為子協議來證明多項式的低階，並且 FRI 本身是用 Merkle 樹例項化的
• 零知識是可選的。

本教程的這一部分主要是解釋 STARK 定義中的關鍵術語。

互動式證明系統

在計算複雜性理論中，互動式證明系統是至少需要兩方參與的協議，其中的一方為驗證者，當且僅當該宣告為真時，他才確信某個數學宣告的正確性。從理論上講，該主張可以是任何可以用數學符號表達的東西，例如 Birch 和 Swinnerton-Dyer 猜想，\(P \ne NP\), 或 “第十五個斐波那契數是 643617。” （在可靠的證明系統中，驗證者將拒絕後面的宣告。）

A cryptographic proof system turns this abstract notion of interactive proof systems into a concrete object intended for deployment in the real world. This restriction to real world applications induces a couple of simplifications:

• 該宣告不是關於數學猜想，而是關於特定計算的完整性，例如“circuit \(C\) 在輸入為 \(x\) 時輸出為 \(y\)”, 或者“圖靈機器 \(M\) 在 \(T\) 步後輸出 \(y\)”。我們稱該證明系統建立了 計算完整性
• 協議有兩方，證明者和驗證者。一般情況下驗證者向證明者傳送的訊息包含純粹的隨機性，在這種情況下可以通過 Fiat-Shamir 變換讓證明系統變為非互動。非互動式證明系統由從證明者到驗證者的單個訊息組成。
• 驗證者可以接受非零但可以忽略不計的誤報率或誤報率，而不是要求完美的安全性。或者，證明系統僅在證明者計算能力有限的前提下提供安全性也是可以接受的。畢竟，所有計算機在實踐中都是計算能力有限的。有時，作者使用術語argument system來區分 the protocol from a proof system that offers security against computationally unbounded provers, and argument for the transcript resulting from the non-interactivity transform.
• 之所以驗證者不能重新執行整個計算來判斷計算的完整性，是因為證明者可以訪問驗證者無法訪問的資源。
  • 當受限資源是時間時，驗證者的執行速度應該比天真的重新執行程式快一個數量級。實現此屬性的證明系統被認為是簡潔的(succinct)
  • 簡潔的驗證需要簡短的證明，但一些證明系統（如 Bulletproofs 或 Aurora）雖然具有緊湊的證明，但驗證仍然很慢。
  • 當驗證者無法訪問證明者可用的祕密資訊時，並且當證明系統保護該祕密的機密性時，證明系統滿足零知識性(zero-knowledge)。 驗證者能夠在不瞭解有關該計算的部分或全部輸入的情況下確信該計算宣告的真實性。
• 特別是在零知識證明系統的背景下，計算完整性宣告可能需要進行細微的修改。 在某些情況下，僅僅證明一個宣告的正確性是不夠的，but the prover must additionally prove that he knows the secret additional input, and could as well have outputted the secret directly instead of producing the proof. Proof systems that achieve this stronger notion of soundness called knowledge-soundness are called proofs (or arguments) of knowledge.

A SNARK is a Succinct Non-interactive ARgument of Knowledge. The paper that coined the term SNARK used succinct to denote proof system with efficient verifiers. 然而，近年來，該術語的含義已被淡化為包括任何證明緊湊的系統。 本教程站在原始定義的一邊。

STARK概述

STARK 代表 Scalable Transparent ARgument of Knowledge。

• Scalable 指需要同時滿足兩個條件：（1）證明時間在計算量上至多quasilinear的 \(T(n) = O(nlog(n))\)，而 SNARK 則允許證明者具有非常昂貴的複雜性，並且 (2) 驗證時間在計算量上是polylogarithmic的 \(T(n) = O(log(n)^k)\)。
• Transparent refers to the fact that all verifier messages are just publicly sampled random coins. In particular, no trusted setup procedure is needed to instantiate the proof system, and hence there is no cryptographic toxic waste.

The acronym’s denotation suggests that non-interactive STARKs are a subclass of SNARKs, and indeed they are, but the term is generally used to refer to a specific construction for scalable transparent SNARKs.

For the purpose of introducing STARKs, the compilation pipeline is divided into four stages and three transformations. Later on in this tutorial there will be a much more fine-grained pipeline and diagram.

Computation

整個管道的輸入是計算(computation)，您可以將其視為程式+輸入+輸出。 所有這三個都以機器友好的格式提供，例如位元組列表。通常，程式由決定機器如何操作其資源的指令組成。如果正確的指令列表可以模擬任意圖靈機，那麼機器架構就是圖靈完備的。

在本教程中，程式被硬編碼到機器架構中，這也使得可以執行的計算是受限的。然而，輸入和輸出仍然是可變的。

The resources that a computation requires could be time, memory, randomness, secret information, parallelism. The goal is to transform the computation into a format that enables resource-constrained verifier to verify its integrity. It is possible to study more types of resources still, such as entangled qubits, non-determinism, or oracles that compute a given black box function, but the resulting questions are typically the subject of computational complexity theory rather than cryptographical practice.

Arithmetization and Arithmetic Constraint System

管道中的第一個轉換稱為算術化(arithmetization)。在這個過程中，對bit的基本邏輯和算術運算操作被轉換為對有限域元素的本地有限域操作，它們最終表達了相同的計算。輸出是一個算術約束系統，本質上是一堆方程，其係數和變數從有限域中取值。當且僅當約束系統具有符合條件的解時，計算才是完整的——這意味著，變數的某個取值使得所有方程都成立。

STARK證明系統對計算進行算數化的邏輯如下。 在任何時間點，計算狀態都包含在 \(w\) 個暫存器的元組中，這些暫存器從有限域 \(\rm F\) 中獲取值。機器定義了一個狀態轉換函式 \(f: {\rm F}^w \rightarrow {\rm F}^w\)，它在每個週期更新狀態。The algebraic execution trace (AET) is the list of all state tuples in chronological order.

The arithmetic constraint system defines at least two types of constraints on the algebraic execution trace:

• Boundary constraints: at the start or at the end of the computation an indicated register has a given value.
• Transition constraints: any two consecutive state tuples evolved in accordance with the state transition function.

這些約束統稱為 代數中間表示(algebraic intermediate representation) 或 AIR。Advanced STARKs may define more constraint types in order to deal with memory or with consistency of registers within one cycle.

Interpolation and Polynomial IOPs

通常意義上的插值(Interpolation)意味著找到一個通過一組資料點的多項式。在STARK的上下文中，插值意味著找到算數約束系統(arithmetic constraint system)的一個多項式表示。The resulting object is not an arithmetic constraint system but an abstract protocol called a Polynomial IOP.

The prover in a regular proof system sends messages to the verifier. But what happens when the verifier is not allowed to read them? 具體的說，如果來自證明者的訊息能夠被oracles取代(oracle指的是一種驗證者可以在他選擇的點中查詢的抽象黑盒功能),那麼協議就是一個 interactive oracle proof (IOP). 當oracles對應低度多項式時, 它是 Polynomial IOP. 直覺就是誠信的prover可以獲得一個等式都成立的多項式約束系統，而作弊的prover獲得的約束系統中，至少有一個等式是不成立的。當多項式相等時，它們在任何地方都相等，尤其是在驗證者選擇的隨機點上。但是當多項式不相等時，它們幾乎處處不相等，並且當驗證者在隨機點處驗證時，這種不相等有極大的概率會暴露出來。

The STARK proof system interpolates the algebraic execution trace literally – 也就是說，它找出 \(w\) 個多項式 \(t_{i}(X)\), 使得 \(t_{i}(X)\) 在域 \(D\) 上的取值和 AET 中的第i個暫存器上的值對應. 這些多項式被作為oracle傳送給verifier. At this point the AIR constraints give rise to operations on polynomials that send low-degree polynomials to low-degree polynomials only if the constraints are satisfied. 驗證者模擬這些操作，因此可以推匯出新的多項式，其低度(low degree)證明了約束系統的可滿足性，從而證明了計算的完整性。換句話說，插值步驟將算術約束系統的可滿足性降低到關於某些多項式的低階的宣告。

Cryptographic Compilation with FRI

在現實世界中，多項式預言機(polynomial oracles)並不存在。想要使用多項式 IOP 作為中間階段的協議設計者必須找到一種方法來commit多項式，然後在驗證者選擇的點開啟該多項式。 FRI 是 STARK 證明的關鍵組成部分，它通過使用 Reed-Solomon Codewords 的 Merkle 樹來證明多項式次數的有界性，從而實現了這一任務。

與多項式 \(f(X) \in {\rm F}[X]\) 相關的 Reed-Solomon codeword 是它在給定域 \(D \subset {\rm F}\) 上的值列表. 考慮不失一般性的域 \(D\)，其元素個數大於多項式的最大允許次數。這些值可以放入 Merkle 樹中，在這種情況下，Merkle樹的根代表對多項式的承諾(commitment)。Fast Reed-Solomon IOP of Proximity (FRI) 是一種協議，它的證明者傳送一個 Merkle 根序列，對應的codeword在每次迭代中長度減半。驗證者檢查連續輪次的merkle樹（驗證merkle path）以測試簡單的線性關係。對於誠實的證明者，所表示的多項式的次數同樣在每一輪中減半，因此遠小於codeword的長度。然而對於惡意證明者來說，這個度數比codeword的長度小一。在最後一步，證明者傳送一個與常數多項式相對應的non-trivial codeword。

上面沒有提及的一個問題是：驗證者如何在不屬於域的點 \(z\) 處查詢一個 committed polynomial \(f(X)\) ? 原則上，有一個明顯而直接的解決方案：verifier將 \(z\) 傳送給prover, prover則響應 \(y = f(z)\). 多項式 \(f(x) - y\) 在 \(X = z\) 處等於0, 因此 \(f(x) - y\) 必須被 \(X-z\) 整除. 所以證明者和驗證者都可以訪問一個新的低次多項式 \(\frac{f(X)-y}{X-z}\) . 如果prover在 \(f(z) = y\) 上撒謊, 那麼他就無法證明 \(\frac{f(X)-y}{X-z}\) 是低度的, 所以他的欺詐行為將在 FRI 協議的過程中暴露出來。This is in fact the exact mechanism that enforces the boundary constraints; a slightly more involved but similar construction enforces the transition constraints. 新的多項式是已知因子相除的結果，因此它們將被稱為 商(quotients) 並表示為 \(q_{i}(X)\) .

至此，多項式 IOP 已編譯為一個互動式具體證明系統。 原則上，該協議是可以執行的。 然而，多做一步加密編譯是值得的：用偽隨機(但具有確定性)的東西替換驗證者的隨機硬幣（隨機性）。 這正是 Fiat-Shamir 變換，其結果是稱為 STARK 的非互動式證明。