fix rewards minting and rebate burning issues

crates/sui-cost/tests/snapshots/empirical_transaction_cost__good_snapshot-2.snap

@@ -4,13 +4,13 @@ expression: common_costs_estimate
 ---
 {
   "MergeCoin": {
-    "computation_cost": 5911,
-    "storage_cost": 8727,
+    "computation_cost": 5922,
+    "storage_cost": 8743,
     "storage_rebate": 0
   },
   "Publish": {
-    "computation_cost": 6691,
-    "storage_cost": 9812,
+    "computation_cost": 6702,
+    "storage_cost": 9828,
     "storage_rebate": 0
   },
   "SharedCounterAssertValue": {
@@ -29,8 +29,8 @@ expression: common_costs_estimate
     "storage_rebate": 0
   },
   "SplitCoin": {
-    "computation_cost": 5889,
-    "storage_cost": 8694,
+    "computation_cost": 5900,
+    "storage_cost": 8710,
     "storage_rebate": 0
   },
   "TransferPortionSuiCoin": {

crates/sui-cost/tests/snapshots/empirical_transaction_cost__good_snapshot.snap

@@ -4,12 +4,12 @@ expression: common_costs_actual
 ---
 {
   "MergeCoin": {
-    "computation_cost": 709,
+    "computation_cost": 710,
     "storage_cost": 32,
     "storage_rebate": 0
   },
   "Publish": {
-    "computation_cost": 958,
+    "computation_cost": 959,
     "storage_cost": 119,
     "storage_rebate": 0
   },
@@ -29,7 +29,7 @@ expression: common_costs_actual
     "storage_rebate": 15
   },
   "SplitCoin": {
-    "computation_cost": 819,
+    "computation_cost": 820,
     "storage_cost": 80,
     "storage_rebate": 0
   },

crates/sui-framework/docs/balance.md

@@ -20,6 +20,8 @@ custom coins with <code><a href="balance.md#0x2_balance_Supply">Supply</a></code
 -  [Function `join`](#0x2_balance_join)
 -  [Function `split`](#0x2_balance_split)
 -  [Function `destroy_zero`](#0x2_balance_destroy_zero)
+-  [Function `create_staking_rewards`](#0x2_balance_create_staking_rewards)
+-  [Function `destroy_storage_rebates`](#0x2_balance_destroy_storage_rebates)
 
 
 <pre><code></code></pre>
@@ -404,4 +406,58 @@ Destroy a zero <code><a href="balance.md#0x2_balance_Balance">Balance</a></code>
 
 
 
+</details>
+
+<a name="0x2_balance_create_staking_rewards"></a>
+
+## Function `create_staking_rewards`
+
+CAUTION: this function creates a <code><a href="balance.md#0x2_balance_Balance">Balance</a></code> without increasing the supply.
+It should only be called by <code><a href="sui_system.md#0x2_sui_system_advance_epoch">sui_system::advance_epoch</a></code> to create staking rewards,
+and nowhere else.
+
+
+<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="balance.md#0x2_balance_create_staking_rewards">create_staking_rewards</a>&lt;T&gt;(value: u64): <a href="balance.md#0x2_balance_Balance">balance::Balance</a>&lt;T&gt;
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="balance.md#0x2_balance_create_staking_rewards">create_staking_rewards</a>&lt;T&gt;(value: u64): <a href="balance.md#0x2_balance_Balance">Balance</a>&lt;T&gt; {
+    <a href="balance.md#0x2_balance_Balance">Balance</a> { value }
+}
+</code></pre>
+
+
+
+</details>
+
+<a name="0x2_balance_destroy_storage_rebates"></a>
+
+## Function `destroy_storage_rebates`
+
+CAUTION: this function destroys a <code><a href="balance.md#0x2_balance_Balance">Balance</a></code> without decreasing the supply.
+It should only be called by <code><a href="sui_system.md#0x2_sui_system_advance_epoch">sui_system::advance_epoch</a></code> to destroy storage rebates,
+and nowhere else.
+
+
+<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="balance.md#0x2_balance_destroy_storage_rebates">destroy_storage_rebates</a>&lt;T&gt;(self: <a href="balance.md#0x2_balance_Balance">balance::Balance</a>&lt;T&gt;)
+</code></pre>
+
+
+
+<details>
+<summary>Implementation</summary>
+
+
+<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="balance.md#0x2_balance_destroy_storage_rebates">destroy_storage_rebates</a>&lt;T&gt;(self: <a href="balance.md#0x2_balance_Balance">Balance</a>&lt;T&gt;) {
+    <b>let</b> <a href="balance.md#0x2_balance_Balance">Balance</a> { value: _ } = self;
+}
+</code></pre>
+
+
+
 </details>

crates/sui-framework/docs/sui_system.md

@@ -804,8 +804,8 @@ gas coins.
     // Validator will make a special system call <b>with</b> sender set <b>as</b> 0x0.
     <b>assert</b>!(<a href="tx_context.md#0x2_tx_context_sender">tx_context::sender</a>(ctx) == @0x0, 0);
 
-    <b>let</b> storage_reward = <a href="balance.md#0x2_balance_increase_supply">balance::increase_supply</a>(&<b>mut</b> self.sui_supply, storage_charge);
-    <b>let</b> computation_reward = <a href="balance.md#0x2_balance_increase_supply">balance::increase_supply</a>(&<b>mut</b> self.sui_supply, computation_charge);
+    <b>let</b> storage_reward = <a href="balance.md#0x2_balance_create_staking_rewards">balance::create_staking_rewards</a>(storage_charge);
+    <b>let</b> computation_reward = <a href="balance.md#0x2_balance_create_staking_rewards">balance::create_staking_rewards</a>(computation_charge);
 
     <b>let</b> delegation_stake = <a href="validator_set.md#0x2_validator_set_total_delegation_stake">validator_set::total_delegation_stake</a>(&self.validators);
     <b>let</b> validator_stake = <a href="validator_set.md#0x2_validator_set_total_validator_stake">validator_set::total_validator_stake</a>(&self.validators);
@@ -848,9 +848,9 @@ gas coins.
     <a href="balance.md#0x2_balance_join">balance::join</a>(&<b>mut</b> self.storage_fund, storage_fund_reward);
     <a href="balance.md#0x2_balance_join">balance::join</a>(&<b>mut</b> self.storage_fund, computation_reward);
 
-    // Burn the storage rebate.
+    // Destroy the storage rebate.
     <b>assert</b>!(<a href="balance.md#0x2_balance_value">balance::value</a>(&self.storage_fund) &gt;= storage_rebate, 0);
-    <a href="balance.md#0x2_balance_decrease_supply">balance::decrease_supply</a>(&<b>mut</b> self.sui_supply, <a href="balance.md#0x2_balance_split">balance::split</a>(&<b>mut</b> self.storage_fund, storage_rebate));
+    <a href="balance.md#0x2_balance_destroy_storage_rebates">balance::destroy_storage_rebates</a>(<a href="balance.md#0x2_balance_split">balance::split</a>(&<b>mut</b> self.storage_fund, storage_rebate));
 
     // Validator reports are only valid for the epoch.
     // TODO: or do we want <b>to</b> make it persistent and validators have <b>to</b> explicitly change their scores?
@@ -860,6 +860,21 @@ gas coins.
 
 
 
+</details>
+
+<details>
+<summary>Specification</summary>
+
+
+Total supply of SUI shouldn't change.
+
+
+<pre><code><b>ensures</b> <a href="balance.md#0x2_balance_supply_value">balance::supply_value</a>(self.sui_supply)
+    == <b>old</b>(<a href="balance.md#0x2_balance_supply_value">balance::supply_value</a>(self.sui_supply));
+</code></pre>
+
+
+
 </details>
 
 <a name="0x2_sui_system_epoch"></a>

crates/sui-framework/sources/balance.move

@@ -5,6 +5,8 @@
 /// module to allow balance operations and can be used to implement
 /// custom coins with `Supply` and `Balance`s.
 module sui::balance {
+    friend sui::sui_system;
+
     /// For when trying to destroy a non-zero balance.
     const ENonZero: u64 = 0;
 
@@ -101,6 +103,20 @@ module sui::balance {
         aborts_if balance.value != 0 with ENonZero;
     }
 
+    /// CAUTION: this function creates a `Balance` without increasing the supply. 
+    /// It should only be called by `sui_system::advance_epoch` to create staking rewards,
+    /// and nowhere else.
+    public(friend) fun create_staking_rewards<T>(value: u64): Balance<T> {
+        Balance { value }
+    }
+
+    /// CAUTION: this function destroys a `Balance` without decreasing the supply. 
+    /// It should only be called by `sui_system::advance_epoch` to destroy storage rebates,
+    /// and nowhere else.
+    public(friend) fun destroy_storage_rebates<T>(self: Balance<T>) {
+        let Balance { value: _ } = self;
+    }
+
     #[test_only]
     /// Create a `Balance` of any coin for testing purposes.
     public fun create_for_testing<T>(value: u64): Balance<T> {

crates/sui-framework/sources/governance/sui_system.move

@@ -360,8 +360,8 @@ module sui::sui_system {
         // Validator will make a special system call with sender set as 0x0.
         assert!(tx_context::sender(ctx) == @0x0, 0);
 
-        let storage_reward = balance::increase_supply(&mut self.sui_supply, storage_charge);
-        let computation_reward = balance::increase_supply(&mut self.sui_supply, computation_charge);
+        let storage_reward = balance::create_staking_rewards(storage_charge);
+        let computation_reward = balance::create_staking_rewards(computation_charge);
 
         let delegation_stake = validator_set::total_delegation_stake(&self.validators);
         let validator_stake = validator_set::total_validator_stake(&self.validators);
@@ -404,15 +404,21 @@ module sui::sui_system {
         balance::join(&mut self.storage_fund, storage_fund_reward);
         balance::join(&mut self.storage_fund, computation_reward);
 
-        // Burn the storage rebate.
+        // Destroy the storage rebate.
         assert!(balance::value(&self.storage_fund) >= storage_rebate, 0);
-        balance::decrease_supply(&mut self.sui_supply, balance::split(&mut self.storage_fund, storage_rebate));
+        balance::destroy_storage_rebates(balance::split(&mut self.storage_fund, storage_rebate));
 
         // Validator reports are only valid for the epoch.
         // TODO: or do we want to make it persistent and validators have to explicitly change their scores?
         self.validator_report_records = vec_map::empty();
     }
 
+    spec advance_epoch {
+        /// Total supply of SUI shouldn't change.
+        ensures balance::supply_value(self.sui_supply) 
+            == old(balance::supply_value(self.sui_supply));
+    }
+
     /// Return the current epoch number. Useful for applications that need a coarse-grained concept of time,
     /// since epochs are ever-increasing and epoch changes are intended to happen every 24 hours.
     public fun epoch(self: &SuiSystemState): u64 {

crates/sui/src/sui_move/sui-natives.bpl

@@ -122,7 +122,7 @@ procedure {:inline 1} $2_ed25519_ed25519_verify(signature: Vec (int), public_key
 // ==================================================================================
 // Native bulletproofs
 
-procedure {:inline 1} $2_bulletproofs_native_verify_full_range_proof(proof: Vec (int), commitment: Vec (int), bit_length: int);
+procedure {:inline 1} $2_bulletproofs_native_verify_full_range_proof(proof: Vec (int), commitment: Vec (int), bit_length: int) returns (res: bool);
 
 // ==================================================================================
 // Native elliptic_curve