白皮書(shū)的描述語(yǔ)言move語(yǔ)法詳細(xì)解析

move語(yǔ)法

白皮書(shū)使用了一種半形式化（semi-formal）的描述語(yǔ)言進(jìn)行了描敘。至于這套描述語(yǔ)言，主要符號(hào)解釋如下：

=： 定義

：：= ： 賦值

?： 映射

×： product type，也就是表示結(jié)構(gòu)體

∈： 表示屬于某個(gè)類型或者集合中的一個(gè)元素

通過(guò)這些符號(hào)，Move定義了如下的語(yǔ)法類型：

Global state： 地址到賬戶的map，賬戶由Resource和Module構(gòu)成。形式化定義如下：

Modules：由名字，結(jié)構(gòu)體聲明以及過(guò)程聲明組成， 可以簡(jiǎn)單理解為c++的class。module通過(guò)ModuleId被外部索引（訪問(wèn)），結(jié)構(gòu)體通過(guò)structId被外部索引，結(jié)構(gòu)體聲明是一個(gè)《kind， FieldName-》非引用類型》的product類型。

Module定義了資源的作用域，類似于c++的namespace的功能。其中Module內(nèi)置了幾個(gè)重要的函數(shù)用來(lái)進(jìn)行類型操作：

· Pack and Unpack 用于從非受限類型創(chuàng)建和銷(xiāo)毀模塊的資源；

· MoveToSender/MoveFrom 在當(dāng)前賬戶地址下面發(fā)布或者刪除對(duì)應(yīng)的資源；

· BorrowField ：獲得結(jié)構(gòu)體的一個(gè)字段的引用

Types： 包含基本類型（bytes是fixed-size字符串，AccountAddress是256bits），結(jié)構(gòu)體類型，非引用類型，以及

在Module里面除去被聲明為資源的類型（標(biāo)記了resource kind），其余的類型統(tǒng)稱為unrestricted types（不受限類型）。資源類型的變量或者字段只能被move，并且資源類型變量的引用不能被解引用，也不能被重復(fù)賦值。另外an unrestricted struct不能包含restricted field，原因很簡(jiǎn)單， unrestricted 結(jié)構(gòu)體被賦值或者復(fù)制的時(shí)候，如果有restricted字段，那這個(gè)字段不會(huì)實(shí)際被操作到。

Values：

Move支持引用，引用是短暫的，因此不能被用來(lái)定義結(jié)構(gòu)體的字段，也不能引用引用，應(yīng)用的聲明周期就是交易腳本的執(zhí)行過(guò)程。通過(guò)Borrow{Loc， Field， Global}可以分別可以獲得局部變量，結(jié)構(gòu)體變量或者全局變量的引用（敲黑板，請(qǐng)學(xué)習(xí)rust）。

另外因?yàn)閟truct里不能存儲(chǔ)reference，所以可以保證struct一定是一個(gè)tree而不會(huì)有backedge。這也是move比rust簡(jiǎn)化的最重要的一點(diǎn)，正因此move不需要復(fù)雜的lifetime。 因此Resource同樣也不可能出現(xiàn)圖結(jié)構(gòu)。這樣確實(shí)大大簡(jiǎn)化了語(yǔ)言的處理。

Procedures and transaction scripts：

過(guò)程的簽名包含函數(shù)的訪問(wèn)控制修飾符，參數(shù)類型和返回值類型。過(guò)程聲明包括一個(gè)過(guò)程簽名，局部變量和一系列的指令，（作者認(rèn)為，這個(gè)聲明理解為定義（definition）更合適一些）。一個(gè)交易腳本是一個(gè)不關(guān)聯(lián)具體module的過(guò)程，因此他不會(huì)被復(fù)用，交易腳本操作的全局狀態(tài)轉(zhuǎn)換，這些狀態(tài)的修改要么全部成功，要么全部失敗。

