[Spec] Added specs for module aggregator & aggregator_factory & optional_aggregator & staking_config & version & event & guid & timestamp #5653

0xOutOfGas · 2022-11-20T12:48:07Z

Description

This is a part of spec work for Aptos Framework from MoveBit, we updated below files/modules in this PR:

aggregator/aggregator.spec.move
aggregator/aggregator_factory.spec.move
aggregator/optional_aggregator.spec.move
configs/staking_config.spec.move
configs/version.spec.move
event.spec.move
guid.spec.move
timestamp.spec.move

Test Plan

aptos move prove --package-dir ./aptos-framework

…version.

junkil-park · 2022-11-21T19:54:32Z

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

@@ -6,20 +6,24 @@ spec aptos_framework::aggregator {
    spec add {
        // TODO: temporary mockup.
        pragma opaque;
+        aborts_if false;


This native function can actually abort. Please refer to the comment in aggregator.move. (cc: @georgemitenkov )

Remove aborts if false does not affect the validation.

Remove aborts if false does not affect the validation.

I didn't get this. Could you elaborate what you mean?

According the comment in aggregator.move, this function "Aborts on overflowing the limit."

junkil-park · 2022-11-21T19:54:54Z

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

    }

    spec sub {
        // TODO: temporary mockup.
        pragma opaque;
+        aborts_if false;


Same as the above. This native function can actually abort. Please refer to the comment in aggregator.move.

Already updated.

What is updated?

According to the comment in the code, this function "Aborts on going below zero.".

The specs of add and sub have been redone.

junkil-park · 2022-11-21T19:55:29Z

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

    }

    spec read {
        // TODO: temporary mockup.
        pragma opaque;
+        aborts_if false;


@georgemitenkov , can there be any cases where read and destroy may potentially abort?

destroy never aborts, and so should read. Say you have an aggregator with an overflow limit of 10. And some transaction does this:

a = Aggregator(limit=10) // actual storage value is 5 already, but this transaction doesn't know a.add(7) a.read() // aborts the transaction since we read 5+7 > 10

So technically read aborts because it checks if previous deltas made sense. At the same time,

a = Aggregator(limit=10) // actual storage value is 5 already, but this transaction doesn't know a.add(7)

equally aborts because at the end of the transaction we check if it should have been aborted (e.g. in sequential execution this means read the value, in parallel execution it is a bit more convoluted).

So, in my opinion, this shows that read never aborts, but rather catches an abort in add/sub. Not sure how you would qualify this for the prover?

Looking at native implementation, we can abort if aggregator value is not found in storage, do we count this is as well? Technically should never happen...

@georgemitenkov @junkil-park read never aborts. But destroy indeed abort.

┌─ aptos-framework/sources/aggregator/optional_aggregator.move:105:9 │ 105 │ aggregator::destroy(aggregator); │ ------------------------------- abort happened here with code 0x0 │ = at aptos-framework/sources/aggregator/optional_aggregator.move:100: switch_to_integer_and_zero_out = optional_aggregator = = &optional_aggregator.OptionalAggregator{ = aggregator = = option.Option{ = vec = = vector{ = aggregator.Aggregator{ = handle = 0x6784, = key = 0x18be, = limit = 18467u128}}}, = integer = option.Option{vec = vector{}}} = at aptos-framework/sources/aggregator/optional_aggregator.move:103: destroy_optional_integer = at <internal>:1 = at aptos-framework/sources/aggregator/optional_aggregator.move:103: destroy_optional_integer = optional_aggregator = = &optional_aggregator.OptionalAggregator{ = aggregator = option.Option{vec = vector{}}, = integer = option.Option{vec = vector{}}} = aggregator = = aggregator.Aggregator{ = handle = 0x6784, = key = 0x18be, = limit = 18467u128} = at aptos-framework/sources/aggregator/optional_aggregator.move:104: destroy_optional_integer = at aptos-framework/sources/aggregator/aggregator.move:80: limit = aggregator = = aggregator.Aggregator{ = handle = 0x6784, = key = 0x18be, = limit = 18467u128} = at aptos-framework/sources/aggregator/aggregator.move:81: limit = result = 18467u128 = at aptos-framework/sources/aggregator/aggregator.move:82: limit = limit = 18467u128 = at aptos-framework/sources/aggregator/optional_aggregator.move:105: switch_to_integer_and_zero_out = at <internal>:1 = at aptos-framework/sources/aggregator/optional_aggregator.move:105: switch_to_integer_and_zero_out = ABORTED { "Error": "Move Prover failed: exiting with verification errors" }

@qpb8023 I am a bit confused with the error log and the inputs that lead to abort -- why there is a line ...optional_aggregator.move:103: destroy_optional_integer?

Is it possible to reproduce an error? This abort is not expected.

'not implemented: Not yet supported constant vector type: Vector(Primitive(U64))'

This seems a separate issue. Do you still have the same problem when using the latest move-cli?

@junkil-park The code you gave will still abort. By using the latest move cli.

@rahxephon89, we support the constant vector type like Vector(Primitive(U64)), right?

Just to unblock this PR from the constant vector issue, can you use this spec and proceed?

spec destroy(aggregator: Aggregator) { pragma opaque; // TODO: this aborts_if condition is a temporary mockup, which needs to be refined. aborts_if false; }

@junkil-park I have solved this.

junkil-park · 2022-11-30T20:04:44Z

aptos-move/framework/aptos-framework/sources/configs/version.spec.move

+        aborts_if exists<SetVersionCapability>(@aptos_framework);
+    }
+
+    /// Only for test


Test functions don't need to be specified. Could you remove this spec?

we add spec for initialize_for_test and set verify = false, because we opened aborts_if_is_strict in spec module, if we remove spec for initialize_for_test, prover will not let it pass.

spec aptos_framework::version { spec module { pragma verify = true; pragma aborts_if_is_strict; }

Two solutions from us:
1 keep the spec and add a comment like "no need to add spec for test functions, just because the module turns on aborts_if_is_strict".(which we preferred)
2 remove the spec, and turn aborts_if_is_strict to false.

OK. The current way looks fine.

junkil-park

I left a few question and comment. Other than that, it looks good to me.

junkil-park · 2022-12-08T17:36:22Z

There is a CI check failure: https://github.com/aptos-labs/aptos-core/actions/runs/3645474643/jobs/6155656855#step:6:864. I am not sure why.

Could you try to rebase it and regenerate the doc (cargo test -p framework) if you didn't recently? Let's see if that resolves the error.

github-actions · 2022-12-08T18:26:04Z

✅ Forge suite `land_blocking` success on `3756a3b65315371cd0ab54274bb939a0267313ea`

performance benchmark with full nodes : 6718 TPS, 5907 ms latency, 10800 ms p99 latency,(!) expired 80 out of 2869080 txns
Test Ok

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

github-actions · 2022-12-08T18:29:36Z

✅ Forge suite `compat` success on `testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b` ==> `3756a3b65315371cd0ab54274bb939a0267313ea`

Compatibility test results for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 3756a3b65315371cd0ab54274bb939a0267313ea (PR)
1. Check liveness of validators at old version: testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b
compatibility::simple-validator-upgrade::liveness-check : 7172 TPS, 5418 ms latency, 7700 ms p99 latency,no expired txns
2. Upgrading first Validator to new version: 3756a3b65315371cd0ab54274bb939a0267313ea
compatibility::simple-validator-upgrade::single-validator-upgrade : 4855 TPS, 8777 ms latency, 11800 ms p99 latency,no expired txns
3. Upgrading rest of first batch to new version: 3756a3b65315371cd0ab54274bb939a0267313ea
compatibility::simple-validator-upgrade::half-validator-upgrade : 4692 TPS, 8628 ms latency, 11200 ms p99 latency,no expired txns
4. upgrading second batch to new version: 3756a3b65315371cd0ab54274bb939a0267313ea
compatibility::simple-validator-upgrade::rest-validator-upgrade : 6406 TPS, 6114 ms latency, 10700 ms p99 latency,no expired txns
5. check swarm health
Compatibility test for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 3756a3b65315371cd0ab54274bb939a0267313ea passed
Test Ok

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

…nal_aggregator & staking_config & version & event & guid & timestamp (aptos-labs#5653) * add aggregator_factory & optional_aggregator.move spec * Updated specs for module event & guid & timestamp & staking_config & version. * Documentation updated. * add ensures for sub_integer & add_integer function * replace tab to spaces * remove add & sub aborts_if false * update aggregator.spec.move * remove version.move test fun spec * make fun initialize_for_test verify false * [spec] added comments for test functions * Updated aggregator.move spec Co-authored-by: tiutiutiu <qiu971009@gmail.com> Co-authored-by: yoyoping <zhangping_ymd@outlook.com>

qpb8023 and others added 8 commits November 18, 2022 16:30

add aggregator_factory & optional_aggregator.move spec

8766550

Merge branch 'main' of https://github.com/movebit/aptos-core into main

8f77159

Updated specs for module event & guid & timestamp & staking_config & …

0e17761

…version.

Documentation updated.

a4849de

add ensures for sub_integer & add_integer function

9366fc3

Merge branch 'main' of https://github.com/movebit/aptos-core into main

a4b96c8

replace tab to spaces

b85d0f8

Merge branch 'aptos-labs:main' into main

23886e6

0xOutOfGas requested review from junkil-park, davidiw, movekevin and wrwg as code owners November 20, 2022 12:48

junkil-park reviewed Nov 21, 2022

View reviewed changes

qpb8023 added 5 commits November 23, 2022 14:41

Merge branch 'aptos-labs:main' into main

5ce45e7

remove add & sub aborts_if false

97dcdbd

Merge branch 'main' of https://github.com/movebit/aptos-core into main

bc9d422

update aggregator.spec.move

cca468d

Merge branch 'aptos-labs:main' into main

855fbd3

junkil-park reviewed Nov 30, 2022

View reviewed changes

junkil-park approved these changes Nov 30, 2022

View reviewed changes

Merge branch 'aptos-labs:main' into main

952b4d5

qpb8023 force-pushed the main branch from 3aa6786 to 952b4d5 Compare December 1, 2022 01:34

qpb8023 and others added 6 commits December 1, 2022 09:51

remove version.move test fun spec

3766571

make fun initialize_for_test verify false

408c6c6

[spec] added comments for test functions

096fff3

Merge branch 'aptos-labs:main' into main

62a04a5

Merge branch 'aptos-labs:main' into main

5a49760

Merge branch 'aptos-labs:main' into main

3aa3ebd

qpb8023 added 3 commits December 8, 2022 10:00

Updated aggregator.move spec

e39ab51

Merge branch 'main' of https://github.com/movebit/aptos-core into main

09d928a

Merge branch 'aptos-labs:main' into main

3756a3b

rahxephon89 self-requested a review December 8, 2022 17:38

rahxephon89 approved these changes Dec 8, 2022

View reviewed changes

junkil-park enabled auto-merge (squash) December 8, 2022 17:39

This comment has been minimized.

Sign in to view

junkil-park merged commit cc19be9 into aptos-labs:main Dec 8, 2022

JoshLind mentioned this pull request Dec 8, 2022

[Move Documentation] Update broken move documentation. #5829

Merged

Markuze mentioned this pull request Dec 26, 2022

markuze/aptos perf #5998

Closed

Markuze mentioned this pull request Jan 3, 2023

[Network] Adding AptosPerf Client #6054

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Spec] Added specs for module aggregator & aggregator_factory & optional_aggregator & staking_config & version & event & guid & timestamp #5653

[Spec] Added specs for module aggregator & aggregator_factory & optional_aggregator & staking_config & version & event & guid & timestamp #5653

0xOutOfGas commented Nov 20, 2022

junkil-park Nov 21, 2022

qpb8023 Nov 23, 2022

junkil-park Nov 28, 2022 •

edited

Loading

junkil-park Nov 21, 2022

qpb8023 Nov 23, 2022

junkil-park Nov 28, 2022

qpb8023 Nov 29, 2022

junkil-park Nov 21, 2022

georgemitenkov Nov 23, 2022

georgemitenkov Nov 23, 2022

qpb8023 Nov 29, 2022

georgemitenkov Nov 29, 2022

junkil-park Dec 6, 2022

qpb8023 Dec 7, 2022

junkil-park Dec 7, 2022

junkil-park Dec 8, 2022

qpb8023 Dec 8, 2022

junkil-park Nov 30, 2022

qpb8023 Dec 1, 2022

0xOutOfGas Dec 1, 2022

junkil-park Dec 5, 2022

junkil-park left a comment

junkil-park commented Dec 8, 2022

This comment has been minimized.

This comment has been minimized.

github-actions bot commented Dec 8, 2022

github-actions bot commented Dec 8, 2022

[Spec] Added specs for module aggregator & aggregator_factory & optional_aggregator & staking_config & version & event & guid & timestamp #5653

[Spec] Added specs for module aggregator & aggregator_factory & optional_aggregator & staking_config & version & event & guid & timestamp #5653

Conversation

0xOutOfGas commented Nov 20, 2022

Description

Test Plan

Choose a reason for hiding this comment

Choose a reason for hiding this comment

junkil-park Nov 28, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

junkil-park left a comment

Choose a reason for hiding this comment

junkil-park commented Dec 8, 2022

This comment has been minimized.

This comment has been minimized.

github-actions bot commented Dec 8, 2022

✅ Forge suite land_blocking success on 3756a3b65315371cd0ab54274bb939a0267313ea

github-actions bot commented Dec 8, 2022

✅ Forge suite compat success on testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 3756a3b65315371cd0ab54274bb939a0267313ea

junkil-park Nov 28, 2022 •

edited

Loading

✅ Forge suite `land_blocking` success on `3756a3b65315371cd0ab54274bb939a0267313ea`

✅ Forge suite `compat` success on `testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b` ==> `3756a3b65315371cd0ab54274bb939a0267313ea`