[Spec] update specs of voting, transaction_fee, code #8172

xudon9 · 2023-05-12T08:35:42Z

Description

This is a part of spec work for Aptos Framework from MoveBit. The changes are:

Completed all specs left as TODO in transaction_fee and voting;
Some functions in code gets specified.

Test Plan

aptos move prove -f voting.move
aptos move prove -f transaction_fee.move
aptos move prove -f code.move

rahxephon89 · 2023-05-12T23:57:19Z

aptos-move/framework/aptos-framework/sources/voting.move

@@ -364,6 +364,11 @@ module aptos_framework::voting {
        proposal_id: u64,
    ) acquires VotingForum {
        let proposal_state = get_proposal_state<ProposalType>(voting_forum_address, proposal_id);
+


Using assume with ghost state is not an ideal way to specify aborts_if condition. Could you try to write a spec fun version of get_proposal_state instead? If it is difficult to do so, we can visit this aborts_if condition later.

rahxephon89 · 2023-05-12T23:57:34Z

aptos-move/framework/aptos-framework/sources/voting.move

        let resolvable_time = to_u64(*simple_map::borrow(&proposal.metadata, &utf8(RESOLVABLE_TIME_METADATA_KEY)));
+


Same as above

UIZorrot

We have fixed it on the newest commit

junkil-park · 2023-05-25T05:18:35Z

aptos-move/framework/aptos-framework/sources/voting.spec.move

        use aptos_framework::chain_status;
-
+        


remove the trailing whitespaces.

junkil-park · 2023-05-25T05:19:07Z

aptos-move/framework/aptos-framework/sources/voting.spec.move

        requires chain_status::is_operating(); // Ensures existence of Timestamp
        // Addition of yes_votes and no_votes might overflow.
        pragma addition_overflow_unchecked;
+
        include AbortsIfNotContainProposalID<ProposalType>;
        // Any way to specify the result?


what does this mean?

github-actions · 2023-06-14T12:03:05Z

✅ Forge suite `compat` success on `testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b` ==> `9f2f8c4c30105cd09293c8f52de9c79585f43851`

Compatibility test results for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 9f2f8c4c30105cd09293c8f52de9c79585f43851 (PR)
1. Check liveness of validators at old version: testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b
compatibility::simple-validator-upgrade::liveness-check : committed: 8811 txn/s, latency: 3756 ms, (p50: 3700 ms, p90: 5100 ms, p99: 6000 ms), latency samples: 299600
2. Upgrading first Validator to new version: 9f2f8c4c30105cd09293c8f52de9c79585f43851
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 4060 txn/s, latency: 7645 ms, (p50: 8300 ms, p90: 10500 ms, p99: 11000 ms), latency samples: 158340
3. Upgrading rest of first batch to new version: 9f2f8c4c30105cd09293c8f52de9c79585f43851
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 4768 txn/s, latency: 6725 ms, (p50: 7600 ms, p90: 8300 ms, p99: 8800 ms), latency samples: 176440
4. upgrading second batch to new version: 9f2f8c4c30105cd09293c8f52de9c79585f43851
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 6913 txn/s, latency: 4771 ms, (p50: 4700 ms, p90: 6600 ms, p99: 7700 ms), latency samples: 241960
5. check swarm health
Compatibility test for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 9f2f8c4c30105cd09293c8f52de9c79585f43851 passed
Test Ok

Grafana dashboard
Humio Logs
Test runner output
Test run is land-blocking

github-actions · 2023-06-14T12:04:02Z

✅ Forge suite `land_blocking` success on `9f2f8c4c30105cd09293c8f52de9c79585f43851`

performance benchmark : committed: 5616 txn/s, latency: 7054 ms, (p50: 5400 ms, p90: 11500 ms, p99: 27100 ms), latency samples: 2398274
Max round gap was 1 [limit 4] at version 260854. Max no progress secs was 3.841776 [limit 10] at version 2637844.
Test Ok

Grafana dashboard
Humio Logs
Test runner output
Test run is land-blocking

github-actions · 2023-06-14T12:08:10Z

✅ Forge suite `framework_upgrade` success on `aptos-node-v1.3.0_3fc3d42b6cfe27460004f9a0326451bcda840a60` ==> `9f2f8c4c30105cd09293c8f52de9c79585f43851`

Compatibility test results for aptos-node-v1.3.0_3fc3d42b6cfe27460004f9a0326451bcda840a60 ==> 9f2f8c4c30105cd09293c8f52de9c79585f43851 (PR)
Upgrade the nodes to version: 9f2f8c4c30105cd09293c8f52de9c79585f43851
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 4555 txn/s, latency: 7176 ms, (p50: 7800 ms, p90: 9700 ms, p99: 12700 ms), latency samples: 168560
5. check swarm health
Compatibility test for aptos-node-v1.3.0_3fc3d42b6cfe27460004f9a0326451bcda840a60 ==> 9f2f8c4c30105cd09293c8f52de9c79585f43851 passed
Test Ok

Grafana dashboard
Humio Logs
Test runner output
Test run is land-blocking

* [spec] update specs of voting, transaction_fee, code * [spec] add account and voting module * run linter * [spec] Fix timeout of smart_vector.move * [spec] Update docs of smart_vector --------- Co-authored-by: zorrot <ui_zorrot@163.com>

[spec] update specs of voting, transaction_fee, code

db29f5f

xudon9 requested review from saharct, junkil-park, davidiw, movekevin and wrwg as code owners May 12, 2023 08:35

rahxephon89 requested changes May 12, 2023

View reviewed changes

UIZorrot and others added 3 commits May 17, 2023 21:55

[spec] add account and voting module

2f36f2c

Merge branch 'aptos-labs:main' into spec-update

480857b

Merge branch 'main' into spec-update

50039a1

UIZorrot reviewed May 18, 2023

View reviewed changes

This comment was marked as duplicate.

Sign in to view

UIZorrot added 3 commits May 24, 2023 14:00

Merge branch 'aptos-labs:main' into spec-update

396c5fe

run linter

508ee75

Merge branch 'aptos-labs:main' into spec-update

44deb43

junkil-park reviewed May 25, 2023

View reviewed changes

junkil-park approved these changes May 25, 2023

View reviewed changes

rahxephon89 self-requested a review May 27, 2023 07:42

rahxephon89 approved these changes May 27, 2023

View reviewed changes

rahxephon89 enabled auto-merge (squash) May 27, 2023 07:42

This comment has been minimized.

Sign in to view

[spec] sync with main and remove trailing whitespaces

bc69eb6

auto-merge was automatically disabled June 12, 2023 06:31
Head branch was pushed to by a user without write access

rahxephon89 enabled auto-merge (squash) June 12, 2023 06:37

Merge branch 'aptos-labs:main' into spec-update

3d21496

junkil-park added move-prover CICD:run-prover-test and removed move-prover labels Jun 14, 2023

junkil-park disabled auto-merge June 14, 2023 09:14

junkil-park enabled auto-merge (squash) June 14, 2023 09:14

junkil-park disabled auto-merge June 14, 2023 09:24

junkil-park added move-prover and removed move-prover CICD:run-prover-test labels Jun 14, 2023

junkil-park enabled auto-merge (squash) June 14, 2023 09:24

Merge branch 'main' into spec-update

9f2f8c4

junkil-park disabled auto-merge June 14, 2023 11:28

junkil-park added move-prover CICD:run-prover-test and removed move-prover labels Jun 14, 2023

junkil-park enabled auto-merge (squash) June 14, 2023 11:29

This comment has been minimized.

Sign in to view

junkil-park merged commit 22d6280 into aptos-labs:main Jun 14, 2023

qdrs mentioned this pull request Jun 20, 2023

dearb patching otter-sec/aptos-core#1

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Spec] update specs of voting, transaction_fee, code #8172

