Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Refactor vesting for prove #28

Merged
merged 9 commits into from
Aug 12, 2024
Merged

Refactor vesting for prove #28

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
c79581a
Extract function for writing formal proof
axiongsupra Jul 12, 2024
87c50b3
Add proof for vesting contract state
axiongsupra Jul 12, 2024
81e412d
Update proof for vest_transfer
axiongsupra Jul 16, 2024
60f4e4f
Remove postconditions are not in use
axiongsupra Jul 17, 2024
0a8fd01
Merge branch 'integrate_consensus_key' into refactor-vesting-for-prove
axiongsupra Jul 17, 2024
339b576
One format change
axiongsupra Jul 17, 2024
2a427c0
Address comment on move code
axiongsupra Jul 24, 2024
92d4642
Fix the spec according to code change
axiongsupra Jul 24, 2024
5c9d8d2
Disable one postcondition because of havoc
axiongsupra Jul 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
107 changes: 58 additions & 49 deletions aptos-move/framework/supra-framework/sources/vesting_without_staking.move
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -390,60 +390,69 @@ module supra_framework::vesting_without_staking {
//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<VestingContract>(contract_address).signer_cap);
//extract beneficiary address
let beneficiary = beneficiary(contract_address,shareholder_address);
{
let vesting_contract = borrow_global_mut<VestingContract>(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<SupraCoin>(&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<VestingContract>(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(&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 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) {
vest_transfer(&mut next_period_to_vest, contract_address, shareholder_address);
};
}

fun vest_transfer(next_period_to_vest: &mut u64, contract_address: address,
shareholder_address: address) acquires VestingContract {
let vesting_signer = account::create_signer_with_capability(&borrow_global<VestingContract>(contract_address).signer_cap);
//extract beneficiary address
let beneficiary = beneficiary(contract_address,shareholder_address);

let vesting_contract = borrow_global_mut<VestingContract>(contract_address);
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;

// 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)
};

axiongsupra marked this conversation as resolved.
Show resolved Hide resolved
//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<SupraCoin>(&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;
axiongsupra marked this conversation as resolved.
Show resolved Hide resolved
}

/// 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 {
Expand Down
92 changes: 53 additions & 39 deletions aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<VestingContract>(contract_address);
Expand All @@ -85,46 +85,60 @@ 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<VestingContract>(contract_address);
// let post total_balance = coin::balance<SupraCoin>(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<coin::CoinStore<SupraCoin>>(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<SupraCoin>(address_to_beneficiary) == old(coin::balance<SupraCoin>(address_to_beneficiary)) + amount
// && coin::balance<SupraCoin>(address_from) == old(coin::balance<SupraCoin>(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<SupraCoin>(shareholder) == old(coin::balance<SupraCoin>(shareholder)) + amount
// && coin::balance<SupraCoin>(address_from) == old(coin::balance<SupraCoin>(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<VestingContract>(contract_address);
let post vesting_contract_post = global<VestingContract>(contract_address);
let vesting_schedule = vesting_contract_pre.vesting_schedule;
let last_vested_period = vesting_schedule.last_vested_period;
axiongsupra marked this conversation as resolved.
Show resolved Hide resolved
let next_period_to_vest = last_vested_period + 1;
axiongsupra marked this conversation as resolved.
Show resolved Hide resolved
let last_completed_period =
(timestamp::spec_now_seconds() - vesting_schedule.start_timestamp_secs) / vesting_schedule.period_duration;
let post post_balance = coin::balance<SupraCoin>(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 vesting_contract_pre = global<VestingContract>(contract_address);
let post vesting_contract_post = global<VestingContract>(contract_address);
// ensures the state of the vesting contract is the same after the transfer
ensures vesting_contract_pre.state == vesting_contract_post.state;
let shareholder_record = simple_map::spec_get(vesting_contract_pre.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_pre.vesting_schedule;
let schedule = vesting_schedule.schedule;
let schedule_index = next_period_to_vest - 1;
let vesting_fraction = if (schedule_index < vector::length(schedule)) {
schedule[schedule_index]
} else {
// Last vesting schedule fraction will repeat until the grant runs out.
schedule[vector::length(schedule) - 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_pre.shareholders, shareholder_address);
let post shareholder_amount_post = simple_map::spec_get(vesting_contract_post.shareholders, shareholder_address);
let address_from = global<VestingContract>(contract_address).signer_cap.account;
let address_to_beneficiary = simple_map::spec_get(vesting_contract_pre.beneficiaries, shareholder_address);
let flag = simple_map::spec_contains_key(vesting_contract_pre.beneficiaries, shareholder_address);
// 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<SupraCoin>(address_to_beneficiary) == old(coin::balance<SupraCoin>(address_to_beneficiary)) + amount
&& coin::balance<SupraCoin>(address_from) == old(coin::balance<SupraCoin>(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_address)
==> (coin::balance<SupraCoin>(shareholder_address) == old(coin::balance<SupraCoin>(shareholder_address)) + amount
&& coin::balance<SupraCoin>(address_from) == old(coin::balance<SupraCoin>(address_from)) - amount
&& shareholder_amount_post.left_amount == shareholder_amount.left_amount - amount);
}

spec remove_shareholder {
pragma verify = true;
Expand Down