[Move][Spec] Fix specs and other miscs

[rahxephon89]

Description

This PR improves formal verification coverage for aptos-stdlib and move-stdlib, fixes two pre-existing spec bugs that were silently skipping verification, and fixes bugs in the Move Prover's Boogie code generation.

Spec coverage improvements

New spec files created:

• storage_slots_allocator.spec.move — specs for 9 public functions using pragma opaque + pragma aborts_if_is_partial for enum-pattern/loop paths: add, remove, borrow, borrow_mut, fill_reserved_slot, remove_and_reserve, free_reserved_slot, allocate_spare_slots, reserve_slot. Specs use enum is/.value field access syntax and table_with_length::spec_contains/spec_get.
• math_fixed.spec.move — specs for sqrt (aborts_if false, proved), pow_raw (requires x < 2^96; no ensures — recursive spec_bexp hits MBQI timeout at full-package scale), and mul_div (aborts_if z==0 + overflow); exp/log2_plus_32/ln_plus_32ln2 unspecced (non-linear iteration, unprovable abort conditions)
• math_fixed64.spec.move — specs for sqrt (aborts_if x==0, proved) and mul_div (aborts_if z==0 + overflow); exp/log2_plus_64/ln_plus_32ln2 unspecced
• math_fixed8.move — new small fixed-point module in prover unit test with pow_raw fully verified via pragma unroll = 4 + closed-form spec_pow_raw reference implementation

Significantly expanded:

• ed25519.spec.move — 6 new specs for delegating functions: public_key_validate, signature_verify_strict, signature_verify_strict_t, new_signed_message, unvalidated_public_key_to_authentication_key, validated_public_key_to_authentication_key (all pragma opaque)
• big_vector.spec.move — strong struct invariant (bucket consistency, end_index accounting); full function specs including push_back/pop_back/swap_remove/swap (pragma opaque); pop_back with bucket-level postconditions (nested forall over bucket/position); append with length ensures; remove with pragma opaque and full postconditions; index_of with pragma opaque and bucket-level no-element formulation; contains (aborts_if false). Added global initial_end_index: u64 for use in remove loop invariants. Replaced division-based bucket-count invariant (spec_table_len == ceil(end_index/bucket_size)) with arithmetic identity (bucket-length sum == end_index) + explicit trigger {spec_table_contains(buckets, i)} on the out-of-bounds invariant to avoid TypeDomain cascade.
• smart_vector.spec.move — full struct invariant; added spec_get helper (delegates to inline vec or big_vec); new/empty/empty_with_config ensures; is_empty (pragma opaque); length result ensures; borrow result ensures; borrow_mut spec; push_back (pragma opaque; pragma verify = false) with complete aborts_if enumeration (6 cases covering inline/big_vec branches, size arithmetic, and option::fill guard); pop_back result ensures; swap_remove result ensures; swap spec (pragma aborts_if_is_partial); remove (pragma opaque); singleton ensures.
• smart_table.spec.move — fixed borrow_kv, borrow_kv_mut (removed pragma verify = false, added proper aborts_if false/ensures); removed stale borrow_with_default pragma verify = false block
• pool_u64.spec.move — restructured struct invariant from ∀∃ to ∀∀ (forward containment + cardinality + no-duplicates) to fix Z3 quantifier alternation timeout; replaced eq_push_back with element-level ensures

Loop invariants added to function bodies (post-while spec { invariant ... } blocks):

• big_vector.move:append — two-phase loop: first loop tracks other.length() == other_len - i and self.length() == length(old(self)) + i; second loop same invariants with half_other_len <= i
• big_vector.move:remove — post-while invariant tracking cur_bucket_index bounds, end_index (-1 from old), bucket_size, and forall j in 0..spec_len: spec_table_contains(buckets, j); uses global initial_end_index set before the loop

Minor additions:

• capability.spec.move — aborts_if to delegate (when neither delegate cap exists nor cap held) and revoke (when delegate cap exists but cap not held)
• comparator.spec.move, hash.spec.move, simple_map.spec.move, type_info.spec.move — additional conditions

math128.spec.move improvements:

• floor_log2: upgraded aborts_if x == 0 from [abstract] (axiom) to concretely proved via three linear loop invariants in math128.move; added proved ensures result <= 127
• sqrt: added concretely proved ensures x == 0 ==> result == 0 (previously only abstract ensures for the x > 0 case)
• log2/log2_64: left with only pragma opaque — their abort condition (x == 0) and loop properties depend on the normalization step floor_log2(x) >= 32 iff x >= 1<<32, which requires evaluating spec_pow(2, 32) = 1<<32 as a concrete integer; Z3 MBQI cannot evaluate this depth of recursive unfolding within timeout