[Spec] update specs of voting, transaction_fee, code #8172

xudon9 commented May 12, 2023

rahxephon89 May 12, 2023

rahxephon89 May 12, 2023

UIZorrot left a comment

This comment was marked as duplicate.

junkil-park May 25, 2023

junkil-park May 25, 2023

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

github-actions bot commented Jun 14, 2023

github-actions bot commented Jun 14, 2023

github-actions bot commented Jun 14, 2023

		let resolvable_time = to_u64(*simple_map::borrow(&proposal.metadata, &utf8(RESOLVABLE_TIME_METADATA_KEY)));

[Spec] update specs of voting, transaction_fee, code #8172

[Spec] update specs of voting, transaction_fee, code #8172

Conversation

xudon9 commented May 12, 2023

Description

Test Plan

rahxephon89 May 12, 2023

Choose a reason for hiding this comment

rahxephon89 May 12, 2023

Choose a reason for hiding this comment

UIZorrot left a comment

Choose a reason for hiding this comment

This comment was marked as duplicate.

junkil-park May 25, 2023

Choose a reason for hiding this comment

junkil-park May 25, 2023

Choose a reason for hiding this comment

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

github-actions bot commented Jun 14, 2023

✅ Forge suite compat success on testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 9f2f8c4c30105cd09293c8f52de9c79585f43851

github-actions bot commented Jun 14, 2023

✅ Forge suite land_blocking success on 9f2f8c4c30105cd09293c8f52de9c79585f43851

github-actions bot commented Jun 14, 2023

✅ Forge suite framework_upgrade success on aptos-node-v1.3.0_3fc3d42b6cfe27460004f9a0326451bcda840a60 ==> 9f2f8c4c30105cd09293c8f52de9c79585f43851

✅ Forge suite `compat` success on `testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b` ==> `9f2f8c4c30105cd09293c8f52de9c79585f43851`

✅ Forge suite `land_blocking` success on `9f2f8c4c30105cd09293c8f52de9c79585f43851`

✅ Forge suite `framework_upgrade` success on `aptos-node-v1.3.0_3fc3d42b6cfe27460004f9a0326451bcda840a60` ==> `9f2f8c4c30105cd09293c8f52de9c79585f43851`