From 112060283aeeeca8ee95ed9a837d15e367a26b0d Mon Sep 17 00:00:00 2001 From: Junkil Park Date: Thu, 1 Dec 2022 12:44:13 -0800 Subject: [PATCH] [Spec] Updated the spec of the Genesis module This commits update the `verify_only` genesis steps to reflect the `encode_aptos_mainnet_genesis_transaction` of `vm-genesis`. The spec of `create_signer` is added. One TODO is removed because the `Table` issue has been fixed. --- .../framework/aptos-framework/doc/genesis.md | 23 ++++++++++++------- .../aptos-framework/sources/genesis.move | 17 ++++++++++---- .../aptos-framework/sources/genesis.spec.move | 9 ++++---- 3 files changed, 32 insertions(+), 17 deletions(-) diff --git a/aptos-move/framework/aptos-framework/doc/genesis.md b/aptos-move/framework/aptos-framework/doc/genesis.md index 4f57cff1ea606..75e3ee10b6b0f 100644 --- a/aptos-move/framework/aptos-framework/doc/genesis.md +++ b/aptos-move/framework/aptos-framework/doc/genesis.md @@ -38,6 +38,7 @@ use 0x1::coin; use 0x1::consensus_config; use 0x1::error; +use 0x1::features; use 0x1::fixed_point32; use 0x1::gas_schedule; use 0x1::reconfiguration; @@ -850,7 +851,7 @@ The last step of genesis. -
fun initialize_for_verification(gas_schedule: vector<u8>, chain_id: u8, initial_version: u64, consensus_config: vector<u8>, epoch_interval_microsecs: u64, minimum_stake: u64, maximum_stake: u64, recurring_lockup_duration_secs: u64, allow_validator_set_change: bool, rewards_rate: u64, rewards_rate_denominator: u64, voting_power_increase_limit: u64, aptos_framework: &signer, validators: vector<genesis::ValidatorConfiguration>, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64)
+
fun initialize_for_verification(gas_schedule: vector<u8>, chain_id: u8, initial_version: u64, consensus_config: vector<u8>, epoch_interval_microsecs: u64, minimum_stake: u64, maximum_stake: u64, recurring_lockup_duration_secs: u64, allow_validator_set_change: bool, rewards_rate: u64, rewards_rate_denominator: u64, voting_power_increase_limit: u64, aptos_framework: &signer, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64, accounts: vector<genesis::AccountMap>, employee_vesting_start: u64, employee_vesting_period_duration: u64, employees: vector<genesis::EmployeeAccountMap>, validators: vector<genesis::ValidatorConfigurationWithCommission>)
 

 
 
@@ -873,10 +874,14 @@ The last step of genesis.
     rewards_rate_denominator: u64,
     voting_power_increase_limit: u64,
     aptos_framework: &signer,
-    validators: vector<ValidatorConfiguration>,
     min_voting_threshold: u128,
     required_proposer_stake: u64,
     voting_duration_secs: u64,
+    accounts: vector<AccountMap>,
+    employee_vesting_start: u64,
+    employee_vesting_period_duration: u64,
+    employees: vector<EmployeeAccountMap>,
+    validators: vector<ValidatorConfigurationWithCommission>
 ) {
     initialize(
         gas_schedule,
@@ -892,17 +897,17 @@ The last step of genesis.
         rewards_rate_denominator,
         voting_power_increase_limit
     );
-
+    features::change_feature_flags(aptos_framework, vector[1, 2], vector[]);
     initialize_aptos_coin(aptos_framework);
-
     aptos_governance::initialize_for_verification(
         aptos_framework,
         min_voting_threshold,
         required_proposer_stake,
         voting_duration_secs
     );
-
-    create_initialize_validators(aptos_framework, validators);
+    create_accounts(aptos_framework, accounts);
+    create_employee_validators(employee_vesting_start, employee_vesting_period_duration, employees);
+    create_initialize_validators_with_commission(aptos_framework, true, validators);
     set_genesis_end(aptos_framework);
 }
