Skip to content

Commit

Permalink
Refactor vesting for prove (#28)
Browse files Browse the repository at this point in the history 
* Extract function for writing formal proof

* Add proof for vesting contract state

* Update proof for vest_transfer

* Remove postconditions are not in use

* One format change

* Address comment on move code

* Fix the spec according to code change

* Disable one postcondition because of havoc
  • Loading branch information
@axiongsupra
axiongsupra authored Aug 12, 2024
1 parent b56e74e commit b9057fa
Show file tree
Hide file tree
Showing 2 changed files with 86 additions and 92 deletions.
108 changes: 55 additions & 53 deletions aptos-move/framework/supra-framework/sources/vesting_without_staking.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<SupraCoin>(contract_address);
if (total_balance == 0) {
set_terminate_vesting_contract(contract_address);
};
let total_balance = coin::balance<SupraCoin>(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<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_mut<VestingContract>(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<SupraCoin>(&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 {
Expand Down
70 changes: 31 additions & 39 deletions aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move
View file
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,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<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_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<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 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<SupraCoin>(beneficiary) == old(coin::balance<SupraCoin>(beneficiary)) + amount
&& coin::balance<SupraCoin>(address_from) == old(coin::balance<SupraCoin>(address_from)) - amount);
}

spec remove_shareholder {
pragma verify = true;
Expand Down

0 comments on commit b9057fa

Please sign in to comment.