diff --git a/language/ir-testsuite/tests/block/expired_transaction.mvir b/language/ir-testsuite/tests/block/expired_transaction.mvir index 9e6f52dc91e5..c8283024de03 100644 --- a/language/ir-testsuite/tests/block/expired_transaction.mvir +++ b/language/ir-testsuite/tests/block/expired_transaction.mvir @@ -4,6 +4,16 @@ //! proposer: vivian //! block-time: 100000000 +//! new-transaction +//! expiration-time: 99 +import 0x1.LibraSystem; +import 0x1.LibraTimestamp; + +main() { + return; +} +// check: TRANSACTION_EXPIRED + //! new-transaction //! expiration-time: 100 import 0x1.LibraSystem; @@ -24,7 +34,6 @@ main() { } // check: EXECUTED -// TODO: 100 + 86400 = 86500, should be rejected after we fix the mempool flakiness. See details in issues #2346. //! new-transaction //! expiration-time: 86500 import 0x1.LibraSystem; @@ -67,4 +76,4 @@ import 0x1.LibraTimestamp; main() { return; } -// check: TRANSACTION_EXPIRED +// check: EXECUTED diff --git a/language/move-lang/functional-tests/tests/libra_transaction_timeout/basic.move b/language/move-lang/functional-tests/tests/libra_transaction_timeout/basic.move deleted file mode 100644 index 3ca170de8890..000000000000 --- a/language/move-lang/functional-tests/tests/libra_transaction_timeout/basic.move +++ /dev/null @@ -1,38 +0,0 @@ -//! new-transaction -script { - use 0x1::LibraTransactionTimeout; - fun main(account: &signer) { - LibraTransactionTimeout::initialize(account); - } -} -// check: ABORTED -// check: 1 - -//! new-transaction -script { - use 0x1::LibraTransactionTimeout; - fun main(account: &signer) { - LibraTransactionTimeout::set_timeout(account, 0); - } -} -// check: ABORTED -// check: 3 - -//! new-transaction -script { - use 0x1::LibraTransactionTimeout; - fun main(account: &signer) { - LibraTransactionTimeout::set_timeout(account, 0); - } -} -// check: ABORTED -// check: 3 - -//! new-transaction -//! sender: libraroot -script { - use 0x1::LibraTransactionTimeout; - fun main(account: &signer) { - LibraTransactionTimeout::set_timeout(account, 86400000000); - } -} diff --git a/language/stdlib/compiled/error_descriptions/error_descriptions.errmap b/language/stdlib/compiled/error_descriptions/error_descriptions.errmap index eca6e2a168e5..fc2aad964f53 100644 Binary files a/language/stdlib/compiled/error_descriptions/error_descriptions.errmap and b/language/stdlib/compiled/error_descriptions/error_descriptions.errmap differ diff --git a/language/stdlib/compiled/stdlib/32_LibraTransactionPublishingOption.mv b/language/stdlib/compiled/stdlib/31_LibraTransactionPublishingOption.mv similarity index 100% rename from language/stdlib/compiled/stdlib/32_LibraTransactionPublishingOption.mv rename to language/stdlib/compiled/stdlib/31_LibraTransactionPublishingOption.mv diff --git a/language/stdlib/compiled/stdlib/31_LibraTransactionTimeout.mv b/language/stdlib/compiled/stdlib/31_LibraTransactionTimeout.mv deleted file mode 100644 index a6bd05930bcd..000000000000 Binary files a/language/stdlib/compiled/stdlib/31_LibraTransactionTimeout.mv and /dev/null differ diff --git a/language/stdlib/compiled/stdlib/33_LibraAccount.mv b/language/stdlib/compiled/stdlib/32_LibraAccount.mv similarity index 59% rename from language/stdlib/compiled/stdlib/33_LibraAccount.mv rename to language/stdlib/compiled/stdlib/32_LibraAccount.mv index 0a269ade5ecf..6e3dbe659b65 100644 Binary files a/language/stdlib/compiled/stdlib/33_LibraAccount.mv and b/language/stdlib/compiled/stdlib/32_LibraAccount.mv differ diff --git a/language/stdlib/compiled/stdlib/34_LibraWriteSetManager.mv b/language/stdlib/compiled/stdlib/33_LibraWriteSetManager.mv similarity index 100% rename from language/stdlib/compiled/stdlib/34_LibraWriteSetManager.mv rename to language/stdlib/compiled/stdlib/33_LibraWriteSetManager.mv diff --git a/language/stdlib/compiled/stdlib/35_LibraVersion.mv b/language/stdlib/compiled/stdlib/34_LibraVersion.mv similarity index 100% rename from language/stdlib/compiled/stdlib/35_LibraVersion.mv rename to language/stdlib/compiled/stdlib/34_LibraVersion.mv diff --git a/language/stdlib/compiled/stdlib/36_LibraVMConfig.mv b/language/stdlib/compiled/stdlib/35_LibraVMConfig.mv similarity index 100% rename from language/stdlib/compiled/stdlib/36_LibraVMConfig.mv rename to language/stdlib/compiled/stdlib/35_LibraVMConfig.mv diff --git a/language/stdlib/compiled/stdlib/37_LibraSystem.mv b/language/stdlib/compiled/stdlib/36_LibraSystem.mv similarity index 100% rename from language/stdlib/compiled/stdlib/37_LibraSystem.mv rename to language/stdlib/compiled/stdlib/36_LibraSystem.mv diff --git a/language/stdlib/compiled/stdlib/38_LibraBlock.mv b/language/stdlib/compiled/stdlib/37_LibraBlock.mv similarity index 100% rename from language/stdlib/compiled/stdlib/38_LibraBlock.mv rename to language/stdlib/compiled/stdlib/37_LibraBlock.mv diff --git a/language/stdlib/compiled/stdlib/39_Genesis.mv b/language/stdlib/compiled/stdlib/38_Genesis.mv similarity index 58% rename from language/stdlib/compiled/stdlib/39_Genesis.mv rename to language/stdlib/compiled/stdlib/38_Genesis.mv index 8db6ca79c507..f5de67a8fa15 100644 Binary files a/language/stdlib/compiled/stdlib/39_Genesis.mv and b/language/stdlib/compiled/stdlib/38_Genesis.mv differ diff --git a/language/stdlib/compiled/stdlib/40_Offer.mv b/language/stdlib/compiled/stdlib/39_Offer.mv similarity index 100% rename from language/stdlib/compiled/stdlib/40_Offer.mv rename to language/stdlib/compiled/stdlib/39_Offer.mv diff --git a/language/stdlib/compiled/stdlib/41_RecoveryAddress.mv b/language/stdlib/compiled/stdlib/40_RecoveryAddress.mv similarity index 100% rename from language/stdlib/compiled/stdlib/41_RecoveryAddress.mv rename to language/stdlib/compiled/stdlib/40_RecoveryAddress.mv diff --git a/language/stdlib/compiled/stdlib/42_SharedEd25519PublicKey.mv b/language/stdlib/compiled/stdlib/41_SharedEd25519PublicKey.mv similarity index 100% rename from language/stdlib/compiled/stdlib/42_SharedEd25519PublicKey.mv rename to language/stdlib/compiled/stdlib/41_SharedEd25519PublicKey.mv diff --git a/language/stdlib/compiled/stdlib/4_LibraTimestamp.mv b/language/stdlib/compiled/stdlib/4_LibraTimestamp.mv index bd32a88a5dfa..81787447a426 100644 Binary files a/language/stdlib/compiled/stdlib/4_LibraTimestamp.mv and b/language/stdlib/compiled/stdlib/4_LibraTimestamp.mv differ diff --git a/language/stdlib/modules/Genesis.move b/language/stdlib/modules/Genesis.move index 4efcaca1e9fd..308b0a3ca0a3 100644 --- a/language/stdlib/modules/Genesis.move +++ b/language/stdlib/modules/Genesis.move @@ -19,7 +19,6 @@ module Genesis { use 0x1::LibraSystem; use 0x1::LibraTimestamp; use 0x1::LibraTransactionPublishingOption; - use 0x1::LibraTransactionTimeout; use 0x1::LibraVersion; use 0x1::LibraWriteSetManager; use 0x1::Signer; @@ -82,7 +81,6 @@ module Genesis { copy dummy_auth_key_prefix, ); - LibraTransactionTimeout::initialize(lr_account); LibraSystem::initialize_validator_set( lr_account, ); diff --git a/language/stdlib/modules/LibraAccount.move b/language/stdlib/modules/LibraAccount.move index 6dd2f63e0123..05f67ca04571 100644 --- a/language/stdlib/modules/LibraAccount.move +++ b/language/stdlib/modules/LibraAccount.move @@ -16,7 +16,6 @@ module LibraAccount { use 0x1::LCS; use 0x1::LibraTimestamp; use 0x1::LibraTransactionPublishingOption; - use 0x1::LibraTransactionTimeout; use 0x1::Signer; use 0x1::SlidingNonce; use 0x1::TransactionFee; @@ -924,7 +923,7 @@ module LibraAccount { txn_public_key: vector, txn_gas_price: u64, txn_max_gas_units: u64, - txn_expiration_time: u64, + txn_expiration_time_seconds: u64, chain_id: u8, ) acquires LibraAccount, Balance { let transaction_sender = Signer::address_of(sender); @@ -973,7 +972,7 @@ module LibraAccount { PROLOGUE_ESEQUENCE_NUMBER_TOO_NEW ); assert( - LibraTransactionTimeout::is_valid_transaction_timestamp(txn_expiration_time), + LibraTimestamp::now_seconds() < txn_expiration_time_seconds, PROLOGUE_ETRANSACTION_EXPIRED ); } diff --git a/language/stdlib/modules/LibraTimestamp.move b/language/stdlib/modules/LibraTimestamp.move index 0df8d7cb38b9..21058da661ac 100644 --- a/language/stdlib/modules/LibraTimestamp.move +++ b/language/stdlib/modules/LibraTimestamp.move @@ -8,7 +8,6 @@ address 0x1 { /// * LibraSystem, LibraAccount, LibraConfig: to check if the current state is in the genesis state /// * LibraBlock: to reach consensus on the global wall clock time /// * AccountLimits: to limit the time of account limits -/// * LibraTransactionTimeout: to determine whether a transaction is still valid /// module LibraTimestamp { use 0x1::CoreAddresses; @@ -23,6 +22,9 @@ module LibraTimestamp { /// is called at the end of genesis. resource struct TimeHasStarted {} + /// Conversion factor between seconds and microseconds + const MICRO_CONVERSION_FACTOR: u64 = 1000000; + /// The blockchain is not in the genesis state anymore const ENOT_GENESIS: u64 = 0; /// The blockchain is not in an operating state yet @@ -151,7 +153,7 @@ module LibraTimestamp { } - /// Gets the timestamp representing `now` in microseconds. + /// Gets the current time in microseconds. public fun now_microseconds(): u64 acquires CurrentTimeMicroseconds { assert( exists(CoreAddresses::LIBRA_ROOT_ADDRESS()), @@ -168,6 +170,19 @@ module LibraTimestamp { global(CoreAddresses::LIBRA_ROOT_ADDRESS()).microseconds } + /// Gets the current time in seconds. + public fun now_seconds(): u64 acquires CurrentTimeMicroseconds { + now_microseconds() / MICRO_CONVERSION_FACTOR + } + spec fun now_seconds { + pragma opaque; + include AbortsIfNoTime; + ensures result == spec_now_microseconds() / MICRO_CONVERSION_FACTOR; + } + spec define spec_now_seconds(): u64 { + global(CoreAddresses::LIBRA_ROOT_ADDRESS()).microseconds / MICRO_CONVERSION_FACTOR + } + /// Schema specifying that a function aborts if the timer is not published. spec schema AbortsIfNoTime { aborts_if !spec_timer_initialized() with Errors::NOT_PUBLISHED; diff --git a/language/stdlib/modules/LibraTransactionTimeout.move b/language/stdlib/modules/LibraTransactionTimeout.move deleted file mode 100644 index a9da29a860f4..000000000000 --- a/language/stdlib/modules/LibraTransactionTimeout.move +++ /dev/null @@ -1,67 +0,0 @@ -address 0x1 { - -module LibraTransactionTimeout { - use 0x1::CoreAddresses; - use 0x1::Errors; - use 0x1::LibraTimestamp; - use 0x1::Roles; - - resource struct TTL { - // Only transactions with timestamp in between block time and block time + duration would be accepted. - duration_microseconds: u64, - } - - spec module { - invariant [global] LibraTimestamp::is_operating() ==> is_initialized(); - } - - // U64_MAX / 1_000_000 - const MAX_TIMESTAMP: u64 = 18446744073709551615 / 1000000; - const MICROS_MULTIPLIER: u64 = 1000000; - const ONE_DAY_MICROS: u64 = 86400000000; - - /// The `TTL` resource was not in the required state - const ETTL: u64 = 0; - - public fun initialize(lr_account: &signer) { - LibraTimestamp::assert_genesis(); - // Operational constraint, only callable by the libra root account - CoreAddresses::assert_libra_root(lr_account); - assert(!is_initialized(), Errors::already_published(ETTL)); - // Currently set to 1day. - move_to(lr_account, TTL {duration_microseconds: ONE_DAY_MICROS}); - } - - fun is_initialized(): bool { - exists(CoreAddresses::LIBRA_ROOT_ADDRESS()) - } - - // TODO (dd): is this called anywhere? - public fun set_timeout(lr_account: &signer, new_duration: u64) acquires TTL { - LibraTimestamp::assert_operating(); - Roles::assert_libra_root(lr_account); - let timeout = borrow_global_mut(CoreAddresses::LIBRA_ROOT_ADDRESS()); - timeout.duration_microseconds = new_duration; - } - - public fun is_valid_transaction_timestamp(timestamp: u64): bool acquires TTL { - LibraTimestamp::assert_operating(); - // Reject timestamp greater than u64::MAX / 1_000_000. - // This allows converting the timestamp from seconds to microseconds. - if (timestamp > MAX_TIMESTAMP) { - return false - }; - - let current_block_time = LibraTimestamp::now_microseconds(); - let timeout = borrow_global(CoreAddresses::LIBRA_ROOT_ADDRESS()).duration_microseconds; - let _max_txn_time = current_block_time + timeout; - - let txn_time_microseconds = timestamp * MICROS_MULTIPLIER; - // TODO: Add LibraTimestamp::is_before_exclusive(&txn_time_microseconds, &max_txn_time) - // This is causing flaky test right now. The reason is that we will use this logic for AC, where its wall - // clock time might be out of sync with the real block time stored in StateStore. - // See details in issue #2346. - current_block_time < txn_time_microseconds - } -} -} diff --git a/language/stdlib/modules/doc/Genesis.md b/language/stdlib/modules/doc/Genesis.md index 16404422615d..3ec7d8045a88 100644 --- a/language/stdlib/modules/doc/Genesis.md +++ b/language/stdlib/modules/doc/Genesis.md @@ -79,7 +79,6 @@ copy dummy_auth_key_prefix, ); - LibraTransactionTimeout::initialize(lr_account); LibraSystem::initialize_validator_set( lr_account, ); diff --git a/language/stdlib/modules/doc/LibraAccount.md b/language/stdlib/modules/doc/LibraAccount.md index 143b0bd73b0e..819a33f5c826 100644 --- a/language/stdlib/modules/doc/LibraAccount.md +++ b/language/stdlib/modules/doc/LibraAccount.md @@ -2247,7 +2247,7 @@ It verifies: - That the sequence number matches the transaction's sequence key -
fun prologue_common<Token>(sender: &signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8)
+
fun prologue_common<Token>(sender: &signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time_seconds: u64, chain_id: u8)
 