ProcedureID標(biāo)識(shí)一個(gè)過(guò)程，被moduleId和過(guò)程簽名唯一確定，并且Call指定將其作為第一個(gè)參數(shù)，進(jìn)行調(diào)用。這也就意味著函數(shù)調(diào)用是靜態(tài)可確定（staticly determined）的，不存在什么函數(shù)指針或者函數(shù)表。同時(shí)模塊內(nèi)的過(guò)程依賴是無(wú)環(huán)的，加上模塊本身的沒(méi)有動(dòng)態(tài)指派，這樣就加強(qiáng)了執(zhí)行期間的函數(shù)調(diào)用的不可變性：也就是一個(gè)procedure在執(zhí)行過(guò)程的call frame必然是相鄰的。因此也防止了類似于以太坊里面的re-entrancy攻擊（這個(gè)就是有名導(dǎo)致分叉出ETC的攻擊）。

move解釋器

Move的字節(jié)碼指令在一個(gè)棧式的解釋器進(jìn)行執(zhí)行，棧式虛擬機(jī)的好處是易于實(shí)現(xiàn)和控制，對(duì)硬件環(huán)境的要求較少，非常適合區(qū)塊鏈場(chǎng)景。同時(shí)文中也提到，相對(duì)寄存器式的解釋器， 棧式解釋器在不同的變量之間進(jìn)行copy和move更容易控制和檢測(cè)。

解釋器的定義如下：

解釋器由一個(gè)Value Stack，Call Stack以及全局變量引用計(jì)數(shù)器和一個(gè)GasUnits（類似以太坊的Gas Limits）組成。CallStackFrame包含了一個(gè)過(guò)程執(zhí)行的所有上下文信息以及指令編號(hào)（指令會(huì)被唯一編碼，減少代碼體積，常規(guī)處理方法）。Locals是一個(gè)變量名到運(yùn)行時(shí)候的Value的map。

字節(jié)碼解釋器支持過(guò)程調(diào)用（廢話?。?。當(dāng)在一個(gè)過(guò)程中執(zhí)行Call指令調(diào)用其他的過(guò)程的時(shí)候，會(huì)創(chuàng)建一個(gè)新的CallStackFrame對(duì)象，然后將對(duì)應(yīng)的調(diào)用參數(shù)存儲(chǔ)到Locals上面，最后解釋器開(kāi)始以此執(zhí)行新的合約的指令。執(zhí)行過(guò)程遇到分支指令的時(shí)候，會(huì)在本過(guò)程內(nèi)部（也就是Basic Block之前的跳轉(zhuǎn)）發(fā)生一個(gè)靜態(tài)跳轉(zhuǎn)，所謂靜態(tài)跳轉(zhuǎn)實(shí)際上是指跳轉(zhuǎn)的offset是事先已經(jīng)確定好的，不會(huì)像evm一樣動(dòng)態(tài)跳轉(zhuǎn)。這也就是之前提到的no dynamic dispath。最后調(diào)用return結(jié)束調(diào)用，同時(shí)返回值放在棧頂。

Gas衡量的思路跟EVM是一樣的，每個(gè)指令有對(duì)應(yīng)的Gas Units，執(zhí)行一次，減去對(duì)應(yīng)指令的Gas消耗，直到減到0或者所有指令執(zhí)行完成。

Move的指令包括6大類：

· 變量操作： CopyLoc/MoveLoc實(shí)現(xiàn)數(shù)據(jù)從本地變量到棧的拷貝和移動(dòng)，StoreLoc是講數(shù)據(jù)存回來(lái)到本地

· 常量/數(shù)值/邏輯操作

· Pack/Unpack/MoveToSender/MoveFrom/BorrowField 等資源操作，具體的解釋可以看前一篇文章

· 引用相關(guān)的指令，包括ReadRef/WriteRef/ReleaseRef/FreezeRef， 其中FreezeRef轉(zhuǎn)換一個(gè)可變引用到一個(gè)不可變引用

· 控制流結(jié)構(gòu)，包括call和return，branch，BranchIfTrue，BranchIfFalse等

