RChain的一鍵形式化驗證：關於RCast 33 – LADL話題的討論摘要

<!-- /\* Font Definitions \*/ @font-face {font-family:Helvetica; panose-1:2 11 6 4 2 2 2 2 2 4; mso-font-charset:0; mso-generic-font-family:swiss; mso-font-pitch:variable; mso-font-signature:-536859905 -1073711037 9 0 511 0;} @font-face {font-family:宋體; panose-1:2 1 6 0 3 1 1 1 1 1; mso-font-alt:SimSun; mso-font-charset:134; mso-generic-font-family:auto; mso-font-pitch:variable; mso-font-signature:3 680460288 22 0 262145 0;} @font-face {font-family:"Cambria Math"; panose-1:2 4 5 3 5 4 6 3 2 4; mso-font-charset:0; mso-generic-font-family:roman; mso-font-pitch:variable; mso-font-signature:-1610611985 1107304683 0 0 159 0;} @font-face {font-family:Calibri; panose-1:2 15 5 2 2 2 4 3 2 4; mso-font-charset:0; mso-generic-font-family:swiss; mso-font-pitch:variable; mso-font-signature:-520092929 1073786111 9 0 415 0;} @font-face {font-family:微軟雅黑; panose-1:2 11 5 3 2 2 4 2 2 4; mso-font-charset:134; mso-generic-font-family:swiss; mso-font-pitch:variable; mso-font-signature:-2147483001 672087122 22 0 262175 0;} @font-face {font-family:"\\@微軟雅黑"; panose-1:2 11 5 3 2 2 4 2 2 4; mso-font-charset:134; mso-generic-font-family:swiss; mso-font-pitch:variable; mso-font-signature:-2147483001 672087122 22 0 262175 0;} @font-face {font-family:"\\@宋體"; panose-1:2 1 6 0 3 1 1 1 1 1; mso-font-charset:134; mso-generic-font-family:auto; mso-font-pitch:variable; mso-font-signature:3 680460288 22 0 262145 0;} /\* Style Definitions \*/ p.MsoNormal, li.MsoNormal, div.MsoNormal {mso-style-unhide:no; mso-style-qformat:yes; mso-style-parent:""; margin:0cm; margin-bottom:.0001pt; text-align:justify; text-justify:inter-ideograph; mso-pagination:none; font-size:10.5pt; mso-bidi-font-size:11.0pt; font-family:"Calibri","sans-serif"; mso-ascii-font-family:Calibri; mso-ascii-theme-font:minor-latin; mso-fareast-font-family:宋體; mso-fareast-theme-font:minor-fareast; mso-hansi-font-family:Calibri; mso-hansi-theme-font:minor-latin; mso-bidi-font-family:"Times New Roman"; mso-bidi-theme-font:minor-bidi; mso-font-kerning:1.0pt;} p {mso-style-noshow:yes; mso-style-priority:99; mso-margin-top-alt:auto; margin-right:0cm; mso-margin-bottom-alt:auto; margin-left:0cm; mso-pagination:widow-orphan; font-size:12.0pt; font-family:宋體; mso-bidi-font-family:宋體;} .MsoChpDefault {mso-style-type:export-only; mso-default-props:yes; mso-bidi-font-family:"Times New Roman"; mso-bidi-theme-font:minor-bidi;} /\* Page Definitions \*/ @page {mso-page-border-surround-header:no; mso-page-border-surround-footer:no;} @page WordSection1 {size:612.0pt 792.0pt; margin:72.0pt 90.0pt 72.0pt 90.0pt; mso-header-margin:36.0pt; mso-footer-margin:36.0pt; mso-paper-source:0;} div.WordSection1 {page:WordSection1;} -->

做者／Atticbee

在這一集，Greg和RChain的研究人員Isaac，Christian討論了TLA（Temporal Logic of Actions）和RChain的LADL（Logic As Distribution Law）。下面是Atticbee作的摘要，而後加了一些本身的理解。

TLA （Temporal Logic of Actions，行爲時序邏輯）是併發系統進行形式化驗證的首選工具，不少分佈式的併發系統都用選用這個工具來進行驗。有一些背景介紹在這些文章裏：

https://www.zhihu.com/questio...。

頗有意思，亞馬遜的雲服務就利用TLA找出了不少設計上的bug。

用TLA進行驗證相對與傳統的軟件測試來講已是很大的進步了。傳統的測試，對於併發系統來講是遠遠不夠的。有過多線程代碼經驗的碼工應該有體會，有些錯誤是很難重現的，可能運行100萬次會崩潰一次。對於非重要應用這個無所謂，由於學習這些形式化驗證工具的成本很高，而後業界以爲對大多數的傳統應用，有bug也無所謂，大不了重啓，回滾交易。

Atticbee__注：但對於區塊鏈這種直接和錢打交道的，無法回滾的去中心化系統，這種bug就很要命了。儘管有些項目用了更安全的語言好比Rust，以及更安全的設計模式如OCAP來減小不少bug，可是智能合約的安全性是0和1的關係，不是0.9999999和1的關係。只要不經過形式驗證，黑客老是能夠用模型檢測器找到發起攻擊的途徑。