@@ -2262,7 +2262,7 @@ It verifies: txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, - txn_expiration_time: u64, + txn_expiration_time_seconds: u64, chain_id: u8, ) acquires LibraAccount, Balance { let transaction_sender = Signer::address_of(sender); @@ -2311,7 +2311,7 @@ It verifies: PROLOGUE_ESEQUENCE_NUMBER_TOO_NEW ); assert( - LibraTransactionTimeout::is_valid_transaction_timestamp(txn_expiration_time), + LibraTimestamp::now_seconds() < txn_expiration_time_seconds, PROLOGUE_ETRANSACTION_EXPIRED ); } diff --git a/language/stdlib/modules/doc/LibraTimestamp.md b/language/stdlib/modules/doc/LibraTimestamp.md index 695f36007e52..b0eb4f6663aa 100644 --- a/language/stdlib/modules/doc/LibraTimestamp.md +++ b/language/stdlib/modules/doc/LibraTimestamp.md @@ -7,6 +7,7 @@ - [Resource `CurrentTimeMicroseconds`](#0x1_LibraTimestamp_CurrentTimeMicroseconds) - [Resource `TimeHasStarted`](#0x1_LibraTimestamp_TimeHasStarted) +- [Const `MICRO_CONVERSION_FACTOR`](#0x1_LibraTimestamp_MICRO_CONVERSION_FACTOR) - [Const `ENOT_GENESIS`](#0x1_LibraTimestamp_ENOT_GENESIS) - [Const `ENOT_OPERATING`](#0x1_LibraTimestamp_ENOT_OPERATING) - [Const `ETIMER_RESOURCE`](#0x1_LibraTimestamp_ETIMER_RESOURCE) @@ -16,6 +17,7 @@ - [Function `reset_time_has_started_for_test`](#0x1_LibraTimestamp_reset_time_has_started_for_test) - [Function `update_global_time`](#0x1_LibraTimestamp_update_global_time) - [Function `now_microseconds`](#0x1_LibraTimestamp_now_microseconds) +- [Function `now_seconds`](#0x1_LibraTimestamp_now_seconds) - [Function `is_genesis`](#0x1_LibraTimestamp_is_genesis) - [Function `assert_genesis`](#0x1_LibraTimestamp_assert_genesis) - [Function `is_operating`](#0x1_LibraTimestamp_is_operating) @@ -26,6 +28,7 @@ - [Function `set_time_has_started`](#0x1_LibraTimestamp_Specification_set_time_has_started) - [Function `update_global_time`](#0x1_LibraTimestamp_Specification_update_global_time) - [Function `now_microseconds`](#0x1_LibraTimestamp_Specification_now_microseconds) + - [Function `now_seconds`](#0x1_LibraTimestamp_Specification_now_seconds) - [Function `assert_genesis`](#0x1_LibraTimestamp_Specification_assert_genesis) - [Function `assert_operating`](#0x1_LibraTimestamp_Specification_assert_operating) @@ -37,7 +40,6 @@ It interacts with the other modules in the following ways: * LibraSystem, LibraAccount, LibraConfig: to check if the current state is in the genesis state * LibraBlock: to reach consensus on the global wall clock time * AccountLimits: to limit the time of account limits -* LibraTransactionTimeout: to determine whether a transaction is still valid @@ -99,6 +101,18 @@ is called at the end of genesis. + + +## Const `MICRO_CONVERSION_FACTOR` + +Conversion factor between seconds and microseconds + + +
const MICRO_CONVERSION_FACTOR: u64 = 1000000;
+
+ + + ## Const `ENOT_GENESIS` @@ -293,8 +307,7 @@ Updates the wall clock time by consensus. Requires VM privilege and will be invo ## Function `now_microseconds` -Gets the timestamp representing -now in microseconds. +Gets the current time in microseconds.
public fun now_microseconds(): u64
@@ -317,6 +330,31 @@ Gets the timestamp representing
 
 
 
+
+
+
+
+## Function `now_seconds`
+
+Gets the current time in seconds.
+
+
+
public fun now_seconds(): u64
+
+ + + +
+Implementation + + +
public fun now_seconds(): u64 acquires CurrentTimeMicroseconds {
+    now_microseconds() / MICRO_CONVERSION_FACTOR
+}
+
+ + +
@@ -558,7 +596,7 @@ these assertions verify.
include AbortsIfNotOperating;
 include CoreAddresses::AbortsIfNotVM;
-
+
 let now = old(spec_now_microseconds());
 aborts_if [assume]
     (if (proposer == CoreAddresses::VM_RESERVED_ADDRESS()) {
@@ -601,6 +639,35 @@ these assertions verify.
 
+ + + +### Function `now_seconds` + + +
public fun now_seconds(): u64
+
+ + + + +
pragma opaque;
+include AbortsIfNoTime;
+ensures result == spec_now_microseconds() /  MICRO_CONVERSION_FACTOR;
+
+ + + + + + + +
define spec_now_seconds(): u64 {
+global<CurrentTimeMicroseconds>(CoreAddresses::LIBRA_ROOT_ADDRESS()).microseconds / MICRO_CONVERSION_FACTOR
+}
+
+ + Schema specifying that a function aborts if the timer is not published. diff --git a/language/stdlib/modules/doc/LibraTransactionTimeout.md b/language/stdlib/modules/doc/LibraTransactionTimeout.md deleted file mode 100644 index 5b387315bc9d..000000000000 --- a/language/stdlib/modules/doc/LibraTransactionTimeout.md +++ /dev/null @@ -1,222 +0,0 @@ - - - -# Module `0x1::LibraTransactionTimeout` - -### Table of Contents - -- [Resource `TTL`](#0x1_LibraTransactionTimeout_TTL) -- [Const `MAX_TIMESTAMP`](#0x1_LibraTransactionTimeout_MAX_TIMESTAMP) -- [Const `MICROS_MULTIPLIER`](#0x1_LibraTransactionTimeout_MICROS_MULTIPLIER) -- [Const `ONE_DAY_MICROS`](#0x1_LibraTransactionTimeout_ONE_DAY_MICROS) -- [Const `ETTL`](#0x1_LibraTransactionTimeout_ETTL) -- [Function `initialize`](#0x1_LibraTransactionTimeout_initialize) -- [Function `is_initialized`](#0x1_LibraTransactionTimeout_is_initialized) -- [Function `set_timeout`](#0x1_LibraTransactionTimeout_set_timeout) -- [Function `is_valid_transaction_timestamp`](#0x1_LibraTransactionTimeout_is_valid_transaction_timestamp) -- [Specification](#0x1_LibraTransactionTimeout_Specification) - - - - - -## Resource `TTL` - - - -
resource struct TTL
-
- - - -
-Fields - - -
-
- -duration_microseconds: u64 -
-
- -
-
- - -
- - - -## Const `MAX_TIMESTAMP` - - - -
const MAX_TIMESTAMP: u64 = 18446744073709;
-
- - - - - -## Const `MICROS_MULTIPLIER` - - - -
const MICROS_MULTIPLIER: u64 = 1000000;
-
- - - - - -## Const `ONE_DAY_MICROS` - - - -
const ONE_DAY_MICROS: u64 = 86400000000;
-
- - - - - -## Const `ETTL` - -The -TTL resource was not in the required state - - -
const ETTL: u64 = 0;
-
- - - - - -## Function `initialize` - - - -
public fun initialize(lr_account: &signer)
-
- - - -
-Implementation - - -
public fun initialize(lr_account: &signer) {
-    LibraTimestamp::assert_genesis();
-    // Operational constraint, only callable by the libra root account
-    CoreAddresses::assert_libra_root(lr_account);
-    assert(!is_initialized(), Errors::already_published(ETTL));
-    // Currently set to 1day.
-    move_to(lr_account, TTL {duration_microseconds: ONE_DAY_MICROS});
-}
-
- - - -
- - - -## Function `is_initialized` - - - -
fun is_initialized(): bool
-
- - - -
-Implementation - - -
fun is_initialized(): bool {
-    exists<TTL>(CoreAddresses::LIBRA_ROOT_ADDRESS())
-}
-
- - - -
- - - -## Function `set_timeout` - - - -
public fun set_timeout(lr_account: &signer, new_duration: u64)
-
- - - -
-Implementation - - -
public fun set_timeout(lr_account: &signer, new_duration: u64) acquires TTL {
-    LibraTimestamp::assert_operating();
-    Roles::assert_libra_root(lr_account);
-    let timeout = borrow_global_mut<TTL>(CoreAddresses::LIBRA_ROOT_ADDRESS());
-    timeout.duration_microseconds = new_duration;
-}
-
- - - -
- - - -## Function `is_valid_transaction_timestamp` - - - -
public fun is_valid_transaction_timestamp(timestamp: u64): bool
-
- - - -
-Implementation - - -
public fun is_valid_transaction_timestamp(timestamp: u64): bool acquires TTL {
-    LibraTimestamp::assert_operating();
-    // Reject timestamp greater than u64::MAX / 1_000_000.
-    // This allows converting the timestamp from seconds to microseconds.
-    if (timestamp > MAX_TIMESTAMP) {
-      return false
-    };
-
-    let current_block_time = LibraTimestamp::now_microseconds();
-    let timeout = borrow_global<TTL>(CoreAddresses::LIBRA_ROOT_ADDRESS()).duration_microseconds;
-    let _max_txn_time = current_block_time + timeout;
-
-    let txn_time_microseconds = timestamp * MICROS_MULTIPLIER;
-    // TODO: Add LibraTimestamp::is_before_exclusive(&txn_time_microseconds, &max_txn_time)
-    //       This is causing flaky test right now. The reason is that we will use this logic for AC, where its wall
-    //       clock time might be out of sync with the real block time stored in StateStore.
-    //       See details in issue #2346.
-    current_block_time < txn_time_microseconds
-}
-
- - - -
- - - -## Specification - - - -
invariant [global] LibraTimestamp::is_operating() ==> is_initialized();
-