[Spec] Added more specs to the coin and account modules

[junkil-park]

Description

• this PR completes many TODOs in the specs of coin and account modules.
• added more specs and helper spec functions to ed25519 and multi_ed25519 modules
• enhanced the spec of type_info module
  • TODO: the spec of chain_id() is blocked by the bit operation support.

Test Plan

move prove

[meng-xu-cs]

Leaving the ed25519 spec to crypto experts, the rest looks good to me.

[alinush]

Can we make the specs more modular? (see comments)

[github-actions]

✅ Forge suite compat success on testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 140494c7414ac019d92ca213b8a4960db6933c19

Compatibility test results for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 140494c7414ac019d92ca213b8a4960db6933c19 (PR)
1. Check liveness of validators at old version: testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b
compatibility::simple-validator-upgrade::liveness-check : 7355 TPS, 5491 ms latency, 7700 ms p99 latency,no expired txns
2. Upgrading first Validator to new version: 140494c7414ac019d92ca213b8a4960db6933c19
compatibility::simple-validator-upgrade::single-validator-upgrade : 4532 TPS, 8759 ms latency, 11500 ms p99 latency,no expired txns
3. Upgrading rest of first batch to new version: 140494c7414ac019d92ca213b8a4960db6933c19
compatibility::simple-validator-upgrade::half-validator-upgrade : 5042 TPS, 8222 ms latency, 10900 ms p99 latency,no expired txns
4. upgrading second batch to new version: 140494c7414ac019d92ca213b8a4960db6933c19
compatibility::simple-validator-upgrade::rest-validator-upgrade : 6453 TPS, 5883 ms latency, 10000 ms p99 latency,no expired txns
5. check swarm health
Compatibility test for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 140494c7414ac019d92ca213b8a4960db6933c19 passed
Test Ok

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

[github-actions]

✅ Forge suite land_blocking success on 140494c7414ac019d92ca213b8a4960db6933c19

performance benchmark with full nodes : 6640 TPS, 5988 ms latency, 10500 ms p99 latency,no expired txns
Test Ok

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

Alin, I've addressed your comment making the spec more modular. I will move forward and land this for now to unblock the other spec work. However, please let me know if you have a further comment on this. I will be happy to re-iterate it. Thank you so much!