用TLA進行驗證，有個重要的缺陷就是，TLA的模型語言和最後的產品實現語言是不一樣的。在TLA的流程中，你首先用TLA建模語言定義一個模型，而後用這個語言定義一些目標性質（好比沒有死鎖，系統不會進入非法狀態等等），最後用這個自動化工具檢驗這個模型是否知足指定的目標性質。檢驗完成後，產品代碼按照這個模型來實現。然而，你驗證了TLA模型的正確性，並不代表你最後的代碼實現是正確的。

Atticbee__注：這就比如你設計了一座橋，進行力學計算驗證了這座橋是安全的，但你最後的工程實施若是和設計有所差距，造出的橋仍是會倒。

因此，最好的解決方案就是，發明一種語言，它既能夠是用來形式驗證的建模語言，同時又能夠做爲產品化的代碼語言。這就是爲何咱們對名字空間邏輯中的LADL感興趣的緣由。Rholang中的名字空間邏輯能夠用來創建一套行爲類型系統，對不少有意思的性質進行表達和檢查。因此在這個意義上，Rholang同時是一個產品化的代碼語言，也是一個TLA那樣的形式化建模語言。

Rholang能夠推導出的類型能夠表達TLA能驗證的一樣的目標性質，實際上更接近空間邏輯模型檢測器（Spatial Logic Model Checker）能驗證的目標性質。但Rholang的名字空間邏輯更具備表達力，由於因爲反射它能夠檢查名字之間的結構。因此有不少事，Rholang的名字空間邏輯能夠作，但Spatial Logic Model Checker作不到。一個很好的例子就是編譯期的防火牆：在類型檢查期間（遠在代碼執行以前），你就能夠判斷一個進程是否只在規定的名字集合中進行通訊，而不會超出這個範圍。甚至，你能夠隨時調整這個約束，好比規定在某些狀態下你的進程能夠在規定的名字上進行通訊。這種都是在代碼類型檢查期間完成的，因此稱之爲編譯期防火牆。

注意現有的RChain尚未實現這個名字空間邏輯，這是金星的規劃，水星是不帶類型的。儘管在Rholang 0.1的規格中，Greg給出了一個類型系統的草案，但還有不少事情要作，好比讓類型定義的語法變得對開發人員更加友好。巧合的是，TLA中目標性質定義的語法和Rholang 0.1中類型定義的語法很是相似。事實上，名字空間邏輯中的類型、空間邏輯模型裏的類型、TLA中的目標性質這幾個都有相應的對應關係，都是很是有意思的數學概念。而Rholang名字空間邏輯上的推導類型的LADL算法（用分配律表示邏輯）是這些概念的一個推廣，不光是數學上頗有意思，在分佈式系統的工程實現中也有很是重要的好處。

要理解LADL，須要知道上世紀三十年代就被發現了的柯里-霍華德同構（zh.wikipedia.org/wiki/%）：人們發現，Lambda演算和直覺邏輯的公式之間是緊密對應的，二者能夠相互轉換。直覺邏輯中的公式或命題能夠對應成爲Lambda演算中的類型。直覺邏輯中對命題的證實的推導（規約）步驟對應了Lambda演算中的beta規約。上世紀的90年代，Pi演算提出後，人們也進而發現用Pi演算中的進程代替Lambda演算中的項（Term）也獲得一樣的對應關係：一個進程要知足的邏輯命題等價於這個進程知足的類型。你的進程經過了一個類型檢查，也就天然證實了這個進程知足對應的邏輯命題，從而實現了自動化的形式驗證。_（Atticbee注：Greg在接下來說了不少LADL的知識，須要不少數學功底才能理解，因此略過不少細節。）_

LADL（用分配律表達邏輯）是一種推導、檢查類型的算法。注意有一些類型是不知足分配律的，好比列表，由於列表中元素存在次序關係因此不知足交換律。但集合這個類型是知足的。然而咱們並不須要支持最通用的類型集合（那就太複雜了，很難快速、自動的求解），只須要支持一個儘量大的子集就行。

因此LADL的思路是放棄了對最廣泛的代數結構的支持，這就不用求解很是難解的問題了，轉而只支持一個子集_（Atticbee注：最廣泛的狀況很是難解，須要窮舉各類狀態的組合，計算量很是大。）_用LADL有不少好處，首先，能夠一鍵快速生成類型系統_（Atticbee注：從而也實現了在這個子集上的代碼的一鍵形式化證實）_；而後，能夠用來做爲一個更好的查詢語言。好比現有的github系統，你是沒法根據代碼的結構進行查詢的。若是可能根據代碼的結構和行爲進行查詢，那會使得程序員的效率大大提升。

本文不構成任何投資建議。

加RChain小助手

帶你進RChain微信羣，找到組織