作者：郭宇

本文已更新至Github:https://github.com/

引言：

引言：

我認為區塊鏈很難稱為一個“技術”。它更像是一個領域，包羅萬象。或者形而上地說，區塊鏈更像一個有機體，融合了各種不同的理論技術。

二級標題

證明

"證明"證明

的前世今生

什麼是證明？很多人可能和我一樣，看到這兩個字，會不禁想起中學考卷中各種三角相似的幾何圖形，當老師在神奇地畫出一條輔助線後，證明過程突然顯而易見，然後會懊悔自己為何沒想到。

古希臘：「證明」 == 「洞見」

數學證明最早源於古希臘。他們發明（發現）了公理與邏輯，他們用證明來說服對方，而不是靠權威。這是徹頭徹尾的「去中心化」。自古希臘以降，這種方法論影響了整個人類文明的進程。

上圖是「勾股定理」的巧妙證明。歷史上曾出現過許許多多精巧的證明，神奇的思路，天才的靈感。一旦一個命題被證明，上帝都無能為力。嗯，對了，還有那個「上帝不是萬能的」證明：上帝不能造出一塊他舉不起來的石頭。

一個數學證明往往暗藏無比深刻的「洞見」，相信很多人都看過「費馬大定理」的故事[1]，這個定理證明橫跨四百年，從費馬寫下「這裡空間太小，我寫不下」，到懷爾斯最終登頂，耗費了許多代人的聰明才智。最近如「彭加萊猜想」，稍微帶點年代感的如「哥德巴赫猜想」，還有我非常敬佩的華裔科學家張益唐十年磨一劍，在仔細研究了「Goldston-Pintz-Yıldırım」和「Bombieri-Friedlander-Iwaniec.」的證明「洞見」之後，證明了「質數間的有界間隔」[2]。

自十七世紀，萊布尼茨起，人們就夢想找到一種機械的手段，可以來自動完成證明，而不再依賴天才的靈光一現。

二十世紀初：「證明」 == 「符號推理」

時間到了十九世紀末，康托、布爾、弗雷格、希爾伯特、羅素、布勞威、哥德爾等人定義了形式化邏輯的符號系統。而「證明」則是在利用形式化邏輯的符號語言編寫的推理過程。邏輯本身靠譜麼？邏輯本身「自恰」嗎？邏輯推理本身對不對，能夠證明嗎？這讓數學家/邏輯學家/計算機科學家發明（發現） 了符號系統，語法vs. 語義，可靠vs. 完備，遞歸vs. 無窮。 （這部分精彩故事請參看『邏輯的引擎』一書[3]）。

1910年，羅素發表了洪(zhuan)荒(tou)巨著『數學原理』。在書中，羅素與懷特海試圖將數學完整地「形式化」下來。如果能達到這樣的目標，所有的數學成果都將以證明的方式建立在堅實的基礎上。下圖就是『數學原理（卷二）』中的一頁：

其中110.643這是一個命題：「1+1=2」，然後接下來就是這個定理的證明。大家可能奇怪，難道1+1 還需要證明嗎？是的，在數學原理一書中，數字0，1，2，…… 都有嚴格定義，「加法」、「乘法」、「等於」都要嚴格定義，然後每一步的推理都需要指出依據。證明意味著什麼？證明是可能繁瑣無比的、但是每一步推理都嚴格無誤。書中大量的證明都機械式的，按照公理和推理規則進行一種證明的構造，尋找證明就好像可以交給一個人，然後他無腦在公理與推理規則的集合中進行機械查找。

似乎人們距離「定理的自動證明」並不遙遠了。

不幸的是，哥德爾在1931 年證明了「哥德爾不完備性定理」[4]，圖靈在1936 年證明了圖靈機停機問題的不可判定性[5]。這些成果徹底終結了這個幾百年的幻想。無論公理系統如何精巧設計，都無法抓住所有的真理。

證明不僅僅是一個嚴格推理，而且凝結了似乎很難機械化的創造性思維。證明中蘊含了大量的「知識」，每一次的突破，都將我們的認知提升到一個新的高度。不管是「洞見」，還是推理過程中所構造的「算法」，一個定理的證明的內涵往往遠超出定理本身的結論。

六十年代：「證明」 == 「程序」