Spec bug fixes in fixed_point32 and fixed_point64

Two long-standing spec bugs that were silently skipped via pragma verify_duration_estimate (which acts as a skip guard when estimate > vc_timeout):

fixed_point32::ceil, fixed_point32::round — spec_floor had an unnecessary conditional: both branches reduce to self.value >> 32, since right-shifting discards the lower 32 bits regardless of their value. When ceil calls floor opaquely, the prover had to connect (spec_floor(self)) << 32 back to self.value - fractional, requiring Z3 to prove ((x - x%2^32) >> 32) << 32 == x - x%2^32 — non-linear modulo reasoning. Simplified spec_floor to self.value >> 32 (unconditional) and rewrote spec_ceil/spec_round in terms of floor_val with only shift and add. Both now verify in < 5s.

fixed_point64::create_from_rational — The spec used (numerator << 128) / (denominator << 64) while the body computes (numerator << 64) / denominator. Mathematically equivalent, but Z3 must prove cancellation of 2^64 in unbounded integer division — non-linear reasoning that exceeds 40s. Changed spec to (numerator << 64) / denominator to directly mirror the body. Verifies in < 5s. The original spec was written by analogy with the fixed_point32 pattern (n << 2*bits) / (d << bits) without accounting for the body's simplified computation.

Prover bug fixes

BV-mode vector length double-emission (bytecode_translator.rs): Fix double-emission of vector::length() calls when the result is assigned into a BV-typed destination. Adds a supporting bv2int(int2bv(n)) == n roundtrip axiom to the Boogie prelude and a new regression test bv_vector_length_bv_dest.move.

BV/int mode conversion for spec function calls (spec_translator.rs): Fix per-parameter bv-mode conversion in translate_spec_fun_call — insert $bv2int / $int2bv wrappers when a spec function's parameter mode differs from the call-site mode. Use get_node_type_opt to avoid panic on typeless synthetic nodes.

move-flow MCP tool fixes

• package_verify.rs + package_spec_infer.rs: Added aptos_framework::prover::configure_aptos_custom_natives call when building prover/inference options. Without this, full-package verification of any package that transitively depends on move-stdlib (which includes cmp with pragma intrinsic types) failed with Boogie compilation errors: undeclared type: $1_cmp_Ordering. The framework's ProverOptions::prove_to already called this; the move-flow MCP tools were the missing callers.
• package_verify.rs: Updated max VC timeout from 10s to 60s in the tool parameter description.

How Has This Been Tested?

• All modified specs verified with the Move Prover (Z3 + Boogie, 40s timeout)
• Full aptos-stdlib and move-stdlib prover runs pass at 40s timeout
• fixed_point32::ceil, fixed_point32::round, fixed_point64::create_from_rational now actually verify (not skipped) at 40s
• Regression test bv_vector_length_bv_dest.move passes via cargo test -p move-prover --test testsuite -- bv_vector_length_bv_dest
• move-flow full-package verification no longer fails with $1_cmp_Ordering Boogie errors

Type of Change

• Bug fix
• Aptos Framework
• Tests

Which Components or Systems Does This Change Impact?

• Move/Aptos Virtual Machine
• Aptos Framework
• Move Compiler

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

---

Note

Medium Risk
Touches prover code generation and verification configuration, which can affect correctness of formal verification results and tool stability, though runtime Move behavior is largely unchanged.

Overview
Improves Move Prover robustness and verification coverage by fixing Boogie/BV translation issues and expanding/repairing specs across aptos-stdlib and move-stdlib.

Key functional changes: Move-flow MCP tools (move_package_verify, move_package_wp) now configure Aptos-specific Boogie natives via a shared aptos_framework::prover::configure_aptos_custom_natives helper (also refactored into framework/src/prover.rs), and the tool schema reflects a higher max VC timeout (60s).

Spec work is substantial: adds new spec files (e.g. storage_slots_allocator.spec.move, math_fixed*.spec.move, transaction_limits.spec.move), strengthens/rewrites specs and invariants for core data structures (big_vector, smart_vector, pool_u64, smart_table), and fixes previously-skipped or hard-to-prove specs (notably fixed_point32 and fixed_point64) by aligning spec math with implementation and adding loop invariants/ensures. Prover backend changes include preventing double-emission of certain BV-mode calls, adding BV/int bridge axioms in the Boogie prelude, and adjusting spec-call translation behavior; new regression tests cover the BV vector length case and small fixed-point verification.

^{Reviewed by Cursor Bugbot for commit 0c248bc. Bugbot is set up for automated code reviews on this repo. Configure here.}

[rahxephon89]

