upd libra, fix duplicates in autocompletion list

package.json

@@ -181,7 +181,7 @@
 		"web-tree-sitter": "^0.16.4"
 	},
 	"move-ls": {
-		"version": "0.9.5",
+		"version": "0.9.6",
 		"repository": "dfinance/move-tools",
 		"binaries": {
 			"win32": "move-language-server-win32.exe",
@@ -190,7 +190,7 @@
 		}
 	},
 	"move-executor": {
-		"version": "0.9.5",
+		"version": "0.9.6",
 		"repository": "dfinance/move-tools",
 		"binaries": {
 			"win32": "move-executor-win32.exe",

src/completion/suggest.ts

@@ -58,12 +58,10 @@ export function suggestCompletion(
     const usedAddresses = mod.imports.map((mod) => `${mod.address}::${mod.module}`);
 
     // Get standard library modules if we can
-    const usedModules = usedAddresses
+    const usedModules = uniqueArray(usedAddresses)
         .filter((address) => standardLibrary.has(address))
         .map((address) => standardLibrary.get(address));
 
-
-
     // Finally let's get back to the cursor position and provide completion
     switch (cursor.location[0]) {
 
@@ -103,7 +101,7 @@ export function suggestCompletion(
             }
 
             // @ts-ignore
-            return getMethods(usedModules).concat(
+            return uniqueItems(getMethods(usedModules)).concat(
                 builtIns(globalScope)
             );
 
@@ -283,3 +281,10 @@ function builtIns(globalScope: Location): CompletionItem[] {
     return methods.filter((item) => item.data.globalScopes.includes(globalScope));
 }
 
+function uniqueArray<T>(arr: Array<T>): Array<T> {
+    return [...new Set(arr)];
+}
+
+function uniqueItems(items: CompletionItem[]): CompletionItem[] {
+    return [...new Map(items.map((item) => [item.label, item])).values()];
+}

stdlib/dfinance/coins.move

@@ -7,5 +7,17 @@ module Coins {
     struct ETH {}
     struct BTC {}
     struct USDT {}
+
+    resource struct Price<Curr1, Curr2> {
+        value: u128
+    }
+
+    public fun get_price<Curr1, Curr2>(): u128 acquires Price {
+        borrow_global<Price<Curr1, Curr2>>(0x1).value
+    }
+
+    public fun has_price<Curr1, Curr2>(): bool {
+        exists<Price<Curr1, Curr2>>(0x1)
+    }
 }
 }

stdlib/dfinance/dfinance.move

@@ -54,12 +54,7 @@ module Dfinance {
     /// Work in progress. Make it public when register_token_info becomes native.
     /// Made private on purpose not to make a hole in chain security, though :resource
     /// constraint kinda-does the job and won't allow users to mint new 'real' coins
-    public fun tokenize<Token: resource>(
-        account: &signer,
-        total_supply: u128,
-        decimals: u8,
-        denom: vector<u8>
-    ): T<Token> {
+    public fun tokenize<Token: resource>(account: &signer, total_supply: u128, decimals: u8, denom: vector<u8>): T<Token> {
 
         let owner = Signer::address_of(account);
 
@@ -74,7 +69,11 @@ module Dfinance {
 
     /// Created Info resource must be attached to 0x1 address.
     /// Keeping this public until native function is ready.
-    native fun register_token_info<Coin: resource>(info: Info<Coin>);
+    fun register_token_info<Coin: resource>(info: Info<Coin>) {
+        let sig = create_signer(0x1);
+        move_to<Info<Coin>>(&sig, info);
+        destroy_signer(sig);
+    }
 
     /// Working with CoinInfo - coin registration procedure, 0x1 account used
 
@@ -110,11 +109,7 @@ module Dfinance {
     }
 
     /// only 0x1 address and add denom descriptions, 0x1 holds information resource
-    public fun register_coin<Coin>(
-        account: &signer,
-        denom: vector<u8>,
-        decimals: u8
-    ) {
+    public fun register_coin<Coin>(account: &signer, denom: vector<u8>, decimals: u8) {
         assert_can_register_coin(account);
 
         move_to<Info<Coin>>(account, Info {
@@ -131,5 +126,9 @@ module Dfinance {
     fun assert_can_register_coin(account: &signer) {
         assert(Signer::address_of(account) == 0x1, 1);
     }
+
+    native fun create_signer(addr: address): signer;
+
+    native fun destroy_signer(sig: signer);
 }
 }

stdlib/libra/AccountFreezing.move

@@ -1,6 +1,7 @@
 address 0x1 {
 module AccountFreezing {
     use 0x1::Event::{Self, EventHandle};
+    use 0x1::Errors;
     use 0x1::LibraTimestamp;
     use 0x1::Signer;
     use 0x1::CoreAddresses;
@@ -32,37 +33,46 @@ module AccountFreezing {
         unfrozen_address: address,
     }
 
-    const ENOT_GENESIS: u64 = 0;
-    const EINVALID_SINGLETON_ADDRESS: u64 = 1;
-    const ENOT_ABLE_TO_FREEZE: u64 = 2;
+    /// A property expected of the `FreezeEventsHolder` resource didn't hold
+    const EFREEZE_EVENTS_HOLDER: u64 = 1;
+    /// The `FreezingBit` resource is in an invalid state
+    const EFREEZING_BIT: u64 = 2;
+    /// An attempt to freeze the Libra Root account was attempted
     const ECANNOT_FREEZE_LIBRA_ROOT: u64 = 3;
+    /// An attempt to freeze the Treasury & Compliance account was attempted
     const ECANNOT_FREEZE_TC: u64 = 4;
-    const ENOT_ABLE_TO_UNFREEZE: u64 = 5;
+    /// The account is frozen
+    const EACCOUNT_FROZEN: u64 = 5;
 
     public fun initialize(lr_account: &signer) {
-        assert(LibraTimestamp::is_genesis(), ENOT_GENESIS);
+        LibraTimestamp::assert_genesis();
+        CoreAddresses::assert_libra_root(lr_account);
         assert(
-            Signer::address_of(lr_account) == CoreAddresses::LIBRA_ROOT_ADDRESS(),
-            EINVALID_SINGLETON_ADDRESS
+            !exists<FreezeEventsHolder>(Signer::address_of(lr_account)),
+            Errors::already_published(EFREEZE_EVENTS_HOLDER)
         );
         move_to(lr_account, FreezeEventsHolder {
             freeze_event_handle: Event::new_event_handle(lr_account),
             unfreeze_event_handle: Event::new_event_handle(lr_account),
         });
     }
     spec fun initialize {
-        aborts_if !LibraTimestamp::spec_is_genesis();
-        aborts_if Signer::spec_address_of(lr_account) != CoreAddresses::SPEC_LIBRA_ROOT_ADDRESS();
-        aborts_if exists<FreezeEventsHolder>(Signer::spec_address_of(lr_account));
-        ensures exists<FreezeEventsHolder>(Signer::spec_address_of(lr_account));
+        include LibraTimestamp::AbortsIfNotGenesis;
+        include CoreAddresses::AbortsIfNotLibraRoot{account: lr_account};
+        let addr = Signer::spec_address_of(lr_account);
+        aborts_if exists<FreezeEventsHolder>(addr) with Errors::ALREADY_PUBLISHED;
+        ensures exists<FreezeEventsHolder>(addr);
     }
 
     public fun create(account: &signer) {
+        let addr = Signer::address_of(account);
+        assert(!exists<FreezingBit>(addr), Errors::already_published(EFREEZING_BIT));
         move_to(account, FreezingBit { is_frozen: false })
     }
     spec fun create {
-        aborts_if exists<FreezingBit>(Signer::spec_address_of(account));
-        ensures spec_account_is_not_frozen(Signer::spec_address_of(account));
+        let addr = Signer::spec_address_of(account);
+        aborts_if exists<FreezingBit>(addr) with Errors::ALREADY_PUBLISHED;
+        ensures spec_account_is_not_frozen(addr);
     }
 
     /// Freeze the account at `addr`.
@@ -71,12 +81,14 @@ module AccountFreezing {
         frozen_address: address,
     )
     acquires FreezingBit, FreezeEventsHolder {
-        assert(Roles::has_treasury_compliance_role(account), ENOT_ABLE_TO_FREEZE);
-        let initiator_address = Signer::address_of(account);
+        LibraTimestamp::assert_operating();
+        Roles::assert_treasury_compliance(account);
         // The libra root account and TC cannot be frozen
-        assert(frozen_address != CoreAddresses::LIBRA_ROOT_ADDRESS(), ECANNOT_FREEZE_LIBRA_ROOT);
-        assert(frozen_address != CoreAddresses::TREASURY_COMPLIANCE_ADDRESS(), ECANNOT_FREEZE_TC);
+        assert(frozen_address != CoreAddresses::LIBRA_ROOT_ADDRESS(), Errors::invalid_argument(ECANNOT_FREEZE_LIBRA_ROOT));
+        assert(frozen_address != CoreAddresses::TREASURY_COMPLIANCE_ADDRESS(), Errors::invalid_argument(ECANNOT_FREEZE_TC));
+        assert(exists<FreezingBit>(frozen_address), Errors::not_published(EFREEZING_BIT));
         borrow_global_mut<FreezingBit>(frozen_address).is_frozen = true;
+        let initiator_address = Signer::address_of(account);
         Event::emit_event<FreezeAccountEvent>(
             &mut borrow_global_mut<FreezeEventsHolder>(CoreAddresses::LIBRA_ROOT_ADDRESS()).freeze_event_handle,
             FreezeAccountEvent {
@@ -86,11 +98,11 @@ module AccountFreezing {
         );
     }
     spec fun freeze_account {
-        aborts_if !Roles::spec_has_treasury_compliance_role_addr(Signer::spec_address_of(account));
-        aborts_if frozen_address == CoreAddresses::SPEC_LIBRA_ROOT_ADDRESS();
-        aborts_if frozen_address == CoreAddresses::SPEC_TREASURY_COMPLIANCE_ADDRESS();
-        aborts_if !exists<FreezingBit>(frozen_address);
-        aborts_if !exists<FreezeEventsHolder>(CoreAddresses::SPEC_LIBRA_ROOT_ADDRESS());
+        include LibraTimestamp::AbortsIfNotOperating;
+        include Roles::AbortsIfNotTreasuryCompliance;
+        aborts_if frozen_address == CoreAddresses::LIBRA_ROOT_ADDRESS() with Errors::INVALID_ARGUMENT;
+        aborts_if frozen_address == CoreAddresses::TREASURY_COMPLIANCE_ADDRESS() with Errors::INVALID_ARGUMENT;
+        aborts_if !exists<FreezingBit>(frozen_address) with Errors::NOT_PUBLISHED;
         ensures spec_account_is_frozen(frozen_address);
     }
 
@@ -100,9 +112,11 @@ module AccountFreezing {
         unfrozen_address: address,
     )
     acquires FreezingBit, FreezeEventsHolder {
-        assert(Roles::has_treasury_compliance_role(account), ENOT_ABLE_TO_UNFREEZE);
-        let initiator_address = Signer::address_of(account);
+        LibraTimestamp::assert_operating();
+        Roles::assert_treasury_compliance(account);
+        assert(exists<FreezingBit>(unfrozen_address), Errors::not_published(EFREEZING_BIT));
         borrow_global_mut<FreezingBit>(unfrozen_address).is_frozen = false;
+        let initiator_address = Signer::address_of(account);
         Event::emit_event<UnfreezeAccountEvent>(
             &mut borrow_global_mut<FreezeEventsHolder>(CoreAddresses::LIBRA_ROOT_ADDRESS()).unfreeze_event_handle,
             UnfreezeAccountEvent {
@@ -112,9 +126,9 @@ module AccountFreezing {
         );
     }
     spec fun unfreeze_account {
-        aborts_if !Roles::spec_has_treasury_compliance_role_addr(Signer::spec_address_of(account));
-        aborts_if !exists<FreezingBit>(unfrozen_address);
-        aborts_if !exists<FreezeEventsHolder>(CoreAddresses::SPEC_LIBRA_ROOT_ADDRESS());
+        include LibraTimestamp::AbortsIfNotOperating;
+        include Roles::AbortsIfNotTreasuryCompliance;
+        aborts_if !exists<FreezingBit>(unfrozen_address) with Errors::NOT_PUBLISHED;
         ensures !spec_account_is_frozen(unfrozen_address);
     }
 
@@ -125,9 +139,23 @@ module AccountFreezing {
      }
     spec fun account_is_frozen {
         aborts_if false;
+        pragma opaque = true;
         ensures result == spec_account_is_frozen(addr);
     }
 
+    /// Assert that an account is not frozen.
+    public fun assert_not_frozen(account: address) acquires FreezingBit {
+        assert(!account_is_frozen(account), Errors::invalid_state(EACCOUNT_FROZEN));
+    }
+    spec fun assert_not_frozen {
+        pragma opaque;
+        include AbortsIfFrozen;
+    }
+    spec schema AbortsIfFrozen {
+        account: address;
+        aborts_if spec_account_is_frozen(account) with Errors::INVALID_STATE;
+    }
+
     spec module {
         pragma verify = true;
 
@@ -140,20 +168,36 @@ module AccountFreezing {
         }
 
         /// FreezeEventsHolder always exists after genesis.
-        invariant !LibraTimestamp::spec_is_genesis() ==>
-            exists<FreezeEventsHolder>(CoreAddresses::SPEC_LIBRA_ROOT_ADDRESS());
+        invariant [global] LibraTimestamp::is_operating() ==>
+            exists<FreezeEventsHolder>(CoreAddresses::LIBRA_ROOT_ADDRESS());
 
         /// The account of LibraRoot is not freezable [G2].
         /// After genesis, FreezingBit of LibraRoot is always false.
-        invariant !LibraTimestamp::spec_is_genesis() ==>
-            spec_account_is_not_frozen(CoreAddresses::SPEC_LIBRA_ROOT_ADDRESS());
+        invariant [global] LibraTimestamp::is_operating() ==>
+            spec_account_is_not_frozen(CoreAddresses::LIBRA_ROOT_ADDRESS());
 
         /// The account of TreasuryCompliance is not freezable [G3].
         /// After genesis, FreezingBit of TreasuryCompliance is always false.
-        invariant !LibraTimestamp::spec_is_genesis() ==>
-            spec_account_is_not_frozen(CoreAddresses::SPEC_TREASURY_COMPLIANCE_ADDRESS());
+        invariant [global] LibraTimestamp::is_operating() ==>
+            spec_account_is_not_frozen(CoreAddresses::TREASURY_COMPLIANCE_ADDRESS());
+
+        /// The permission "{Freeze,Unfreeze}Account" is granted to TreasuryCompliance [B16].
+        apply Roles::AbortsIfNotTreasuryCompliance to freeze_account, unfreeze_account;
 
         // TODO: Need to decide the freezability of the roles such as Validator, ValidatorOperator, DesginatedDealer.
     }
+
+    spec schema FreezingBitRemainsSame {
+        /// The freezing bit stays constant.
+        ensures forall a: address where old(exists<FreezingBit>(a)):
+            global<FreezingBit>(a).is_frozen == old(global<FreezingBit>(a).is_frozen);
+    }
+
+    spec module {
+        /// only (un)freeze functions can change the freezing bits of accounts [B16].
+        apply FreezingBitRemainsSame to * except freeze_account, unfreeze_account;
+    }
+
+
 }
 }