· 區(qū)塊鏈特定的操作，包括獲得交易腳本的sender或者創(chuàng)建一個(gè)賬號(hào)等指令。

詳細(xì)的指令列表在白皮書(shū)的Appendix A已經(jīng)列出。

Bytecode驗(yàn)證器

驗(yàn)證器我們?cè)诤芏嗑幾g器里面都能看到，例如普遍使用的SMT證明器Z3. 驗(yàn)證器的核心功能就是在編譯階段保證語(yǔ)言（合約）的安全特性能夠得到滿足和增強(qiáng)。驗(yàn)證器靜態(tài)驗(yàn)證是合約腳本發(fā)布的必經(jīng)步驟。

驗(yàn)證器的狀態(tài)如下：

對(duì)于一段可能包含多個(gè)module的交易腳本，進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果返回ok，或者各種不滿足條件的報(bào)錯(cuò)。

Move的模塊的二進(jìn)制格式里面編碼了一系列實(shí)體的集合，這些實(shí)體都放在一個(gè)table里面， 包括常量，類型簽，結(jié)構(gòu)體定義以及過(guò)程定義。檢測(cè)過(guò)程主要有三類：

· 結(jié)構(gòu)體合法檢查： 保證字節(jié)碼的table的完整性（well-formed）， 檢測(cè)的錯(cuò)誤非法的table index， 重復(fù)的資源實(shí)體以及非法的類型簽名，例如引用了一個(gè)引用等

· 過(guò)程定義的語(yǔ)義檢測(cè)：包括參數(shù)類型錯(cuò)誤，懸垂索引以及資源重復(fù)定義。

· 鏈接時(shí)錯(cuò)誤，非法調(diào)用內(nèi)部過(guò)程，或者鏈接一個(gè)聲明和定義不匹配的流程。

下面重點(diǎn)解釋下語(yǔ)義檢測(cè)和鏈接時(shí)錯(cuò)誤檢測(cè)。

Control-flow graph construction

驗(yàn)證器會(huì)首先創(chuàng)建一個(gè)bytescode的BasicBlock的控制流圖，一個(gè)BasicBlock可以理解為中途沒(méi)有分支指令的指令塊。

Stack balance checking

檢測(cè)棧里面被調(diào)用者的訪問(wèn)范圍，保證合約的被調(diào)用者不能訪問(wèn)到調(diào)用者的?？臻g。例如一個(gè)過(guò)程被執(zhí)行的時(shí)候，調(diào)用者首先在CallStackFrame里面初始化局部變量，然后將局部變量放入到棧里面，假設(shè)當(dāng)前棧的高度是n，那么有效的bytecode必須滿足不變性： 當(dāng)?shù)竭_(dá)basic block的結(jié)束的時(shí)候，棧的高度依然還是n。驗(yàn)證器主要是通過(guò)分析每個(gè)基本塊的指令對(duì)棧的可能影響，保證不操作高度低于n的?？臻g。這里有一個(gè)例外就是，一個(gè)以return結(jié)尾的block，他退出的時(shí)候高度必須是n+m，其中m是過(guò)程返回值的個(gè)數(shù)。（這個(gè)特殊的操作有點(diǎn)匪夷所思，難道是把棧的高度默認(rèn)放在了過(guò)程的第一個(gè)參數(shù)，退出的時(shí)候這樣可以進(jìn)一步的進(jìn)行檢測(cè)？后面確認(rèn)了，確實(shí)是因?yàn)槟壳安恢С侄喾祷刂?，所以才加在一起）?/p>

Type checking

在二進(jìn)制格式里面，局部變量的類型是定義好的，但是棧的value確實(shí)需要推導(dǎo)的。在每個(gè)基本快這種推導(dǎo)和類型檢測(cè)獨(dú)立執(zhí)行的，因?yàn)榍懊姹ＷC了調(diào)用過(guò)程訪問(wèn)的棧的高度是合法的，因此，這個(gè)時(shí)候就能安全的推導(dǎo)棧里面變量的類型了。具體檢測(cè)就是給Value Stack維護(hù)了一個(gè)對(duì)應(yīng)的Type Stack，執(zhí)行的時(shí)候TypeStack也跟這指令執(zhí)行進(jìn)行pop和push。

