[aptos-framework] Add specs for account.move and coin.move

[qpb8023]

Description

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

Added specs for module account & coin.

Test Plan

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

---

This change is 

[wrwg]

This looks like a good start, but the specifications are incomplete. State updates are not described. If we want to keep state changes unspecified for now, we should add a TODO. However, really the hard work here is to described the state updates ;-)

• add modifies global<T>(addr) clause for each modified state.
• specify the post state of the modified slot

This should happen at least to all public functions (eventually).

[junkil-park]

Thank you for your contribution to the Aptos Framework spec! My few general comments would be:

• if there are complex specs, please also add some comments (texts) to them for the readability sake
• please make sure the specs look fine in the generated document. The command to generate the document is:

$ aptos move document --include-impl --include-specs --collapsed-sections

$ cargo test -p framework

[wrwg]

Thank you for your contribution to the Aptos Framework spec! My few general comments would be:

• if there are complex specs, please also add some comments (texts) to them for the readability sake
• please make sure the specs look fine in the generated document. The command to run the document generator is:

$ aptos move document --include-impl --include-specs --collapsed-sections

The documentation generator is run automatically! Don't run it manually please, because it won't have the right options. Documentation is automatically updated if you run cargo test -p framework and placed in <framework>/doc directory.

[qpb8023]

Thank you for your contribution to the Aptos Framework spec! My few general comments would be:

• if there are complex specs, please also add some comments (texts) to them for the readability sake
• please make sure the specs look fine in the generated document. The command to run the document generator is:

$ aptos move document --include-impl --include-specs --collapsed-sections

The documentation generator is run automatically! Don't run it manually please, because it won't have the right options. Documentation is automatically updated if you run cargo test -p framework and placed in <framework>/doc directory.

Just to ensure: Do I need to add the changes in the doc directory to the commit content?

[junkil-park]

Just to ensure: Do I need to add the changes in the doc directory to the commit content?

Yes, the source files and the generated doc need to be synced. So, If you update .move or .spec.move files, please update the doc by cargo test -p framework as well.

[junkil-park]

Loos good to me. Thank you again for the contribution!

[junkil-park]

It seems that there is a lint test failure in CI. It complains about trailing whitespaces. Could you fix it?
Also, The new Move commit update (#5380) just landed which includes an update on the document generator. Could you rebase and regenerate the document one more time?

[qpb8023]

Finished

[github-actions]

✅ Forge suite land_blocking success on fa42151098095624c24967eff7c632b259fed9b7

performance benchmark with full nodes : 6853 TPS, 5710 ms latency, 20600 ms p99 latency,(!) expired 4032 out of 2930500 txns
Test Ok

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

[github-actions]

✅ Forge suite compat success on 2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> fa42151098095624c24967eff7c632b259fed9b7

Compatibility test results for 2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> fa42151098095624c24967eff7c632b259fed9b7 (PR)
1. Check liveness of validators at old version: 2d8b1b57553d869190f61df1aaf7f31a8fc19a7b
compatibility::simple-validator-upgrade::liveness-check : 7603 TPS, 5098 ms latency, 7400 ms p99 latency,no expired txns
2. Upgrading first Validator to new version: fa42151098095624c24967eff7c632b259fed9b7
compatibility::simple-validator-upgrade::single-validator-upgrade : 4554 TPS, 9028 ms latency, 12000 ms p99 latency,no expired txns
3. Upgrading rest of first batch to new version: fa42151098095624c24967eff7c632b259fed9b7
compatibility::simple-validator-upgrade::half-validator-upgrade : 4566 TPS, 9042 ms latency, 11800 ms p99 latency,no expired txns
4. upgrading second batch to new version: fa42151098095624c24967eff7c632b259fed9b7
compatibility::simple-validator-upgrade::rest-validator-upgrade : 6975 TPS, 5685 ms latency, 9100 ms p99 latency,no expired txns
5. check swarm health
Compatibility test for 2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> fa42151098095624c24967eff7c632b259fed9b7 passed
Test Ok

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