又過了半個世紀，到了六十年代，邏輯學家Haskell Curry 和William Howard 相繼發現了在「邏輯系統」和「計算系統— Lambda 演算」中出現了很多「神奇的對應」，這就是後來被命名的「Curry-Howard Correspondence」。這個發現使得大家恍然大悟，「編寫程序」和「編寫證明」實際在概念上是完全統一的。而在這之後的50 年，相關理論與技術發展使得證明不再停留在草稿紙上，而是可以用程序來表達。這個同構映射非常有趣：程序的類型對應於證明的定理；循環對應於歸納；……（這裡推荐一本書：『軟件基礎』（Software Foundations 中譯本）[6]）。在直覺主義框架中，證明就意味著構造算法，構造算法實際上就是在寫代碼。 (反過來也成立，嗯，碼農碼的不是代碼，是數學證明，:P)

目前在計算機科學領域，許多理論的證明已經從紙上的草圖變成了代碼的形式，比較流行的「證明編程語言」有Coq，Isabelle，Agda 等等。採用編程的方式來構造證明，證明的正確性檢查可以機械地由程序完成，並且許多囉嗦重複性的勞動可以由程序來輔助完成。數學理論證明的大廈正在像計算機軟件一樣，逐步地構建過程中。 1996 年12 月W. McCune 利用自動定理證明工具EQP 證明了一個長達63 年曆史的數學猜想「Ronbins 猜想」，『紐約時報』隨後發表了一篇題為「Computer Math Proof Shows Reasoning Power」的文章[7]，再一次探討機器能否代替人類創造性思維的可能性。

利用機器的輔助確實能夠有效幫助數學家的思維達到更多的未知空間，但是「尋找證明」仍然是最有挑戰性的工作。 「驗證證明」，則必須是一個簡單、機械、並且有限的工作。這是種天然的「不對稱性」。

八十年代：「證明」 == 「交互」

時間撥到1985年，喬布斯剛剛離開蘋果，而S. Goldwasser 博士畢業後來到了MIT，與S. Micali，Rackoff 合寫了一篇能載入計算機科學史冊的經典：『交互式證明系統中的知識複雜性』[8]。

二級標題

二級標題

二級標題

交互式證明

Alice: 我想向你證明我有一個方程的解，w^3 - （w+1)^2 + 7 = 0 （方程的解：w=3）

Bob: 好啊，我聽著呢

Alice: 但是我不會告訴你x 具體是多少，除非你願意掏錢，我才告訴你。

Bob: 可以啊，但是你要先證明你有方程的解，我再給錢你。

Alice: @#$%^& （黑科技）

Alice: &*#$@! （黑科技）

Bob: ??????（黑科技）

...... （繼續黑科技）

Alice: 好了，完了

Alice: 好了，完了

Bob: 好吧，你確實有方程的解，不過是不是我掏了錢，你就會把答案告訴我？

Alice: 別廢話，掏錢！

上面例子就是一個「交互式證明」。假設Alice知道方程的解， f(w) = 0，那麼Alice 如何讓Bob 確信她知道w 呢？ Alice 在「黑科技階段」 告訴了Bob 一大堆的信息。好了，關鍵問題是，Bob 能不能從Alice 所說的一大堆信息中猜出w 到底是幾，或者能分析出關於w 的蛛絲馬跡呢？如果Bob 有這個能力，Bob也許就沒必要掏錢了，因為他已經獲得了這個值錢的信息。

證明

• 零

• 證明

• 證明

證明

• 各位可能已經有點感覺了，我們來嘗試著解讀一下：

• 零： Alice 洩露了關於w 的「零」知識，也就是沒有洩露知識。

• 二級標題

二級標題

二級標題

零知識證明有什麼用處？

一提零知識證明技術，很多人就想到了匿名Coin，比如Monero, 比如ZCash。確實，這幾個Coin 很好地普及了零知識證明，我本人也是通過ZCash 才第一次聽說了零知識證明這個詞。但是在更深入地了解這個技術之後，深深感覺這個技術的威力遠不止這一點。

零知識證明技術可以解決數據的信任問題，計算的信任問題！

張三說他有100塊錢，李四說他北大畢業，王五說要和八菲特共進午餐。空口無憑，Show me the proof。

那麼「零知識證明」能解決數據的信任如何理解呢？在上一篇文章『zkPoD: 區塊鏈，零知識證明與形式化驗證，實現無中介、零信任的公平交易』[9]裡面，我提到了一個概念「模擬」：