Kind checking

kind和type的區(qū)別是type可能包含別名。 kind的檢查主要檢資源是滿足

· 不可雙花

· 不可銷(xiāo)毀

· 必有歸屬（返回值必須被接受）

對(duì)于非資源類型的話，就沒(méi)有這些限制了。

reference checking

引用的語(yǔ)法包括可變引用，不可變引用。所以引用檢測(cè)結(jié)合了動(dòng)態(tài)和靜態(tài)分析。 靜態(tài)分析利用類似rust類型系統(tǒng)的borrow checking機(jī)制，保證：1. 所以引用必須指向的是一個(gè)已經(jīng)被分配的存儲(chǔ)上，防止懸空； 2. 所有的引用都有安全的讀寫(xiě)權(quán)限，引用訪問(wèn)既可以共享，也可以排斥（也就是有限的讀寫(xiě)權(quán)限）。

為了保證2點(diǎn)， BorrowGlobal調(diào)用的時(shí)候會(huì)動(dòng)態(tài)的對(duì)全局變量的引用進(jìn)行了計(jì)數(shù)， 解釋器會(huì)對(duì)每個(gè)發(fā)布了的資源進(jìn)行判斷，如果被borrow或者move了，再次引用就會(huì)報(bào)錯(cuò)。

Linking with global state

鏈接的時(shí)候還需要對(duì)鏈接的對(duì)象和聲明是否匹配，過(guò)程的訪問(wèn)控制等做再次的檢查。

以上就是目前Move的大部分的靜態(tài)驗(yàn)證了?？梢钥吹矫總€(gè)流程都有非常嚴(yán)格的分析和限制，最大程度的保證Resouce的安全轉(zhuǎn)移和訪問(wèn)。

最后將虛擬機(jī)所有的狀態(tài)和轉(zhuǎn)移總結(jié)如下：

Move虛擬機(jī)通過(guò)執(zhí)行區(qū)塊交易里面的腳本實(shí)現(xiàn)全局狀態(tài)Σ的轉(zhuǎn)移。E表示交易腳本產(chǎn)生的針對(duì)某個(gè)賬戶的狀態(tài)修改集（可以理解為XuperChain的讀寫(xiě)集）：

虛擬機(jī)會(huì)順序執(zhí)行區(qū)塊的每個(gè)交易，產(chǎn)生一系列的E，并且前一個(gè)E在后面交易執(zhí)行的時(shí)候是生效的。

當(dāng)前vm是串行執(zhí)行交易，然后產(chǎn)生一系列的讀寫(xiě)集。 但是Move在設(shè)計(jì)的時(shí)候，已經(jīng)考慮到了預(yù)測(cè)執(zhí)行產(chǎn)生讀寫(xiě)集，然后合并的時(shí)候根據(jù)資源的access path（可以對(duì)比與XuperChain的讀寫(xiě)集版本）進(jìn)行沖突檢測(cè)來(lái)解決沖突。。

最后將講到了未來(lái)的規(guī)劃，重點(diǎn)還是完善類型系統(tǒng)，提供更多類庫(kù)支持。

這個(gè)白皮書(shū)分享系列到此為止，可以整體可以看到，Move通過(guò)借助logic type，module。 system在資源的轉(zhuǎn)移控制上面做了大量的靜態(tài)檢測(cè)來(lái)保證資產(chǎn)轉(zhuǎn)移的安全，相對(duì)EVM來(lái)說(shuō)，避免了很多問(wèn)題，Libra主網(wǎng)上線之后，在DeFi領(lǐng)域可能應(yīng)該會(huì)對(duì)以太坊的DeFi Dapp造成不小的沖擊。