From 724beb3d3333bd6a49677dbad987b275deb7315b Mon Sep 17 00:00:00 2001 From: Jayfromthe13th Date: Mon, 6 Jan 2025 21:40:20 -0600 Subject: [PATCH 1/4] Update lockbox.move with standard duration validation --- .../sources/ol_sources/lockbox.move | 53 ++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/framework/libra-framework/sources/ol_sources/lockbox.move b/framework/libra-framework/sources/ol_sources/lockbox.move index af8173059..f5051ab1c 100644 --- a/framework/libra-framework/sources/ol_sources/lockbox.move +++ b/framework/libra-framework/sources/ol_sources/lockbox.move @@ -37,8 +37,10 @@ module ol_framework::lockbox { /// The locked units for this box duration should have changed. const EDURATION_UNITS_SHOULD_CHANGE: u64 = 8; + /// Duration not in allowed list + const EINVALID_DURATION: u64 = 9; - const DEFAULT_LOCKS: vector = vector[1*12, 4*12, 8*12, 16*12, 20*12, 24*12, 28*12, 32*12]; + const DEFAULT_LOCKS: vector = vector[1*12, 2*12, 3*12, 4*12, 8*12, 16*12, 20*12, 24*12, 28*12, 32*12]; struct Lockbox has key, store { locked_coins: Coin, @@ -61,9 +63,25 @@ module ol_framework::lockbox { } } + /// Checks if a duration is in the DEFAULT_LOCKS list + fun is_valid_duration(duration: u64): bool { + let i = 0; + let len = vector::length(&DEFAULT_LOCKS); + while (i < len) { + if (*vector::borrow(&DEFAULT_LOCKS, i) == duration) { + return true + }; + i = i + 1; + }; + false + } + /// Creates a lockbox. The lockbox cannot be dropped, and so must be /// stored in the same call. public(friend) fun new(locked_coins: Coin, duration_type: u64): Lockbox { + // Validate that the duration is in the allowed list + assert!(is_valid_duration(duration_type), error::invalid_argument(EINVALID_DURATION)); + Lockbox { locked_coins, duration_type, @@ -366,4 +384,37 @@ module ol_framework::lockbox { assert!(bal2 == 123, 7357007); } + #[test(framework = @0x1, bob_sig = @0x10002)] + #[expected_failure(abort_code = 65545)] // error::invalid_argument(EINVALID_DURATION) + fun test_non_standard_duration(framework: &signer, bob_sig: &signer) acquires SlowWalletV2 { + let bob_addr = signer::address_of(bob_sig); + let coin = test_setup(framework, 100); + + // Try to create a lockbox with a non-standard duration (5*12 months) + // This should fail because 5*12 is not in DEFAULT_LOCKS + add_to_or_create_box(bob_sig, coin, 5*12); + + // These assertions should never be reached because the above call should fail + let (found, _) = idx_by_duration(bob_addr, 5*12); + assert!(!found, 7357001); + } + + #[test(framework = @0x1, bob_sig = @0x10002)] + fun test_standard_duration(framework: &signer, bob_sig: &signer) acquires SlowWalletV2 { + let bob_addr = signer::address_of(bob_sig); + let coin = test_setup(framework, 100); + + // Try to create a lockbox with a standard duration (4*12 months) + // This should succeed because 4*12 is in DEFAULT_LOCKS + add_to_or_create_box(bob_sig, coin, 4*12); + + // Verify the lockbox was created with the standard duration + let (found, idx) = idx_by_duration(bob_addr, 4*12); + assert!(found, 7357001); + assert!(idx == 0, 7357002); + + // Verify the balance + let balance = balance_duration(bob_addr, 4*12); + assert!(balance == 100, 7357003); + } } From 79e334308e99fdd8b774b85185e4e8224d2c0fa0 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Tue, 7 Jan 2025 10:31:30 -0600 Subject: [PATCH 2/4] Update lockbox.spec.move added spec for now --- .../sources/ol_sources/lockbox.spec.move | 109 +++++++++++++++--- 1 file changed, 96 insertions(+), 13 deletions(-) diff --git a/framework/libra-framework/sources/ol_sources/lockbox.spec.move b/framework/libra-framework/sources/ol_sources/lockbox.spec.move index e3414b554..f3258cdfa 100644 --- a/framework/libra-framework/sources/ol_sources/lockbox.spec.move +++ b/framework/libra-framework/sources/ol_sources/lockbox.spec.move @@ -1,22 +1,105 @@ +/// 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); + } + +File file without spec above spec ol_framework::lockbox { - spec maybe_initialize(user: &signer) { - ensures exists(signer::address_of(user)); - } + /// Specification for maybe_initialize: + /// Initializes a new SlowWalletV2 for a user if one doesn't exist + spec maybe_initialize(user: &signer) { + // Post-condition: ensures a SlowWalletV2 exists for the user after execution + ensures exists(signer::address_of(user)); + } + + /// Specification for new: + /// Creates a new Lockbox with initial values + spec new(locked_coins: Coin, duration_type: u64): Lockbox { + // Post-conditions: verify all fields are properly initialized + ensures result.duration_type == duration_type; // Duration is set correctly + ensures result.lifetime_deposits == 0; // No deposits yet + ensures result.lifetime_unlocked == 0; // Nothing unlocked yet + ensures result.last_unlock_timestamp == 0; // No unlocks performed + } + + /// Specification for add_to_or_create_box: + /// Adds coins to an existing box or creates a new one + 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 + } - spec delay_impl(user: &signer, duration_from: u64, duration_to: u64, units: u64) { + /// Specification for deposit_impl: + /// Internal implementation for depositing coins + spec deposit_impl(user_addr: address, locked_coins: Coin, duration_type: u64) { + // Pre-conditions + requires user_addr != @0x0; // Address must be valid + requires exists(user_addr); // SlowWalletV2 must exist + } - // cannot move to same duration - ensures duration_from != duration_to; - // cannot move to lower duration - ensures duration_from < duration_to; + /// Specification for balance_list: + /// Calculates total balance of all lockboxes in a list + spec balance_list(list: &vector): u64 { + // Post-conditions + ensures result >= 0; // Balance can never be negative + } - } + /// Specification for delay_impl: + /// Implements the delay mechanism for shifting coins to longer durations + 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 + } - spec checked_transfer_impl(from: &signer, to: address, duration_type: u64, units: u64) { - requires exists(signer::address_of(from)); - requires exists(to); + /// Specification for checked_transfer_impl: + /// Implements safe transfer between two SlowWalletV2 accounts + spec checked_transfer_impl(from: &signer, to: address, duration_type: u64, units: u64) { + // Pre-conditions + requires exists(signer::address_of(from)); // Sender must have SlowWalletV2 + 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 + } - } + /// Specification for deposit: + /// Handles depositing coins into a lockbox + spec deposit(box: &mut Lockbox, more_coins: Coin) { + // Post-conditions + ensures box.locked_coins.value == old(box.locked_coins.value) + more_coins.value; // Balance increases by deposited amount + } + /// Specification for withdraw_drip_impl: + /// Implements the drip withdrawal mechanism + spec withdraw_drip_impl(user: &signer, idx: u64): Option> { + requires exists(signer::address_of(user)); + 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 + } + + } + From 520abdb327b6a9a557ea8d3a9c6bbe7c8221d855 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Tue, 7 Jan 2025 10:35:31 -0600 Subject: [PATCH 3/4] Update lockbox.spec.move clean up --- .../sources/ol_sources/lockbox.spec.move | 25 +++++++++---------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/framework/libra-framework/sources/ol_sources/lockbox.spec.move b/framework/libra-framework/sources/ol_sources/lockbox.spec.move index f3258cdfa..e1fdb0744 100644 --- a/framework/libra-framework/sources/ol_sources/lockbox.spec.move +++ b/framework/libra-framework/sources/ol_sources/lockbox.spec.move @@ -1,16 +1,5 @@ -/// 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); - } -File file without spec above + spec ol_framework::lockbox { /// Specification for maybe_initialize: @@ -100,6 +89,16 @@ spec ol_framework::lockbox { days / 10000000 + 1 } - + /// 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); + } } From b301d7f7642b668305a3eed3924784303a7138de Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Tue, 7 Jan 2025 15:39:29 -0600 Subject: [PATCH 4/4] Update lockbox.spec.move --- .../sources/ol_sources/lockbox.spec.move | 107 +++--------------- 1 file changed, 13 insertions(+), 94 deletions(-) diff --git a/framework/libra-framework/sources/ol_sources/lockbox.spec.move b/framework/libra-framework/sources/ol_sources/lockbox.spec.move index e1fdb0744..e1ba160f2 100644 --- a/framework/libra-framework/sources/ol_sources/lockbox.spec.move +++ b/framework/libra-framework/sources/ol_sources/lockbox.spec.move @@ -1,104 +1,23 @@ - - spec ol_framework::lockbox { - /// Specification for maybe_initialize: - /// Initializes a new SlowWalletV2 for a user if one doesn't exist - spec maybe_initialize(user: &signer) { - // Post-condition: ensures a SlowWalletV2 exists for the user after execution - ensures exists(signer::address_of(user)); - } - - /// Specification for new: - /// Creates a new Lockbox with initial values - spec new(locked_coins: Coin, duration_type: u64): Lockbox { - // Post-conditions: verify all fields are properly initialized - ensures result.duration_type == duration_type; // Duration is set correctly - ensures result.lifetime_deposits == 0; // No deposits yet - ensures result.lifetime_unlocked == 0; // Nothing unlocked yet - ensures result.last_unlock_timestamp == 0; // No unlocks performed - } - - /// Specification for add_to_or_create_box: - /// Adds coins to an existing box or creates a new one - 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 - } - - /// Specification for deposit_impl: - /// Internal implementation for depositing coins - spec deposit_impl(user_addr: address, locked_coins: Coin, duration_type: u64) { - // Pre-conditions - requires user_addr != @0x0; // Address must be valid - requires exists(user_addr); // SlowWalletV2 must exist - } - - /// Specification for balance_list: - /// Calculates total balance of all lockboxes in a list - spec balance_list(list: &vector): u64 { - // Post-conditions - ensures result >= 0; // Balance can never be negative - } + spec maybe_initialize(user: &signer) { + ensures exists(signer::address_of(user)); + } - /// Specification for delay_impl: - /// Implements the delay mechanism for shifting coins to longer durations - 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 - } + spec delay_impl(user: &signer, duration_from: u64, duration_to: u64, units: u64) { - /// Specification for checked_transfer_impl: - /// Implements safe transfer between two SlowWalletV2 accounts - spec checked_transfer_impl(from: &signer, to: address, duration_type: u64, units: u64) { - // Pre-conditions - requires exists(signer::address_of(from)); // Sender must have SlowWalletV2 - 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 - } + // cannot move to same duration + ensures duration_from != duration_to; + // cannot move to lower duration + ensures duration_from < duration_to; - /// Specification for deposit: - /// Handles depositing coins into a lockbox - spec deposit(box: &mut Lockbox, more_coins: Coin) { - // Post-conditions - ensures box.locked_coins.value == old(box.locked_coins.value) + more_coins.value; // Balance increases by deposited amount - } + } - /// Specification for withdraw_drip_impl: - /// Implements the drip withdrawal mechanism - spec withdraw_drip_impl(user: &signer, idx: u64): Option> { - requires exists(signer::address_of(user)); - requires idx < vector::length(global(signer::address_of(user)).list); - } + spec checked_transfer_impl(from: &signer, to: address, duration_type: u64, units: u64) { + requires exists(signer::address_of(from)); + requires exists(to); - - /// 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 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); - } }