From 76a344de3cee5b5ca40756522440a9c24a0b7a1f Mon Sep 17 00:00:00 2001
From: Maksim Kurnikov <maxim.kurnikov@gmail.com>
Date: Thu, 10 Mar 2022 21:23:10 +0300
Subject: [PATCH 1/5] refactoring, prover fixes

---
 Move.toml                   |   2 +-
 sources/ChainId.move        |   4 +-
 sources/PontAccount.move    | 369 +++++++++++-------------------------
 sources/PontTimestamp.move  |  24 +--
 sources/Token.move          |  22 +--
 tests/NativeTokenTests.move |   5 +-
 tests/PontAccountTests.move |   6 +-
 tests/TokenTests.move       |   3 +-
 8 files changed, 136 insertions(+), 299 deletions(-)

diff --git a/Move.toml b/Move.toml
index 8c0de80..02aa3fe 100644
--- a/Move.toml
+++ b/Move.toml
@@ -10,4 +10,4 @@ PontemFramework = "0x1"
 Root = "0xA550C18"
 
 [dependencies]
-MoveStdlib = { git = "https://github.com/pontem-network/move-stdlib.git", rev = "release-v1.0.0"}
+MoveStdlib = { git = "https://github.com/pontem-network/move-stdlib.git", rev = "new-reflect-module"}
diff --git a/sources/ChainId.move b/sources/ChainId.move
index 7d129e3..2e45d2e 100644
--- a/sources/ChainId.move
+++ b/sources/ChainId.move
@@ -28,8 +28,10 @@ module PontemFramework::ChainId {
         pragma opaque;
         let root_addr = Signer::address_of(root_account);
         modifies global<ChainId>(root_addr);
+
         include PontTimestamp::AbortsIfNotGenesis;
         include CoreAddresses::AbortsIfNotRoot{ account: root_account };
+
         aborts_if exists<ChainId>(root_addr) with Errors::ALREADY_PUBLISHED;
         ensures exists<ChainId>(root_addr);
     }