零知識證明技術可以「模擬」出一個第三方，來保證某一個論斷是可信的

換句話說，當我們收到一個加了密的數據， 然後還有一個零知識證明。這個零知識證明是說「關於數據的X 斷言成立」，那麼這等價於有一個天使在我們耳邊悄聲說，「關於數據的X 斷言成立」！

對於這個X 斷言，可以非常靈活，它可以是一個NP複雜度的算法。大白話講只要我們能寫一段程序（一個多項式時間的算法）來判斷一個數據是否滿足X 斷言，那麼這個斷言就可以用零知識證明的方式來表達。通俗點講，只要數據判定是客觀的，那麼就零知識證明就適用。

• 零知識證明的一些用處：

• 數據的隱私保護：在一個數據表格中，多多少少都有一些信息不想被暴露，比如當年我的成績單，我只想向人證明，我的成績及格了，但是我不想讓別人知道我到底考了61分還是62分，這會很尷尬。我沒有心髒病，但是保險公司需要了解這一點，但是我不想讓保險公司知道我的隱私信息。那我可以證明給保險公司看，我沒有心髒病，但是病歷的全部並不需要暴露。我是一家企業，我想向銀行貸款，我只想向銀行證明我具備健康的業務與還款能力，但是我不想讓銀行知道我們的一些商業秘密。

• 計算壓縮與區塊鏈擴容：在眾多的區塊鏈擴容技術中，Vitalik 採用zkSNARK 技術能夠給現有的以太坊框架帶來幾十倍的性能提升。因為有了計算的證明，同樣一個計算就沒必要重複多次了，在傳統的區塊鏈架構中，同樣的計算被重複多次，比如簽名的校驗，交易合法性校驗，智能合約的執行等等。這些計算過程都可以被零知識證明技術進行壓縮。

• 端到端的通訊加密：用戶之間可以互相發消息，但是不用擔心服務器拿到所有的消息記錄，同時消息也可以按照服務器的要求，出示相應的零知識證明，比如消息的來源、與發送的目的地。

• 身份認證：用戶可以向網站證明，他擁有私鑰，或者知道某個只要用戶自己才知道的秘密答案，而網站並不需要知道，但是網站可以通過驗證這個零知識證明， 從而確認用戶的身份

• 去中心化存儲：服務器可以向用戶證明他們的數據被妥善保存，並且不洩露數據的任何內容。

• 二級標題

• 二級標題

二級標題

舉例：地圖三染色問題

下面講一個經典的問題，地圖的三染色問題。如何用三種顏色染色一個地圖，保證任意兩個相鄰的地區都是不同的顏色。我們把這個「地圖三染色問題」轉變成一個「連通圖的頂點三染色問題」。假設每個地區都有一個首府（節點），然後把相鄰的節點連接起來，這樣地圖染色問題可以變成一個連通圖的頂點染色問題。

• 下面我們設計一個交互協議：

• 「證明者」Alice

「驗證者」 Bob

Alice 手裡有一個地圖三染色的答案，請見下圖。這個圖總共有6 個頂點，9 條邊。

現在Alice 想證明給Bob 她有答案，但是又不想讓Bob 知道這個答案。 Alice 要怎麼做呢？

Alice 先要對染過色的圖進行一些「變換」，把顏色做一次大挪移，例如把所有的綠色變成橙色，把所有的藍色變成綠色，把所有的綠色變成橙色。然後Alice 得到了一個新的染色答案，這時候她把新的圖的每一個頂點都用紙片蓋上，然後出示給Bob 看。

看下圖，這時候Bob 要出手了（請見下圖），他要隨機挑選一條「邊」，注意是隨機，不讓Alice 提前預測到的隨機數。

假設Bob 挑選的是最下面的一條邊，然後告訴Alice。

這時候Alice 揭開這條邊兩端的紙片，讓Bob 檢查，Bob 發現這兩個頂點的顏色是不同的，那麼Bob 認為這次檢驗同構。這時候，Bob 只看到了圖的局部，能被說服剩下的圖頂點的染色都沒問題嗎？你肯定覺得這遠遠不夠，也許恰好Alice 蒙對了呢？其它沒暴露的頂點可能是胡亂染色的。

沒關係，Bob 可以要求Alice 再來一遍，看下圖

