[Spec] Added spec of code, resource_account & staking_proxy module

[xudon9]

Description

This is a part of spec work for Aptos Framework from MoveBit. This PR added specs for following modules:

• code
• resource_account
• staking_proxy

Test Plan

Using command aptos prove -f FILE for each files

[junkil-park]

TODOs should be taken care of in the following PRs.

[github-actions]

✅ Forge suite land_blocking success on affd0eaac5285aebfa7ebd3513476ffc2a9352a1

performance benchmark with full nodes : 6379 TPS, 6214 ms latency, 8100 ms p99 latency,no expired txns
Test Ok

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

[github-actions]

✅ Forge suite compat success on testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> affd0eaac5285aebfa7ebd3513476ffc2a9352a1

Compatibility test results for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> affd0eaac5285aebfa7ebd3513476ffc2a9352a1 (PR)
1. Check liveness of validators at old version: testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b
compatibility::simple-validator-upgrade::liveness-check : 7909 TPS, 4922 ms latency, 6700 ms p99 latency,no expired txns
2. Upgrading first Validator to new version: affd0eaac5285aebfa7ebd3513476ffc2a9352a1
compatibility::simple-validator-upgrade::single-validator-upgrade : 4815 TPS, 8394 ms latency, 10800 ms p99 latency,no expired txns
3. Upgrading rest of first batch to new version: affd0eaac5285aebfa7ebd3513476ffc2a9352a1
compatibility::simple-validator-upgrade::half-validator-upgrade : 4776 TPS, 8380 ms latency, 10300 ms p99 latency,no expired txns
4. upgrading second batch to new version: affd0eaac5285aebfa7ebd3513476ffc2a9352a1
compatibility::simple-validator-upgrade::rest-validator-upgrade : 7177 TPS, 5379 ms latency, 8500 ms p99 latency,no expired txns
5. check swarm health
Compatibility test for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> affd0eaac5285aebfa7ebd3513476ffc2a9352a1 passed
Test Ok

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

[github-actions]

✅ Forge suite framework_upgrade success on cb4ba0a57c998c60cbab65af31a64875d2588ca5 ==> affd0eaac5285aebfa7ebd3513476ffc2a9352a1

Compatibility test results for cb4ba0a57c998c60cbab65af31a64875d2588ca5 ==> affd0eaac5285aebfa7ebd3513476ffc2a9352a1 (PR)
Upgrade the nodes to version: affd0eaac5285aebfa7ebd3513476ffc2a9352a1
framework_upgrade::framework-upgrade::full-framework-upgrade : 6895 TPS, 5551 ms latency, 9400 ms p99 latency,no expired txns
5. check swarm health
Compatibility test for cb4ba0a57c998c60cbab65af31a64875d2588ca5 ==> affd0eaac5285aebfa7ebd3513476ffc2a9352a1 passed
Test Ok

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