diff --git a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/BuildInfo.yaml b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/BuildInfo.yaml index 28e34cd3234a0..b0368d198af7f 100644 --- a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/BuildInfo.yaml +++ b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/BuildInfo.yaml @@ -175,7 +175,7 @@ compiled_package_info: ? address: "00000000000000000000000000000001" name: XUS : DiemFramework - source_digest: C5415C7DFBC3B6BC4AB994BFE0B6B8C580089AD7D664589FF329434BA328B3AD + source_digest: 8728DA1AAB23BC8D232C36BB5800CD53D16D26533F5B895203D6C5EAE22C4EEA build_flags: dev_mode: false test_mode: false diff --git a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiToken.mv b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiToken.mv index b19bdb21f3b04..5e550a09edc09 100644 Binary files a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiToken.mv and b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiToken.mv differ diff --git a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiTokenBalance.mv b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiTokenBalance.mv index 37cb55e8e832e..7a2c139b7d503 100644 Binary files a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiTokenBalance.mv and b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiTokenBalance.mv differ diff --git a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/docs/MultiToken.md b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/docs/MultiToken.md index 79f4d8f9d0193..4017522e1db14 100644 --- a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/docs/MultiToken.md +++ b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/docs/MultiToken.md @@ -23,6 +23,7 @@ - [Function `split`](#0x1_MultiToken_split) - [Function `initialize_multi_token`](#0x1_MultiToken_initialize_multi_token) - [Function `create`](#0x1_MultiToken_create) +- [Module Specification](#@Module_Specification_1) 
use 0x1::Errors;
@@ -451,6 +452,23 @@ Returns the supply of tokens with id on the chain.
 
 
 
+
+
+

+Specification
+
+
+
+
let addr = GUID::id_creator_address(id);
+let token_collection = get_tokens<TokenType>(addr);
+let min_token_idx = find_token_index_by_id(token_collection,id);
+aborts_if !exists<TokenDataCollection<TokenType>>(addr);
+aborts_if !is_in_tokens(token_collection, id);
+ensures result == token_collection[min_token_idx].supply;
+

+
+
+
 

 
 
@@ -483,6 +501,27 @@ Extract the MultiToken data of the given token into a hot potato wrapper.
 
 
 
+
+
+

+Specification
+
+
+
+
let addr = GUID::id_creator_address(nft.id);
+let token_collection = get_tokens<TokenType>(addr);
+let id = nft.id;
+let min_token_idx = find_token_index_by_id(token_collection, id);
+aborts_if !exists<TokenDataCollection<TokenType>>(addr);
+aborts_if token_collection[min_token_idx].metadata == Option::spec_none();
+aborts_if !is_in_tokens(token_collection, id);
+ensures result == TokenDataWrapper { origin: addr, index: min_token_idx,
+metadata: Option::borrow(token_collection[min_token_idx].metadata)};
+ensures get_tokens<TokenType>(addr)[min_token_idx].metadata == Option::spec_none();
+

+
+
+
 

 
 
@@ -513,6 +552,24 @@ Restore the token in the wrapper back into global storage under original address
 
 
 
+
+
+

+Specification
+
+
+
+
let addr = wrapper.origin;
+let token_collection = get_tokens<TokenType>(addr);
+let item_opt = token_collection[wrapper.index].metadata;
+aborts_if !exists<TokenDataCollection<TokenType>>(addr);
+aborts_if len(token_collection) <= wrapper.index;
+aborts_if item_opt != Option::spec_none();
+ensures get_tokens<TokenType>(addr)[wrapper.index].metadata == Option::spec_some(wrapper.metadata);
+

+
+
+
 

 
 
@@ -534,7 +591,11 @@ Finds the index of token with the given id in the gallery.
 
fun index_of_token<TokenType: store>(gallery: &vector<TokenData<TokenType>>, id: &GUID::ID): Option<u64> {
     let i = 0;
     let len = Vector::length(gallery);
-    while (i < len) {
+    while ({spec {
+        invariant i >= 0;
+        invariant i <= len(gallery);
+        invariant forall k in 0..i: gallery[k].token_id.id != id;
+    };(i < len)}) {
         if (GUID::eq_id(&Vector::borrow(gallery, i).token_id, id)) {
             return Option::some(i)
         };
@@ -546,6 +607,21 @@ Finds the index of token with the given id in the gallery.
 
 
 
+
+
+

+Specification
+
+
+
+
let min_token_idx = find_token_index_by_id(gallery, id);
+let post res_id = Option::borrow(result);
+ensures is_in_tokens(gallery, id) <==> (Option::is_some(result) && res_id == min_token_idx);
+ensures result ==  Option::spec_none() <==> !is_in_tokens(gallery, id);
+

+
+
+
 

 
 
@@ -574,6 +650,20 @@ Join two multi tokens and return a multi token with the combined value of the tw
 
 
 
+
+
+

+Specification
+
+
+
+
aborts_if token.id != other.id with EWRONG_TOKEN_ID;
+aborts_if MAX_U64 - token.balance < other.balance with ETOKEN_BALANCE_OVERFLOWS;
+ensures token.balance == old(token).balance + other.balance;
+

+
+
+
 

 
 
@@ -606,6 +696,21 @@ Split the token into two tokens, one with balance amount and the ot
 
 
 
+
+
+

+Specification
+
+
+
+
aborts_if token.balance < amount with EAMOUNT_EXCEEDS_TOKEN_BALANCE;
+ensures result_1.balance == token.balance - amount;
+ensures result_2.balance == amount;
+ensures result_1.id == result_2.id;
+

+
+
+
 

 
 
@@ -634,6 +739,21 @@ Initialize this module, to be called in genesis.
 
 
 
+
+
+

+Specification
+
+
+
+
let addr = Signer::address_of(account);
+aborts_if addr != ADMIN;
+aborts_if exists<Admin>(addr);
+ensures exists<Admin>(addr);
+

+
+
+
 

 
 
@@ -681,3 +801,59 @@ Create a TokenData<
 
 
 
+
+

+Specification
+
+
+
+
let addr = Signer::address_of(account);
+let post post_tokens = get_tokens<TokenType>(addr);
+aborts_if !exists<Admin>(ADMIN);
+aborts_if exists<GUID::Generator>(addr) && global<GUID::Generator>(addr).counter + 1 > MAX_U64;
+ensures result.balance == amount;
+ensures GUID::id_creator_address(result.id) == addr;
+ensures exists<TokenDataCollection<TokenType>>(addr);
+ensures post_tokens[len(post_tokens) - 1] ==
+        TokenData<TokenType> {metadata: Option::spec_some(metadata), token_id: GUID::GUID {id: result.id}, content_uri, supply:amount};
+

+
+
+
+

+
+
+
+## Module Specification
+
+
+
+
+
+
+
fun get_tokens<TokenType>(addr: address): vector<TokenData<TokenType>>{
+   global<TokenDataCollection<TokenType>>(addr).tokens
+}
+

+
+
+
+
+
+
+
+
fun is_in_tokens<TokenType>(tokens: vector<TokenData<TokenType>>, token_id: GUID::ID): bool {
+   exists token in tokens: token.token_id.id == token_id
+}
+

+
+
+
+
+
+
+
+
fun find_token_index_by_id<TokenType>(tokens: vector<TokenData<TokenType>>, id: GUID::ID): u64 {
+   choose min i in range(tokens) where tokens[i].token_id.id == id
+}
+

diff --git a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/docs/MultiTokenBalance.md b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/docs/MultiTokenBalance.md
index 588d86e0573be..aad95c08c3f53 100644
--- a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/docs/MultiTokenBalance.md
+++ b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/docs/MultiTokenBalance.md
@@ -52,6 +52,52 @@ Balance holding tokens of TokenType as well as information of appro
 
 
 
+
+
+

+Specification
+
+
+
+
invariant forall i1 in range(gallery), i2 in range(gallery) where gallery[i1].id == gallery[i2].id:
+i1 == i2;
+

+
+
+
+
+
+
+
+
fun get_token_balance_gallery<TokenType>(addr: address): vector<Token<TokenType>>{
+   global<TokenBalance<TokenType>>(addr).gallery
+}
+

+
+
+
+
+
+
+
+
fun is_in_gallery<TokenType>(gallery: vector<Token<TokenType>>, token_id: GUID::ID): bool {
+   exists i in range(gallery): gallery[i].id == token_id
+}
+

+
+
+
+
+
+
+
+
fun find_token_index_by_id<TokenType>(gallery: vector<Token<TokenType>>, id: GUID::ID): u64 {
+   choose i in range(gallery) where gallery[i].id == id
+}
+

+
+
+
 

 
 
@@ -159,12 +205,35 @@ gallery, we combine it with the new one and make a token of greater value.
         MultiToken::join<TokenType>(&mut token, original_token);
     };
     let gallery = &mut borrow_global_mut<TokenBalance<TokenType>>(owner).gallery;
-    Vector::push_back(gallery, token)
+    Vector::push_back(gallery, token);
 }
 

 
 
 
+
+
+

+Specification
+
+
+
+
let gallery = get_token_balance_gallery<TokenType>(owner);
+let token_bal = token.balance;
+let min_token_idx = find_token_index_by_id(gallery, token.id);
+let balance = gallery[min_token_idx].balance;
+let post post_gallery = get_token_balance_gallery<TokenType>(owner);
+aborts_if !exists<TokenBalance<TokenType>>(owner);
+aborts_if is_in_gallery(gallery, token.id) && MAX_U64 - token.balance < balance;
+ensures is_in_gallery(gallery, token.id) ==> len(gallery) == len(post_gallery);
+ensures !is_in_gallery(gallery, token.id) ==> len(gallery) + 1 == len(post_gallery);
+ensures is_in_gallery(gallery, token.id) ==> post_gallery[len(gallery) - 1].balance ==
+    token_bal + gallery[min_token_idx].balance;
+ensures post_gallery[len(post_gallery) - 1].id == token.id;
+

+
+
+
 

 
 
@@ -195,6 +264,21 @@ Remove a token of certain id from the owner's gallery and return it.
 
 
 
+
+
+

+Specification
+
+
+
+
let gallery = get_token_balance_gallery<TokenType>(owner);
+aborts_if !exists<TokenBalance<TokenType>>(owner);
+aborts_if !is_in_gallery(gallery, id);
+ensures !is_in_gallery(get_token_balance_gallery<TokenType>(owner), id);
+

+
+
+
 

 
 
@@ -216,7 +300,11 @@ Finds the index of token with the given id in the gallery.
 
fun index_of_token<TokenType: store>(gallery: &vector<Token<TokenType>>, id: &GUID::ID): Option<u64> {
     let i = 0;
     let len = Vector::length(gallery);
-    while (i < len) {
+    while ({spec {
+        invariant i >= 0;
+        invariant i <= len(gallery);
+        invariant forall k in 0..i: gallery[k].id != id;
+    };(i < len)}) {
         if (MultiToken::id<TokenType>(Vector::borrow(gallery, i)) == *id) {
             return Option::some(i)
         };
@@ -228,6 +316,21 @@ Finds the index of token with the given id in the gallery.
 
 
 
+
+
+

+Specification
+
+
+
+
let min_token_idx = choose min i in range(gallery) where gallery[i].id == id;
+let post res_id = Option::borrow(result);
+ensures is_in_gallery(gallery, id) <==> (Option::is_some(result) && res_id == min_token_idx);
+ensures result ==  Option::spec_none() <==> !is_in_gallery(gallery, id);
+

+
+
+
 

 
 
@@ -253,6 +356,19 @@ Returns whether the owner has a token with given id.
 
 
 
+
+
+

+Specification
+
+
+
+
let gallery = global<TokenBalance<TokenType>>(owner).gallery;
+ensures result <==> is_in_gallery(gallery, token_id);
+

+
+
+
 

 
 
@@ -286,6 +402,21 @@ Returns whether the owner has a token with given id.
 
 
 
+
+
+

+Specification
+
+
+
+
let gallery = get_token_balance_gallery<TokenType>(owner);
+let min_token_idx = find_token_index_by_id(gallery, token_id);
+ensures !is_in_gallery(gallery, token_id) ==> result == 0;
+ensures is_in_gallery(gallery, token_id) ==> result == gallery[min_token_idx].balance;
+

+
+
+
 

 
 
@@ -335,13 +466,54 @@ approved operator of the owner.
 
         // Add tokens to `to`'s gallery
         add_to_gallery<TokenType>(to, to_token);
-    }
+    };
+
     // TODO: add event emission
 }
 

 
 
 
+
+
+

+Specification
+
+
+
+
let owner = Signer::address_of(account);
+let gallery_owner = get_token_balance_gallery<TokenType>(owner);
+let gallery_to = get_token_balance_gallery<TokenType>(to);
+let post post_gallery_owner = get_token_balance_gallery<TokenType>(owner);
+let post post_gallery_to = get_token_balance_gallery<TokenType>(to);
+let id = GUID::create_id(creator, creation_num);
+let min_token_idx = find_token_index_by_id(gallery_owner, id);
+let min_token_idx_to = find_token_index_by_id(gallery_to, id);
+aborts_if amount <= 0;
+aborts_if !exists<TokenBalance<TokenType>>(owner);
+aborts_if !exists<TokenBalance<TokenType>>(to);
+aborts_if !is_in_gallery(gallery_owner, id);
+aborts_if amount > gallery_owner[min_token_idx].balance;
+aborts_if owner != to && is_in_gallery(gallery_to, id) && MAX_U64 - amount < gallery_to[min_token_idx_to].balance;
+ensures (gallery_owner[min_token_idx].balance == amount && to != owner) ==>
+        !is_in_gallery(post_gallery_owner, id);
+ensures gallery_owner[min_token_idx].balance > amount ==>
+        post_gallery_owner[len(post_gallery_owner) - 1].id == id;
+ensures post_gallery_to[len(post_gallery_to) - 1].id == id;
+ensures (gallery_owner[min_token_idx].balance > amount && to != owner) ==>
+        post_gallery_owner[len(post_gallery_owner) - 1].balance ==
+          gallery_owner[min_token_idx].balance - amount;
+ensures (to != owner && !is_in_gallery(gallery_to, id) )==>
+        post_gallery_to[len(post_gallery_to) - 1].balance == amount;
+ensures (to != owner && is_in_gallery(gallery_to, id) )==>
+        post_gallery_to[len(post_gallery_to) - 1].balance ==
+           gallery_to[min_token_idx_to].balance + amount;
+ensures to == owner ==> post_gallery_owner[len(post_gallery_owner) - 1].balance ==
+                        gallery_owner[min_token_idx].balance;
+

+
+
+
 

 
 
@@ -367,4 +539,18 @@ approved operator of the owner.
 
 
 
+
+
+

+Specification
+
+
+
+
let addr = Signer::address_of(account);
+aborts_if exists<TokenBalance<TokenType>>(addr);
+ensures exists<TokenBalance<TokenType>>(addr);
+

+
+
+
 

diff --git a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/source_maps/MultiToken.mvsm b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/source_maps/MultiToken.mvsm
index 795aaf0f6c5fb..8db4715832701 100644
Binary files a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/source_maps/MultiToken.mvsm and b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/source_maps/MultiToken.mvsm differ
diff --git a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/source_maps/MultiTokenBalance.mvsm b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/source_maps/MultiTokenBalance.mvsm
index 5056a63dc6863..c7da2458dcd11 100644
Binary files a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/source_maps/MultiTokenBalance.mvsm and b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/source_maps/MultiTokenBalance.mvsm differ
diff --git a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/sources/MultiToken.move b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/sources/MultiToken.move
index 81c630ceb689c..54580bb7a269c 100644
--- a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/sources/MultiToken.move
+++ b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/sources/MultiToken.move
@@ -53,6 +53,18 @@ module MultiToken {
         tokens: vector>,
     }
 
+    spec fun get_tokens(addr: address): vector>{
+        global>(addr).tokens
+    }
+
+    spec fun is_in_tokens(tokens: vector>, token_id: GUID::ID): bool {
+        exists token in tokens: token.token_id.id == token_id
+    }
+
+    spec fun find_token_index_by_id(tokens: vector>, id: GUID::ID): u64 {
+        choose min i in range(tokens) where tokens[i].token_id.id == id
+    }
+
     const ADMIN: address = @0xa550c18;
     const MAX_U64: u64 = 18446744073709551615u64;
     // Error codes
@@ -89,6 +101,15 @@ module MultiToken {
         Vector::borrow(tokens, index).supply
     }
 
+    spec supply {
+        let addr = GUID::id_creator_address(id);
+        let token_collection = get_tokens(addr);
+        let min_token_idx = find_token_index_by_id(token_collection,id);
+        aborts_if !exists>(addr);
+        aborts_if !is_in_tokens(token_collection, id);
+        ensures result == token_collection[min_token_idx].supply;
+    }
+
     /// Extract the MultiToken data of the given token into a hot potato wrapper.
     public fun extract_token(nft: &Token): TokenDataWrapper acquires TokenDataCollection {
         let owner_addr = GUID::id_creator_address(&nft.id);
@@ -101,6 +122,19 @@ module MultiToken {
         TokenDataWrapper { origin: owner_addr, index, metadata: Option::extract(item_opt) }
     }
 
+    spec extract_token {
+        let addr = GUID::id_creator_address(nft.id);
+        let token_collection = get_tokens(addr);
+        let id = nft.id;
+        let min_token_idx = find_token_index_by_id(token_collection, id);
+        aborts_if !exists>(addr);
+        aborts_if token_collection[min_token_idx].metadata == Option::spec_none();
+        aborts_if !is_in_tokens(token_collection, id);
+        ensures result == TokenDataWrapper { origin: addr, index: min_token_idx,
+        metadata: Option::borrow(token_collection[min_token_idx].metadata)};
+        ensures get_tokens(addr)[min_token_idx].metadata == Option::spec_none();
+    }
+
     /// Restore the token in the wrapper back into global storage under original address.
     public fun restore_token(wrapper: TokenDataWrapper) acquires TokenDataCollection {
         let TokenDataWrapper { origin, index, metadata } = wrapper;
@@ -111,11 +145,25 @@ module MultiToken {
         Option::fill(item_opt, metadata);
     }
 
+    spec restore_token {
+        let addr = wrapper.origin;
+        let token_collection = get_tokens(addr);
+        let item_opt = token_collection[wrapper.index].metadata;
+        aborts_if !exists>(addr);
+        aborts_if len(token_collection) <= wrapper.index;
+        aborts_if item_opt != Option::spec_none();
+        ensures get_tokens(addr)[wrapper.index].metadata == Option::spec_some(wrapper.metadata);
+    }
+
     /// Finds the index of token with the given id in the gallery.
     fun index_of_token(gallery: &vector>, id: &GUID::ID): Option {
         let i = 0;
         let len = Vector::length(gallery);
-        while (i < len) {
+        while ({spec {
+            invariant i >= 0;
+            invariant i <= len(gallery);
+            invariant forall k in 0..i: gallery[k].token_id.id != id;
+        };(i < len)}) {
             if (GUID::eq_id(&Vector::borrow(gallery, i).token_id, id)) {
                 return Option::some(i)
             };
@@ -124,6 +172,13 @@ module MultiToken {
         Option::none()
     }
 
+    spec index_of_token{
+        let min_token_idx = find_token_index_by_id(gallery, id);
+        let post res_id = Option::borrow(result);
+        ensures is_in_tokens(gallery, id) <==> (Option::is_some(result) && res_id == min_token_idx);
+        ensures result ==  Option::spec_none() <==> !is_in_tokens(gallery, id);
+    }
+
     /// Join two multi tokens and return a multi token with the combined value of the two.
     public fun join(token: &mut Token, other: Token) {
         let Token { id, balance } = other;
@@ -132,6 +187,12 @@ module MultiToken {
         token.balance = token.balance + balance
     }
 
+    spec join{
+        aborts_if token.id != other.id with EWRONG_TOKEN_ID;
+        aborts_if MAX_U64 - token.balance < other.balance with ETOKEN_BALANCE_OVERFLOWS;
+        ensures token.balance == old(token).balance + other.balance;
+    }
+
     /// Split the token into two tokens, one with balance `amount` and the other one with balance
     public fun split(token: Token, amount: u64): (Token, Token) {
         assert!(token.balance >= amount, EAMOUNT_EXCEEDS_TOKEN_BALANCE);
@@ -144,6 +205,13 @@ module MultiToken {
         } )
     }
 
+    spec split {
+        aborts_if token.balance < amount with EAMOUNT_EXCEEDS_TOKEN_BALANCE;
+        ensures result_1.balance == token.balance - amount;
+        ensures result_2.balance == amount;
+        ensures result_1.id == result_2.id;
+    }
+
     /// Initialize this module, to be called in genesis.
     public fun initialize_multi_token(account: signer) {
         assert!(Signer::address_of(&account) == ADMIN, ENOT_ADMIN);
@@ -152,6 +220,13 @@ module MultiToken {
         })
     }
 
+    spec initialize_multi_token{
+        let addr = Signer::address_of(account);
+        aborts_if addr != ADMIN;
+        aborts_if exists(addr);
+        ensures exists(addr);
+    }
+
     /// Create a` TokenData` that wraps `metadata` and with balance of `amount`
     public fun create(
         account: &signer, metadata: TokenType, content_uri: vector, amount: u64
@@ -177,5 +252,20 @@ module MultiToken {
         );
         Token { id, balance: amount }
     }
+
+    spec create {
+        let addr = Signer::address_of(account);
+        let post post_tokens = get_tokens(addr);
+
+        aborts_if !exists(ADMIN);
+        aborts_if exists(addr) && global(addr).counter + 1 > MAX_U64;
+
+        ensures result.balance == amount;
+        ensures GUID::id_creator_address(result.id) == addr;
+        ensures exists>(addr);
+        ensures post_tokens[len(post_tokens) - 1] ==
+                TokenData {metadata: Option::spec_some(metadata), token_id: GUID::GUID {id: result.id}, content_uri, supply:amount};
+    }
+
 }
 }
diff --git a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/sources/MultiTokenBalance.move b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/sources/MultiTokenBalance.move
index ac56b85741875..6f998a7891e74 100644
--- a/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/sources/MultiTokenBalance.move
+++ b/diem-move/diem-framework/experimental/releases/artifacts/current/build/DiemExperimental/sources/MultiTokenBalance.move
@@ -12,6 +12,23 @@ module DiemFramework::MultiTokenBalance {
         gallery: vector>
     }
 
+    spec TokenBalance {
+        invariant forall i1 in range(gallery), i2 in range(gallery) where gallery[i1].id == gallery[i2].id:
+        i1 == i2;
+    }
+
+    spec fun get_token_balance_gallery(addr: address): vector>{
+        global>(addr).gallery
+    }
+
+    spec fun is_in_gallery(gallery: vector>, token_id: GUID::ID): bool {
+        exists i in range(gallery): gallery[i].id == token_id
+    }
+
+    spec fun find_token_index_by_id(gallery: vector>, id: GUID::ID): u64 {
+        choose i in range(gallery) where gallery[i].id == id
+    }
+
     const MAX_U64: u128 = 18446744073709551615u128;
     // Error codes
     const EID_NOT_FOUND: u64 = 0;
@@ -22,6 +39,8 @@ module DiemFramework::MultiTokenBalance {
     const ENOT_OPERATOR: u64 = 5;
     const EINVALID_APPROVAL_TARGET: u64 = 6;
 
+
+
     /// Add a token to the owner's gallery. If there is already a token of the same id in the
     /// gallery, we combine it with the new one and make a token of greater value.
     public fun add_to_gallery(owner: address, token: Token)
@@ -35,7 +54,27 @@ module DiemFramework::MultiTokenBalance {
             MultiToken::join(&mut token, original_token);
         };
         let gallery = &mut borrow_global_mut>(owner).gallery;
-        Vector::push_back(gallery, token)
+        Vector::push_back(gallery, token);
+    }
+
+
+
+    spec add_to_gallery {
+        let gallery = get_token_balance_gallery(owner);
+        let token_bal = token.balance;
+        let min_token_idx = find_token_index_by_id(gallery, token.id);
+        let balance = gallery[min_token_idx].balance;
+        let post post_gallery = get_token_balance_gallery(owner);
+
+        aborts_if !exists>(owner);
+        aborts_if is_in_gallery(gallery, token.id) && MAX_U64 - token.balance < balance;
+
+        ensures is_in_gallery(gallery, token.id) ==> len(gallery) == len(post_gallery);
+        ensures !is_in_gallery(gallery, token.id) ==> len(gallery) + 1 == len(post_gallery);
+
+        ensures is_in_gallery(gallery, token.id) ==> post_gallery[len(gallery) - 1].balance ==
+            token_bal + gallery[min_token_idx].balance;
+        ensures post_gallery[len(post_gallery) - 1].id == token.id;
     }
 
     /// Remove a token of certain id from the owner's gallery and return it.
@@ -48,11 +87,22 @@ module DiemFramework::MultiTokenBalance {
         Vector::remove(gallery, Option::extract(&mut index_opt))
     }
 
+    spec remove_from_gallery {
+        let gallery = get_token_balance_gallery(owner);
+        aborts_if !exists>(owner);
+        aborts_if !is_in_gallery(gallery, id);
+        ensures !is_in_gallery(get_token_balance_gallery(owner), id);
+    }
+
     /// Finds the index of token with the given id in the gallery.
     fun index_of_token(gallery: &vector>, id: &GUID::ID): Option {
         let i = 0;
         let len = Vector::length(gallery);
-        while (i < len) {
+        while ({spec {
+            invariant i >= 0;
+            invariant i <= len(gallery);
+            invariant forall k in 0..i: gallery[k].id != id;
+        };(i < len)}) {
             if (MultiToken::id(Vector::borrow(gallery, i)) == *id) {
                 return Option::some(i)
             };
@@ -61,11 +111,23 @@ module DiemFramework::MultiTokenBalance {
         Option::none()
     }
 
+    spec index_of_token{
+        let min_token_idx = choose min i in range(gallery) where gallery[i].id == id;
+        let post res_id = Option::borrow(result);
+        ensures is_in_gallery(gallery, id) <==> (Option::is_some(result) && res_id == min_token_idx);
+        ensures result ==  Option::spec_none() <==> !is_in_gallery(gallery, id);
+    }
+
     /// Returns whether the owner has a token with given id.
     public fun has_token(owner: address, token_id: &GUID::ID): bool acquires TokenBalance {
         Option::is_some(&index_of_token(&borrow_global>(owner).gallery, token_id))
     }
 
+    spec has_token {
+        let gallery = global>(owner).gallery;
+        ensures result <==> is_in_gallery(gallery, token_id);
+    }
+
     public fun get_token_balance(owner: address, token_id: &GUID::ID
     ): u64 acquires TokenBalance {
         let gallery = &borrow_global>(owner).gallery;
@@ -79,6 +141,13 @@ module DiemFramework::MultiTokenBalance {
         }
     }
 
+    spec get_token_balance {
+        let gallery = get_token_balance_gallery(owner);
+        let min_token_idx = find_token_index_by_id(gallery, token_id);
+        ensures !is_in_gallery(gallery, token_id) ==> result == 0;
+        ensures is_in_gallery(gallery, token_id) ==> result == gallery[min_token_idx].balance;
+    }
+
     /// Transfer `amount` of token with id `GUID::id(creator, creation_num)` from `owner`'s
     /// balance to `to`'s balance. This operation has to be done by either the owner or an
     /// approved operator of the owner.
@@ -111,12 +180,60 @@ module DiemFramework::MultiTokenBalance {
 
             // Add tokens to `to`'s gallery
             add_to_gallery(to, to_token);
-        }
+        };
+
         // TODO: add event emission
     }
 
+    spec transfer_multi_token_between_galleries {
+        let owner = Signer::address_of(account);
+        let gallery_owner = get_token_balance_gallery(owner);
+        let gallery_to = get_token_balance_gallery(to);
+        let post post_gallery_owner = get_token_balance_gallery(owner);
+        let post post_gallery_to = get_token_balance_gallery(to);
+
+        let id = GUID::create_id(creator, creation_num);
+
+        let min_token_idx = find_token_index_by_id(gallery_owner, id);
+        let min_token_idx_to = find_token_index_by_id(gallery_to, id);
+
+        aborts_if amount <= 0;
+        aborts_if !exists>(owner);
+        aborts_if !exists>(to);
+        aborts_if !is_in_gallery(gallery_owner, id);
+        aborts_if amount > gallery_owner[min_token_idx].balance;
+        aborts_if owner != to && is_in_gallery(gallery_to, id) && MAX_U64 - amount < gallery_to[min_token_idx_to].balance;
+
+        ensures (gallery_owner[min_token_idx].balance == amount && to != owner) ==>
+                !is_in_gallery(post_gallery_owner, id);
+
+        ensures gallery_owner[min_token_idx].balance > amount ==>
+                post_gallery_owner[len(post_gallery_owner) - 1].id == id;
+        ensures post_gallery_to[len(post_gallery_to) - 1].id == id;
+
+        ensures (gallery_owner[min_token_idx].balance > amount && to != owner) ==>
+                post_gallery_owner[len(post_gallery_owner) - 1].balance ==
+                  gallery_owner[min_token_idx].balance - amount;
+
+        ensures (to != owner && !is_in_gallery(gallery_to, id) )==>
+                post_gallery_to[len(post_gallery_to) - 1].balance == amount;
+        ensures (to != owner && is_in_gallery(gallery_to, id) )==>
+                post_gallery_to[len(post_gallery_to) - 1].balance ==
+                   gallery_to[min_token_idx_to].balance + amount;
+
+        ensures to == owner ==> post_gallery_owner[len(post_gallery_owner) - 1].balance ==
+                                gallery_owner[min_token_idx].balance;
+
+    }
+
     public fun publish_balance(account: &signer) {
         assert!(!exists>(Signer::address_of(account)), EBALANCE_ALREADY_PUBLISHED);
         move_to(account, TokenBalance { gallery: Vector::empty() });
     }
+
+    spec publish_balance {
+        let addr = Signer::address_of(account);
+        aborts_if exists>(addr);
+        ensures exists>(addr);
+    }
 }
diff --git a/diem-move/diem-framework/experimental/sources/MultiToken.move b/diem-move/diem-framework/experimental/sources/MultiToken.move
index 81c630ceb689c..54580bb7a269c 100644
--- a/diem-move/diem-framework/experimental/sources/MultiToken.move
+++ b/diem-move/diem-framework/experimental/sources/MultiToken.move
@@ -53,6 +53,18 @@ module MultiToken {
         tokens: vector>,
     }
 
+    spec fun get_tokens(addr: address): vector>{
+        global>(addr).tokens
+    }
+
+    spec fun is_in_tokens(tokens: vector>, token_id: GUID::ID): bool {
+        exists token in tokens: token.token_id.id == token_id
+    }
+
+    spec fun find_token_index_by_id(tokens: vector>, id: GUID::ID): u64 {
+        choose min i in range(tokens) where tokens[i].token_id.id == id
+    }
+
     const ADMIN: address = @0xa550c18;
     const MAX_U64: u64 = 18446744073709551615u64;
     // Error codes
@@ -89,6 +101,15 @@ module MultiToken {
         Vector::borrow(tokens, index).supply
     }
 
+    spec supply {
+        let addr = GUID::id_creator_address(id);
+        let token_collection = get_tokens(addr);
+        let min_token_idx = find_token_index_by_id(token_collection,id);
+        aborts_if !exists>(addr);
+        aborts_if !is_in_tokens(token_collection, id);
+        ensures result == token_collection[min_token_idx].supply;
+    }
+
     /// Extract the MultiToken data of the given token into a hot potato wrapper.
     public fun extract_token(nft: &Token): TokenDataWrapper acquires TokenDataCollection {
         let owner_addr = GUID::id_creator_address(&nft.id);
@@ -101,6 +122,19 @@ module MultiToken {
         TokenDataWrapper { origin: owner_addr, index, metadata: Option::extract(item_opt) }
     }
 
+    spec extract_token {
+        let addr = GUID::id_creator_address(nft.id);
+        let token_collection = get_tokens(addr);
+        let id = nft.id;
+        let min_token_idx = find_token_index_by_id(token_collection, id);
+        aborts_if !exists>(addr);
+        aborts_if token_collection[min_token_idx].metadata == Option::spec_none();
+        aborts_if !is_in_tokens(token_collection, id);
+        ensures result == TokenDataWrapper { origin: addr, index: min_token_idx,
+        metadata: Option::borrow(token_collection[min_token_idx].metadata)};
+        ensures get_tokens(addr)[min_token_idx].metadata == Option::spec_none();
+    }
+
     /// Restore the token in the wrapper back into global storage under original address.
     public fun restore_token(wrapper: TokenDataWrapper) acquires TokenDataCollection {
         let TokenDataWrapper { origin, index, metadata } = wrapper;
@@ -111,11 +145,25 @@ module MultiToken {
         Option::fill(item_opt, metadata);
     }
 
+    spec restore_token {
+        let addr = wrapper.origin;
+        let token_collection = get_tokens(addr);
+        let item_opt = token_collection[wrapper.index].metadata;
+        aborts_if !exists>(addr);
+        aborts_if len(token_collection) <= wrapper.index;
+        aborts_if item_opt != Option::spec_none();
+        ensures get_tokens(addr)[wrapper.index].metadata == Option::spec_some(wrapper.metadata);
+    }
+
     /// Finds the index of token with the given id in the gallery.
     fun index_of_token(gallery: &vector>, id: &GUID::ID): Option {
         let i = 0;
         let len = Vector::length(gallery);
-        while (i < len) {
+        while ({spec {
+            invariant i >= 0;
+            invariant i <= len(gallery);
+            invariant forall k in 0..i: gallery[k].token_id.id != id;
+        };(i < len)}) {
             if (GUID::eq_id(&Vector::borrow(gallery, i).token_id, id)) {
                 return Option::some(i)
             };
@@ -124,6 +172,13 @@ module MultiToken {
         Option::none()
     }
 
+    spec index_of_token{
+        let min_token_idx = find_token_index_by_id(gallery, id);
+        let post res_id = Option::borrow(result);
+        ensures is_in_tokens(gallery, id) <==> (Option::is_some(result) && res_id == min_token_idx);
+        ensures result ==  Option::spec_none() <==> !is_in_tokens(gallery, id);
+    }
+
     /// Join two multi tokens and return a multi token with the combined value of the two.
     public fun join(token: &mut Token, other: Token) {
         let Token { id, balance } = other;
@@ -132,6 +187,12 @@ module MultiToken {
         token.balance = token.balance + balance
     }
 
+    spec join{
+        aborts_if token.id != other.id with EWRONG_TOKEN_ID;
+        aborts_if MAX_U64 - token.balance < other.balance with ETOKEN_BALANCE_OVERFLOWS;
+        ensures token.balance == old(token).balance + other.balance;
+    }
+
     /// Split the token into two tokens, one with balance `amount` and the other one with balance
     public fun split(token: Token, amount: u64): (Token, Token) {
         assert!(token.balance >= amount, EAMOUNT_EXCEEDS_TOKEN_BALANCE);
@@ -144,6 +205,13 @@ module MultiToken {
         } )
     }
 
+    spec split {
+        aborts_if token.balance < amount with EAMOUNT_EXCEEDS_TOKEN_BALANCE;
+        ensures result_1.balance == token.balance - amount;
+        ensures result_2.balance == amount;
+        ensures result_1.id == result_2.id;
+    }
+
     /// Initialize this module, to be called in genesis.
     public fun initialize_multi_token(account: signer) {
         assert!(Signer::address_of(&account) == ADMIN, ENOT_ADMIN);
@@ -152,6 +220,13 @@ module MultiToken {
         })
     }
 
+    spec initialize_multi_token{
+        let addr = Signer::address_of(account);
+        aborts_if addr != ADMIN;
+        aborts_if exists(addr);
+        ensures exists(addr);
+    }
+
     /// Create a` TokenData` that wraps `metadata` and with balance of `amount`
     public fun create(
         account: &signer, metadata: TokenType, content_uri: vector, amount: u64
@@ -177,5 +252,20 @@ module MultiToken {
         );
         Token { id, balance: amount }
     }
+
+    spec create {
+        let addr = Signer::address_of(account);
+        let post post_tokens = get_tokens(addr);
+
+        aborts_if !exists(ADMIN);
+        aborts_if exists(addr) && global(addr).counter + 1 > MAX_U64;
+
+        ensures result.balance == amount;
+        ensures GUID::id_creator_address(result.id) == addr;
+        ensures exists>(addr);
+        ensures post_tokens[len(post_tokens) - 1] ==
+                TokenData {metadata: Option::spec_some(metadata), token_id: GUID::GUID {id: result.id}, content_uri, supply:amount};
+    }
+
 }
 }
diff --git a/diem-move/diem-framework/experimental/sources/MultiTokenBalance.move b/diem-move/diem-framework/experimental/sources/MultiTokenBalance.move
index ac56b85741875..6f998a7891e74 100644
--- a/diem-move/diem-framework/experimental/sources/MultiTokenBalance.move
+++ b/diem-move/diem-framework/experimental/sources/MultiTokenBalance.move
@@ -12,6 +12,23 @@ module DiemFramework::MultiTokenBalance {
         gallery: vector>
     }
 
+    spec TokenBalance {
+        invariant forall i1 in range(gallery), i2 in range(gallery) where gallery[i1].id == gallery[i2].id:
+        i1 == i2;
+    }
+
+    spec fun get_token_balance_gallery(addr: address): vector>{
+        global>(addr).gallery
+    }
+
+    spec fun is_in_gallery(gallery: vector>, token_id: GUID::ID): bool {
+        exists i in range(gallery): gallery[i].id == token_id
+    }
+
+    spec fun find_token_index_by_id(gallery: vector>, id: GUID::ID): u64 {
+        choose i in range(gallery) where gallery[i].id == id
+    }
+
     const MAX_U64: u128 = 18446744073709551615u128;
     // Error codes
     const EID_NOT_FOUND: u64 = 0;
@@ -22,6 +39,8 @@ module DiemFramework::MultiTokenBalance {
     const ENOT_OPERATOR: u64 = 5;
     const EINVALID_APPROVAL_TARGET: u64 = 6;
 
+
+
     /// Add a token to the owner's gallery. If there is already a token of the same id in the
     /// gallery, we combine it with the new one and make a token of greater value.
     public fun add_to_gallery(owner: address, token: Token)
@@ -35,7 +54,27 @@ module DiemFramework::MultiTokenBalance {
             MultiToken::join(&mut token, original_token);
         };
         let gallery = &mut borrow_global_mut>(owner).gallery;
-        Vector::push_back(gallery, token)
+        Vector::push_back(gallery, token);
+    }
+
+
+
+    spec add_to_gallery {
+        let gallery = get_token_balance_gallery(owner);
+        let token_bal = token.balance;
+        let min_token_idx = find_token_index_by_id(gallery, token.id);
+        let balance = gallery[min_token_idx].balance;
+        let post post_gallery = get_token_balance_gallery(owner);
+
+        aborts_if !exists>(owner);
+        aborts_if is_in_gallery(gallery, token.id) && MAX_U64 - token.balance < balance;
+
+        ensures is_in_gallery(gallery, token.id) ==> len(gallery) == len(post_gallery);
+        ensures !is_in_gallery(gallery, token.id) ==> len(gallery) + 1 == len(post_gallery);
+
+        ensures is_in_gallery(gallery, token.id) ==> post_gallery[len(gallery) - 1].balance ==
+            token_bal + gallery[min_token_idx].balance;
+        ensures post_gallery[len(post_gallery) - 1].id == token.id;
     }
 
     /// Remove a token of certain id from the owner's gallery and return it.
@@ -48,11 +87,22 @@ module DiemFramework::MultiTokenBalance {
         Vector::remove(gallery, Option::extract(&mut index_opt))
     }
 
+    spec remove_from_gallery {
+        let gallery = get_token_balance_gallery(owner);
+        aborts_if !exists>(owner);
+        aborts_if !is_in_gallery(gallery, id);
+        ensures !is_in_gallery(get_token_balance_gallery(owner), id);
+    }
+
     /// Finds the index of token with the given id in the gallery.
     fun index_of_token(gallery: &vector>, id: &GUID::ID): Option {
         let i = 0;
         let len = Vector::length(gallery);
-        while (i < len) {
+        while ({spec {
+            invariant i >= 0;
+            invariant i <= len(gallery);
+            invariant forall k in 0..i: gallery[k].id != id;
+        };(i < len)}) {
             if (MultiToken::id(Vector::borrow(gallery, i)) == *id) {
                 return Option::some(i)
             };
@@ -61,11 +111,23 @@ module DiemFramework::MultiTokenBalance {
         Option::none()
     }
 
+    spec index_of_token{
+        let min_token_idx = choose min i in range(gallery) where gallery[i].id == id;
+        let post res_id = Option::borrow(result);
+        ensures is_in_gallery(gallery, id) <==> (Option::is_some(result) && res_id == min_token_idx);
+        ensures result ==  Option::spec_none() <==> !is_in_gallery(gallery, id);
+    }
+
     /// Returns whether the owner has a token with given id.
     public fun has_token(owner: address, token_id: &GUID::ID): bool acquires TokenBalance {
         Option::is_some(&index_of_token(&borrow_global>(owner).gallery, token_id))
     }
 
+    spec has_token {
+        let gallery = global>(owner).gallery;
+        ensures result <==> is_in_gallery(gallery, token_id);
+    }
+
     public fun get_token_balance(owner: address, token_id: &GUID::ID
     ): u64 acquires TokenBalance {
         let gallery = &borrow_global>(owner).gallery;
@@ -79,6 +141,13 @@ module DiemFramework::MultiTokenBalance {
         }
     }
 
+    spec get_token_balance {
+        let gallery = get_token_balance_gallery(owner);
+        let min_token_idx = find_token_index_by_id(gallery, token_id);
+        ensures !is_in_gallery(gallery, token_id) ==> result == 0;
+        ensures is_in_gallery(gallery, token_id) ==> result == gallery[min_token_idx].balance;
+    }
+
     /// Transfer `amount` of token with id `GUID::id(creator, creation_num)` from `owner`'s
     /// balance to `to`'s balance. This operation has to be done by either the owner or an
     /// approved operator of the owner.
@@ -111,12 +180,60 @@ module DiemFramework::MultiTokenBalance {
 
             // Add tokens to `to`'s gallery
             add_to_gallery(to, to_token);
-        }
+        };
+
         // TODO: add event emission
     }
 
+    spec transfer_multi_token_between_galleries {
+        let owner = Signer::address_of(account);
+        let gallery_owner = get_token_balance_gallery(owner);
+        let gallery_to = get_token_balance_gallery(to);
+        let post post_gallery_owner = get_token_balance_gallery(owner);
+        let post post_gallery_to = get_token_balance_gallery(to);
+
+        let id = GUID::create_id(creator, creation_num);
+
+        let min_token_idx = find_token_index_by_id(gallery_owner, id);
+        let min_token_idx_to = find_token_index_by_id(gallery_to, id);
+
+        aborts_if amount <= 0;
+        aborts_if !exists>(owner);
+        aborts_if !exists>(to);
+        aborts_if !is_in_gallery(gallery_owner, id);
+        aborts_if amount > gallery_owner[min_token_idx].balance;
+        aborts_if owner != to && is_in_gallery(gallery_to, id) && MAX_U64 - amount < gallery_to[min_token_idx_to].balance;
+
+        ensures (gallery_owner[min_token_idx].balance == amount && to != owner) ==>
+                !is_in_gallery(post_gallery_owner, id);
+
+        ensures gallery_owner[min_token_idx].balance > amount ==>
+                post_gallery_owner[len(post_gallery_owner) - 1].id == id;
+        ensures post_gallery_to[len(post_gallery_to) - 1].id == id;
+
+        ensures (gallery_owner[min_token_idx].balance > amount && to != owner) ==>
+                post_gallery_owner[len(post_gallery_owner) - 1].balance ==
+                  gallery_owner[min_token_idx].balance - amount;
+
+        ensures (to != owner && !is_in_gallery(gallery_to, id) )==>
+                post_gallery_to[len(post_gallery_to) - 1].balance == amount;
+        ensures (to != owner && is_in_gallery(gallery_to, id) )==>
+                post_gallery_to[len(post_gallery_to) - 1].balance ==
+                   gallery_to[min_token_idx_to].balance + amount;
+
+        ensures to == owner ==> post_gallery_owner[len(post_gallery_owner) - 1].balance ==
+                                gallery_owner[min_token_idx].balance;
+
+    }
+
     public fun publish_balance(account: &signer) {
         assert!(!exists>(Signer::address_of(account)), EBALANCE_ALREADY_PUBLISHED);
         move_to(account, TokenBalance { gallery: Vector::empty() });
     }
+
+    spec publish_balance {
+        let addr = Signer::address_of(account);
+        aborts_if exists>(addr);
+        ensures exists>(addr);
+    }
 }