Skip to content

Commit

Permalink
add #test to lockbox spec
Browse files Browse the repository at this point in the history
  • Loading branch information
0o-de-lally committed Jan 9, 2025
1 parent a63e912 commit e0d0ec3
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions framework/libra-framework/sources/ol_sources/lockbox.spec.move
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ spec ol_framework::lockbox {
spec add_to_or_create_box(user: &signer, locked_coins: Coin<LibraCoin>, duration_type: u64) {
// Pre-conditions
requires signer::address_of(user) != @0x0; // User must have valid address

// Post-conditions
ensures exists<SlowWalletV2>(signer::address_of(user)); // SlowWalletV2 must exist after operation
}
Expand All @@ -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
}
Expand All @@ -62,7 +62,7 @@ spec ol_framework::lockbox {
requires exists<SlowWalletV2>(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
Expand All @@ -82,23 +82,23 @@ spec ol_framework::lockbox {
requires idx < vector::length(global<SlowWalletV2>(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);
}
}

0 comments on commit e0d0ec3

Please sign in to comment.