Alice 再次把顏色做一次變換，把藍色改成紫色，改綠色改成棕色，把橙色改成灰色，然後把所有的頂點蓋上紙片。然後Bob 再挑選一條邊，比如像上圖一樣，選擇的是一條豎著的邊，然後讓Alice 揭開紙片看看，如果這時候Bob 再次發現這條邊兩端的頂點顏色不同，那麼Bob 這時候已經有點動搖了，可能Alice 真的有這個染色答案。可是，兩次仍然不夠，Bob 還想再多來幾遍。

二級標題

二級標題

二級標題

• 信息vs. 知識

• 信息「Information」

知識「Knowledge」

在地圖三染色問題的交互證明中，當重複交互很多次之後，Bob 得到了大量的信息，但是這好比Alice 發給Bob 一堆隨機數一樣，Bob 並沒有「知道」更多的東西。打個比方，如果Alice 告訴Bob 「1+1=2」，Bob 得到了這個信息，可是Bob 並沒有額外獲取更多的「知識」，因為這個事實人人皆知。

假如Alice 告訴Bob 2^2^41-1這個數是一個質數，很顯然這個是「知識」，因為要算出來這個數是不是一個質數，這需要耗費大量的算力。

假如Alice 告訴Bob，總共有兩個頂點用了綠顏色，那麼Bob 就獲得了寶貴的「知識」，因為基於他剛剛獲取的這個信息，Bob 可以用更短的時間用一台圖靈機去求解三染色問題。假如Alice 又透露給Bob，最左邊的頂點顏色是用橙色，那麼很顯然，這個「信息」對於Bob 求解問題並沒有實質上的幫助。

我們可以嘗試定義一下，如果Bob 在交互過程中獲得的「信息」，可以幫助提升Bob 直接破解Alice 秘密的能力，那麼我們說Bob 「獲得了知識」。由此可見，知識這個詞的定義與Bob 的計算能力相關，如果信息並不能增加Bob 的計算能力，那麼信息不能被稱為「知識」。比如在Alice 與Bob 交互過程中，Alice 每次都擲一個硬幣，然後告訴Bob 結果，從信息角度看，Bob 得到的信息只是一個「事件」，然而Bob 並沒有得到任何「知識」，因為Bob 完全可以自己來擲硬幣。

• 下面引用『Foundations of Cryptography—— Basic Tools』一書[10]中的總結

• 二級標題

二級標題

二級標題

可驗證計算與電路可滿足性問題

看了上面的地圖三染色問題，大家是不是沒有感覺，好像這只是一個學術問題，如何跟現實問題關聯起來？地圖三染色問題是一個NP-Complete 問題，這是「計算理論」中的一個名詞。另外有一個叫做「電路可滿足問題」也是同樣是NP-Complete 問題。 NP-Complete 是一類問題，他的求解過程是多項式時間內難以完成的，即「求解困難」，但是驗證解的過程是多項式時間可以完成的，即「驗證簡單」。

那什麼是電路呢？下面是三個不同的「算術電路」：

可以看到一個電路由很多個門組成，其中有加法門，還有乘法門。每一個門有幾個輸入引腳，有幾個輸出引腳。每一個門做一次加法運算，或乘法運算。別看這麼簡單，我們平時跑的（沒有死循環）代碼，都可以用算術電路來表示。

這意味著什麼呢？我們下面結合「零知識證明」與「電路可滿足性問題」來試著解決數據的隱私保護問題。

下面請思考一個場景：Bob 交給Alice 一段代碼P，和一個輸入x，讓Alice 來運行一遍，然後把運行結果告訴Bob。可能這個計算需要消耗資源，而Bob 把計算過程外包給了Alice。然後Alice 運行了一遍，得到了結果y。然後把y 告訴Bob。下面問題來了：

如何讓Bob 在不運行代碼的前提下，相信代碼P 運行的結果一定是y 呢？

這裡是思考時間，大家可以想個五分鐘……

（五分鐘後……）

Alice 的一種做法是可以把整個計算過程用手機拍下來，這個視頻裡麵包含了計算機CPU，還有內存，在整個運行過程中的每一晶體管的狀態。很顯然這麼做是不現實的。那麼有沒有更可行的方案呢？

