[Spec] update specs of voting.move

[UIZorrot]

Description

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

Completed all specs left as TODO in voting.

Test Plan

aptos move prove -f voting.move

[rahxephon89]

Thanks! Please fix the linter error in the PR.

[junkil-park]

Could you take care of the minor comments?

[github-actions]

✅ Forge suite compat success on testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 5c7f81443fb59781b5414f300e0c6cbbad168cf0

Compatibility test results for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 5c7f81443fb59781b5414f300e0c6cbbad168cf0 (PR)
1. Check liveness of validators at old version: testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b
compatibility::simple-validator-upgrade::liveness-check : committed: 8808 txn/s, latency: 3673 ms, (p50: 3600 ms, p90: 5100 ms, p99: 5800 ms), latency samples: 308300
2. Upgrading first Validator to new version: 5c7f81443fb59781b5414f300e0c6cbbad168cf0
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 4814 txn/s, latency: 6731 ms, (p50: 7400 ms, p90: 8500 ms, p99: 8800 ms), latency samples: 182940
3. Upgrading rest of first batch to new version: 5c7f81443fb59781b5414f300e0c6cbbad168cf0
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 4893 txn/s, latency: 6408 ms, (p50: 6900 ms, p90: 7900 ms, p99: 9500 ms), latency samples: 190840
4. upgrading second batch to new version: 5c7f81443fb59781b5414f300e0c6cbbad168cf0
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 6362 txn/s, latency: 5030 ms, (p50: 4800 ms, p90: 7500 ms, p99: 8900 ms), latency samples: 229060
5. check swarm health
Compatibility test for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 5c7f81443fb59781b5414f300e0c6cbbad168cf0 passed
Test Ok

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

[github-actions]

✅ Forge suite land_blocking success on 5c7f81443fb59781b5414f300e0c6cbbad168cf0

performance benchmark : committed: 5566 txn/s, submitted: 5567 txn/s, latency: 7120 ms, (p50: 6000 ms, p90: 9300 ms, p99: 26800 ms), latency samples: 2376953
Max round gap was 2 [limit 4] at version 2151335. Max no progress secs was 4.576684 [limit 10] at version 2151335.
Test Ok

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

[github-actions]

✅ Forge suite framework_upgrade success on aptos-node-v1.3.0_3fc3d42b6cfe27460004f9a0326451bcda840a60 ==> 5c7f81443fb59781b5414f300e0c6cbbad168cf0

Compatibility test results for aptos-node-v1.3.0_3fc3d42b6cfe27460004f9a0326451bcda840a60 ==> 5c7f81443fb59781b5414f300e0c6cbbad168cf0 (PR)
Upgrade the nodes to version: 5c7f81443fb59781b5414f300e0c6cbbad168cf0
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 4862 txn/s, latency: 6839 ms, (p50: 6700 ms, p90: 9900 ms, p99: 12000 ms), latency samples: 179920
5. check swarm health
Compatibility test for aptos-node-v1.3.0_3fc3d42b6cfe27460004f9a0326451bcda840a60 ==> 5c7f81443fb59781b5414f300e0c6cbbad168cf0 passed
Test Ok

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