Skip to content

Commit

Permalink
[move] adding formal verification tests to coin & renames (#65)
Browse files Browse the repository at this point in the history
Co-authored-by: 0o-de-lally <[email protected]>
  • Loading branch information
0xzoz and 0o-de-lally committed Aug 8, 2024
1 parent b0c6942 commit aed64b1
Show file tree
Hide file tree
Showing 39 changed files with 158 additions and 68 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ module diem_framework::diem_governance {
use diem_framework::timestamp;
use diem_framework::voting;

use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
// use diem_std::debug::print;


Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -246,7 +246,7 @@ spec diem_framework::diem_governance {
spec reconfigure(diem_framework: &signer) {
use diem_framework::chain_status;
use diem_framework::coin::CoinInfo;
use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::transaction_fee;
// use diem_framework::staking_config;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ module diem_framework::genesis {
use ol_framework::musical_chairs;
use ol_framework::proof_of_fee;
use ol_framework::slow_wallet;
use ol_framework::gas_coin::{Self, GasCoin};
use ol_framework::gas_coin::{Self, LibraCoin as GasCoin};
use ol_framework::infra_escrow;
use ol_framework::tower_state;
use ol_framework::safe;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ spec diem_framework::reconfiguration {

spec reconfigure {
use diem_framework::coin::CoinInfo;
use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::transaction_fee;
// use diem_framework::staking_config;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ module diem_framework::stake {
use diem_std::table::Table;
use diem_std::comparator;

use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::account;
use diem_framework::coin::{Self, Coin, MintCapability};
use diem_framework::event::{Self, EventHandle};
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,9 @@ module diem_framework::transaction_fee {
use std::error;
use std::vector;
use std::option::{Self, Option};
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use ol_framework::fee_maker;
use ol_framework::slow_wallet;

// use diem_std::debug::print;

Expand Down Expand Up @@ -180,6 +181,8 @@ module diem_framework::transaction_fee {
// we burn them all at once. This way we avoid having a check for every transaction epilogue.
let collected_amount = &mut collected_fees.amount;
coin::collect_into_aggregatable_coin<GasCoin>(account, fee, collected_amount);
// must adjust slow wallet tracker for all transactions
slow_wallet::maybe_track_unlocked_withdraw(account, fee);
}

//////// 0L ////////
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ spec diem_framework::transaction_fee {
use diem_framework::optional_aggregator;
use diem_framework::aggregator;
use diem_framework::coin::CoinInfo;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
requires burn_percentage <= 100;
requires exists<GasCoinCapabilities>(@diem_framework);
requires exists<CoinInfo<GasCoin>>(@diem_framework);
Expand Down Expand Up @@ -62,7 +62,7 @@ spec diem_framework::transaction_fee {

spec process_collected_fees() {
use diem_framework::coin::CoinInfo;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
requires exists<GasCoinCapabilities>(@diem_framework);
// requires exists<stake::ValidatorFees>(@diem_framework);
requires exists<CoinInfo<GasCoin>>(@diem_framework);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ module diem_framework::transaction_validation {

use diem_framework::account;
// use diem_framework::diem_coin::DiemCoin;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::chain_id;
use diem_framework::coin;
use diem_framework::system_addresses;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ spec diem_framework::transaction_validation {
) {
use diem_framework::coin::{CoinStore};
use diem_framework::account::{Account};
use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
// TODO: Can't verify `burn_fee`, complex aborts conditions.
pragma aborts_if_is_partial;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ spec diem_framework::block {
spec block_prologue {
use diem_framework::chain_status;
use diem_framework::coin::CoinInfo;
use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::transaction_fee;
// use diem_framework::staking_config;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ spec diem_framework::consensus_config {
use std::signer;
use diem_framework::stake;
use diem_framework::coin::CoinInfo;
use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::transaction_fee;
// use diem_framework::staking_config;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ spec diem_framework::gas_schedule {
use diem_framework::util;
use diem_framework::stake;
use diem_framework::coin::CoinInfo;
use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::transaction_fee;
// use diem_framework::staking_config;

Expand All @@ -38,7 +38,7 @@ spec diem_framework::gas_schedule {
spec set_storage_gas_config(diem_framework: &signer, config: StorageGasConfig) {
use diem_framework::stake;
use diem_framework::coin::CoinInfo;
use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::transaction_fee;
// use diem_framework::staking_config;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ spec diem_framework::version {
use diem_framework::timestamp;
use diem_framework::stake;
use diem_framework::coin::CoinInfo;
use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::transaction_fee;
// use diem_framework::staking_config;
// Not verified when verify_duration_estimate > vc_timeout
Expand Down
2 changes: 1 addition & 1 deletion framework/libra-framework/sources/multisig_account.move
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@
/// and implement the governance voting logic on top.
module diem_framework::multisig_account {
use diem_framework::account::{Self, SignerCapability, new_event_handle, create_resource_address};
use diem_framework::gas_coin::GasCoin;
use diem_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::chain_id;
use diem_framework::create_signer::create_signer;
use diem_framework::coin;
Expand Down
2 changes: 1 addition & 1 deletion framework/libra-framework/sources/ol_sources/burn.move
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ module ol_framework::burn {
use std::vector;
// use ol_framework::ol_account;
use ol_framework::system_addresses;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
// use ol_framework::transaction_fee;
use ol_framework::coin::{Self, Coin};
use ol_framework::match_index;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ module diem_framework::epoch_boundary {
use ol_framework::musical_chairs;
use ol_framework::proof_of_fee;
use ol_framework::stake;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use ol_framework::rewards;
use ol_framework::jail;
// use ol_framework::grade;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ module ol_framework::genesis_migration {
use ol_framework::ol_account;
use ol_framework::validator_universe;
use ol_framework::gas_coin;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use ol_framework::transaction_fee;
use ol_framework::slow_wallet;
use ol_framework::pledge_accounts;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
module ol_framework::infra_escrow{
use std::option::{Self, Option};
use diem_framework::system_addresses;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use ol_framework::pledge_accounts;
// use ol_framework::slow_wallet;
use ol_framework::ol_account;
Expand Down
58 changes: 29 additions & 29 deletions framework/libra-framework/sources/ol_sources/libra_coin.move
Original file line number Diff line number Diff line change
Expand Up @@ -136,10 +136,10 @@ module ol_framework::gas_coin {
/// Cannot find delegation of mint capability to this account
const EDELEGATION_NOT_FOUND: u64 = 3;

struct GasCoin has key {}
struct LibraCoin has key {}

struct MintCapStore has key {
mint_cap: MintCapability<GasCoin>,
mint_cap: MintCapability<LibraCoin>,
}

/// Delegation token created by delegator and can be claimed by the delegatee as MintCapability.
Expand All @@ -156,10 +156,10 @@ module ol_framework::gas_coin {
public(friend) fun initialize(diem_framework: &signer) {
system_addresses::assert_diem_framework(diem_framework);

let (burn_cap, freeze_cap, mint_cap) = coin::initialize_with_parallelizable_supply<GasCoin>(
let (burn_cap, freeze_cap, mint_cap) = coin::initialize_with_parallelizable_supply<LibraCoin>(
diem_framework,
string::utf8(b"Gas Coin"),
string::utf8(b"GAS"),
string::utf8(b"LibraCoin"),
string::utf8(b"LIBRA"),
globals::get_coin_decimal_places(), /* decimals MATCHES LEGACY 0L */
true, /* monitor_supply */
);
Expand All @@ -175,13 +175,13 @@ module ol_framework::gas_coin {

/// FOR TESTS ONLY
/// Can only called during genesis to initialize the Diem coin.
public(friend) fun initialize_for_core(diem_framework: &signer): (BurnCapability<GasCoin>, MintCapability<GasCoin>) {
public(friend) fun initialize_for_core(diem_framework: &signer): (BurnCapability<LibraCoin>, MintCapability<LibraCoin>) {
system_addresses::assert_diem_framework(diem_framework);

let (burn_cap, freeze_cap, mint_cap) = coin::initialize_with_parallelizable_supply<GasCoin>(
let (burn_cap, freeze_cap, mint_cap) = coin::initialize_with_parallelizable_supply<LibraCoin>(
diem_framework,
string::utf8(b"Gas Coin"),
string::utf8(b"GAS"),
string::utf8(b"LibraCoin"),
string::utf8(b"LIBRA"),
globals::get_coin_decimal_places(), /* decimals MATCHES LEGACY 0L */
true, /* monitor_supply */
);
Expand Down Expand Up @@ -212,7 +212,7 @@ module ol_framework::gas_coin {
/// get the gas coin supply. Helper which wraps coin::supply and extracts option type
// NOTE: there is casting between u128 and u64, but 0L has final supply below the u64.
public fun supply(): u64 {
let supply_opt = coin::supply<GasCoin>();
let supply_opt = coin::supply<LibraCoin>();
if (option::is_some(&supply_opt)) {
return (*option::borrow(&supply_opt) as u64)
};
Expand All @@ -221,7 +221,7 @@ module ol_framework::gas_coin {


#[test_only]
public fun restore_mint_cap(diem_framework: &signer, mint_cap: MintCapability<GasCoin>) {
public fun restore_mint_cap(diem_framework: &signer, mint_cap: MintCapability<LibraCoin>) {
system_addresses::assert_diem_framework(diem_framework);
move_to(diem_framework, MintCapStore { mint_cap });
}
Expand All @@ -233,18 +233,18 @@ module ol_framework::gas_coin {
public(friend) fun configure_accounts_for_test(
diem_framework: &signer,
core_resources: &signer,
mint_cap: MintCapability<GasCoin>,
mint_cap: MintCapability<LibraCoin>,
){
system_addresses::assert_diem_framework(diem_framework);

// Mint the core resource account GasCoin for gas so it can execute system transactions.
coin::register<GasCoin>(core_resources);
// Mint the core resource account LibraCoin for gas so it can execute system transactions.
coin::register<LibraCoin>(core_resources);

let coins = coin::mint<GasCoin>(
let coins = coin::mint<LibraCoin>(
18446744073709551615,
&mint_cap,
);
coin::deposit<GasCoin>(signer::address_of(core_resources), coins);
coin::deposit<LibraCoin>(signer::address_of(core_resources), coins);

move_to(core_resources, MintCapStore { mint_cap });
move_to(core_resources, Delegations { inner: vector::empty() });
Expand All @@ -255,11 +255,11 @@ module ol_framework::gas_coin {
// mint_impl(
// root: &signer,
// amount: u64,
// ): Coin<GasCoin> acquires MintCapStore {
// ): Coin<LibraCoin> acquires MintCapStore {
// system_addresses::assert_ol(root);

// let mint_cap = &borrow_global<MintCapStore>(signer::address_of(root)).mint_cap;
// coin::mint<GasCoin>(amount, mint_cap)
// coin::mint<LibraCoin>(amount, mint_cap)
// }

// NOTE: needed for smoke tests
Expand All @@ -280,8 +280,8 @@ module ol_framework::gas_coin {
);

let mint_cap = &borrow_global<MintCapStore>(account_addr).mint_cap;
let coins_minted = coin::mint<GasCoin>(amount, mint_cap);
coin::deposit<GasCoin>(dst_addr, coins_minted);
let coins_minted = coin::mint<LibraCoin>(amount, mint_cap);
coin::deposit<LibraCoin>(dst_addr, coins_minted);
}

#[test_only]
Expand Down Expand Up @@ -341,20 +341,20 @@ module ol_framework::gas_coin {
#[view]
/// helper to get balance in gas coin
public fun get_balance(account: address): u64 {
coin::balance<GasCoin>(account)
coin::balance<LibraCoin>(account)
}


#[test_only]
use diem_framework::aggregator_factory;

#[test_only]
public fun initialize_for_test(diem_framework: &signer): (BurnCapability<GasCoin>, MintCapability<GasCoin>) {
public fun initialize_for_test(diem_framework: &signer): (BurnCapability<LibraCoin>, MintCapability<LibraCoin>) {
aggregator_factory::initialize_aggregator_factory_for_test(diem_framework);
let (burn_cap, freeze_cap, mint_cap) = coin::initialize_with_parallelizable_supply<GasCoin>(
let (burn_cap, freeze_cap, mint_cap) = coin::initialize_with_parallelizable_supply<LibraCoin>(
diem_framework,
string::utf8(b"Gas Coin"),
string::utf8(b"GAS"),
string::utf8(b"LibraCoin"),
string::utf8(b"LIBRA"),
8, /* decimals */
true, /* monitor_supply */
);
Expand All @@ -366,11 +366,11 @@ module ol_framework::gas_coin {

// This is particularly useful if the aggregator_factory is already initialized via another call path.
#[test_only]
public fun initialize_for_test_without_aggregator_factory(diem_framework: &signer): (BurnCapability<GasCoin>, MintCapability<GasCoin>) {
let (burn_cap, freeze_cap, mint_cap) = coin::initialize_with_parallelizable_supply<GasCoin>(
public fun initialize_for_test_without_aggregator_factory(diem_framework: &signer): (BurnCapability<LibraCoin>, MintCapability<LibraCoin>) {
let (burn_cap, freeze_cap, mint_cap) = coin::initialize_with_parallelizable_supply<LibraCoin>(
diem_framework,
string::utf8(b"Gas Coin"),
string::utf8(b"GAS"),
string::utf8(b"LibraCoin"),
string::utf8(b"LIBRA"),
8, /* decimals */
true, /* monitor_supply */
);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
module ol_framework::match_index {
use diem_framework::system_addresses;
use ol_framework::cumulative_deposits;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use ol_framework::ol_account;
use diem_framework::coin::{Self, Coin};
use diem_framework::transaction_fee;
Expand Down
2 changes: 1 addition & 1 deletion framework/libra-framework/sources/ol_sources/mock.move
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ module ol_framework::mock {
use diem_framework::system_addresses;
use ol_framework::epoch_boundary;
use diem_framework::coin;
use ol_framework::gas_coin::{Self, GasCoin};
use ol_framework::gas_coin::{Self, LibraCoin as GasCoin};
use diem_framework::transaction_fee;
use ol_framework::ol_account;
use ol_framework::tower_state;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module ol_framework::ol_account {
use std::option::{Self, Option};
use diem_std::from_bcs;

use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use ol_framework::slow_wallet;
use ol_framework::receipts;
use ol_framework::cumulative_deposits;
Expand Down
2 changes: 1 addition & 1 deletion framework/libra-framework/sources/ol_sources/oracle.move
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ module ol_framework::oracle {
use diem_framework::event::{Self, EventHandle};
use diem_framework::coin::{Self, Coin};
use ol_framework::ol_account;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use ol_framework::globals;
use ol_framework::gas_coin::GasCoin;
use ol_framework::vouch;
use ol_framework::epoch_helper;
use std::error;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@
use std::error;
use std::option::{Self, Option};
use std::fixed_point64;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use ol_framework::ol_account;
use ol_framework::epoch_helper;
use diem_framework::system_addresses;
Expand Down
2 changes: 1 addition & 1 deletion framework/libra-framework/sources/ol_sources/rewards.move
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@

module ol_framework::rewards {
use diem_framework::system_addresses;
use ol_framework::gas_coin::GasCoin;
use ol_framework::gas_coin::LibraCoin as GasCoin;
use diem_framework::coin::{Self, Coin};
use std::vector;
use diem_framework::stake;
Expand Down
Loading

0 comments on commit aed64b1

Please sign in to comment.