[move framework][move-prover][DRAFT] Refactor coins for better verifi…

…cation

Previous, Genesis called Coin1::initialize, which returned mint and
burn capabilities.  Genesis then called
LibraAccount::create_treasury_compliance_account with these, and that
function called Libra::publish_mint_capability with it as an argument.

This code bypasses genesis. The capabilities are published directly in
Coin1.  The main advantage is that this will make it possible to
verify that only the treasury compliance account can mint Coin1
based only on the code in the Coin1 module and its dependencies.
This is a step in trying to make it easier to prove properties such
as only the specified account can mint the coin.

Similarly, Coin2 for all of the above.

Closes: aptos-labs#4879
Approved by: sblackshear

language/stdlib/modules/Coin1.move

@@ -1,27 +1,28 @@
 address 0x1 {
 
 module Coin1 {
-    use 0x1::Libra::{Self,
-    // RegisterNewCurrency
-    };
+    use 0x1::Libra;
     use 0x1::FixedPoint32;
 
     struct Coin1 { }
 
     public fun initialize(
-        account: &signer,
+        lr_account: &signer,
         tc_account: &signer,
-    ): (Libra::MintCapability<Coin1>, Libra::BurnCapability<Coin1>) {
+    ) {
         // Register the Coin1 currency.
-        Libra::register_currency<Coin1>(
-            account,
-            tc_account,
-            FixedPoint32::create_from_rational(1, 2), // exchange rate to LBR
-            false,   // is_synthetic
-            1000000, // scaling_factor = 10^6
-            100,     // fractional_part = 10^2
-            b"Coin1",
-        )
+        let (coin1_mint_cap, coin1_burn_cap) =
+            Libra::register_currency<Coin1>(
+                lr_account,
+                tc_account,
+                FixedPoint32::create_from_rational(1, 2), // exchange rate to LBR
+                false,   // is_synthetic
+                1000000, // scaling_factor = 10^6
+                100,     // fractional_part = 10^2
+                b"Coin1"
+            );
+        Libra::publish_mint_capability<Coin1>(tc_account, coin1_mint_cap, tc_account);
+        Libra::publish_burn_capability<Coin1>(tc_account, coin1_burn_cap, tc_account);
     }
 }
 

language/stdlib/modules/Coin2.move

@@ -2,26 +2,27 @@ address 0x1 {
 
 module Coin2 {
     use 0x1::FixedPoint32;
-    use 0x1::Libra::{Self,
-    // RegisterNewCurrency
-    };
+    use 0x1::Libra;
 
     struct Coin2 { }
 
     public fun initialize(
-        account: &signer,
+        lr_account: &signer,
         tc_account: &signer,
-    ): (Libra::MintCapability<Coin2>, Libra::BurnCapability<Coin2>) {
+    ) {
         // Register the Coin2 currency.
-        Libra::register_currency<Coin2>(
-            account,
-            tc_account,
-            FixedPoint32::create_from_rational(1, 2), // exchange rate to LBR
-            false,   // is_synthetic
-            1000000, // scaling_factor = 10^6
-            100,     // fractional_part = 10^2
-            b"Coin2",
-        )
+        let (coin2_mint_cap, coin2_burn_cap) =
+            Libra::register_currency<Coin2>(
+                lr_account,
+                tc_account,
+                FixedPoint32::create_from_rational(1, 2), // exchange rate to LBR
+                false,   // is_synthetic
+                1000000, // scaling_factor = 10^6
+                100,     // fractional_part = 10^2
+                b"Coin2",
+            );
+        Libra::publish_mint_capability<Coin2>(tc_account, coin2_mint_cap, tc_account);
+        Libra::publish_burn_capability<Coin2>(tc_account, coin2_burn_cap, tc_account);
     }
 }
 

language/stdlib/modules/Genesis.move

@@ -49,14 +49,9 @@ module Genesis {
         VASP::initialize(lr_account);
 
         // Currency setup
-        let (coin1_mint_cap, coin1_burn_cap) = Coin1::initialize(
-            lr_account,
-            tc_account,
-        );
-        let (coin2_mint_cap, coin2_burn_cap) = Coin2::initialize(
-            lr_account,
-            tc_account,
-        );
+        Coin1::initialize(lr_account, tc_account);
+        Coin2::initialize(lr_account, tc_account);
+
         LBR::initialize(
             lr_account,
             tc_account,
@@ -77,13 +72,8 @@ module Genesis {
         // Create the treasury compliance account
         LibraAccount::create_treasury_compliance_account(
             lr_account,
-            tc_account,
             tc_addr,
             copy dummy_auth_key_prefix,
-            coin1_mint_cap,
-            coin1_burn_cap,
-            coin2_mint_cap,
-            coin2_burn_cap,
         );
 
         LibraTransactionTimeout::initialize(lr_account);

language/stdlib/modules/Libra.move

@@ -212,10 +212,10 @@ module Libra {
     public fun publish_mint_capability<CoinType>(
         publish_account: &signer,
         cap: MintCapability<CoinType>,
-        tc_signer: &signer,
+        tc_account: &signer,
     ) {
         // TODO: abort code
-        assert(has_treasury_compliance_role(tc_signer), 919402);
+        assert(has_treasury_compliance_role(tc_account), 919402);
         assert_is_currency<CoinType>();
         move_to(publish_account, cap)
     }

language/stdlib/modules/LibraAccount.move

@@ -504,23 +504,13 @@ module LibraAccount {
     /// `auth_key_prefix` | `new_account_address`
     public fun create_treasury_compliance_account(
         lr_account: &signer,
-        tc_account: &signer,
-
         new_account_address: address,
         auth_key_prefix: vector<u8>,
-        coin1_mint_cap: Libra::MintCapability<Coin1>,
-        coin1_burn_cap: Libra::BurnCapability<Coin1>,
-        coin2_mint_cap: Libra::MintCapability<Coin2>,
-        coin2_burn_cap: Libra::BurnCapability<Coin2>,
     ) {
         LibraTimestamp::assert_is_genesis();
         // TODO: abort code
         assert(Roles::has_libra_root_role(lr_account), 919408);
         let new_account = create_signer(new_account_address);
-        Libra::publish_mint_capability<Coin1>(&new_account, coin1_mint_cap, tc_account);
-        Libra::publish_burn_capability<Coin1>(&new_account, coin1_burn_cap, tc_account);
-        Libra::publish_mint_capability<Coin2>(&new_account, coin2_mint_cap, tc_account);
-        Libra::publish_burn_capability<Coin2>(&new_account, coin2_burn_cap, tc_account);
         SlidingNonce::publish_nonce_resource(lr_account, &new_account);
         Event::publish_generator(&new_account);
         make_account(new_account, auth_key_prefix)

language/stdlib/modules/doc/Coin1.md

@@ -44,7 +44,7 @@
 
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="#0x1_Coin1_initialize">initialize</a>(account: &signer, tc_account: &signer): (<a href="Libra.md#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;<a href="#0x1_Coin1_Coin1">Coin1::Coin1</a>&gt;, <a href="Libra.md#0x1_Libra_BurnCapability">Libra::BurnCapability</a>&lt;<a href="#0x1_Coin1_Coin1">Coin1::Coin1</a>&gt;)
+<pre><code><b>public</b> <b>fun</b> <a href="#0x1_Coin1_initialize">initialize</a>(lr_account: &signer, tc_account: &signer)
 </code></pre>
 
 
@@ -54,19 +54,22 @@
 
 
 <pre><code><b>public</b> <b>fun</b> <a href="#0x1_Coin1_initialize">initialize</a>(
-    account: &signer,
+    lr_account: &signer,
     tc_account: &signer,
-): (<a href="Libra.md#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;<a href="#0x1_Coin1">Coin1</a>&gt;, <a href="Libra.md#0x1_Libra_BurnCapability">Libra::BurnCapability</a>&lt;<a href="#0x1_Coin1">Coin1</a>&gt;) {
+) {
     // Register the <a href="#0x1_Coin1">Coin1</a> currency.
-    <a href="Libra.md#0x1_Libra_register_currency">Libra::register_currency</a>&lt;<a href="#0x1_Coin1">Coin1</a>&gt;(
-        account,
-        tc_account,
-        <a href="FixedPoint32.md#0x1_FixedPoint32_create_from_rational">FixedPoint32::create_from_rational</a>(1, 2), // exchange rate <b>to</b> <a href="LBR.md#0x1_LBR">LBR</a>
-        <b>false</b>,   // is_synthetic
-        1000000, // scaling_factor = 10^6
-        100,     // fractional_part = 10^2
-        b"<a href="#0x1_Coin1">Coin1</a>",
-    )
+    <b>let</b> (coin1_mint_cap, coin1_burn_cap) =
+        <a href="Libra.md#0x1_Libra_register_currency">Libra::register_currency</a>&lt;<a href="#0x1_Coin1">Coin1</a>&gt;(
+            lr_account,
+            tc_account,
+            <a href="FixedPoint32.md#0x1_FixedPoint32_create_from_rational">FixedPoint32::create_from_rational</a>(1, 2), // exchange rate <b>to</b> <a href="LBR.md#0x1_LBR">LBR</a>
+            <b>false</b>,   // is_synthetic
+            1000000, // scaling_factor = 10^6
+            100,     // fractional_part = 10^2
+            b"<a href="#0x1_Coin1">Coin1</a>"
+        );
+    <a href="Libra.md#0x1_Libra_publish_mint_capability">Libra::publish_mint_capability</a>&lt;<a href="#0x1_Coin1">Coin1</a>&gt;(tc_account, coin1_mint_cap, tc_account);
+    <a href="Libra.md#0x1_Libra_publish_burn_capability">Libra::publish_burn_capability</a>&lt;<a href="#0x1_Coin1">Coin1</a>&gt;(tc_account, coin1_burn_cap, tc_account);
 }
 </code></pre>
 

language/stdlib/modules/doc/Coin2.md

@@ -44,7 +44,7 @@
 
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="#0x1_Coin2_initialize">initialize</a>(account: &signer, tc_account: &signer): (<a href="Libra.md#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;<a href="#0x1_Coin2_Coin2">Coin2::Coin2</a>&gt;, <a href="Libra.md#0x1_Libra_BurnCapability">Libra::BurnCapability</a>&lt;<a href="#0x1_Coin2_Coin2">Coin2::Coin2</a>&gt;)
+<pre><code><b>public</b> <b>fun</b> <a href="#0x1_Coin2_initialize">initialize</a>(lr_account: &signer, tc_account: &signer)
 </code></pre>
 
 
@@ -54,19 +54,22 @@
 
 
 <pre><code><b>public</b> <b>fun</b> <a href="#0x1_Coin2_initialize">initialize</a>(
-    account: &signer,
+    lr_account: &signer,
     tc_account: &signer,
-): (<a href="Libra.md#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;<a href="#0x1_Coin2">Coin2</a>&gt;, <a href="Libra.md#0x1_Libra_BurnCapability">Libra::BurnCapability</a>&lt;<a href="#0x1_Coin2">Coin2</a>&gt;) {
+) {
     // Register the <a href="#0x1_Coin2">Coin2</a> currency.
-    <a href="Libra.md#0x1_Libra_register_currency">Libra::register_currency</a>&lt;<a href="#0x1_Coin2">Coin2</a>&gt;(
-        account,
-        tc_account,
-        <a href="FixedPoint32.md#0x1_FixedPoint32_create_from_rational">FixedPoint32::create_from_rational</a>(1, 2), // exchange rate <b>to</b> <a href="LBR.md#0x1_LBR">LBR</a>
-        <b>false</b>,   // is_synthetic
-        1000000, // scaling_factor = 10^6
-        100,     // fractional_part = 10^2
-        b"<a href="#0x1_Coin2">Coin2</a>",
-    )
+    <b>let</b> (coin2_mint_cap, coin2_burn_cap) =
+        <a href="Libra.md#0x1_Libra_register_currency">Libra::register_currency</a>&lt;<a href="#0x1_Coin2">Coin2</a>&gt;(
+            lr_account,
+            tc_account,
+            <a href="FixedPoint32.md#0x1_FixedPoint32_create_from_rational">FixedPoint32::create_from_rational</a>(1, 2), // exchange rate <b>to</b> <a href="LBR.md#0x1_LBR">LBR</a>
+            <b>false</b>,   // is_synthetic
+            1000000, // scaling_factor = 10^6
+            100,     // fractional_part = 10^2
+            b"<a href="#0x1_Coin2">Coin2</a>",
+        );
+    <a href="Libra.md#0x1_Libra_publish_mint_capability">Libra::publish_mint_capability</a>&lt;<a href="#0x1_Coin2">Coin2</a>&gt;(tc_account, coin2_mint_cap, tc_account);
+    <a href="Libra.md#0x1_Libra_publish_burn_capability">Libra::publish_burn_capability</a>&lt;<a href="#0x1_Coin2">Coin2</a>&gt;(tc_account, coin2_burn_cap, tc_account);
 }
 </code></pre>
 

language/stdlib/modules/doc/Genesis.md

@@ -48,14 +48,9 @@
     <a href="VASP.md#0x1_VASP_initialize">VASP::initialize</a>(lr_account);
 
     // Currency setup
-    <b>let</b> (coin1_mint_cap, coin1_burn_cap) = <a href="Coin1.md#0x1_Coin1_initialize">Coin1::initialize</a>(
-        lr_account,
-        tc_account,
-    );
-    <b>let</b> (coin2_mint_cap, coin2_burn_cap) = <a href="Coin2.md#0x1_Coin2_initialize">Coin2::initialize</a>(
-        lr_account,
-        tc_account,
-    );
+    <a href="Coin1.md#0x1_Coin1_initialize">Coin1::initialize</a>(lr_account, tc_account);
+    <a href="Coin2.md#0x1_Coin2_initialize">Coin2::initialize</a>(lr_account, tc_account);
+
     <a href="LBR.md#0x1_LBR_initialize">LBR::initialize</a>(
         lr_account,
         tc_account,
@@ -76,13 +71,8 @@
     // Create the treasury compliance account
     <a href="LibraAccount.md#0x1_LibraAccount_create_treasury_compliance_account">LibraAccount::create_treasury_compliance_account</a>(
         lr_account,
-        tc_account,
         tc_addr,
         <b>copy</b> dummy_auth_key_prefix,
-        coin1_mint_cap,
-        coin1_burn_cap,
-        coin2_mint_cap,
-        coin2_burn_cap,
     );
 
     <a href="LibraTransactionTimeout.md#0x1_LibraTransactionTimeout_initialize">LibraTransactionTimeout::initialize</a>(lr_account);

language/stdlib/modules/doc/Libra.md

@@ -753,7 +753,7 @@ The caller must pass a
 <code>TreasuryComplianceRole</code> capability.
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="#0x1_Libra_publish_mint_capability">publish_mint_capability</a>&lt;CoinType&gt;(publish_account: &signer, cap: <a href="#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;CoinType&gt;, tc_signer: &signer)
+<pre><code><b>public</b> <b>fun</b> <a href="#0x1_Libra_publish_mint_capability">publish_mint_capability</a>&lt;CoinType&gt;(publish_account: &signer, cap: <a href="#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;CoinType&gt;, tc_account: &signer)
 </code></pre>
 
 
@@ -765,10 +765,10 @@ The caller must pass a
 <pre><code><b>public</b> <b>fun</b> <a href="#0x1_Libra_publish_mint_capability">publish_mint_capability</a>&lt;CoinType&gt;(
     publish_account: &signer,
     cap: <a href="#0x1_Libra_MintCapability">MintCapability</a>&lt;CoinType&gt;,
-    tc_signer: &signer,
+    tc_account: &signer,
 ) {
     // TODO: <b>abort</b> code
-    <b>assert</b>(has_treasury_compliance_role(tc_signer), 919402);
+    <b>assert</b>(has_treasury_compliance_role(tc_account), 919402);
     <a href="#0x1_Libra_assert_is_currency">assert_is_currency</a>&lt;CoinType&gt;();
     move_to(publish_account, cap)
 }

language/stdlib/modules/doc/LibraAccount.md

@@ -1304,7 +1304,7 @@ Create a treasury/compliance account at
 <code>new_account_address</code>
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="#0x1_LibraAccount_create_treasury_compliance_account">create_treasury_compliance_account</a>(lr_account: &signer, tc_account: &signer, new_account_address: address, auth_key_prefix: vector&lt;u8&gt;, coin1_mint_cap: <a href="Libra.md#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;<a href="Coin1.md#0x1_Coin1_Coin1">Coin1::Coin1</a>&gt;, coin1_burn_cap: <a href="Libra.md#0x1_Libra_BurnCapability">Libra::BurnCapability</a>&lt;<a href="Coin1.md#0x1_Coin1_Coin1">Coin1::Coin1</a>&gt;, coin2_mint_cap: <a href="Libra.md#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;<a href="Coin2.md#0x1_Coin2_Coin2">Coin2::Coin2</a>&gt;, coin2_burn_cap: <a href="Libra.md#0x1_Libra_BurnCapability">Libra::BurnCapability</a>&lt;<a href="Coin2.md#0x1_Coin2_Coin2">Coin2::Coin2</a>&gt;)
+<pre><code><b>public</b> <b>fun</b> <a href="#0x1_LibraAccount_create_treasury_compliance_account">create_treasury_compliance_account</a>(lr_account: &signer, new_account_address: address, auth_key_prefix: vector&lt;u8&gt;)
 </code></pre>
 
 
@@ -1315,23 +1315,13 @@ Create a treasury/compliance account at
 
 <pre><code><b>public</b> <b>fun</b> <a href="#0x1_LibraAccount_create_treasury_compliance_account">create_treasury_compliance_account</a>(
     lr_account: &signer,
-    tc_account: &signer,
-
     new_account_address: address,
     auth_key_prefix: vector&lt;u8&gt;,
-    coin1_mint_cap: <a href="Libra.md#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;<a href="Coin1.md#0x1_Coin1">Coin1</a>&gt;,
-    coin1_burn_cap: <a href="Libra.md#0x1_Libra_BurnCapability">Libra::BurnCapability</a>&lt;<a href="Coin1.md#0x1_Coin1">Coin1</a>&gt;,
-    coin2_mint_cap: <a href="Libra.md#0x1_Libra_MintCapability">Libra::MintCapability</a>&lt;<a href="Coin2.md#0x1_Coin2">Coin2</a>&gt;,
-    coin2_burn_cap: <a href="Libra.md#0x1_Libra_BurnCapability">Libra::BurnCapability</a>&lt;<a href="Coin2.md#0x1_Coin2">Coin2</a>&gt;,
 ) {
     <a href="LibraTimestamp.md#0x1_LibraTimestamp_assert_is_genesis">LibraTimestamp::assert_is_genesis</a>();
     // TODO: <b>abort</b> code
     <b>assert</b>(<a href="Roles.md#0x1_Roles_has_libra_root_role">Roles::has_libra_root_role</a>(lr_account), 919408);
     <b>let</b> new_account = <a href="#0x1_LibraAccount_create_signer">create_signer</a>(new_account_address);
-    <a href="Libra.md#0x1_Libra_publish_mint_capability">Libra::publish_mint_capability</a>&lt;<a href="Coin1.md#0x1_Coin1">Coin1</a>&gt;(&new_account, coin1_mint_cap, tc_account);
-    <a href="Libra.md#0x1_Libra_publish_burn_capability">Libra::publish_burn_capability</a>&lt;<a href="Coin1.md#0x1_Coin1">Coin1</a>&gt;(&new_account, coin1_burn_cap, tc_account);
-    <a href="Libra.md#0x1_Libra_publish_mint_capability">Libra::publish_mint_capability</a>&lt;<a href="Coin2.md#0x1_Coin2">Coin2</a>&gt;(&new_account, coin2_mint_cap, tc_account);
-    <a href="Libra.md#0x1_Libra_publish_burn_capability">Libra::publish_burn_capability</a>&lt;<a href="Coin2.md#0x1_Coin2">Coin2</a>&gt;(&new_account, coin2_burn_cap, tc_account);
     <a href="SlidingNonce.md#0x1_SlidingNonce_publish_nonce_resource">SlidingNonce::publish_nonce_resource</a>(lr_account, &new_account);
     <a href="Event.md#0x1_Event_publish_generator">Event::publish_generator</a>(&new_account);
     <a href="#0x1_LibraAccount_make_account">make_account</a>(new_account, auth_key_prefix)