@@ -934,6 +939,8 @@ The last step of genesis. 
pragma opaque;
+aborts_if false;
+ensures signer::address_of(result) == addr;
@@ -943,13 +950,13 @@ The last step of genesis. ### Function `initialize_for_verification` -
fun initialize_for_verification(gas_schedule: vector<u8>, chain_id: u8, initial_version: u64, consensus_config: vector<u8>, epoch_interval_microsecs: u64, minimum_stake: u64, maximum_stake: u64, recurring_lockup_duration_secs: u64, allow_validator_set_change: bool, rewards_rate: u64, rewards_rate_denominator: u64, voting_power_increase_limit: u64, aptos_framework: &signer, validators: vector<genesis::ValidatorConfiguration>, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64)
+
fun initialize_for_verification(gas_schedule: vector<u8>, chain_id: u8, initial_version: u64, consensus_config: vector<u8>, epoch_interval_microsecs: u64, minimum_stake: u64, maximum_stake: u64, recurring_lockup_duration_secs: u64, allow_validator_set_change: bool, rewards_rate: u64, rewards_rate_denominator: u64, voting_power_increase_limit: u64, aptos_framework: &signer, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64, accounts: vector<genesis::AccountMap>, employee_vesting_start: u64, employee_vesting_period_duration: u64, employees: vector<genesis::EmployeeAccountMap>, validators: vector<genesis::ValidatorConfigurationWithCommission>)
 

 
 
 
 
-
pragma verify = false;
+
pragma verify = true;
 

 
 
diff --git a/aptos-move/framework/aptos-framework/sources/genesis.move b/aptos-move/framework/aptos-framework/sources/genesis.move
index 6bbc6cd0079b3..99a321a25d40b 100644
--- a/aptos-move/framework/aptos-framework/sources/genesis.move
+++ b/aptos-move/framework/aptos-framework/sources/genesis.move
@@ -392,6 +392,9 @@ module aptos_framework::genesis {
 
     native fun create_signer(addr: address): signer;
 
+    #[verify_only]
+    use std::features;
+
     #[verify_only]
     fun initialize_for_verification(
         gas_schedule: vector,
@@ -407,10 +410,14 @@ module aptos_framework::genesis {
         rewards_rate_denominator: u64,
         voting_power_increase_limit: u64,
         aptos_framework: &signer,
-        validators: vector,
         min_voting_threshold: u128,
         required_proposer_stake: u64,
         voting_duration_secs: u64,
+        accounts: vector,
+        employee_vesting_start: u64,
+        employee_vesting_period_duration: u64,
+        employees: vector,
+        validators: vector
     ) {
         initialize(
             gas_schedule,
@@ -426,17 +433,17 @@ module aptos_framework::genesis {
             rewards_rate_denominator,
             voting_power_increase_limit
         );
-
+        features::change_feature_flags(aptos_framework, vector[1, 2], vector[]);
         initialize_aptos_coin(aptos_framework);
-
         aptos_governance::initialize_for_verification(
             aptos_framework,
             min_voting_threshold,
             required_proposer_stake,
             voting_duration_secs
         );
-
-        create_initialize_validators(aptos_framework, validators);
+        create_accounts(aptos_framework, accounts);
+        create_employee_validators(employee_vesting_start, employee_vesting_period_duration, employees);
+        create_initialize_validators_with_commission(aptos_framework, true, validators);
         set_genesis_end(aptos_framework);
     }
 
diff --git a/aptos-move/framework/aptos-framework/sources/genesis.spec.move b/aptos-move/framework/aptos-framework/sources/genesis.spec.move
index afea55af3c918..64b3f25bd07b0 100644
--- a/aptos-move/framework/aptos-framework/sources/genesis.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/genesis.spec.move
@@ -9,12 +9,13 @@ spec aptos_framework::genesis {
     }
 
     spec initialize_for_verification {
-        // TODO: disabled due to the issue of Table.
-        pragma verify = false;
+        pragma verify = true;
     }
 
-    spec create_signer {
-        // TODO: temporary mockup.
+    spec create_signer(addr: address): signer {
+        use std::signer;
         pragma opaque;
+        aborts_if false;
+        ensures signer::address_of(result) == addr;
     }
 }