From c79581acb553132f82b98887e5020370ae8a8b20 Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Thu, 11 Jul 2024 22:25:02 -0400 Subject: [PATCH 1/8] Extract function for writing formal proof --- .../sources/vesting_without_staking.move | 115 ++++++++++-------- 1 file changed, 62 insertions(+), 53 deletions(-) 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 2f56cdae3936c..b779b563eef9a 100644 --- a/aptos-move/framework/supra-framework/sources/vesting_without_staking.move +++ b/aptos-move/framework/supra-framework/sources/vesting_without_staking.move @@ -384,64 +384,73 @@ module supra_framework::vesting_without_staking { public entry fun vest_individual(contract_address: address, shareholder_address: address) acquires VestingContract { assert_active_vesting_contract(contract_address); - //extract beneficiary address - let vesting_signer = account::create_signer_with_capability(&borrow_global(contract_address).signer_cap); - 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(contract_address); + // Short-circuit if vesting hasn't started yet. + if (vesting_contract.vesting_schedule.start_timestamp_secs > timestamp::now_seconds()) { + return }; - let total_balance = coin::balance(contract_address); - if (total_balance == 0) { - set_terminate_vesting_contract(contract_address); - }; + 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); + }; + let total_balance = coin::balance(contract_address); + if (total_balance == 0) { + set_terminate_vesting_contract(contract_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(contract_address).signer_cap); + //extract beneficiary address + let beneficiary = beneficiary(contract_address,shareholder_address); + + let vesting_contract = borrow_global_mut(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) + }; + + //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; + } + /// 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 { From 87c50b30031a74e10c7966e054c901e2135f305a Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Thu, 11 Jul 2024 23:08:33 -0400 Subject: [PATCH 2/8] Add proof for vesting contract state --- .../sources/vesting_without_staking.spec.move | 30 ++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) 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..7cb4460ce8346 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); @@ -88,6 +88,34 @@ spec supra_framework::vesting_without_staking { // ensures last_completed_period > next_period_to_vest ==> TRACE(vesting_contract_post.vesting_schedule.last_vested_period) == TRACE(next_period_to_vest); } + 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_schedule = vesting_contract_pre.vesting_schedule; + let last_vested_period = vesting_schedule.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; + // ensure the vesting contract is terminated if the post_balance is 0 + ensures post_balance == 0 ==> vesting_contract_pre.state == VESTING_POOL_ACTIVE && TRACE(vesting_contract_post).state == VESTING_POOL_TERMINATED; + } + + spec vest_transfer { + pragma verify = true; + let vesting_contract_pre = global(contract_address); + let post vesting_contract_post = global(contract_address); + // ensures the state of the vesting contract is the same after the transfer + ensures vesting_contract_pre.state == vesting_contract_post.state; + } + // spec distribute { // pragma verify = true; // pragma aborts_if_is_partial = true; From 81e412d8e009059f2d9f9aba870a3e156e7bb1b5 Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Mon, 15 Jul 2024 22:42:22 -0400 Subject: [PATCH 3/8] Update proof for vest_transfer --- .../sources/vesting_without_staking.spec.move | 67 ++++++++----------- 1 file changed, 28 insertions(+), 39 deletions(-) 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 7cb4460ce8346..8b2dc52ca518a 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 @@ -105,7 +105,7 @@ spec supra_framework::vesting_without_staking { // 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; // ensure the vesting contract is terminated if the post_balance is 0 - ensures post_balance == 0 ==> vesting_contract_pre.state == VESTING_POOL_ACTIVE && TRACE(vesting_contract_post).state == VESTING_POOL_TERMINATED; + // ensures post_balance == 0 ==> vesting_contract_pre.state == VESTING_POOL_ACTIVE && TRACE(vesting_contract_post).state == VESTING_POOL_TERMINATED; } spec vest_transfer { @@ -114,46 +114,35 @@ spec supra_framework::vesting_without_staking { let post vesting_contract_post = global(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(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(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_address) + ==> (coin::balance(shareholder_address) == old(coin::balance(shareholder_address)) + amount + && coin::balance(address_from) == old(coin::balance(address_from)) - amount + && shareholder_amount_post.left_amount == shareholder_amount.left_amount - amount); } - // 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 remove_shareholder { pragma verify = true; pragma aborts_if_is_partial = true; From 60f4e4fdb8bc9077c5db4228f63c914101ff4402 Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Tue, 16 Jul 2024 22:10:33 -0400 Subject: [PATCH 4/8] Remove postconditions are not in use --- .../supra-framework/sources/vesting_without_staking.spec.move | 3 --- 1 file changed, 3 deletions(-) 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 8b2dc52ca518a..fb308f94e385b 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 @@ -85,7 +85,6 @@ 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 vest_individual { @@ -104,8 +103,6 @@ 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 && post_balance > 0) ==> vesting_contract_pre == vesting_contract_post; - // ensure the vesting contract is terminated if the post_balance is 0 - // ensures post_balance == 0 ==> vesting_contract_pre.state == VESTING_POOL_ACTIVE && TRACE(vesting_contract_post).state == VESTING_POOL_TERMINATED; } spec vest_transfer { From 339b5761a3266e862c6ceff25389831ea4538d59 Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Tue, 16 Jul 2024 22:17:51 -0400 Subject: [PATCH 5/8] One format change --- .../sources/vesting_without_staking.move | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) 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 66e1be6245f2b..6266cadc7724b 100644 --- a/aptos-move/framework/supra-framework/sources/vesting_without_staking.move +++ b/aptos-move/framework/supra-framework/sources/vesting_without_staking.move @@ -390,23 +390,23 @@ 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_contract = borrow_global(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); - }; + let vesting_contract = borrow_global(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, From 2a427c0dd4e59a4132f14c7b9abfc8d3718c1e7f Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Tue, 23 Jul 2024 22:53:06 -0400 Subject: [PATCH 6/8] Address comment on move code --- .../sources/vesting_without_staking.move | 73 +++++++++---------- 1 file changed, 33 insertions(+), 40 deletions(-) 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 6266cadc7724b..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,56 +380,61 @@ 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_contract = borrow_global(contract_address); + 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(&vesting_contract.shareholders,&shareholder_address); + 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) { - vest_transfer(&mut next_period_to_vest, contract_address, shareholder_address); + 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(next_period_to_vest: &mut u64, contract_address: address, - shareholder_address: address) acquires VestingContract { - 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); - 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) - }; + 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( @@ -439,18 +444,6 @@ module supra_framework::vesting_without_staking { //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; } /// Remove the lockup period for the vesting contract. This can only be called by the admin of the vesting contract. From 92d46421c95d43a48f0007cf191a94e7d55b1dfe Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Tue, 23 Jul 2024 23:00:16 -0400 Subject: [PATCH 7/8] Fix the spec according to code change --- .../sources/vesting_without_staking.spec.move | 39 ++++--------------- 1 file changed, 8 insertions(+), 31 deletions(-) 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 fb308f94e385b..bbb21893bda53 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 @@ -107,37 +107,14 @@ spec supra_framework::vesting_without_staking { spec vest_transfer { pragma verify = true; - let vesting_contract_pre = global(contract_address); - let post vesting_contract_post = global(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(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(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_address) - ==> (coin::balance(shareholder_address) == old(coin::balance(shareholder_address)) + amount - && coin::balance(address_from) == old(coin::balance(address_from)) - amount - && shareholder_amount_post.left_amount == shareholder_amount.left_amount - amount); + 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 { From 5c9d8d23d6b6900e39ad067a89871ac62f2320ed Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Tue, 23 Jul 2024 23:08:08 -0400 Subject: [PATCH 8/8] Disable one postcondition because of havoc --- .../sources/vesting_without_staking.spec.move | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) 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 bbb21893bda53..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 @@ -93,16 +93,17 @@ spec supra_framework::vesting_without_staking { include VestingContractActive; let vesting_contract_pre = global(contract_address); let post vesting_contract_post = global(contract_address); - let vesting_schedule = vesting_contract_pre.vesting_schedule; - let last_vested_period = vesting_schedule.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); + // 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; + // ensures (last_completed_period < next_period_to_vest && post_balance > 0) ==> vesting_contract_pre == vesting_contract_post; } spec vest_transfer {