diff --git a/framework/libra-framework/sources/ol_sources/burn.spec.move b/framework/libra-framework/sources/ol_sources/burn.spec.move new file mode 100644 index 000000000..bbecd3b3b --- /dev/null +++ b/framework/libra-framework/sources/ol_sources/burn.spec.move @@ -0,0 +1,53 @@ +spec ol_framework::burn { + spec module { + pragma verify = true; // Enables verification of the module + pragma aborts_if_is_strict = true; // Ensures strict checking of aborts_if conditions + invariant [suspendable] exists(@ol_framework); // Ensures a BurnCounter always exists + } + + spec initialize { + pragma aborts_if_is_partial = true; // Allows partial aborts + let addr = signer::address_of(vm); + requires system_addresses::is_ol_framework_address(addr); // Checks if the address is a system address + ensures global(@ol_framework).lifetime_recycled == 0; // Ensures lifetime_recycled is initialized to 0 + } + + spec burn_and_track(coin: Coin) { + requires exists(@ol_framework); // Requires a BurnCounter to exist + aborts_if !exists(@ol_framework); // Aborts if no BurnCounter exists + ensures global(@ol_framework).lifetime_burned == + old(global(@ol_framework).lifetime_burned) + coin::value(coin); // Ensures lifetime_burned is incremented by the coin value + pragma aborts_if_is_partial = true; // Allows partial aborts + } + + spec set_send_community(sender: &signer, community: bool) { + let addr = signer::address_of(sender); + + // No aborts_if conditions needed since function handles both cases + aborts_if false; // Never aborts + + // Postconditions + ensures exists(addr); // Ensures UserBurnPreference exists for the address + ensures global(addr).send_community == community; // Ensures send_community is set correctly + requires exists(signer::address_of(sender)); // Ensures UserBurnPreference can be set for the address + } + + spec epoch_burn_fees { + pragma aborts_if_is_partial = true; // Allows partial aborts + ensures global(@ol_framework).lifetime_burned >= old(global(@ol_framework).lifetime_burned); // Ensures lifetime_burned does not decrease + requires global(@ol_framework).lifetime_burned < MAX_U64; // Requires lifetime_burned to be less than MAX_U64 + } + + spec vm_migration { + pragma aborts_if_is_partial = true; // Allows partial aborts + } + + spec vm_burn_with_user_preference { + pragma aborts_if_is_partial = true; // Allows partial aborts + } + + spec BurnCounter { + invariant lifetime_burned <= MAX_U64; // Ensures lifetime_burned does not exceed MAX_U64 + invariant lifetime_recycled <= MAX_U64; // Ensures lifetime_recycled does not exceed MAX_U64 + } +} diff --git a/framework/libra-framework/sources/ol_sources/vouch.spec.move b/framework/libra-framework/sources/ol_sources/vouch.spec.move new file mode 100644 index 000000000..90e330e6a --- /dev/null +++ b/framework/libra-framework/sources/ol_sources/vouch.spec.move @@ -0,0 +1,81 @@ +spec ol_framework::vouch { + spec module { + pragma verify = true; // Enables verification of the module + } + + // Specification for identifying true friends of a given address + spec true_friends(addr: address): vector
{ + pragma aborts_if_is_partial = true; // Allows partial aborts + + // Basic vector property + ensures vector::length(result) >= 0; // Ensures the result is a valid vector + + // If there are no vouches, result should be empty + ensures !exists(addr) ==> + vector::length(result) == 0; // Ensures result is empty if no vouches exist + + // If we have vouches, they must be in a valid state + ensures exists(addr) ==> + vector::length(global(addr).incoming_vouches) >= 0; // Ensures vouches are valid if they exist + + // If result is non-empty, we must have vouches + ensures vector::length(result) > 0 ==> + exists(addr); // Ensures vouches exist if result is non-empty + } + + // Specification for revoking a vouch + spec revoke { + pragma aborts_if_is_partial = true; // Allows partial aborts + + // Basic property - function should not abort + aborts_if false; // Never aborts + + // After revoke, vouches vector should be valid + ensures forall addr: address where exists(addr): + vector::length(global(addr).incoming_vouches) >= 0; // Ensures vouches are valid after revoke + + // After revoke, the number of vouches should decrease or stay the same + ensures forall addr: address where exists(addr): + vector::length(global(addr).incoming_vouches) <= + old(vector::length(global(addr).incoming_vouches)); // Ensures vouches do not increase after revoke + } + + // Specification for checking non-expired vouches + spec all_not_expired(addr: address): vector
{ + pragma aborts_if_is_partial = true; // Allows partial aborts + + // Basic vector property - result must be a valid vector + ensures vector::length(result) >= 0; // Ensures the result is a valid vector + + // If we have vouches, they must be in a valid state + ensures exists(addr) ==> + vector::length(global(addr).incoming_vouches) >= 0; // Ensures vouches are valid if they exist + } + + // Specification for bulk setting vouch records + spec bulk_set(val: address, buddy_list: vector
) { + pragma aborts_if_is_partial = true; // Allows partial aborts + + // Function should not abort + aborts_if false; // Never aborts + + // If ReceivedVouches doesn't exist, nothing changes + ensures !exists(val) ==> true; // No change if vouches do not exist + + // If ReceivedVouches exists, ensure basic properties + ensures exists(val) ==> { + let post = global(val); + // Length of incoming_vouches must be less than or equal to buddy_list + vector::length(post.incoming_vouches) <= vector::length(buddy_list) // Ensures vouches do not exceed buddy list + }; + + // Ensures the state is modified + modifies global(val); // Indicates that vouches are modified + } + + // Add a helper function to make specifications more readable + spec fun is_subset_of_buddy_list(addr_vec: vector
, buddy_list: vector
): bool { + forall i in 0..vector::length(addr_vec): + exists j in 0..vector::length(buddy_list): addr_vec[i] == buddy_list[j] // Checks if addr_vec is a subset of buddy_list + } +} \ No newline at end of file