diff --git a/framework/libra-framework/sources/ol_sources/lockbox.spec.move b/framework/libra-framework/sources/ol_sources/lockbox.spec.move index e1fdb0744..d49eda95c 100644 --- a/framework/libra-framework/sources/ol_sources/lockbox.spec.move +++ b/framework/libra-framework/sources/ol_sources/lockbox.spec.move @@ -24,7 +24,7 @@ spec ol_framework::lockbox { spec add_to_or_create_box(user: &signer, locked_coins: Coin, duration_type: u64) { // Pre-conditions requires signer::address_of(user) != @0x0; // User must have valid address - + // Post-conditions ensures exists(signer::address_of(user)); // SlowWalletV2 must exist after operation } @@ -49,7 +49,7 @@ spec ol_framework::lockbox { spec delay_impl(user: &signer, duration_from: u64, duration_to: u64, units: u64) { // Pre-conditions requires signer::address_of(user) != @0x0; // User must have valid address - + // Post-conditions ensures duration_from < duration_to; // Can only move to longer duration } @@ -62,7 +62,7 @@ spec ol_framework::lockbox { requires exists(to); // Receiver must have SlowWalletV2 requires units > 0; // Must transfer positive amount requires to != @0x0; // Receiver address must be valid - + // Post-conditions ensures units > 0; // Amount remains positive ensures to != @0x0; // Receiver remains valid @@ -82,23 +82,23 @@ spec ol_framework::lockbox { requires idx < vector::length(global(signer::address_of(user)).list); } - + /// Helper function to calculate minimum amount needed to get non-zero drip spec fun min_amount_for_drip(duration_months: u64): u64 { let days = math64::mul_div(duration_months, 365, 12); days / 10000000 + 1 } + #[test] /// Test that verifies a user CANNOT create a lockbox with a non-standard duration /// This test demonstrates that the DEFAULT_LOCKS list IS enforced spec test_non_standard_duration(framework: &signer, bob_sig: &signer) { // Pre-conditions requires signer::address_of(bob_sig) != @0x0; // Bob must have valid address - + // Post-conditions // The test should fail when attempting a non-standard duration (e.g., 5*12 months) // This shows that DEFAULT_LOCKS is enforced aborts_with error::invalid_argument(EINVALID_DURATION); } } -