diff --git a/aptos-move/framework/supra-framework/sources/vesting_without_staking.move b/aptos-move/framework/supra-framework/sources/vesting_without_staking.move index ac206ea7de8ef..517c389cfa353 100644 --- a/aptos-move/framework/supra-framework/sources/vesting_without_staking.move +++ b/aptos-move/framework/supra-framework/sources/vesting_without_staking.move @@ -380,70 +380,72 @@ module supra_framework::vesting_without_staking { let shareholder = vector::pop_back(&mut shareholders); vest_individual(contract_address,shareholder); }; - let total_balance = coin::balance(contract_address); - if (total_balance == 0) { - set_terminate_vesting_contract(contract_address); - }; + let total_balance = coin::balance(contract_address); + if (total_balance == 0) { + set_terminate_vesting_contract(contract_address); + }; } public entry fun vest_individual(contract_address: address, shareholder_address: address) acquires VestingContract { //check if contract exist, active and shareholder is a member of the contract assert_shareholder_exists(contract_address,shareholder_address); - let vesting_signer = account::create_signer_with_capability(&borrow_global(contract_address).signer_cap); - //extract beneficiary address - let beneficiary = beneficiary(contract_address,shareholder_address); - { - let vesting_contract = borrow_global_mut(contract_address); - // Short-circuit if vesting hasn't started yet. - if (vesting_contract.vesting_schedule.start_timestamp_secs > timestamp::now_seconds()) { - return - }; - - let vesting_record = simple_map::borrow_mut(&mut vesting_contract.shareholders,&shareholder_address); - - // Check if the next vested period has already passed. If not, short-circuit since there's nothing to vest. - let vesting_schedule = vesting_contract.vesting_schedule; - let schedule = &vesting_schedule.schedule; - let last_vested_period = vesting_record.last_vested_period; - let next_period_to_vest = last_vested_period + 1; - let last_completed_period = - (timestamp::now_seconds() - vesting_schedule.start_timestamp_secs) / vesting_schedule.period_duration; - while(last_completed_period>=next_period_to_vest) { - // Index is 0-based while period is 1-based so we need to subtract 1. - let schedule_index = next_period_to_vest - 1; - let vesting_fraction = if (schedule_index < vector::length(schedule)) { - *vector::borrow(schedule, schedule_index) - } else { - // Last vesting schedule fraction will repeat until the grant runs out. - *vector::borrow(schedule, vector::length(schedule) - 1) - }; - - //amount to be transfer is minimum of what is left and vesting fraction due of init_amount - let amount = min( - vesting_record.left_amount, - fixed_point32::multiply_u64(vesting_record.init_amount, vesting_fraction) - ); - //update left_amount for the shareholder - vesting_record.left_amount = vesting_record.left_amount - amount; - coin::transfer(&vesting_signer, beneficiary, amount); - emit_event( - &mut vesting_contract.vest_events, - VestEvent { - admin: vesting_contract.admin, - shareholder_address: shareholder_address, - vesting_contract_address: contract_address, - period_vested: next_period_to_vest, - }, - ); - //update last_vested_period for the shareholder - vesting_record.last_vested_period = next_period_to_vest; - next_period_to_vest = next_period_to_vest + 1; + let vesting_contract = borrow_global_mut(contract_address); + let beneficiary = get_beneficiary(vesting_contract, shareholder_address); + // Short-circuit if vesting hasn't started yet. + if (vesting_contract.vesting_schedule.start_timestamp_secs > timestamp::now_seconds()) { + return }; + let vesting_record = simple_map::borrow_mut(&mut vesting_contract.shareholders,&shareholder_address); + let signer_cap = &vesting_contract.signer_cap; + + // Check if the next vested period has already passed. If not, short-circuit since there's nothing to vest. + let vesting_schedule = vesting_contract.vesting_schedule; + let schedule = &vesting_schedule.schedule; + let last_vested_period = vesting_record.last_vested_period; + let next_period_to_vest = last_vested_period + 1; + let last_completed_period = + (timestamp::now_seconds() - vesting_schedule.start_timestamp_secs) / vesting_schedule.period_duration; + // Index is 0-based while period is 1-based so we need to subtract 1. + while(last_completed_period>=next_period_to_vest) { + let schedule_index = next_period_to_vest - 1; + let vesting_fraction = if (schedule_index < vector::length(schedule)) { + *vector::borrow(schedule, schedule_index) + } else { + // Last vesting schedule fraction will repeat until the grant runs out. + *vector::borrow(schedule, vector::length(schedule) - 1) + }; + vest_transfer(vesting_record, signer_cap, beneficiary, vesting_fraction); + //update last_vested_period for the shareholder + vesting_record.last_vested_period = next_period_to_vest; + next_period_to_vest = next_period_to_vest + 1; + emit_event( + &mut vesting_contract.vest_events, + VestEvent { + admin: vesting_contract.admin, + shareholder_address: shareholder_address, + vesting_contract_address: contract_address, + period_vested: next_period_to_vest, + }, + ); }; } + fun vest_transfer(vesting_record: &mut VestingRecord, signer_cap: &SignerCapability, + beneficiary: address, vesting_fraction: FixedPoint32) { + let vesting_signer = account::create_signer_with_capability(signer_cap); + + //amount to be transfer is minimum of what is left and vesting fraction due of init_amount + let amount = min( + vesting_record.left_amount, + fixed_point32::multiply_u64(vesting_record.init_amount, vesting_fraction) + ); + //update left_amount for the shareholder + vesting_record.left_amount = vesting_record.left_amount - amount; + coin::transfer(&vesting_signer, beneficiary, amount); + } + /// Remove the lockup period for the vesting contract. This can only be called by the admin of the vesting contract. /// Example usage: If admin find shareholder suspicious, admin can remove it. public entry fun remove_shareholder(admin: &signer, contract_address: address, shareholder_address: address) acquires VestingContract { diff --git a/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move b/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move index 826e41f201e23..3dd2c83d54f8c 100644 --- a/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move +++ b/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move @@ -71,7 +71,7 @@ spec supra_framework::vesting_without_staking { // } spec vest { - pragma verify = true; + pragma verify = false; pragma aborts_if_is_partial = true; include VestingContractActive; let vesting_contract_pre = global(contract_address); @@ -85,46 +85,38 @@ spec supra_framework::vesting_without_staking { ensures vesting_contract_pre.vesting_schedule.start_timestamp_secs > timestamp::spec_now_seconds() ==> vesting_contract_pre == vesting_contract_post; // ensure the vesting contract is the same if the last completed period is greater than the next period to vest ensures last_completed_period < next_period_to_vest ==> vesting_contract_pre == vesting_contract_post; - // ensures last_completed_period > next_period_to_vest ==> TRACE(vesting_contract_post.vesting_schedule.last_vested_period) == TRACE(next_period_to_vest); } - // spec distribute { - // pragma verify = true; - // pragma aborts_if_is_partial = true; - // include VestingContractActive; - // let post vesting_contract_post = global(contract_address); - // let post total_balance = coin::balance(contract_address); - // // ensure if the total balance is 0, the vesting contract is terminated - // ensures total_balance == 0 ==> vesting_contract_post.state == VESTING_POOL_TERMINATED; - // // // ensure if the total balance is not 0, the vesting contract is active - // // ensures total_balance != 0 ==> vesting_contract_post.state == VESTING_POOL_ACTIVE; - // } - // - // spec distribute_to_shareholder { - // pragma verify = true; - // // pragma opaque; - // // modifies global>(address_from); - // let shareholder = shareholders_address[len(shareholders_address) - 1]; - // let shareholder_record = vesting_records[len(vesting_records) - 1]; - // let amount = min(shareholder_record.left_amount, fixed_point32::spec_multiply_u64(shareholder_record.init_amount, vesting_fraction)); - // let shareholder_amount = simple_map::spec_get(vesting_contract.shareholders, shareholder); - // let post shareholder_amount_post = simple_map::spec_get(vesting_contract.shareholders, shareholder); - // let address_from = signer::address_of(vesting_signer); - // let address_to_beneficiary = simple_map::spec_get(vesting_contract.beneficiaries, shareholder); - // let flag = simple_map::spec_contains_key(vesting_contract.beneficiaries, shareholder); - // // Ensure that the amount is transferred to the beneficiary and the amount is substract from left_amount if the beneficiary exists - // ensures (flag && address_from != address_to_beneficiary) - // ==> (coin::balance(address_to_beneficiary) == old(coin::balance(address_to_beneficiary)) + amount - // && coin::balance(address_from) == old(coin::balance(address_from)) - amount - // && shareholder_amount_post.left_amount == shareholder_amount.left_amount - amount); - // // Ensure that the amount is transferred to the shareholder and the amount is substract from left_amount if the beneficiary doesn't exist - // ensures (!flag && address_from != shareholder) - // ==> (coin::balance(shareholder) == old(coin::balance(shareholder)) + amount - // && coin::balance(address_from) == old(coin::balance(address_from)) - amount - // && shareholder_amount_post.left_amount == shareholder_amount.left_amount - amount); - // // Ensure the length of the shareholders_address and vesting_records are the same if they are the same before the function call - // ensures (len(old(shareholders_address)) == len(old(vesting_records))) ==> (len(shareholders_address) == len(vesting_records)); - // } + spec vest_individual { + pragma verify = true; + pragma aborts_if_is_partial = true; + include VestingContractActive; + let vesting_contract_pre = global(contract_address); + let post vesting_contract_post = global(contract_address); + // let vesting_record = simple_map::spec_get(vesting_contract_pre.shareholders, shareholder_address); + // let vesting_schedule = vesting_contract_pre.vesting_schedule; + // let last_vested_period = vesting_record.last_vested_period; + // let next_period_to_vest = last_vested_period + 1; + // let last_completed_period = + // (timestamp::spec_now_seconds() - vesting_schedule.start_timestamp_secs) / vesting_schedule.period_duration; + // let post post_balance = coin::balance(contract_address); + // ensure the vesting contract is the same if the vesting period is not reached + ensures vesting_contract_pre.vesting_schedule.start_timestamp_secs > timestamp::spec_now_seconds() ==> vesting_contract_pre == vesting_contract_post; + // ensure the vesting contract is the same if the last completed period is greater than the next period to vest + // ensures (last_completed_period < next_period_to_vest && post_balance > 0) ==> vesting_contract_pre == vesting_contract_post; + } + + spec vest_transfer { + pragma verify = true; + let amount = min(vesting_record.left_amount, fixed_point32::spec_multiply_u64(vesting_record.init_amount, vesting_fraction)); + // Ensure that the amount is substracted from the left_amount + ensures vesting_record.left_amount == old(vesting_record.left_amount) - amount; + let address_from = signer_cap.account; + // Ensure that the amount is transferred from the address_from to the beneficiary + ensures beneficiary != address_from ==> + (coin::balance(beneficiary) == old(coin::balance(beneficiary)) + amount + && coin::balance(address_from) == old(coin::balance(address_from)) - amount); + } spec remove_shareholder { pragma verify = true;