@@ -48,7 +50,7 @@ module PontemFramework::ChainId {
     /// # Initialization
 
     spec module {
-        /// When Diem is operating, the chain id is always available.
+        /// When Pontem is operating, the chain id is always available.
         invariant [suspendable] PontTimestamp::is_operating() ==> exists<ChainId>(@Root);
 
         // Could also specify that ChainId is not stored on any other address, but it doesn't matter.
diff --git a/sources/PontAccount.move b/sources/PontAccount.move
index 458415c..fb084ba 100644
--- a/sources/PontAccount.move
+++ b/sources/PontAccount.move
@@ -50,47 +50,44 @@ module PontemFramework::PontAccount {
         metadata: vector<u8>,
     }
 
-    /// The `PontAccount` resource is not in the required state
-    const ERR_ACCOUNT: u64 = 0;
     /// Tried to deposit a token whose value was zero
-    const ERR_TOKEN_DEPOSIT_IS_ZERO: u64 = 1;
+    const ERR_ZERO_DEPOSIT_AMOUNT: u64 = 1;
     /// The account does not hold a large enough balance in the specified token
     const ERR_INSUFFICIENT_BALANCE: u64 = 2;
     /// Tried to add a balance in a token that this account already has
-    const ERR_ADD_EXISTING_TOKEN: u64 = 3;
+    const ERR_TOKEN_BALANCE_ALREADY_EXISTS: u64 = 3;
     /// Tried to withdraw funds in a token that the account does hold
-    const ERR_PAYER_DOESNT_HOLD_TOKEN: u64 = 4;
+    const ERR_NO_BALANCE_FOR_TOKEN: u64 = 4;
     /// An account cannot be created at the reserved core code address of 0x1
     const ERR_CANNOT_CREATE_AT_CORE_ADDRESS: u64 = 5;
 
     /// Deposit `Token<TokenType>` to payee account.
-    public fun deposit<TokenType>(payer: &signer, payee: address, token: Token<TokenType>)
+    public fun deposit_token<TokenType>(to_addr: address, token: Token<TokenType>, from_addr: address)
     acquires PontAccount, Balance {
-        deposit_with_metadata(payer, payee, token, b"")
+        deposit_token_with_metadata(from_addr, to_addr, token, b"")
     }
 
-    public fun deposit_with_metadata<TokenType>(
-        payer_acc: &signer,
+    public fun deposit_token_with_metadata<TokenType>(
+        payer: address,
         payee: address,
         token: Token<TokenType>,
         metadata: vector<u8>
     ) acquires Balance, PontAccount {
         PontTimestamp::assert_operating();
+        Token::assert_is_token<TokenType>();
 
         // Check that the `token` amount is non-zero
         let token_amount = Token::value(&token);
-        assert!(token_amount > 0, Errors::invalid_argument(ERR_TOKEN_DEPOSIT_IS_ZERO));
+        assert!(token_amount > 0, Errors::invalid_argument(ERR_ZERO_DEPOSIT_AMOUNT));
 
         // Create signer for payee.
         let payee_acc = create_signer(payee);
 
-        // Check that an account exists at `payee`
-        if (!exists<PontAccount>(payee)) {
-            add_user_account(&payee_acc);
-        };
+        // Create PontAccount storage for events, if doesn't exist.
+        ensure_pont_account_exists(&payee_acc);
 
-        if (!balance_exists<TokenType>(payee)) {
-            add_balance<TokenType>(&payee_acc);
+        if (!has_token_balance<TokenType>(payee)) {
+            create_token_balance<TokenType>(&payee_acc);
         };
 
         // Deposit the `to_deposit` token
@@ -102,60 +99,23 @@ module PontemFramework::PontAccount {
             ReceivedPaymentEvent{
                 amount: token_amount,
                 symbol: Token::symbol<TokenType>(),
-                payer: Signer::address_of(payer_acc),
+                payer,
                 metadata
             }
         );
     }
-    spec deposit_with_metadata {
-        pragma opaque;
-
-        modifies global<Balance<TokenType>>(payee);
-        include ModifiesPontAccount { account_addr: payee };
-
-        let amount = token.value;
-        let payer = Signer::address_of(payer_acc);
-//        let balance = global<Balance<TokenType>>(payee);
-
-        include DepositAbort<TokenType>{ amount: token.value, payee };
-//        include Token::AbortsIfDepositOverflow<TokenType> { token: global<Balance<TokenType>>(payee).token, check: token };
-
-        include DepositEnsures<TokenType>{ amount };
-//        include DepositEmits<TokenType>{ payer, amount };
-    }
-    spec schema DepositAbort<TokenType> {
-        payee: address;
-        amount: u64;
-
+    spec deposit_token_with_metadata {
         include PontTimestamp::AbortsIfNotOperating;
         include Token::AbortsIfTokenNotRegistered<TokenType>;
+        include AbortsIfCoreAddress { addr: payee };
 
-        aborts_if amount == 0 with Errors::INVALID_ARGUMENT;
-        aborts_if !exists<PontAccount>(payee)
-                  && payee == @PontemFramework with Errors::INVALID_ARGUMENT;
-    }
-    spec schema DepositEnsures<TokenType> {
-        payee: address;
-        amount: u64;
+        let deposit_amount = token.value;
+        aborts_if deposit_amount == 0 with Errors::INVALID_ARGUMENT;
 
         ensures exists<PontAccount>(payee);
         ensures exists<Balance<TokenType>>(payee);
         ensures old(exists<Balance<TokenType>>(payee)) ==>
-                balance<TokenType>(payee) == old(balance<TokenType>(payee)) + amount;
-    }
-    spec schema DepositEmits<TokenType> {
-        payer: address;
-        payee: address;
-        amount: u64;
-        metadata: vector<u8>;
-        let handle = global<PontAccount>(payee).received_events;
-        let msg = ReceivedPaymentEvent{
-            amount,
-            symbol: Token::spec_symbol<TokenType>(),
-            payer,
-            metadata
-        };
-        emits msg to handle;
+                balance<TokenType>(payee) == old(balance<TokenType>(payee)) + deposit_amount;
     }
 
     /// Withdraw `amount` `Token<TokenType>`'s from the account balance and return.
@@ -166,18 +126,22 @@ module PontemFramework::PontAccount {
         PontTimestamp::assert_operating();
 
         let payer_address = Signer::address_of(payer);
-        assert!(exists<Balance<TokenType>>(payer_address), Errors::not_published(ERR_PAYER_DOESNT_HOLD_TOKEN));
+        assert!(exists<Balance<TokenType>>(payer_address), Errors::not_published(ERR_NO_BALANCE_FOR_TOKEN));
+
+        let payer_balance = borrow_global_mut<Balance<TokenType>>(payer_address);
 
-        let account_balance = borrow_global_mut<Balance<TokenType>>(payer_address);
-        withdraw_from_balance<TokenType>(account_balance, amount)
+        let token = &mut payer_balance.token;
+        assert!(Token::value(token) >= amount, Errors::limit_exceeded(ERR_INSUFFICIENT_BALANCE));
+
+        Token::withdraw(token, amount)
     }
 
-    public fun pay_from<TokenType>(
+    public fun transfer_tokens<TokenType>(
         payer: &signer,
         payee: address,
         amount: u64,
     ) acquires PontAccount, Balance {
-        pay_from_with_metadata<TokenType>(
+        transfer_tokens_with_metadata<TokenType>(
             payer,
             payee,
             amount,
@@ -186,65 +150,56 @@ module PontemFramework::PontAccount {
     }
 
     /// Withdraw the balance from payer account and deposit to payee.
-    public fun pay_from_with_metadata<TokenType>(
+    public fun transfer_tokens_with_metadata<TokenType>(
         payer_acc: &signer,
-        payee: address,
+        payee_addr: address,
         amount: u64,
         metadata: vector<u8>,
     ) acquires PontAccount, Balance {
-        let withdrawn_tokens = withdraw_from(payer_acc, payee, amount, copy metadata);
-        deposit_with_metadata<TokenType>(
-            payer_acc,
-            payee,
-            withdrawn_tokens,
-            metadata
+        let tokens = withdraw_tokens_from<TokenType>(payer_acc, amount);
+        let payer_addr = Signer::address_of(payer_acc);
+        deposit_token_with_metadata<TokenType>(
+            payer_addr,
+            payee_addr,
+            tokens,
+            copy metadata
+        );
+        Event::emit_event<SentPaymentEvent>(
+            &mut borrow_global_mut<PontAccount>(payer_addr).sent_events,
+            SentPaymentEvent{
+                amount,
+                symbol: Token::symbol<TokenType>(),
+                payee: payee_addr,
+                metadata
+            },
         );
     }
-    spec pay_from_with_metadata {
+    spec transfer_tokens_with_metadata {
         let payer = Signer::address_of(payer_acc);
-        modifies global<PontAccount>(payer);
-        modifies global<PontAccount>(payee);
-        modifies global<Balance<TokenType>>(payer);
-        modifies global<Balance<TokenType>>(payee);
-
-        ensures exists<Balance<TokenType>>(payer);
-        ensures exists<Balance<TokenType>>(payee);
-
-//        include PayFromAbortsIf<TokenType>;
-        include PayFromEnsures<TokenType> { payer, payee };
-//        include PayFromEmits<TokenType>;
-    }
-    spec schema PayFromEnsures<TokenType> {
-        payer: address;
-        payee: address;
-        amount: u64;
+        let payee = payee_addr;
         ensures payer == payee
                 ==> balance<TokenType>(payer) == old(balance<TokenType>(payer));
         ensures payer != payee
                 ==> balance<TokenType>(payer) == old(balance<TokenType>(payer)) - amount;
-        ensures payer != payee && old(balance_exists<TokenType>(payee))
+        ensures payer != payee && old(has_token_balance<TokenType>(payee))
                 ==> balance<TokenType>(payee) == old(balance<TokenType>(payee)) + amount;
+        ensures payer != payee && old(!has_token_balance<TokenType>(payee))
+                ==> balance<TokenType>(payee) == amount;
     }
-//    spec schema PayFromEmits<TokenType> {
-//        payer: address;
-//        payee: address;
-//        amount: u64;
-//        include DepositEmits<TokenType>{ payer };
-//        include WithdrawFromEmits<TokenType> { payer };
-//    }
 
     /// Return the current balance of the account at `addr`.
     public fun balance<TokenType>(addr: address): u64 acquires Balance {
-        assert!(exists<Balance<TokenType>>(addr), Errors::not_published(ERR_PAYER_DOESNT_HOLD_TOKEN));
-        balance_for(borrow_global<Balance<TokenType>>(addr))
+        assert!(exists<Balance<TokenType>>(addr), Errors::not_published(ERR_NO_BALANCE_FOR_TOKEN));
+        let balance = borrow_global<Balance<TokenType>>(addr);
+        Token::value<TokenType>(&balance.token)
     }
     spec balance {
         aborts_if !exists<Balance<TokenType>>(addr) with Errors::NOT_PUBLISHED;
     }
 
     /// Add a balance of `TokenType` type to the sending account.
-    public fun add_balance<TokenType>(account: &signer) {
-        let addr = Signer::address_of(account);
+    public fun create_token_balance<TokenType>(acc: &signer) {
+        let addr = Signer::address_of(acc);
 
         // aborts if `Token` is not a token type in the system
         Token::assert_is_token<TokenType>();
@@ -252,195 +207,89 @@ module PontemFramework::PontAccount {
         // aborts if this account already has a balance in `Token`
         assert!(
             !exists<Balance<TokenType>>(addr),
-            Errors::already_published(ERR_ADD_EXISTING_TOKEN)
+            Errors::already_published(ERR_TOKEN_BALANCE_ALREADY_EXISTS)
         );
-        move_to(account, Balance<TokenType>{ token: Token::zero<TokenType>() })
-    }
-    spec add_balance {
-        /// An account must exist at the address
-        include AddBalanceAborts<TokenType> { account };
-
-        let account_addr = Signer::address_of(account);
-        /// `account` cannot have an existing balance in `Token`
-        aborts_if exists<Balance<TokenType>>(account_addr) with Errors::ALREADY_PUBLISHED;
-
-        include AddTokenEnsures<TokenType> { account_addr };
+        move_to(acc, Balance<TokenType>{ token: Token::zero<TokenType>() })
     }
-    spec schema AddBalanceAborts<TokenType> {
-        account: signer;
+    spec create_token_balance {
         include Token::AbortsIfTokenNotRegistered<TokenType>;
-        /// `account` cannot have an existing balance in `Token`
-        aborts_if exists<Balance<TokenType>>(Signer::address_of(account)) with Errors::ALREADY_PUBLISHED;
-    }
-    spec schema AddTokenEnsures<TokenType> {
-        account_addr: address;
-        modifies global<Balance<TokenType>>(account_addr);
-        // This publishes a `Balance<TokenType>` to the caller's account
-        ensures exists<Balance<TokenType>>(account_addr);
-        ensures global<Balance<TokenType>>(account_addr).token.value == 0;
-    }
-
-
-    ///////////////////////////////////////////////////////////////////////////
-    // General purpose methods
-    ///////////////////////////////////////////////////////////////////////////
-    ///
-    /// Helper to return the u64 value of the `balance` for `account`
-    fun balance_for<TokenType>(balance: &Balance<TokenType>): u64 {
-        Token::value<TokenType>(&balance.token)
-    }
-
-    /// If `Balance<TokenType>` exists on account.
-    fun balance_exists<TokenType>(account: address): bool {
-        exists<Balance<TokenType>>(account)
-    }
-
-    spec schema AbortsIfPontemFrameworkAccount {
-        acc: signer;
-        aborts_if Signer::address_of(acc) == @PontemFramework with Errors::INVALID_ARGUMENT;
-    }
 
-    /// Create a new account.
-    /// Used to automatically create new accounts when needed.
-    fun add_user_account(acc: &signer) {
-        assert!(
-            Signer::address_of(acc) != @PontemFramework,
-            Errors::invalid_argument(ERR_CANNOT_CREATE_AT_CORE_ADDRESS)
-        );
-        move_to(acc, PontAccount{
-            received_events: Event::new_event_handle<ReceivedPaymentEvent>(acc),
-            sent_events: Event::new_event_handle<SentPaymentEvent>(acc),
-        });
-    }
-    spec add_user_account {
-        let account_addr = Signer::address_of(acc);
-        include ModifiesPontAccount { account_addr };
+        let acc_addr = Signer::address_of(acc);
+        aborts_if exists<Balance<TokenType>>(acc_addr) with Errors::ALREADY_PUBLISHED;
 
-        ensures exists<PontAccount>(account_addr);
-//        include PontemFrameworkAccountAbort { acc };
-    }
-    spec schema ModifiesPontAccount {
-        account_addr: address;
-        modifies global<PontAccount>(account_addr);
+        ensures exists<Balance<TokenType>>(acc_addr);
+        ensures balance<TokenType>(acc_addr) == 0;
     }
 
     /// Withdraw `amount` `Token<TokenType>`'s from the account balance.
-    fun withdraw_from<TokenType>(
+    fun withdraw_tokens_from<TokenType>(
         payer_acc: &signer,
-        payee: address,
         amount: u64,
-        metadata: vector<u8>,
-    ): Token<TokenType> acquires Balance, PontAccount {
+    ): Token<TokenType> acquires Balance {
         PontTimestamp::assert_operating();
 
         let payer_address = Signer::address_of(payer_acc);
 
-        // Check that an account exists at `payee`
-        if (!exists<PontAccount>(payer_address)) {
-            add_user_account(payer_acc);
-        };
-
-        if (!balance_exists<TokenType>(payer_address)) {
-            add_balance<TokenType>(payer_acc);
-        };
-
-        let account_balance = borrow_global_mut<Balance<TokenType>>(payer_address);
+        // Create PontAccount storage for events, if doesn't exist.
+        ensure_pont_account_exists(payer_acc);
 
-        // Load the payer's account and emit an event to record the withdrawal
-        Event::emit_event<SentPaymentEvent>(
-            &mut borrow_global_mut<PontAccount>(payer_address).sent_events,
-            SentPaymentEvent{
-                amount,
-                symbol: Token::symbol<TokenType>(),
-                payee,
-                metadata
-            },
+        assert!(
+            has_token_balance<TokenType>(payer_address),
+            Errors::not_published(ERR_NO_BALANCE_FOR_TOKEN)
         );
-        withdraw_from_balance<TokenType>(account_balance, amount)
-    }
-    spec withdraw_from {
-        let payer = Signer::address_of(payer_acc);
-
-        include ModifiesPontAccount { account_addr: payer };
-        modifies global<Balance<TokenType>>(payer);
+        let payer_balance = borrow_global_mut<Balance<TokenType>>(payer_address);
 
-        include WithdrawFromAborts<TokenType> { payer };
-//        include Token::WithdrawAborts<TokenType> { token: global<Balance<TokenType>>(payer).token, amount };
-
-        ensures exists<PontAccount>(payer);
-        ensures exists<Balance<TokenType>>(payer);
+        let token = &mut payer_balance.token;
+        assert!(Token::value(token) >= amount, Errors::limit_exceeded(ERR_INSUFFICIENT_BALANCE));
 
-//        ensures TRACE(balance<TokenType>(payer)) == TRACE(old(balance<TokenType>(payer))) - amount;
-//        include WithdrawFromBalanceEnsures<TokenType>{ balance: global<Balance<TokenType>>(payer) };
-//        include WithdrawFromEmits<TokenType> { payer };
+        Token::withdraw(token, amount)
     }
-    spec schema WithdrawFromAborts<TokenType> {
-        payer: address;
-        payee: address;
-        amount: u64;
-
+    spec withdraw_tokens_from {
         include PontTimestamp::AbortsIfNotOperating;
-        include Token::AbortsIfTokenNotRegistered<TokenType>;
-        aborts_if !exists<PontAccount>(payer)
-                  && payer == @PontemFramework with Errors::INVALID_ARGUMENT;
-//        include Token::WithdrawAbortsIf<TokenType> { token: global<Balance<TokenType>>(payer).token, amount };
-    }
-    spec schema WithdrawFromEmits<TokenType> {
-        payer: address;
-        payee: address;
-        amount: u64;
-        metadata: vector<u8>;
-        let handle = global<PontAccount>(payer).sent_events;
-        let msg = SentPaymentEvent{
-            amount,
-            symbol: Token::spec_symbol<TokenType>(),
-            payee,
-            metadata
-        };
-        emits msg to handle;
-    }
 
-    /// Helper to withdraw `amount` from the given account balance and return the withdrawn Diem<Token>
-    fun withdraw_from_balance<TokenType>(
-        balance: &mut Balance<TokenType>,
-        amount: u64
-    ): Token<TokenType> {
-        PontTimestamp::assert_operating();
+        let payer_addr = Signer::address_of(payer_acc);
+        include AbortsIfCoreAddress { addr: payer_addr };
+        aborts_if !has_token_balance<TokenType>(payer_addr) with Errors::NOT_PUBLISHED;
 
-        let token = &mut balance.token;
-        assert_enough_tokens_available(token, amount);
+        let payer_balance = global<Balance<TokenType>>(payer_addr);
+        aborts_if Token::value(payer_balance.token) < amount with Errors::LIMIT_EXCEEDED;
 
-        Token::withdraw(token, amount)
+        ensures exists<PontAccount>(payer_addr);
+        ensures exists<Balance<TokenType>>(payer_addr);
+        ensures result.value == amount;
     }
-    spec withdraw_from_balance {
-        include PontTimestamp::AbortsIfNotOperating;
-        include Token::WithdrawAborts<TokenType> { token: balance.token, amount };
 
-        include WithdrawFromBalanceEnsures<TokenType>;
+    ///////////////////////////////////////////////////////////////////////////
+    // General purpose methods
+    ///////////////////////////////////////////////////////////////////////////
+    /// If `Balance<TokenType>` exists on account.
+    fun has_token_balance<TokenType>(account: address): bool {
+        exists<Balance<TokenType>>(account)
     }
-    spec schema WithdrawFromBalanceEnsures<TokenType> {
-        balance: Balance<TokenType>;
-        amount: u64;
-        result: Token<TokenType>;
 
-        ensures balance.token.value == old(balance.token.value) - amount;
-        ensures result.value == amount;
+    fun ensure_pont_account_exists(acc: &signer) {
+        let addr = Signer::address_of(acc);
+        assert!(
+            addr != @PontemFramework,
+            Errors::invalid_argument(ERR_CANNOT_CREATE_AT_CORE_ADDRESS)
+        );
+        if (!exists<PontAccount>(addr)) {
+            move_to(acc, PontAccount{
+                received_events: Event::new_event_handle<ReceivedPaymentEvent>(acc),
+                sent_events: Event::new_event_handle<SentPaymentEvent>(acc),
+            });
+        };
     }
-
-    fun assert_enough_tokens_available<TokenType>(token: &Token<TokenType>, amount: u64) {
-        // Abort if this withdrawal would make the `payer`'s balance go negative
-        assert!(Token::value(token) >= amount, Errors::limit_exceeded(ERR_INSUFFICIENT_BALANCE));
+    spec ensure_pont_account_exists {
+        let acc_addr = Signer::address_of(acc);
+        include AbortsIfCoreAddress { addr: acc_addr };
+        ensures exists<PontAccount>(acc_addr);
     }
-    spec assert_enough_tokens_available {
-        pragma opaque;
-        pragma verify = false;
-        aborts_if false;
+
+    spec schema AbortsIfCoreAddress {
+        addr: address;
+        aborts_if addr == @PontemFramework with Errors::INVALID_ARGUMENT;
     }
 
     native fun create_signer(addr: address): signer;
-    spec create_signer {
-        pragma opaque;
-        aborts_if false;
-        ensures Signer::address_of(result) == addr;
-    }
 }
diff --git a/sources/PontTimestamp.move b/sources/PontTimestamp.move
index 771fcfa..719308b 100644
--- a/sources/PontTimestamp.move
+++ b/sources/PontTimestamp.move
@@ -73,18 +73,6 @@ module PontemFramework::PontTimestamp {
         global<CurrentTimeMicroseconds>(@Root).microseconds / MICRO_CONVERSION_FACTOR
     }
 
-    #[test_only]
-    public fun set_time_microseconds(ms: u64) acquires CurrentTimeMicroseconds {
-        assert!(is_operating(), Errors::invalid_state(ERR_NOT_OPERATING));
-        borrow_global_mut<CurrentTimeMicroseconds>(@Root).microseconds = ms;
-    }
-
-    #[test_only]
-    public fun set_time_seconds(s: u64) acquires CurrentTimeMicroseconds {
-        let microseconds = s * MICRO_CONVERSION_FACTOR;
-        set_time_microseconds(microseconds);
-    }
-
     /// Helper function to determine if Pontem is in genesis state.
     public fun is_genesis(): bool {
         !exists<CurrentTimeMicroseconds>(@Root)
@@ -124,6 +112,18 @@ module PontemFramework::PontTimestamp {
         aborts_if !is_operating() with Errors::INVALID_STATE;
     }
 
+    #[test_only]
+    public fun set_time_microseconds(ms: u64) acquires CurrentTimeMicroseconds {
+        assert!(is_operating(), Errors::invalid_state(ERR_NOT_OPERATING));
+        borrow_global_mut<CurrentTimeMicroseconds>(@Root).microseconds = ms;
+    }
+
+    #[test_only]
+    public fun set_time_seconds(s: u64) acquires CurrentTimeMicroseconds {
+        let microseconds = s * MICRO_CONVERSION_FACTOR;
+        set_time_microseconds(microseconds);
+    }
+
     // ====================
     // Module Specification
     spec module {} // switch documentation context to module level
diff --git a/sources/Token.move b/sources/Token.move
index 8f401c6..ac7722d 100644
--- a/sources/Token.move
+++ b/sources/Token.move
@@ -134,15 +134,13 @@ module PontemFramework::Token {
         Token { value: amount }
     }
     spec withdraw {
-        pragma opaque;
-        pragma verify = false;
-        aborts_if false;
-//        include WithdrawAborts<TokenType> { token, amount };
+//        pragma opaque;
+        include AbortsIfTokenValueLessThanAmount<TokenType> { token, amount };
 
         ensures token.value == old(token.value) - amount;
         ensures result.value == amount;
     }
-    spec schema WithdrawAborts<TokenType> {
+    spec schema AbortsIfTokenValueLessThanAmount<TokenType> {
         token: Token<TokenType>;
         amount: u64;
 
@@ -185,15 +183,8 @@ module PontemFramework::Token {
         pragma opaque;
         pragma verify = false;
         aborts_if false;
-//        aborts_if false;
-//        include AbortsIfDepositOverflow<TokenType>;
         ensures token.value == old(token.value) + check.value;
     }
-    spec schema AbortsIfDepositOverflow<TokenType> {
-        token: Token<TokenType>;
-        check: Token<TokenType>;
-        aborts_if token.value + check.value > MAX_U64 with Errors::LIMIT_EXCEEDED;
-    }
 
     /// Destroy a zero-value token. Calls will fail if the `value` in the passed-in `token` is non-zero
     /// so it is impossible to "burn" any non-zero amount of `Pontem` without having
@@ -386,11 +377,6 @@ module PontemFramework::Token {
         let deployer_addr = get_deployer_addr<TokenType>();
         exists<TokenInfo<TokenType>>(deployer_addr)
     }
-    spec is_token {
-//        pragma opaque;
-        pragma verify = false;
-        aborts_if false;
-    }
 
     /// Returns the decimals for the `TokenType` token as defined
     /// in its `TokenInfo`.
@@ -414,7 +400,6 @@ module PontemFramework::Token {
         *&borrow_global<TokenInfo<TokenType>>(get_deployer_addr<TokenType>()).symbol
     }
     spec symbol {
-        pragma opaque;
         include AbortsIfTokenNotRegistered<TokenType>;
         ensures result == spec_symbol<TokenType>();
     }
@@ -431,7 +416,6 @@ module PontemFramework::Token {
         assert!(is_token<TokenType>(), Errors::not_published(ERR_TOKEN_INFO));
     }
     spec assert_is_token {
-        pragma opaque;
         include AbortsIfTokenNotRegistered<TokenType>;
     }
     spec schema AbortsIfTokenNotRegistered<TokenType> {
diff --git a/tests/NativeTokenTests.move b/tests/NativeTokenTests.move
index ea7707d..9534c6f 100644
--- a/tests/NativeTokenTests.move
+++ b/tests/NativeTokenTests.move
@@ -14,9 +14,10 @@ module PontemFramework::NativeTokenTests {
         let ponts = NOX::mint(&root_acc, 2);
         let ksms = KSM::mint(&root_acc, 3);
 
+        let root_addr = Signer::address_of(&root_acc);
         let user_addr = Signer::address_of(&user_acc);
-        PontAccount::deposit(&root_acc, user_addr, ponts);
-        PontAccount::deposit(&root_acc, user_addr, ksms);
+        PontAccount::deposit_token(user_addr, ponts, root_addr);
+        PontAccount::deposit_token(user_addr, ksms, root_addr);
 
         assert!(PontAccount::balance<NOX>(user_addr) == 2, 1);
         assert!(PontAccount::balance<KSM>(user_addr) == 3, 2);
diff --git a/tests/PontAccountTests.move b/tests/PontAccountTests.move
index 64b52de..1075591 100644
--- a/tests/PontAccountTests.move
+++ b/tests/PontAccountTests.move
@@ -16,13 +16,13 @@ module PontemFramework::PontAccountTests {
         let ponts = NOX::mint(&root_acc, 10);
         let (ponts_7, ponts_3) = Token::split(ponts, 3);
 
-        PontAccount::deposit(&root_acc, user1_addr, ponts_7);
-        PontAccount::deposit(&root_acc, user2_addr, ponts_3);
+        PontAccount::deposit_token(user1_addr, ponts_7, @Root);
+        PontAccount::deposit_token(user2_addr, ponts_3, @Root);
 
         assert!(PontAccount::balance<NOX>(user1_addr) == 7, 1);
         assert!(PontAccount::balance<NOX>(user2_addr) == 3, 2);
 
-        PontAccount::pay_from<NOX>(&user1_acc, user2_addr, 5);
+        PontAccount::transfer_tokens<NOX>(&user1_acc, user2_addr, 5);
         assert!(PontAccount::balance<NOX>(user1_addr) == 2, 3);
         assert!(PontAccount::balance<NOX>(user2_addr) == 8, 4);
     }
diff --git a/tests/TokenTests.move b/tests/TokenTests.move
index 3ab0e88..121b7eb 100644
--- a/tests/TokenTests.move
+++ b/tests/TokenTests.move
@@ -43,8 +43,9 @@ module PontemFramework::TokenTests {
         let ucoins = UCOIN::mint(&minter_acc, 10);
         assert!(Token::value(&ucoins) == 10, 1);
 
+        let minter_addr = @0x42;
         let user_addr = Signer::address_of(&user_acc);
-        PontAccount::deposit(&minter_acc, user_addr, ucoins);
+        PontAccount::deposit_token(user_addr, ucoins, minter_addr);
         assert!(PontAccount::balance<UCOIN>(user_addr) == 10, 2);
 
         let withdrawn_ucoins = PontAccount::withdraw<UCOIN>(&user_acc, 3);

From c875b9beaf47c9736349a3a1a6e3b15b5302db6d Mon Sep 17 00:00:00 2001
From: Maksim Kurnikov <maxim.kurnikov@gmail.com>
Date: Thu, 10 Mar 2022 22:47:23 +0300
Subject: [PATCH 2/5] more cleanups

---
 sources/PontAccount.move    | 99 ++++++++++++++++++-------------------
 tests/NativeTokenTests.move |  4 +-
 tests/TokenTests.move       |  2 +-
 3 files changed, 50 insertions(+), 55 deletions(-)

diff --git a/sources/PontAccount.move b/sources/PontAccount.move
index fb084ba..ce95f05 100644
--- a/sources/PontAccount.move
+++ b/sources/PontAccount.move
@@ -119,13 +119,16 @@ module PontemFramework::PontAccount {
     }
 
     /// Withdraw `amount` `Token<TokenType>`'s from the account balance and return.
-    public fun withdraw<TokenType>(
-        payer: &signer,
+    public fun withdraw_tokens<TokenType>(
+        payer_acc: &signer,
         amount: u64,
     ): Token<TokenType> acquires Balance {
         PontTimestamp::assert_operating();
 
-        let payer_address = Signer::address_of(payer);
+        // Create PontAccount storage for events, if doesn't exist.
+        ensure_pont_account_exists(payer_acc);
+
+        let payer_address = Signer::address_of(payer_acc);
         assert!(exists<Balance<TokenType>>(payer_address), Errors::not_published(ERR_NO_BALANCE_FOR_TOKEN));
 
         let payer_balance = borrow_global_mut<Balance<TokenType>>(payer_address);
@@ -135,6 +138,20 @@ module PontemFramework::PontAccount {
 
         Token::withdraw(token, amount)
     }
+    spec withdraw_tokens {
+        include PontTimestamp::AbortsIfNotOperating;
+
+        let payer_addr = Signer::address_of(payer_acc);
+        include AbortsIfCoreAddress { addr: payer_addr };
+        aborts_if !has_token_balance<TokenType>(payer_addr) with Errors::NOT_PUBLISHED;
+
+        let payer_balance = global<Balance<TokenType>>(payer_addr);
+        aborts_if Token::value(payer_balance.token) < amount with Errors::LIMIT_EXCEEDED;
+
+        ensures exists<PontAccount>(payer_addr);
+        ensures exists<Balance<TokenType>>(payer_addr);
+        ensures result.value == amount;
+    }
 
     public fun transfer_tokens<TokenType>(
         payer: &signer,
@@ -148,6 +165,13 @@ module PontemFramework::PontAccount {
             b""
         );
     }
+    spec transfer_tokens {
+        include TransferTokenEnsures<TokenType> {
+            payer_addr: Signer::address_of(payer),
+            payee_addr: payee,
+            amount,
+        };
+    }
 
     /// Withdraw the balance from payer account and deposit to payee.
     public fun transfer_tokens_with_metadata<TokenType>(
@@ -156,7 +180,7 @@ module PontemFramework::PontAccount {
         amount: u64,
         metadata: vector<u8>,
     ) acquires PontAccount, Balance {
-        let tokens = withdraw_tokens_from<TokenType>(payer_acc, amount);
+        let tokens = withdraw_tokens<TokenType>(payer_acc, amount);
         let payer_addr = Signer::address_of(payer_acc);
         deposit_token_with_metadata<TokenType>(
             payer_addr,
@@ -175,16 +199,25 @@ module PontemFramework::PontAccount {
         );
     }
     spec transfer_tokens_with_metadata {
-        let payer = Signer::address_of(payer_acc);
-        let payee = payee_addr;
-        ensures payer == payee
-                ==> balance<TokenType>(payer) == old(balance<TokenType>(payer));
-        ensures payer != payee
-                ==> balance<TokenType>(payer) == old(balance<TokenType>(payer)) - amount;
-        ensures payer != payee && old(has_token_balance<TokenType>(payee))
-                ==> balance<TokenType>(payee) == old(balance<TokenType>(payee)) + amount;
-        ensures payer != payee && old(!has_token_balance<TokenType>(payee))
-                ==> balance<TokenType>(payee) == amount;
+        include TransferTokenEnsures<TokenType> {
+            payer_addr: Signer::address_of(payer_acc),
+            payee_addr,
+            amount,
+        };
+    }
+
+    spec schema TransferTokenEnsures<TokenType> {
+        payer_addr: address;
+        payee_addr: address;
+        amount: u64;
+        ensures payer_addr == payee_addr
+                ==> balance<TokenType>(payer_addr) == old(balance<TokenType>(payer_addr));
+        ensures payer_addr != payee_addr
+                ==> balance<TokenType>(payer_addr) == old(balance<TokenType>(payer_addr)) - amount;
+        ensures payer_addr != payee_addr && old(has_token_balance<TokenType>(payee_addr))
+                ==> balance<TokenType>(payee_addr) == old(balance<TokenType>(payee_addr)) + amount;
+        ensures payer_addr != payee_addr && old(!has_token_balance<TokenType>(payee_addr))
+                ==> balance<TokenType>(payee_addr) == amount;
     }
 
     /// Return the current balance of the account at `addr`.
@@ -221,44 +254,6 @@ module PontemFramework::PontAccount {
         ensures balance<TokenType>(acc_addr) == 0;
     }
 
-    /// Withdraw `amount` `Token<TokenType>`'s from the account balance.
-    fun withdraw_tokens_from<TokenType>(
-        payer_acc: &signer,
-        amount: u64,
-    ): Token<TokenType> acquires Balance {
-        PontTimestamp::assert_operating();
-
-        let payer_address = Signer::address_of(payer_acc);
-
-        // Create PontAccount storage for events, if doesn't exist.
-        ensure_pont_account_exists(payer_acc);
-
-        assert!(
-            has_token_balance<TokenType>(payer_address),
-            Errors::not_published(ERR_NO_BALANCE_FOR_TOKEN)
-        );
-        let payer_balance = borrow_global_mut<Balance<TokenType>>(payer_address);
-
-        let token = &mut payer_balance.token;
-        assert!(Token::value(token) >= amount, Errors::limit_exceeded(ERR_INSUFFICIENT_BALANCE));
-
-        Token::withdraw(token, amount)
-    }
-    spec withdraw_tokens_from {
-        include PontTimestamp::AbortsIfNotOperating;
-
-        let payer_addr = Signer::address_of(payer_acc);
-        include AbortsIfCoreAddress { addr: payer_addr };
-        aborts_if !has_token_balance<TokenType>(payer_addr) with Errors::NOT_PUBLISHED;
-
-        let payer_balance = global<Balance<TokenType>>(payer_addr);
-        aborts_if Token::value(payer_balance.token) < amount with Errors::LIMIT_EXCEEDED;
-
-        ensures exists<PontAccount>(payer_addr);
-        ensures exists<Balance<TokenType>>(payer_addr);
-        ensures result.value == amount;
-    }
-
     ///////////////////////////////////////////////////////////////////////////
     // General purpose methods
     ///////////////////////////////////////////////////////////////////////////
diff --git a/tests/NativeTokenTests.move b/tests/NativeTokenTests.move
index 9534c6f..2cbce2e 100644
--- a/tests/NativeTokenTests.move
+++ b/tests/NativeTokenTests.move
@@ -22,8 +22,8 @@ module PontemFramework::NativeTokenTests {
         assert!(PontAccount::balance<NOX>(user_addr) == 2, 1);
         assert!(PontAccount::balance<KSM>(user_addr) == 3, 2);
 
-        let withdrawn_ponts = PontAccount::withdraw<NOX>(&user_acc, 1);
-        let withdrawn_ksms = PontAccount::withdraw<KSM>(&user_acc, 1);
+        let withdrawn_ponts = PontAccount::withdraw_tokens<NOX>(&user_acc, 1);
+        let withdrawn_ksms = PontAccount::withdraw_tokens<KSM>(&user_acc, 1);
 
         assert!(PontAccount::balance<NOX>(user_addr) == 1, 3);
         assert!(PontAccount::balance<KSM>(user_addr) == 2, 4);
diff --git a/tests/TokenTests.move b/tests/TokenTests.move
index 121b7eb..bdf95bb 100644
--- a/tests/TokenTests.move
+++ b/tests/TokenTests.move
@@ -48,7 +48,7 @@ module PontemFramework::TokenTests {
         PontAccount::deposit_token(user_addr, ucoins, minter_addr);
         assert!(PontAccount::balance<UCOIN>(user_addr) == 10, 2);
 
-        let withdrawn_ucoins = PontAccount::withdraw<UCOIN>(&user_acc, 3);
+        let withdrawn_ucoins = PontAccount::withdraw_tokens<UCOIN>(&user_acc, 3);
         assert!(PontAccount::balance<UCOIN>(user_addr) == 7, 2);
 
         UCOIN::burn(&minter_acc, withdrawn_ucoins);

From df89e43a932342a848783b2dfd1356a23c4736b5 Mon Sep 17 00:00:00 2001
From: Maksim Kurnikov <maxim.kurnikov@gmail.com>
Date: Thu, 10 Mar 2022 22:50:18 +0300
Subject: [PATCH 3/5] check account exists

---
 sources/PontAccount.move | 1 +
 1 file changed, 1 insertion(+)

diff --git a/sources/PontAccount.move b/sources/PontAccount.move
index ce95f05..f244be9 100644
--- a/sources/PontAccount.move
+++ b/sources/PontAccount.move
@@ -210,6 +210,7 @@ module PontemFramework::PontAccount {
         payer_addr: address;
         payee_addr: address;
         amount: u64;
+        ensures exists<PontAccount>(payee_addr);
         ensures payer_addr == payee_addr
                 ==> balance<TokenType>(payer_addr) == old(balance<TokenType>(payer_addr));
         ensures payer_addr != payee_addr

From 3cb16e31beebc2526ba97c8666bae693c9031ddc Mon Sep 17 00:00:00 2001
From: Maksim Kurnikov <maxim.kurnikov@gmail.com>
Date: Thu, 10 Mar 2022 22:56:19 +0300
Subject: [PATCH 4/5] consistency

---
 sources/PontAccount.move | 118 +++++++++++++++++++--------------------
 1 file changed, 59 insertions(+), 59 deletions(-)

diff --git a/sources/PontAccount.move b/sources/PontAccount.move
index f244be9..4b6a16d 100644
--- a/sources/PontAccount.move
+++ b/sources/PontAccount.move
@@ -33,7 +33,7 @@ module PontemFramework::PontAccount {
         /// The code symbol for the token that was sent
         symbol: String,
         /// The address that was paid
-        payee: address,
+        to_addr: address,
         /// Metadata associated with the payment
         metadata: vector<u8>,
     }
@@ -45,7 +45,7 @@ module PontemFramework::PontAccount {
         /// The code symbol for the token that was received
         symbol: String,
         /// The address that sent the token
-        payer: address,
+        from_addr: address,
         /// Metadata associated with the payment
         metadata: vector<u8>,
     }
@@ -61,15 +61,15 @@ module PontemFramework::PontAccount {
     /// An account cannot be created at the reserved core code address of 0x1
     const ERR_CANNOT_CREATE_AT_CORE_ADDRESS: u64 = 5;
 
-    /// Deposit `Token<TokenType>` to payee account.
+    /// Deposit `Token<TokenType>` to `to_addr` address.
     public fun deposit_token<TokenType>(to_addr: address, token: Token<TokenType>, from_addr: address)
     acquires PontAccount, Balance {
         deposit_token_with_metadata(from_addr, to_addr, token, b"")
     }
 
     public fun deposit_token_with_metadata<TokenType>(
-        payer: address,
-        payee: address,
+        from_addr: address,
+        to_addr: address,
         token: Token<TokenType>,
         metadata: vector<u8>
     ) acquires Balance, PontAccount {
@@ -80,26 +80,26 @@ module PontemFramework::PontAccount {
         let token_amount = Token::value(&token);
         assert!(token_amount > 0, Errors::invalid_argument(ERR_ZERO_DEPOSIT_AMOUNT));
 
-        // Create signer for payee.
-        let payee_acc = create_signer(payee);
+        // Create signer for `to_addr` to create PontAccount and Balance resources.
+        let to_addr_acc = create_signer(to_addr);
 
         // Create PontAccount storage for events, if doesn't exist.
-        ensure_pont_account_exists(&payee_acc);
+        ensure_pont_account_exists(&to_addr_acc);
 
-        if (!has_token_balance<TokenType>(payee)) {
-            create_token_balance<TokenType>(&payee_acc);
+        if (!has_token_balance<TokenType>(to_addr)) {
+            create_token_balance<TokenType>(&to_addr_acc);
         };
 
         // Deposit the `to_deposit` token
-        Token::deposit(&mut borrow_global_mut<Balance<TokenType>>(payee).token, token);
+        Token::deposit(&mut borrow_global_mut<Balance<TokenType>>(to_addr).token, token);
 
         // Log a received event
         Event::emit_event<ReceivedPaymentEvent>(
-            &mut borrow_global_mut<PontAccount>(payee).received_events,
+            &mut borrow_global_mut<PontAccount>(to_addr).received_events,
             ReceivedPaymentEvent{
                 amount: token_amount,
                 symbol: Token::symbol<TokenType>(),
-                payer,
+                from_addr,
                 metadata
             }
         );
@@ -107,33 +107,33 @@ module PontemFramework::PontAccount {
     spec deposit_token_with_metadata {
         include PontTimestamp::AbortsIfNotOperating;
         include Token::AbortsIfTokenNotRegistered<TokenType>;
-        include AbortsIfCoreAddress { addr: payee };
+        include AbortsIfCoreAddress { addr: to_addr };
 
         let deposit_amount = token.value;
         aborts_if deposit_amount == 0 with Errors::INVALID_ARGUMENT;
 
-        ensures exists<PontAccount>(payee);
-        ensures exists<Balance<TokenType>>(payee);
-        ensures old(exists<Balance<TokenType>>(payee)) ==>
-                balance<TokenType>(payee) == old(balance<TokenType>(payee)) + deposit_amount;
+        ensures exists<PontAccount>(to_addr);
+        ensures exists<Balance<TokenType>>(to_addr);
+        ensures old(exists<Balance<TokenType>>(to_addr)) ==>
+                balance<TokenType>(to_addr) == old(balance<TokenType>(to_addr)) + deposit_amount;
     }
 
     /// Withdraw `amount` `Token<TokenType>`'s from the account balance and return.
     public fun withdraw_tokens<TokenType>(
-        payer_acc: &signer,
+        from_acc: &signer,
         amount: u64,
     ): Token<TokenType> acquires Balance {
         PontTimestamp::assert_operating();
 
         // Create PontAccount storage for events, if doesn't exist.
-        ensure_pont_account_exists(payer_acc);
+        ensure_pont_account_exists(from_acc);
 
-        let payer_address = Signer::address_of(payer_acc);
-        assert!(exists<Balance<TokenType>>(payer_address), Errors::not_published(ERR_NO_BALANCE_FOR_TOKEN));
+        let from_acc_addr = Signer::address_of(from_acc);
+        assert!(exists<Balance<TokenType>>(from_acc_addr), Errors::not_published(ERR_NO_BALANCE_FOR_TOKEN));
 
-        let payer_balance = borrow_global_mut<Balance<TokenType>>(payer_address);
+        let from_acc_balance = borrow_global_mut<Balance<TokenType>>(from_acc_addr);
 
-        let token = &mut payer_balance.token;
+        let token = &mut from_acc_balance.token;
         assert!(Token::value(token) >= amount, Errors::limit_exceeded(ERR_INSUFFICIENT_BALANCE));
 
         Token::withdraw(token, amount)
@@ -141,84 +141,84 @@ module PontemFramework::PontAccount {
     spec withdraw_tokens {
         include PontTimestamp::AbortsIfNotOperating;
 
-        let payer_addr = Signer::address_of(payer_acc);
-        include AbortsIfCoreAddress { addr: payer_addr };
-        aborts_if !has_token_balance<TokenType>(payer_addr) with Errors::NOT_PUBLISHED;
+        let from_acc_addr = Signer::address_of(from_acc);
+        include AbortsIfCoreAddress { addr: from_acc_addr };
+        aborts_if !has_token_balance<TokenType>(from_acc_addr) with Errors::NOT_PUBLISHED;
 
-        let payer_balance = global<Balance<TokenType>>(payer_addr);
-        aborts_if Token::value(payer_balance.token) < amount with Errors::LIMIT_EXCEEDED;
+        let from_acc_balance = global<Balance<TokenType>>(from_acc_addr);
+        aborts_if Token::value(from_acc_balance.token) < amount with Errors::LIMIT_EXCEEDED;
 
-        ensures exists<PontAccount>(payer_addr);
-        ensures exists<Balance<TokenType>>(payer_addr);
+        ensures exists<PontAccount>(from_acc_addr);
+        ensures exists<Balance<TokenType>>(from_acc_addr);
         ensures result.value == amount;
     }
 
     public fun transfer_tokens<TokenType>(
-        payer: &signer,
-        payee: address,
+        from_acc: &signer,
+        to_addr: address,
         amount: u64,
     ) acquires PontAccount, Balance {
         transfer_tokens_with_metadata<TokenType>(
-            payer,
-            payee,
+            from_acc,
+            to_addr,
             amount,
             b""
         );
     }
     spec transfer_tokens {
         include TransferTokenEnsures<TokenType> {
-            payer_addr: Signer::address_of(payer),
-            payee_addr: payee,
+            from_addr: Signer::address_of(from_acc),
+            to_addr,
             amount,
         };
     }
 
-    /// Withdraw the balance from payer account and deposit to payee.
+    /// Withdraw the balance from `from_acc` account and deposit to `to_addr`.
     public fun transfer_tokens_with_metadata<TokenType>(
-        payer_acc: &signer,
-        payee_addr: address,
+        from_acc: &signer,
+        to_addr: address,
         amount: u64,
         metadata: vector<u8>,
     ) acquires PontAccount, Balance {
-        let tokens = withdraw_tokens<TokenType>(payer_acc, amount);
-        let payer_addr = Signer::address_of(payer_acc);
+        let tokens = withdraw_tokens<TokenType>(from_acc, amount);
+        let from_acc_addr = Signer::address_of(from_acc);
         deposit_token_with_metadata<TokenType>(
-            payer_addr,
-            payee_addr,
+            from_acc_addr,
+            to_addr,
             tokens,
             copy metadata
         );
         Event::emit_event<SentPaymentEvent>(
-            &mut borrow_global_mut<PontAccount>(payer_addr).sent_events,
+            &mut borrow_global_mut<PontAccount>(from_acc_addr).sent_events,
             SentPaymentEvent{
                 amount,
                 symbol: Token::symbol<TokenType>(),
-                payee: payee_addr,
+                to_addr,
                 metadata
             },
         );
     }
     spec transfer_tokens_with_metadata {
         include TransferTokenEnsures<TokenType> {
-            payer_addr: Signer::address_of(payer_acc),
-            payee_addr,
+            from_addr: Signer::address_of(from_acc),
+            to_addr,
             amount,
         };
     }
 
     spec schema TransferTokenEnsures<TokenType> {
-        payer_addr: address;
-        payee_addr: address;
+        from_addr: address;
+        to_addr: address;
         amount: u64;
-        ensures exists<PontAccount>(payee_addr);
-        ensures payer_addr == payee_addr
-                ==> balance<TokenType>(payer_addr) == old(balance<TokenType>(payer_addr));
-        ensures payer_addr != payee_addr
-                ==> balance<TokenType>(payer_addr) == old(balance<TokenType>(payer_addr)) - amount;
-        ensures payer_addr != payee_addr && old(has_token_balance<TokenType>(payee_addr))
-                ==> balance<TokenType>(payee_addr) == old(balance<TokenType>(payee_addr)) + amount;
-        ensures payer_addr != payee_addr && old(!has_token_balance<TokenType>(payee_addr))
-                ==> balance<TokenType>(payee_addr) == amount;
+        ensures exists<PontAccount>(to_addr);
+        ensures from_addr == to_addr
+                ==> balance<TokenType>(from_addr) == old(balance<TokenType>(from_addr));
+        ensures from_addr != to_addr
+                ==> balance<TokenType>(from_addr) == old(balance<TokenType>(from_addr)) - amount;
+        ensures from_addr != to_addr && old(has_token_balance<TokenType>(to_addr))
+                ==> balance<TokenType>(to_addr) == old(balance<TokenType>(to_addr)) + amount;
+        ensures from_addr != to_addr && old(!has_token_balance<TokenType>(to_addr))
+                ==> balance<TokenType>(to_addr) == amount;
     }
 
     /// Return the current balance of the account at `addr`.

From 5d9945a5fef809802e8d5908d11f818c006afd74 Mon Sep 17 00:00:00 2001
From: Maksim Kurnikov <maxim.kurnikov@gmail.com>
Date: Mon, 14 Mar 2022 18:07:16 +0300
Subject: [PATCH 5/5] improve specs for Token.move

---
 sources/PontAccount.move |  3 ++
 sources/Token.move       | 62 +++++++++++-----------------------------
 2 files changed, 19 insertions(+), 46 deletions(-)

diff --git a/sources/PontAccount.move b/sources/PontAccount.move
index 4b6a16d..9e8f005 100644
--- a/sources/PontAccount.move
+++ b/sources/PontAccount.move
@@ -109,6 +109,9 @@ module PontemFramework::PontAccount {
         include Token::AbortsIfTokenNotRegistered<TokenType>;
         include AbortsIfCoreAddress { addr: to_addr };
 
+        aborts_if exists<Balance<TokenType>>(to_addr) &&
+                  global<Balance<TokenType>>(to_addr).token.value + token.value > max_u64() with Errors::LIMIT_EXCEEDED;
+
         let deposit_amount = token.value;
         aborts_if deposit_amount == 0 with Errors::INVALID_ARGUMENT;
 
diff --git a/sources/Token.move b/sources/Token.move
index ac7722d..da2c9db 100644
--- a/sources/Token.move
+++ b/sources/Token.move
@@ -82,7 +82,7 @@ module PontemFramework::Token {
     /// A property expected of a `TokenInfo` resource didn't hold
     const ERR_TOKEN_INFO: u64 = 1;
     /// A property expected of the token provided didn't hold
-    const ERR_TOKEN: u64 = 2;
+    const ERR_INVALID_TOKEN: u64 = 2;
     /// The destruction of a non-zero token was attempted. Non-zero tokens must be burned.
     const ERR_DESTRUCTION_OF_NONZERO_TOKEN: u64 = 3;
     /// A withdrawal greater than the value of the token was attempted.
@@ -97,8 +97,7 @@ module PontemFramework::Token {
         Token<TokenType> { value: 0 }
     }
     spec zero {
-//        pragma opaque;
-        aborts_if !is_token<TokenType>() with Errors::NOT_PUBLISHED;
+        include AbortsIfTokenNotRegistered<TokenType>;
         ensures result.value == 0;
     }
 
@@ -117,7 +116,7 @@ module PontemFramework::Token {
         (token, other)
     }
     spec split {
-        aborts_if token.value < amount with Errors::LIMIT_EXCEEDED;
+        include AbortsIfTokenValueLessThanAmount<TokenType> { token, amount };
         ensures result_1.value == token.value - amount;
         ensures result_2.value == amount;
     }
@@ -134,9 +133,7 @@ module PontemFramework::Token {
         Token { value: amount }
     }
     spec withdraw {
-//        pragma opaque;
         include AbortsIfTokenValueLessThanAmount<TokenType> { token, amount };
-
         ensures token.value == old(token.value) - amount;
         ensures result.value == amount;
     }
@@ -154,7 +151,6 @@ module PontemFramework::Token {
         withdraw(token, val)
     }
     spec withdraw_all {
-        pragma opaque;
         ensures result.value == old(token.value);
         ensures token.value == 0;
     }
@@ -166,8 +162,7 @@ module PontemFramework::Token {
         token1
     }
     spec join {
-        pragma opaque;
-        aborts_if token1.value + token2.value > max_u64() with Errors::LIMIT_EXCEEDED;
+        include AbortsIfSumMaxU64<TokenType> { token1, token2 };
         ensures result.value == token1.value + token2.value;
     }
 
@@ -176,15 +171,19 @@ module PontemFramework::Token {
     /// The `check` tokens is consumed in the process
     public fun deposit<TokenType>(token: &mut Token<TokenType>, check: Token<TokenType>) {
         let Token { value } = check;
-        assert!(MAX_U64 - token.value >= value, Errors::limit_exceeded(ERR_TOKEN));
+        assert!(MAX_U64 - token.value >= value, Errors::limit_exceeded(ERR_INVALID_TOKEN));
         token.value = token.value + value;
     }
     spec deposit {
-        pragma opaque;
-        pragma verify = false;
-        aborts_if false;
+        include AbortsIfSumMaxU64<TokenType> { token1: token, token2: check };
         ensures token.value == old(token.value) + check.value;
     }
+    spec schema AbortsIfSumMaxU64<TokenType> {
+        token1: Token<TokenType>;
+        token2: Token<TokenType>;
+
+        aborts_if token1.value + token2.value > max_u64() with Errors::LIMIT_EXCEEDED;
+    }
 
     /// Destroy a zero-value token. Calls will fail if the `value` in the passed-in `token` is non-zero
     /// so it is impossible to "burn" any non-zero amount of `Pontem` without having
@@ -194,7 +193,6 @@ module PontemFramework::Token {
         assert!(value == 0, Errors::invalid_argument(ERR_DESTRUCTION_OF_NONZERO_TOKEN))
     }
     spec destroy_zero {
-        pragma opaque;
         aborts_if token.value > 0 with Errors::INVALID_ARGUMENT;
     }
 
@@ -227,40 +225,18 @@ module PontemFramework::Token {
         Token<TokenType> { value }
     }
     spec mint {
-        pragma opaque;
         let deployer_addr = get_deployer_addr<TokenType>();
         modifies global<TokenInfo<TokenType>>(deployer_addr);
-        ensures exists<TokenInfo<TokenType>>(deployer_addr);
-        include MintAbortsIf<TokenType> { deployer_addr };
-        include MintEnsures<TokenType>;
-        include MintEmits<TokenType>;
-    }
-    spec schema MintAbortsIf<TokenType> {
-        value: u64;
-        deployer_addr: address;
+
         include AbortsIfTokenNotRegistered<TokenType>;
         let token_info = global<TokenInfo<TokenType>>(deployer_addr);
         aborts_if token_info.total_value + value > max_u128() with Errors::LIMIT_EXCEEDED;
-    }
-    spec schema MintEnsures<TokenType> {
-        value: u64;
-        result: Token<TokenType>;
-        let deployer_addr = get_deployer_addr<TokenType>();
-        let info = global<TokenInfo<TokenType>>(deployer_addr);
-        let post post_info = global<TokenInfo<TokenType>>(deployer_addr);
+
+        let post post_token_info = global<TokenInfo<TokenType>>(deployer_addr);
         ensures exists<TokenInfo<TokenType>>(deployer_addr);
-        ensures post_info == update_field(info, total_value, info.total_value + value);
+        ensures post_token_info == update_field(token_info, total_value, token_info.total_value + value);
         ensures result.value == value;
     }
-    spec schema MintEmits<TokenType> {
-        value: u64;
-        let info = global<TokenInfo<TokenType>>(get_deployer_addr<TokenType>());
-        let msg = MintEvent{
-            amount: value,
-            symbol: info.symbol,
-        };
-        emits msg to info.mint_events;
-    }
 
     /// Burn `to_burn` tokens.
     /// The function requires `BurnCapability`.
@@ -336,12 +312,6 @@ module PontemFramework::Token {
         (MintCapability<TokenType>{}, BurnCapability<TokenType>{})
     }
     spec register_token {
-        include RegisterTokenAbortsIf<TokenType>;
-    }
-    spec schema RegisterTokenAbortsIf<TokenType> {
-        decimals: u8;
-        account: signer;
-
         let acc_addr = Signer::address_of(account);
         aborts_if exists<TokenInfo<TokenType>>(acc_addr) with Errors::ALREADY_PUBLISHED;
         aborts_if acc_addr != get_deployer_addr<TokenType>() with Errors::CUSTOM;