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造成不小的衝擊。
