[Specs] ordered_map remove_or_none

[JakeSilverman]

Description

Adds specs for new ordered_map function remove_or_none

How Has This Been Tested?

New test added

Key Areas to Review

It is a bit suspicious why prover needs

        let (_key, _value) = map.borrow_back();
        spec{
            assert keys[0] == 1;
            assert keys[1] == 2;
            assert spec_contains_key(map, 1);
            assert spec_contains_key(map, 2);
        };

this seems true for other tests too. Don't fully understand why this hint is necessary

Type of Change

• New feature
• Bug fix
• Breaking change
• Performance improvement
• Refactoring
• Dependency update
• Documentation update
• Tests

Which Components or Systems Does This Change Impact?

• Validator Node
• Full Node (API, Indexer, etc.)
• Move/Aptos Virtual Machine
• Aptos Framework
• Aptos CLI/SDK
• Developer Infrastructure
• Move Compiler
• Other (specify): move prover

Checklist

• I have read and followed the CONTRIBUTING doc
• I have performed a self-review of my own code
• I have commented my code, particularly in hard-to-understand areas
• I identified and added all stakeholders and component owners affected by this change as reviewers
• I tested both happy and unhappy path of the functionality
• I have made corresponding changes to the documentation

[JakeSilverman]

• [Specs] ordered_map remove_or_none #17829 👈 (View in Graphite)
• expose iterators and add utilities to OrderedMap/BigOrderedMap #17441 : 1 other dependent PR (#17821 )
• main

This stack of pull requests is managed by Graphite. Learn more about stacking.

[wrwg]

I think this need rebase.

[JakeSilverman]

I think this need rebase.

Sorry for the messy state. I think this got messed up after base PR landed by me using graphite on top of a PR that wasn't using graphite.

[github-actions]

✅ Forge suite compat success on e4635b4614ac9cd5e6bcfbfa37fc3d21d28c71b9 ==> dc5b40a36021d6d6261f88e7d905a8ff6ff0e240

Compatibility test results for e4635b4614ac9cd5e6bcfbfa37fc3d21d28c71b9 ==> dc5b40a36021d6d6261f88e7d905a8ff6ff0e240 (PR)
1. Check liveness of validators at old version: e4635b4614ac9cd5e6bcfbfa37fc3d21d28c71b9
compatibility::simple-validator-upgrade::liveness-check : committed: 14278.65 txn/s, latency: 2425.80 ms, (p50: 2500 ms, p70: 2700, p90: 2800 ms, p99: 3900 ms), latency samples: 464800
2. Upgrading first Validator to new version: dc5b40a36021d6d6261f88e7d905a8ff6ff0e240
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 5233.70 txn/s, latency: 6592.35 ms, (p50: 7300 ms, p70: 7400, p90: 7400 ms, p99: 7500 ms), latency samples: 181740
3. Upgrading rest of first batch to new version: dc5b40a36021d6d6261f88e7d905a8ff6ff0e240
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 5318.10 txn/s, latency: 6488.81 ms, (p50: 7200 ms, p70: 7300, p90: 7300 ms, p99: 7400 ms), latency samples: 183000
4. upgrading second batch to new version: dc5b40a36021d6d6261f88e7d905a8ff6ff0e240
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 8058.87 txn/s, latency: 4254.22 ms, (p50: 4600 ms, p70: 4700, p90: 4800 ms, p99: 4900 ms), latency samples: 268160
5. check swarm health
Compatibility test for e4635b4614ac9cd5e6bcfbfa37fc3d21d28c71b9 ==> dc5b40a36021d6d6261f88e7d905a8ff6ff0e240 passed
Test Ok

• Grafana dashboard
• Humio Logs
• Axiom Logs
• Validator CPU Profile
• Fullnode CPU Profile
• Test runner output
• Test run is land-blocking

[github-actions]

✅ Forge suite realistic_env_max_load success on dc5b40a36021d6d6261f88e7d905a8ff6ff0e240

two traffics test: inner traffic : committed: 14939.73 txn/s, submitted: 14939.78 txn/s, expired: 0.05 txn/s, latency: 2523.98 ms, (p50: 2400 ms, p70: 2400, p90: 2700 ms, p99: 3600 ms), latency samples: 5680440
two traffics test : committed: 99.99 txn/s, latency: 1260.06 ms, (p50: 1200 ms, p70: 1400, p90: 1600 ms, p99: 3800 ms), latency samples: 1660
Latency breakdown for phase 0: ["MempoolToBlockCreation: max: 1.989, avg: 1.517", "ConsensusProposalToOrdered: max: 0.168, avg: 0.164", "ConsensusOrderedToCommit: max: 0.500, avg: 0.393", "ConsensusProposalToCommit: max: 0.661, avg: 0.557"]
Max non-epoch-change gap was: 2 rounds at version 47649 (avg 0.00) [limit 4], 2.21s no progress at version 47649 (avg 0.07s) [limit 15].
Max epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 0.64s no progress at version 2255890 (avg 0.64s) [limit 16].
Test Ok

• Grafana dashboard
• Humio Logs
• Axiom Logs
• Validator CPU Profile
• Fullnode CPU Profile
• Test runner output
• Test run is land-blocking

[github-actions]

✅ Forge suite framework_upgrade success on e4635b4614ac9cd5e6bcfbfa37fc3d21d28c71b9 ==> dc5b40a36021d6d6261f88e7d905a8ff6ff0e240

Compatibility test results for e4635b4614ac9cd5e6bcfbfa37fc3d21d28c71b9 ==> dc5b40a36021d6d6261f88e7d905a8ff6ff0e240 (PR)
Upgrade the nodes to version: dc5b40a36021d6d6261f88e7d905a8ff6ff0e240
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1986.41 txn/s, submitted: 1994.79 txn/s, failed submission: 8.38 txn/s, expired: 8.38 txn/s, latency: 1426.84 ms, (p50: 1500 ms, p70: 1500, p90: 1800 ms, p99: 2200 ms), latency samples: 180140
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 2081.97 txn/s, submitted: 2088.57 txn/s, failed submission: 6.60 txn/s, expired: 6.60 txn/s, latency: 1410.29 ms, (p50: 1500 ms, p70: 1500, p90: 1800 ms, p99: 2100 ms), latency samples: 189404
5. check swarm health
Compatibility test for e4635b4614ac9cd5e6bcfbfa37fc3d21d28c71b9 ==> dc5b40a36021d6d6261f88e7d905a8ff6ff0e240 passed
Upgrade the remaining nodes to version: dc5b40a36021d6d6261f88e7d905a8ff6ff0e240
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 2087.11 txn/s, submitted: 2094.79 txn/s, failed submission: 7.69 txn/s, expired: 7.69 txn/s, latency: 1391.61 ms, (p50: 1500 ms, p70: 1500, p90: 1800 ms, p99: 2100 ms), latency samples: 190062
Test Ok

• Grafana dashboard
• Humio Logs
• Axiom Logs
• Validator CPU Profile
• Fullnode CPU Profile
• Test runner output
• Test run is land-blocking