Fix acount.txn_epilogue_v2 incompatible

starcoinorg · Oct 3, 2022 · 3b7534b · 3b7534b
1 parent dfbf3d7
commit 3b7534b
Show file tree

Hide file tree

Showing 10 changed files with 126 additions and 26 deletions.
diff --git a/build/StarcoinFramework/BuildInfo.yaml b/build/StarcoinFramework/BuildInfo.yaml
@@ -327,7 +327,7 @@ compiled_package_info:
     ? address: "0x00000000000000000000000000000001"
       name: YieldFarmingV2
     : StarcoinFramework
-  source_digest: BA11C8B16393EE8048481F812F0038A5D20D703FD7F7B2B9BD5F49840B6703E1
+  source_digest: F1E05061776D5ED1B4717B879662E684E66FDC81A2B9B99AAF4A964F4C42E335
   build_flags:
     dev_mode: false
     test_mode: false

diff --git a/build/StarcoinFramework/bytecode_modules/Account.mv b/build/StarcoinFramework/bytecode_modules/Account.mv
diff --git a/build/StarcoinFramework/bytecode_modules/TransactionManager.mv b/build/StarcoinFramework/bytecode_modules/TransactionManager.mv
diff --git a/build/StarcoinFramework/docs/Account.md b/build/StarcoinFramework/docs/Account.md
@@ -86,6 +86,7 @@ The module for the account resource that governs every account
 -  [Function `txn_epilogue`](#0x1_Account_txn_epilogue)
 -  [Function `transaction_fee_simulate`](#0x1_Account_transaction_fee_simulate)
 -  [Function `txn_epilogue_v2`](#0x1_Account_txn_epilogue_v2)
+-  [Function `txn_epilogue_v3`](#0x1_Account_txn_epilogue_v3)
 -  [Function `remove_zero_balance_entry`](#0x1_Account_remove_zero_balance_entry)
 -  [Function `remove_zero_balance`](#0x1_Account_remove_zero_balance)
 -  [Function `make_event_store_if_not_exist`](#0x1_Account_make_event_store_if_not_exist)
@@ -3327,7 +3328,7 @@ It collects gas and bumps the sequence number
     txn_max_gas_units: u64,
     gas_units_remaining: u64,
 ) <b>acquires</b> <a href="Account.md#0x1_Account">Account</a>, <a href="Account.md#0x1_Account_Balance">Balance</a> {
-    <a href="Account.md#0x1_Account_txn_epilogue_v2">txn_epilogue_v2</a>&lt;TokenType&gt;(account, txn_sender, txn_sequence_number, <a href="Vector.md#0x1_Vector_empty">Vector::empty</a>(), txn_gas_price, txn_max_gas_units, gas_units_remaining,1,1)
+    <a href="Account.md#0x1_Account_txn_epilogue_v3">txn_epilogue_v3</a>&lt;TokenType&gt;(account, txn_sender, txn_sequence_number, <a href="Vector.md#0x1_Vector_empty">Vector::empty</a>(), txn_gas_price, txn_max_gas_units, gas_units_remaining,1,1)
 }
 </code></pre>
 
@@ -3388,7 +3389,7 @@ The epilogue is invoked at the end of transactions.
 It collects gas and bumps the sequence number
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="Account.md#0x1_Account_txn_epilogue_v2">txn_epilogue_v2</a>&lt;TokenType: store&gt;(account: &signer, txn_sender: <b>address</b>, txn_sequence_number: u64, txn_authentication_key_preimage: vector&lt;u8&gt;, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, stc_price: u128, stc_price_scaling: u128)
+<pre><code><b>public</b> <b>fun</b> <a href="Account.md#0x1_Account_txn_epilogue_v2">txn_epilogue_v2</a>&lt;TokenType: store&gt;(account: &signer, txn_sender: <b>address</b>, txn_sequence_number: u64, txn_authentication_key_preimage: vector&lt;u8&gt;, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64)
 </code></pre>
 
 
@@ -3405,6 +3406,85 @@ It collects gas and bumps the sequence number
     txn_gas_price: u64,
     txn_max_gas_units: u64,
     gas_units_remaining: u64,
+) <b>acquires</b> <a href="Account.md#0x1_Account">Account</a>, <a href="Account.md#0x1_Account_Balance">Balance</a> {
+    <a href="Account.md#0x1_Account_txn_epilogue_v3">txn_epilogue_v3</a>&lt;TokenType&gt;(
+        account,
+        txn_sender,
+        txn_sequence_number,
+        txn_authentication_key_preimage,
+        txn_gas_price,
+        txn_max_gas_units,
+        gas_units_remaining,1,1)
+}
+</code></pre>
+
+
+
+</details>
+
+<details>
+<summary>Specification</summary>
+
+
+
+<pre><code><b>pragma</b> verify = <b>false</b>;
+<b>aborts_if</b> <a href="Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account) != <a href="CoreAddresses.md#0x1_CoreAddresses_GENESIS_ADDRESS">CoreAddresses::GENESIS_ADDRESS</a>();
+<b>aborts_if</b> !<b>exists</b>&lt;<a href="Account.md#0x1_Account">Account</a>&gt;(txn_sender);
+<b>aborts_if</b> !<b>exists</b>&lt;<a href="Account.md#0x1_Account_Balance">Balance</a>&lt;TokenType&gt;&gt;(txn_sender);
+<b>aborts_if</b> txn_max_gas_units &lt; gas_units_remaining;
+<b>let</b> transaction_fee_amount = txn_gas_price * (txn_max_gas_units - gas_units_remaining);
+<b>aborts_if</b> transaction_fee_amount &gt; max_u128();
+<b>aborts_if</b> <b>global</b>&lt;<a href="Account.md#0x1_Account_Balance">Balance</a>&lt;TokenType&gt;&gt;(txn_sender).token.value &lt; transaction_fee_amount;
+<b>aborts_if</b> txn_sequence_number + 1 &gt; max_u64();
+<b>aborts_if</b> txn_gas_price * (txn_max_gas_units - gas_units_remaining) &gt; 0 &&
+          <b>global</b>&lt;<a href="Account.md#0x1_Account_Balance">Balance</a>&lt;TokenType&gt;&gt;(txn_sender).token.value  &lt; txn_gas_price * (txn_max_gas_units - gas_units_remaining);
+<b>aborts_if</b> txn_gas_price * (txn_max_gas_units - gas_units_remaining) &gt; 0 &&
+          !<b>exists</b>&lt;<a href="TransactionFee.md#0x1_TransactionFee_TransactionFee">TransactionFee::TransactionFee</a>&lt;TokenType&gt;&gt;(<a href="CoreAddresses.md#0x1_CoreAddresses_GENESIS_ADDRESS">CoreAddresses::GENESIS_ADDRESS</a>());
+<b>aborts_if</b> txn_gas_price * (txn_max_gas_units - gas_units_remaining) &gt; 0 &&
+          <b>global</b>&lt;<a href="TransactionFee.md#0x1_TransactionFee_TransactionFee">TransactionFee::TransactionFee</a>&lt;TokenType&gt;&gt;(<a href="CoreAddresses.md#0x1_CoreAddresses_GENESIS_ADDRESS">CoreAddresses::GENESIS_ADDRESS</a>()).fee.value + txn_gas_price * (txn_max_gas_units - gas_units_remaining) &gt; max_u128();
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> verify = <b>false</b>;
+<b>aborts_if</b> <a href="Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account) != <a href="CoreAddresses.md#0x1_CoreAddresses_GENESIS_ADDRESS">CoreAddresses::GENESIS_ADDRESS</a>();
+<b>aborts_if</b> !<b>exists</b>&lt;<a href="Account.md#0x1_Account">Account</a>&gt;(txn_sender);
+<b>aborts_if</b> !<b>exists</b>&lt;<a href="Account.md#0x1_Account_Balance">Balance</a>&lt;TokenType&gt;&gt;(txn_sender);
+<b>aborts_if</b> txn_sequence_number + 1 &gt; max_u64();
+<b>aborts_if</b> !<b>exists</b>&lt;<a href="Account.md#0x1_Account_Balance">Balance</a>&lt;TokenType&gt;&gt;(txn_sender);
+<b>aborts_if</b> txn_max_gas_units &lt; gas_units_remaining;
+</code></pre>
+
+
+
+</details>
+
+<a name="0x1_Account_txn_epilogue_v3"></a>
+
+## Function `txn_epilogue_v3`
+
+The epilogue is invoked at the end of transactions.
+It collects gas and bumps the sequence number
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="Account.md#0x1_Account_txn_epilogue_v3">txn_epilogue_v3</a>&lt;TokenType: store&gt;(account: &signer, txn_sender: <b>address</b>, txn_sequence_number: u64, txn_authentication_key_preimage: vector&lt;u8&gt;, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, stc_price: u128, stc_price_scaling: u128)
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="Account.md#0x1_Account_txn_epilogue_v3">txn_epilogue_v3</a>&lt;TokenType: store&gt;(
+    account: &signer,
+    txn_sender: <b>address</b>,
+    txn_sequence_number: u64,
+    txn_authentication_key_preimage: vector&lt;u8&gt;,
+    txn_gas_price: u64,
+    txn_max_gas_units: u64,
+    gas_units_remaining: u64,
     stc_price: u128,
     stc_price_scaling: u128,
 ) <b>acquires</b> <a href="Account.md#0x1_Account">Account</a>, <a href="Account.md#0x1_Account_Balance">Balance</a> {
@@ -3448,24 +3528,6 @@ It collects gas and bumps the sequence number
 
 
 
-</details>
-
-<details>
-<summary>Specification</summary>
-
-
-
-<pre><code><b>pragma</b> verify = <b>false</b>;
-<b>aborts_if</b> <a href="Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account) != <a href="CoreAddresses.md#0x1_CoreAddresses_GENESIS_ADDRESS">CoreAddresses::GENESIS_ADDRESS</a>();
-<b>aborts_if</b> !<b>exists</b>&lt;<a href="Account.md#0x1_Account">Account</a>&gt;(txn_sender);
-<b>aborts_if</b> !<b>exists</b>&lt;<a href="Account.md#0x1_Account_Balance">Balance</a>&lt;TokenType&gt;&gt;(txn_sender);
-<b>aborts_if</b> txn_sequence_number + 1 &gt; max_u64();
-<b>aborts_if</b> !<b>exists</b>&lt;<a href="Account.md#0x1_Account_Balance">Balance</a>&lt;TokenType&gt;&gt;(txn_sender);
-<b>aborts_if</b> txn_max_gas_units &lt; gas_units_remaining;
-</code></pre>
-
-
-
 </details>
 
 <a name="0x1_Account_remove_zero_balance_entry"></a>

diff --git a/build/StarcoinFramework/docs/TransactionManager.md b/build/StarcoinFramework/docs/TransactionManager.md
@@ -338,7 +338,7 @@ It collects gas and bumps the sequence number
     }<b>else</b>{
         (1,1)
     };
-    <a href="Account.md#0x1_Account_txn_epilogue_v2">Account::txn_epilogue_v2</a>&lt;TokenType&gt;(
+    <a href="Account.md#0x1_Account_txn_epilogue_v3">Account::txn_epilogue_v3</a>&lt;TokenType&gt;(
         &account,
         txn_sender,
         txn_sequence_number,

diff --git a/build/StarcoinFramework/source_maps/Account.mvsm b/build/StarcoinFramework/source_maps/Account.mvsm
diff --git a/build/StarcoinFramework/source_maps/TransactionManager.mvsm b/build/StarcoinFramework/source_maps/TransactionManager.mvsm
diff --git a/integration-tests/account/txn_prologue_and_epilogue.move b/integration-tests/account/txn_prologue_and_epilogue.move
@@ -382,7 +382,7 @@ script {
         );
         // execute the txn...
         let gas_units_remaining = 10;
-        Account::txn_epilogue_v2<DummyToken>(
+        Account::txn_epilogue_v3<DummyToken>(
             &account,
             txn_sender,
             txn_sequence_number,

diff --git a/sources/Account.move b/sources/Account.move
@@ -1083,7 +1083,7 @@ module Account {
         txn_max_gas_units: u64,
         gas_units_remaining: u64,
     ) acquires Account, Balance {
-        txn_epilogue_v2<TokenType>(account, txn_sender, txn_sequence_number, Vector::empty(), txn_gas_price, txn_max_gas_units, gas_units_remaining,1,1)
+        txn_epilogue_v3<TokenType>(account, txn_sender, txn_sequence_number, Vector::empty(), txn_gas_price, txn_max_gas_units, gas_units_remaining,1,1)
     }
 
     spec txn_epilogue {
@@ -1102,7 +1102,6 @@ module Account {
         transaction_fee_token = if (transaction_fee_token == 0 && transaction_fee_stc > 0 ) { 1 } else { transaction_fee_token};
         (transaction_fee_stc, transaction_fee_token)
     }
-
     /// The epilogue is invoked at the end of transactions.
     /// It collects gas and bumps the sequence number
     public fun txn_epilogue_v2<TokenType: store>(
@@ -1113,6 +1112,45 @@ module Account {
         txn_gas_price: u64,
         txn_max_gas_units: u64,
         gas_units_remaining: u64,
+    ) acquires Account, Balance {
+        txn_epilogue_v3<TokenType>(
+            account,
+            txn_sender,
+            txn_sequence_number,
+            txn_authentication_key_preimage,
+            txn_gas_price,
+            txn_max_gas_units,
+            gas_units_remaining,1,1)
+    }
+
+    spec txn_epilogue_v2 {
+        pragma verify = false; // Todo: fix me, cost too much time
+        aborts_if Signer::address_of(account) != CoreAddresses::GENESIS_ADDRESS();
+        aborts_if !exists<Account>(txn_sender);
+        aborts_if !exists<Balance<TokenType>>(txn_sender);
+        aborts_if txn_max_gas_units < gas_units_remaining;
+        let transaction_fee_amount = txn_gas_price * (txn_max_gas_units - gas_units_remaining);
+        aborts_if transaction_fee_amount > max_u128();
+        aborts_if global<Balance<TokenType>>(txn_sender).token.value < transaction_fee_amount;
+        aborts_if txn_sequence_number + 1 > max_u64();
+        aborts_if txn_gas_price * (txn_max_gas_units - gas_units_remaining) > 0 &&
+                  global<Balance<TokenType>>(txn_sender).token.value  < txn_gas_price * (txn_max_gas_units - gas_units_remaining);
+        aborts_if txn_gas_price * (txn_max_gas_units - gas_units_remaining) > 0 &&
+                  !exists<TransactionFee::TransactionFee<TokenType>>(CoreAddresses::GENESIS_ADDRESS());
+        aborts_if txn_gas_price * (txn_max_gas_units - gas_units_remaining) > 0 &&
+                  global<TransactionFee::TransactionFee<TokenType>>(CoreAddresses::GENESIS_ADDRESS()).fee.value + txn_gas_price * (txn_max_gas_units - gas_units_remaining) > max_u128();
+    }
+
+    /// The epilogue is invoked at the end of transactions.
+    /// It collects gas and bumps the sequence number
+    public fun txn_epilogue_v3<TokenType: store>(
+        account: &signer,
+        txn_sender: address,
+        txn_sequence_number: u64,
+        txn_authentication_key_preimage: vector<u8>,
+        txn_gas_price: u64,
+        txn_max_gas_units: u64,
+        gas_units_remaining: u64,
         stc_price: u128,
         stc_price_scaling: u128,
     ) acquires Account, Balance {

diff --git a/sources/TransactionManager.move b/sources/TransactionManager.move
@@ -176,7 +176,7 @@ module TransactionManager {
         }else{
             (1,1)
         };
-        Account::txn_epilogue_v2<TokenType>(
+        Account::txn_epilogue_v3<TokenType>(
             &account,
             txn_sender,
             txn_sequence_number,