答案是Bob 把程序P 轉換成一個完全等價的算術電路，然後把電路交給Alice。 Alice 只要計算這個電路就可以了，然後這個過程是可以用手機拍下來的，或者用紙記下來，如果電路規模沒有那麼大的話。 Alice 只要把參數6 輸入到電路，然後記錄下電路在運算過程中，所有與門相連的引腳線上的值。並且最後的電路輸出引腳的值等於y，那麼Bob 就能確信Alice 確實進行了計算。 Alice 需要把電路的所有門的輸入與輸出寫到一張紙上，交給Bob，這張紙就是一個計算證明。

這樣Bob 完全可以在不重複計算電路的情況下來驗證這張紙上的證明對不對，驗證過程很簡單：

Bob 依次檢查每一個門的輸入輸出能不能滿足一個加法等式或者一個乘法等式。

比如1 號門是一個加法門，它的兩個輸入是3，4，輸出是7，那麼很容易就知道這個門的計算是正確的。當Bob 檢查完所有的門之後，就能確信：

Alice 確確實實進行了計算，沒有作弊。

這張紙上的內容就是「滿足」算術電路P 的一個解「Solution」。

所謂的電路可滿足性就是指，存在滿足電路的一個解。如果這個解的輸出值等於一個確定值，那麼這個解就能「表示」電路的計算過程。

• 對於Alice 而言，Bob 如果用這種方式驗證，她完全沒有作弊的空間。但是這種方法很顯然有個弊端：

• 弊端二：Bob 在驗證過程中，知道了所有的電路運算細節，包括輸入。

• 黑科技

黑科技

我們再對剛才的Alice 與Bob 的場景做些修改。假如，Alice 自己還有一個秘密，比如說網銀密碼。而Bob 想知道Alice 的網銀密碼的長度是不是20 位長。而Alice 想了下，告訴他密碼長度應該問題不大。這時候Bob 把一個計算字符串長度的代碼轉換成了電路Q，並且發給Alice。 Alice 用電路Q 算了一下自己的密碼，然後把電路所有門的引腳發給了Bob，並帶上運算結果20。

Wai……t，這是有問題的，Bob 拿到電路運算過程中的所有內部細節之後，不就知道密碼了嗎？是的，Alice 顯然不能這麼做。那麼Alice 應該怎麼做？

答案是有很多種辦法，熱愛區塊鏈技術的讀者最耳熟的就是zkSNARK[11]，還有zkSTARK[12]，子彈證明BulletProof[13]，以及一些比較小眾的技術，都可以幫Alice 做到：

Alice 以一種零知識的方式，向Bob 證明她計算過了電路，並且使用了她的秘密輸入。

二級標題

寫在最後

寫在最後

寫在最後

二級標題

參考文獻

參考文獻

• 參考文獻

• [2]  Alec Wilkinson. The Pursuit of Beauty: Yitang Zhang solves a pure-math mystery. The New Yorker. Feb. 2015.

• [1] 西蒙, 辛格, 薛密. 費馬大定理: 一個困惑了世間智者358 年的謎[M]. 上海譯文出版社, 1998.

• [4] Raymond Smullyan. Gödel's Incompleteness Theorems, Oxford Univ.Press. 1991.

• [5] Turing, Alan. "On computable numbers, with an application to the Entscheidungsproblem." Proceedings of the London mathematical society 2.1 (1937): 230-265.

• [6] Pierce, Benjamin C., et al. "Software foundations."[3] 馬丁, 戴維斯, 張卜天. 邏輯的引擎[M]. 湖南科學技術出版社, 2012.<https://github.com/Coq-zh/SF-zh

• [7] Kolata, Gina. "Computer math proof shows reasoning power." Math Horizons 4.3 (1997): 22-25.

• [8] Goldwasser, Shafi, Silvio Micali, and Charles Rackoff. "The knowledge complexity of interactive proof systems." SIAM Journal on computing 18.1 (1989): 186-208.

• 中文譯文:

• [10] Oded, Goldreich. "Foundations of cryptography basic tools." (2001).

• [11] Gennaro, Rosario, et al. "Quadratic span programs and succinct NIZKs without PCPs." AnnualInternational Conference on the Theory and Applications of Cryptographic Techniques. Springer Berlin, Heidelberg, 2013.

• [12] Ben-Sasson, Eli, et al. "Scalable, transparent, and post-quantum secure computational integrity." IACR Cryptology ePrint Archive 2018 (2018): 46.

• [13] Bünz, Benedikt, et al. "Bulletproofs: Short proofs for confidential transactions and more." 2018IEEE Symposium on Security and Privacy (SP). IEEE, 2018.