Skip to content

Commit

Permalink
Remove module event feature check
Browse files Browse the repository at this point in the history
  • Loading branch information
lightmark committed Oct 17, 2023
1 parent 0df7eec commit 911b145
Show file tree
Hide file tree
Showing 5 changed files with 27 additions and 27 deletions.
4 changes: 0 additions & 4 deletions aptos-move/framework/aptos-framework/doc/event.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,6 @@ events emitted to a handle and emit events to the event store.


<pre><code><b>use</b> <a href="../../aptos-stdlib/../move-stdlib/doc/bcs.md#0x1_bcs">0x1::bcs</a>;
<b>use</b> <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error">0x1::error</a>;
<b>use</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features">0x1::features</a>;
<b>use</b> <a href="guid.md#0x1_guid">0x1::guid</a>;
</code></pre>

Expand Down Expand Up @@ -106,7 +104,6 @@ Emit an event with payload <code>msg</code> by using <code>handle_ref</code>'s k


<pre><code><b>public</b> <b>fun</b> <a href="event.md#0x1_event_emit">emit</a>&lt;T: store + drop&gt;(msg: T) {
<b>assert</b>!(<a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_module_event_enabled">features::module_event_enabled</a>(), std::error::invalid_state(<a href="event.md#0x1_event_EMODULE_EVENT_NOT_SUPPORTED">EMODULE_EVENT_NOT_SUPPORTED</a>));
<a href="event.md#0x1_event_write_module_event_to_store">write_module_event_to_store</a>&lt;T&gt;(msg);
}
</code></pre>
Expand Down Expand Up @@ -323,7 +320,6 @@ Destroy a unique handle.


<pre><code><b>pragma</b> opaque;
<b>aborts_if</b> !<a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_module_event_enabled">features::spec_module_event_enabled</a>();
</code></pre>


Expand Down
23 changes: 13 additions & 10 deletions aptos-move/framework/aptos-framework/doc/transaction_fee.md
Original file line number Diff line number Diff line change
Expand Up @@ -742,7 +742,7 @@ Only called during genesis.
<b>let</b> aptos_addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(aptos_framework);
<b>aborts_if</b> !<a href="system_addresses.md#0x1_system_addresses_is_aptos_framework_address">system_addresses::is_aptos_framework_address</a>(aptos_addr);
<b>aborts_if</b> <b>exists</b>&lt;ValidatorFees&gt;(aptos_addr);
<b>include</b> <a href="system_addresses.md#0x1_system_addresses_AbortsIfNotAptosFramework">system_addresses::AbortsIfNotAptosFramework</a> {<a href="account.md#0x1_account">account</a>: aptos_framework};
<b>include</b> <a href="system_addresses.md#0x1_system_addresses_AbortsIfNotAptosFramework">system_addresses::AbortsIfNotAptosFramework</a> { <a href="account.md#0x1_account">account</a>: aptos_framework };
<b>include</b> <a href="aggregator_factory.md#0x1_aggregator_factory_CreateAggregatorInternalAbortsIf">aggregator_factory::CreateAggregatorInternalAbortsIf</a>;
<b>aborts_if</b> <b>exists</b>&lt;<a href="transaction_fee.md#0x1_transaction_fee_CollectedFeesPerBlock">CollectedFeesPerBlock</a>&gt;(aptos_addr);
<b>ensures</b> <b>exists</b>&lt;ValidatorFees&gt;(aptos_addr);
Expand Down Expand Up @@ -805,7 +805,7 @@ Only called during genesis.
<b>requires</b> <b>exists</b>&lt;<a href="transaction_fee.md#0x1_transaction_fee_AptosCoinCapabilities">AptosCoinCapabilities</a>&gt;(@aptos_framework);
<b>requires</b> <b>exists</b>&lt;CoinInfo&lt;AptosCoin&gt;&gt;(@aptos_framework);
<b>let</b> amount_to_burn = (burn_percentage * <a href="coin.md#0x1_coin_value">coin::value</a>(<a href="coin.md#0x1_coin">coin</a>)) / 100;
<b>include</b> amount_to_burn &gt; 0 ==&gt; <a href="coin.md#0x1_coin_AbortsIfAggregator">coin::AbortsIfAggregator</a>&lt;AptosCoin&gt;{ <a href="coin.md#0x1_coin">coin</a>: Coin&lt;AptosCoin&gt;{ value: amount_to_burn } };
<b>include</b> amount_to_burn &gt; 0 ==&gt; <a href="coin.md#0x1_coin_AbortsIfAggregator">coin::AbortsIfAggregator</a>&lt;AptosCoin&gt; { <a href="coin.md#0x1_coin">coin</a>: Coin&lt;AptosCoin&gt; { value: amount_to_burn } };
<b>ensures</b> <a href="coin.md#0x1_coin">coin</a>.value == <b>old</b>(<a href="coin.md#0x1_coin">coin</a>).value - amount_to_burn;
</code></pre>

Expand All @@ -831,7 +831,9 @@ Only called during genesis.
<b>requires</b>
(<a href="transaction_fee.md#0x1_transaction_fee_is_fees_collection_enabled">is_fees_collection_enabled</a>() && <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_is_some">option::is_some</a>(maybe_supply)) ==&gt;
(<a href="aggregator.md#0x1_aggregator_spec_aggregator_get_val">aggregator::spec_aggregator_get_val</a>(<b>global</b>&lt;<a href="transaction_fee.md#0x1_transaction_fee_CollectedFeesPerBlock">CollectedFeesPerBlock</a>&gt;(@aptos_framework).amount.value) &lt;=
<a href="optional_aggregator.md#0x1_optional_aggregator_optional_aggregator_value">optional_aggregator::optional_aggregator_value</a>(<a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_borrow">option::spec_borrow</a>(<a href="coin.md#0x1_coin_get_coin_supply_opt">coin::get_coin_supply_opt</a>&lt;AptosCoin&gt;())));
<a href="optional_aggregator.md#0x1_optional_aggregator_optional_aggregator_value">optional_aggregator::optional_aggregator_value</a>(
<a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_borrow">option::spec_borrow</a>(<a href="coin.md#0x1_coin_get_coin_supply_opt">coin::get_coin_supply_opt</a>&lt;AptosCoin&gt;())
));
}
</code></pre>

Expand Down Expand Up @@ -860,9 +862,12 @@ Only called during genesis.
<a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_is_some">option::spec_is_some</a>(collected_fees.proposer) ==&gt;
<b>if</b> (proposer != @vm_reserved) {
<b>if</b> (<a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_contains">table::spec_contains</a>(fees_table, proposer)) {
<a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_get">table::spec_get</a>(post_fees_table, proposer).value == <a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_get">table::spec_get</a>(fees_table, proposer).value + fee_to_add
<a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_get">table::spec_get</a>(post_fees_table, proposer).value == <a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_get">table::spec_get</a>(
fees_table,
proposer
).value + fee_to_add
} <b>else</b> {
<a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_get">table::spec_get</a>(post_fees_table, proposer).value == fee_to_add
<a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_get">table::spec_get</a>(post_fees_table, proposer).value == fee_to_add
}
} <b>else</b> {
<a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_is_none">option::spec_is_none</a>(post_collected_fees.proposer) && post_amount == 0
Expand Down Expand Up @@ -977,7 +982,9 @@ Only called during genesis.
<b>let</b> <b>post</b> post_coin_store = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(<a href="account.md#0x1_account">account</a>);
<b>let</b> <b>post</b> post_collected_fees = <b>global</b>&lt;<a href="transaction_fee.md#0x1_transaction_fee_CollectedFeesPerBlock">CollectedFeesPerBlock</a>&gt;(@aptos_framework).amount;
<b>ensures</b> post_coin_store.<a href="coin.md#0x1_coin">coin</a>.value == coin_store.<a href="coin.md#0x1_coin">coin</a>.value - fee;
<b>ensures</b> <a href="aggregator.md#0x1_aggregator_spec_aggregator_get_val">aggregator::spec_aggregator_get_val</a>(post_collected_fees.value) == <a href="aggregator.md#0x1_aggregator_spec_aggregator_get_val">aggregator::spec_aggregator_get_val</a>(aggr) + fee;
<b>ensures</b> <a href="aggregator.md#0x1_aggregator_spec_aggregator_get_val">aggregator::spec_aggregator_get_val</a>(post_collected_fees.value) == <a href="aggregator.md#0x1_aggregator_spec_aggregator_get_val">aggregator::spec_aggregator_get_val</a>(
aggr
) + fee;
</code></pre>


Expand Down Expand Up @@ -1059,8 +1066,4 @@ Aborts if <code><a href="transaction_fee.md#0x1_transaction_fee_AptosCoinMintCap
Aborts if module event feature is not enabled.


<pre><code><b>aborts_if</b> !std::features::spec_module_event_enabled();
</code></pre>


[move-book]: https://aptos.dev/move/book/SUMMARY
2 changes: 0 additions & 2 deletions aptos-move/framework/aptos-framework/sources/event.move
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ module aptos_framework::event {
use std::bcs;

use aptos_framework::guid::GUID;
use std::features;

friend aptos_framework::account;
friend aptos_framework::object;
Expand All @@ -16,7 +15,6 @@ module aptos_framework::event {

/// Emit an event with payload `msg` by using `handle_ref`'s key and counter.
public fun emit<T: store + drop>(msg: T) {
assert!(features::module_event_enabled(), std::error::invalid_state(EMODULE_EVENT_NOT_SUPPORTED));
write_module_event_to_store<T>(msg);
}

Expand Down
2 changes: 0 additions & 2 deletions aptos-move/framework/aptos-framework/sources/event.spec.move
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ spec aptos_framework::event {

spec emit {
pragma opaque;
aborts_if !features::spec_module_event_enabled();
}

/// Native function use opaque.
Expand All @@ -36,5 +35,4 @@ spec aptos_framework::event {
spec destroy_handle {
aborts_if false;
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ spec aptos_framework::transaction_fee {
aborts_if !system_addresses::is_aptos_framework_address(aptos_addr);
aborts_if exists<ValidatorFees>(aptos_addr);

include system_addresses::AbortsIfNotAptosFramework {account: aptos_framework};
include system_addresses::AbortsIfNotAptosFramework { account: aptos_framework };
include aggregator_factory::CreateAggregatorInternalAbortsIf;
aborts_if exists<CollectedFeesPerBlock>(aptos_addr);

Expand Down Expand Up @@ -71,7 +71,7 @@ spec aptos_framework::transaction_fee {

let amount_to_burn = (burn_percentage * coin::value(coin)) / 100;
// include (amount_to_burn > 0) ==> coin::AbortsIfNotExistCoinInfo<AptosCoin>;
include amount_to_burn > 0 ==> coin::AbortsIfAggregator<AptosCoin>{ coin: Coin<AptosCoin>{ value: amount_to_burn } };
include amount_to_burn > 0 ==> coin::AbortsIfAggregator<AptosCoin> { coin: Coin<AptosCoin> { value: amount_to_burn } };
ensures coin.value == old(coin).value - amount_to_burn;
}

Expand All @@ -87,7 +87,9 @@ spec aptos_framework::transaction_fee {
requires
(is_fees_collection_enabled() && option::is_some(maybe_supply)) ==>
(aggregator::spec_aggregator_get_val(global<CollectedFeesPerBlock>(@aptos_framework).amount.value) <=
optional_aggregator::optional_aggregator_value(option::spec_borrow(coin::get_coin_supply_opt<AptosCoin>())));
optional_aggregator::optional_aggregator_value(
option::spec_borrow(coin::get_coin_supply_opt<AptosCoin>())
));
}

spec schema ProcessCollectedFeesRequiresAndEnsures {
Expand Down Expand Up @@ -116,9 +118,12 @@ spec aptos_framework::transaction_fee {
option::spec_is_some(collected_fees.proposer) ==>
if (proposer != @vm_reserved) {
if (table::spec_contains(fees_table, proposer)) {
table::spec_get(post_fees_table, proposer).value == table::spec_get(fees_table, proposer).value + fee_to_add
table::spec_get(post_fees_table, proposer).value == table::spec_get(
fees_table,
proposer
).value + fee_to_add
} else {
table::spec_get(post_fees_table, proposer).value == fee_to_add
table::spec_get(post_fees_table, proposer).value == fee_to_add
}
} else {
option::spec_is_none(post_collected_fees.proposer) && post_amount == 0
Expand Down Expand Up @@ -211,7 +216,9 @@ spec aptos_framework::transaction_fee {
let post post_coin_store = global<coin::CoinStore<AptosCoin>>(account);
let post post_collected_fees = global<CollectedFeesPerBlock>(@aptos_framework).amount;
ensures post_coin_store.coin.value == coin_store.coin.value - fee;
ensures aggregator::spec_aggregator_get_val(post_collected_fees.value) == aggregator::spec_aggregator_get_val(aggr) + fee;
ensures aggregator::spec_aggregator_get_val(post_collected_fees.value) == aggregator::spec_aggregator_get_val(
aggr
) + fee;
}

/// Ensure caller is admin.
Expand Down Expand Up @@ -247,7 +254,5 @@ spec aptos_framework::transaction_fee {
}

/// Aborts if module event feature is not enabled.
spec emit_fee_statement {
aborts_if !std::features::spec_module_event_enabled();
}
spec emit_fee_statement {}
}

0 comments on commit 911b145

Please sign in to comment.