move語法

白皮書使用了一種半形式化（semi-formal）的描述語言進行了描敘。至于這套描述語言，主要符號解釋如下：

=： 定義

：：= ： 賦值

?： 映射

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

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

通過這些符號，Move定義了如下的語法類型：

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

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

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

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

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

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

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，原因很簡單， unrestricted 結(jié)構(gòu)體被賦值或者復(fù)制的時候，如果有restricted字段，那這個字段不會實際被操作到。

Values：

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

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

Procedures and transaction scripts：

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

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

move解釋器

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

解釋器的定義如下：

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

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

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

Move的指令包括6大類：

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

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

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

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

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

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

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

Bytecode驗證器

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

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

對于一段可能包含多個module的交易腳本，進行驗證，驗證結(jié)果返回ok，或者各種不滿足條件的報錯。

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

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

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

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

下面重點解釋下語義檢測和鏈接時錯誤檢測。

Control-flow graph construction

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

Stack balance checking

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

Type checking

在二進制格式里面，局部變量的類型是定義好的，但是棧的value確實需要推導(dǎo)的。在每個基本快這種推導(dǎo)和類型檢測獨立執(zhí)行的，因為前面保證了調(diào)用過程訪問的棧的高度是合法的，因此，這個時候就能安全的推導(dǎo)棧里面變量的類型了。具體檢測就是給Value Stack維護了一個對應(yīng)的Type Stack，執(zhí)行的時候TypeStack也跟這指令執(zhí)行進行pop和push。

Kind checking

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

· 不可雙花

· 不可銷毀

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

對于非資源類型的話，就沒有這些限制了。

reference checking

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

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

Linking with global state

鏈接的時候還需要對鏈接的對象和聲明是否匹配，過程的訪問控制等做再次的檢查。

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

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

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

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

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

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

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