• [move-prover] add weight for instantiation #19852
• more nla spec #19554
• [Prover] Support map intrinsics and more bug fix in spec inference  #19534
• [prover] fix some bugs in spec inference #19493
• [Move][Spec] Fix specs and other miscs #19310 👈 (View in Graphite)
• main

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

[wrwg]

I guess it should have a lager error because of the division?

[rahxephon89]

Sorry I don't get the hints here. As suggested by Claude, two expressions are equivalent?

[github-actions]

✅ Forge suite compat success on ca049383dd80675149ef2d0042668964f9f9107a ==> 0c248bc6bacc982b0e8d9084b4414dd8204e398f

Compatibility test results for ca049383dd80675149ef2d0042668964f9f9107a ==> 0c248bc6bacc982b0e8d9084b4414dd8204e398f (PR)
1. Check liveness of validators at old version: ca049383dd80675149ef2d0042668964f9f9107a
compatibility::simple-validator-upgrade::liveness-check : committed: 14405.89 txn/s, latency: 2410.40 ms, (p50: 2400 ms, p70: 2700, p90: 3300 ms, p99: 4200 ms), latency samples: 470940
2. Upgrading first Validator to new version: 0c248bc6bacc982b0e8d9084b4414dd8204e398f
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 6378.04 txn/s, latency: 5312.65 ms, (p50: 5800 ms, p70: 5900, p90: 6000 ms, p99: 6300 ms), latency samples: 219860
3. Upgrading rest of first batch to new version: 0c248bc6bacc982b0e8d9084b4414dd8204e398f
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 6343.36 txn/s, latency: 5300.22 ms, (p50: 5800 ms, p70: 6000, p90: 6100 ms, p99: 6200 ms), latency samples: 220000
4. upgrading second batch to new version: 0c248bc6bacc982b0e8d9084b4414dd8204e398f
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 11166.07 txn/s, latency: 2897.74 ms, (p50: 3100 ms, p70: 3200, p90: 3400 ms, p99: 3600 ms), latency samples: 364220
5. check swarm health
Compatibility test for ca049383dd80675149ef2d0042668964f9f9107a ==> 0c248bc6bacc982b0e8d9084b4414dd8204e398f 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 0c248bc6bacc982b0e8d9084b4414dd8204e398f

two traffics test: inner traffic : committed: 16067.18 txn/s, latency: 1073.35 ms, (p50: 1000 ms, p70: 1100, p90: 1200 ms, p99: 1600 ms), latency samples: 6001640
two traffics test : committed: 100.02 txn/s, latency: 837.55 ms, (p50: 800 ms, p70: 900, p90: 1000 ms, p99: 1200 ms), latency samples: 1680
Latency breakdown for phase 0: ["MempoolToBlockCreation: max: 0.291, avg: 0.251", "ConsensusProposalToOrdered: max: 0.115, avg: 0.111", "ConsensusOrderedToCommit: max: 0.234, avg: 0.185", "ConsensusProposalToCommit: max: 0.342, avg: 0.296"]
Max non-epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 0.48s no progress at version 6342131 (avg 0.06s) [limit 15].
Max epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 0.31s no progress at version 3107247 (avg 0.31s) [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 ca049383dd80675149ef2d0042668964f9f9107a ==> 0c248bc6bacc982b0e8d9084b4414dd8204e398f

Compatibility test results for ca049383dd80675149ef2d0042668964f9f9107a ==> 0c248bc6bacc982b0e8d9084b4414dd8204e398f (PR)
Upgrade the nodes to version: 0c248bc6bacc982b0e8d9084b4414dd8204e398f
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 2394.00 txn/s, submitted: 2401.18 txn/s, failed submission: 7.18 txn/s, expired: 7.18 txn/s, latency: 1310.34 ms, (p50: 1200 ms, p70: 1200, p90: 1500 ms, p99: 10900 ms), latency samples: 213481
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 2272.33 txn/s, submitted: 2280.78 txn/s, failed submission: 8.44 txn/s, expired: 8.44 txn/s, latency: 1427.20 ms, (p50: 1200 ms, p70: 1400, p90: 1800 ms, p99: 9500 ms), latency samples: 204502
5. check swarm health
Compatibility test for ca049383dd80675149ef2d0042668964f9f9107a ==> 0c248bc6bacc982b0e8d9084b4414dd8204e398f passed
Upgrade the remaining nodes to version: 0c248bc6bacc982b0e8d9084b4414dd8204e398f
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1793.04 txn/s, submitted: 1798.77 txn/s, failed submission: 5.73 txn/s, expired: 5.73 txn/s, latency: 1625.49 ms, (p50: 1200 ms, p70: 1200, p90: 2300 ms, p99: 10900 ms), latency samples: 162740
Test Ok

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