Skip to content

Commit

Permalink
Finish aborts condition for emit_genesis_reconfiguration_event
Browse files Browse the repository at this point in the history
  • Loading branch information
axiongsupra committed Dec 5, 2024
1 parent f32cb3d commit 6d8398f
Showing 1 changed file with 1 addition and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -113,9 +113,8 @@ spec supra_framework::reconfiguration {
/// Should equal to 0
spec emit_genesis_reconfiguration_event {
use supra_framework::reconfiguration::{Configuration};
// TODO remove aborts_if_is_partial after the property proved
pragma aborts_if_is_partial;
aborts_if !exists<Configuration>(@supra_framework);
aborts_if !exists<timestamp::CurrentTimeMicroseconds>(@supra_framework);
let config_ref = global<Configuration>(@supra_framework);
aborts_if !(config_ref.epoch == 0 && config_ref.last_reconfiguration_time == 0);
ensures global<Configuration>(@supra_framework).epoch == 1;
Expand Down

0 comments on commit 6d8398f

Please sign in to comment.