move語法

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

=： 定義

：：= ： 賦值

?： 映射

×： product type，也就是表示結構體

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

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

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

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

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

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

· MoveToSender/MoveFrom 在當前賬戶地址下面發布或者刪除對應的資源；

· BorrowField ：獲得結構體的一個字段的引用

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

在Module里面除去被聲明為資源的類型（標記了resource kind），其余的類型統稱為unrestricted types（不受限類型）。資源類型的變量或者字段只能被move，并且資源類型變量的引用不能被解引用，也不能被重復賦值。另外an unrestricted struct不能包含restricted field，原因很簡單， unrestricted 結構體被賦值或者復制的時候，如果有restricted字段，那這個字段不會實際被操作到。

Values：

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

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

Procedures and transaction scripts：

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

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

move解釋器

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

解釋器的定義如下：

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

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

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

Move的指令包括6大類：

· 變量操作： CopyLoc/MoveLoc實現數據從本地變量到棧的拷貝和移動，StoreLoc是講數據存回來到本地

· 常量/數值/邏輯操作

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

· 引用相關的指令，包括ReadRef/WriteRef/ReleaseRef/FreezeRef， 其中FreezeRef轉換一個可變引用到一個不可變引用

· 控制流結構，包括call和return，branch，BranchIfTrue，BranchIfFalse等

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

詳細的指令列表在白皮書的Appendix A已經列出。

Bytecode驗證器

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

驗證器的狀態如下：

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

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

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

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

· 鏈接時錯誤，非法調用內部過程，或者鏈接一個聲明和定義不匹配的流程。

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

Control-flow graph construction

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

Stack balance checking

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

Type checking

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

Kind checking

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

· 不可雙花

· 不可銷毀

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

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

reference checking

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

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

Linking with global state

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

以上就是目前Move的大部分的靜態驗證了。可以看到每個流程都有非常嚴格的分析和限制，最大程度的保證Resouce的安全轉移和訪問。

最后將虛擬機所有的狀態和轉移總結如下：

Move虛擬機通過執行區塊交易里面的腳本實現全局狀態Σ的轉移。E表示交易腳本產生的針對某個賬戶的狀態修改集（可以理解為XuperChain的讀寫集）：

虛擬機會順序執行區塊的每個交易，產生一系列的E，并且前一個E在后面交易執行的時候是生效的。

當前vm是串行執行交易，然后產生一系列的讀寫集。 但是Move在設計的時候，已經考慮到了預測執行產生讀寫集，然后合并的時候根據資源的access path（可以對比與XuperChain的讀寫集版本）進行沖突檢測來解決沖突。。

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

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