Skip to content

Fix spec and add spec for supra governance #63

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.

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

Open
wants to merge 45 commits into
base: dev
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
45 commits
Select commit Hold shift + click to select a range
f2b3a63
Fix move spec files
axiongsupra Aug 30, 2024
fdef1f8
Don't verify committee_map
axiongsupra Aug 30, 2024
3847bfa
Merge branch 'dev' into fix-spec
axiongsupra Aug 30, 2024
2909d36
Merge branch 'dev' into fix-spec
axiongsupra Sep 5, 2024
0530b59
Spec for supra_governance
axiongsupra Aug 30, 2024
0b1709f
Commit spec for merge change from dev
axiongsupra Sep 5, 2024
40ba45e
supra_governance spec
axiongsupra Sep 6, 2024
0f0319a
Commit multisig_voting spec
axiongsupra Sep 6, 2024
af60d2a
Finish a few todos
axiongsupra Sep 6, 2024
e4c58d8
Add empty spec first
axiongsupra Sep 6, 2024
3aa67d6
More spec from voting and need to be adjustied
axiongsupra Sep 6, 2024
0d85241
More spec enabled
axiongsupra Sep 11, 2024
817c27e
Precondition works now
axiongsupra Sep 11, 2024
cc3b105
Merge branch 'dev' into fix-spec
axiongsupra Sep 11, 2024
1ed9dd4
Merge branch 'dev' into fix-spec
axiongsupra Sep 27, 2024
8495dbd
Merge branch 'dev' into fix-spec
axiongsupra Oct 2, 2024
35d31d0
Use original genesis.spec.move
axiongsupra Oct 2, 2024
d8f0058
Merge branch 'dev' into fix-spec
axiongsupra Oct 8, 2024
4023ea1
Merge branch 'dev' into fix-spec
axiongsupra Oct 16, 2024
a042dfb
Merge branch 'dev' into fix-spec
axiongsupra Oct 29, 2024
98898d0
Merge branch 'dev' into fix-spec
axiongsupra Nov 27, 2024
5ae1f73
Renaming for `AbortsIfNotSupraFramework`
axiongsupra Oct 30, 2024
4829c55
Prover works now
axiongsupra Nov 29, 2024
3ec69d5
Rename `AbortsIfNotAptosFramework` to `AbortsIfNotSupraFramework`
axiongsupra Nov 29, 2024
65e77e5
Fix function signature mismatch
axiongsupra Nov 29, 2024
1c5eacc
Enable post condition for `is_voting_closed`
axiongsupra Nov 29, 2024
93c26ef
Enable post condition for `get_proposal_state`
axiongsupra Nov 29, 2024
dacd39b
Enable verification for `vest_transfer` and `remove_shareholder`
axiongsupra Dec 4, 2024
6b88e9c
Remove unused specs
axiongsupra Dec 4, 2024
565c1a3
A few proof for coins and supra_account
axiongsupra Dec 5, 2024
dc3c47e
Revert comment outted pre condition
axiongsupra Dec 5, 2024
f32cb3d
Remove a few debug trace
axiongsupra Dec 5, 2024
6d8398f
Finish aborts condition for `emit_genesis_reconfiguration_event`
axiongsupra Dec 5, 2024
494d7c0
One more abort condition for `set_genesis_end`
axiongsupra Dec 5, 2024
ece65d8
More aborts condition
axiongsupra Dec 6, 2024
8aa2279
Correct abort for `IsProposalResolvableAbortsIf`
axiongsupra Dec 6, 2024
6153b4a
Correct abort for `resolve`
axiongsupra Dec 7, 2024
e65045b
More proofs
axiongsupra Dec 10, 2024
13e1b18
Merge branch 'dev' into fix-spec
axiongsupra Dec 25, 2024
f55d083
Merge branch 'dev' into fix-spec
axiongsupra Jan 7, 2025
b0056c5
Merge branch 'dev' into fix-spec
axiongsupra Jan 24, 2025
fcd06bb
Merge branch 'dev' into fix-spec
axiongsupra Feb 5, 2025
9551a1e
Merge branch 'dev' into fix-spec
axiongsupra Mar 27, 2025
e55aba7
Disable verification for new functions
axiongsupra Mar 28, 2025
f6e6256
Merge branch 'dev' into fix-spec
axiongsupra May 21, 2025
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
Prev Previous commit
Next Next commit
Enable verification for vest_transfer and remove_shareholder
  • Loading branch information
axiongsupra committed Dec 4, 2024
commit dacd39b2c208692a082405ea7fbe28dcce931e9f
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ spec supra_framework::vesting_without_staking {

spec vest_transfer {
// TODO(fa_migration)
pragma verify = false;
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;
Expand All @@ -126,7 +126,7 @@ spec supra_framework::vesting_without_staking {

spec remove_shareholder {
// TODO(fa_migration)
pragma verify = false;
pragma verify = true;
pragma aborts_if_is_partial = true;
include AdminAborts;
let vesting_contract = global<VestingContract>(contract_address);
Expand Down