[Prover] Support map intrinsics and more bug fix in spec inference

[rahxephon89]

Description

This PR extends the Move Prover's spec inference (WP/weakest-precondition) pipeline with support for intrinsic map functions and fixes several inference output bugs. It builds on PR #19493.

Closes #19512

Intrinsic map function support (intrinsics.rs, pragmas.rs, spec_inference.rs, Boogie backend)

WP previously treated all intrinsic map functions (table::add, table::borrow, table::contains, table::remove, etc.) as opaque impure calls, producing unverifiable behavior predicates (result_of<f>). These functions have axiomatized spec counterparts (spec_set, spec_get, spec_contains_key, spec_len, etc.) declared in the Boogie prelude.

Fix: the Move→Spec and Move→AbortSpec pairings are now encoded directly in INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS via the new IntrinsicFunDef struct (replacing the former separate static tables INTRINSIC_TYPE_MAP_MOVE_TO_SPEC_FUN / INTRINSIC_TYPE_MAP_MOVE_TO_ABORT_SPEC_FUN). During process_intrinsic_declaration the pairings are materialized into two new IntrinsicDecl fields (move_to_spec_intrinsic, move_to_abort_spec_intrinsic), consistent with how vector intrinsics are handled. IntrinsicsAnnotation::get_spec_fun_for_move_fun and get_abort_spec_fun_for_move_fun read directly from these fields — no separate static table lookups at query time.

The WP transfer function calls try_as_intrinsic_map_spec_call to substitute the spec function directly — producing a verifiable pure spec call instead of a behavior predicate.

mk_call_with_inst records the call-site type instantiation so the sourcifier emits explicit type arguments (e.g., spec_new<K, V>() instead of spec_new()) — required for zero-argument spec functions whose type args cannot be inferred from the argument list.

The Boogie backend's $bp_AbortsOf emission was also extended: get_abort_spec_fun_for_move_fun looks up the abort-spec counterpart for a Move intrinsic and emits it as the abort body, rather than defaulting to false.

Native vector function mapping (spec_inference.rs)

Native std::vector functions (empty, length, borrow) now have direct spec-language equivalents ([], len, index operator) instead of being compiled to uninterpreted behavior predicates. try_as_native_spec_exp handles this mapping.

Spec inference output bug fixes (sourcifier.rs, spec_inference.rs, inference.rs)

• vector<T>[] type annotation: Operation::Vector now emits vector<T>[] for empty vector literals (instead of bare vector[]) so the compiler can infer the element type.
• Nested quantifier name collision: rename_quant_vars_in_exp now excludes (a) variables free in range expressions and (b) binder names used by inner quantifiers when choosing a fresh name, preventing type errors like forall x: BitVector: x >= amount.
• Module header address form: generate_fresh_spec_file now reads the source .move file to extract the exact address token used in the module <addr>::<name> declaration, emitting spec std::bit_vector rather than spec 0x1::bit_vector. This ensures merge_spec_modules can match the generated spec back to its source module.
• Forall distribution over conjuncts: When wrapping a struct reference in a forall quantifier, the WP now distributes over top-level conjuncts so that A(x) && B (where only A(x) mentions the bound variable) becomes (forall x: A(x)) && B rather than forall x: A(x) && B.

Framework spec changes

• aptos-stdlib::pool_u64 — pool_u64.spec.move (modified): re-enabled verification, ∀∀ struct invariants, opaque functions, fixed ensures/frames for buy_in, redeem_shares, add_shares, DeductSharesEnsures, new specs for new, create, amount_to_shares, etc.

• move-stdlib::bit_vector — bit_vector.spec.move (new): opaque spec for length; frame conditions for set/unset in source.

• move-stdlib::acl — acl.spec.move (new): full opaque specs with spec_contains helper, struct uniqueness invariant, aborts/ensures for all public functions.

• aptos-stdlib::math64 — math64.spec.move (modified): pow, floor_log2, sqrt now use pragma verify = false (replacing [abstract] annotations on individual conditions, which is the correct idiom when there is no paired [concrete] version). Also adds pragma opaque to max, min, clamp.

How Has This Been Tested?

New inference test cases:

• tests/inference/intrinsic_map — intrinsic map function WP support
• tests/inference/nested_quant_rename — nested quantifier name collision fix
• tests/inference/vector_typing — vector<T>[] type annotation fix

Framework specs verified with move_package_verify (40s timeout) on bit_vector and acl.

Run inference tests with:

RUST_MIN_STACK=104857600 BOOGIE_EXE=... Z3_EXE=... \
  cargo test -p move-prover --test inference_testsuite -- --test-threads=1

Key Areas to Review

• pragmas.rs: IntrinsicFunDef struct and updated INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS
• intrinsics.rs: new IntrinsicDecl fields and updated populate_intrinsic_decl / get_spec_fun_for_move_fun
• spec_inference.rs: try_as_intrinsic_map_spec_call, try_as_native_spec_exp
• math64.spec.move: pragma verify = false on pow/floor_log2/sqrt

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 tested both happy and unhappy path of the functionality
• I have made corresponding changes to the documentation

---

Note

Medium Risk
Changes core prover inference, intrinsic wiring, and Boogie axiom generation; incorrect behavior could weaken or break verification, though scope is limited to the prover and spec files rather than on-chain execution.

Overview
Extends spec inference so intrinsic map (SimpleMap) and native std::vector calls inline as pure spec expressions (spec_contains_key, spec_new, len, vector<T>[], etc.) instead of opaque result_of / aborts_of behavior predicates. Move↔spec and Move↔abort-spec pairings live in IntrinsicFunDef / INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS, with Boogie $bp_AbortsOf and map prelude hooks for spec_aborts_* functions.

WP / output fixes: typed empty vectors in the sourcifier; fresher quantifier names (ranges + inner binders); forall distribution over top-level conjuncts for struct havoc; skip data/global invariant VC props in the WP; native/pure calls no longer advance memory labels; zero-arg axioms without empty forall; generated .spec.move headers use the source file’s module address token (e.g. std vs 0x1).

Boogie: native functions without Move specs can delegate result_of / ensures_of to $-spec prelude functions.

Framework / tests: stronger opaque specs and verification for pool_u64, math64, acl, bit_vector; new inference tests (intrinsic_map, nested_quant_rename, vector_typing).

^{Reviewed by Cursor Bugbot for commit 603158c. 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 👈 (View in Graphite)
• [prover] fix some bugs in spec inference #19493
• [Move][Spec] Fix specs and other miscs #19310
• main

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

[cursor]

Stale comment

Aptos Security Bugbot has reviewed your changes and found no new issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Stale comment

Aptos Security Bugbot has reviewed your changes and found no new issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Stale comment

Aptos Security Bugbot has reviewed your changes and found no new issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Stale comment

Aptos Security Bugbot has reviewed your changes and found no new issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Stale comment

Aptos Security Bugbot has reviewed your changes and found no new issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Stale comment

Aptos Security Bugbot has reviewed your changes and found no new issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Stale comment

Aptos Security Bugbot has reviewed your changes and found no new issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Stale comment

Aptos Security Bugbot has reviewed your changes and found no new issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes and found no new issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[github-actions]

✅ Forge suite compat success on e8e41d2e33ae0fff6283eaeb37b2d44f898e4404 ==> 603158c97ac3d0c336892300c3b151006f3dea47

Compatibility test results for e8e41d2e33ae0fff6283eaeb37b2d44f898e4404 ==> 603158c97ac3d0c336892300c3b151006f3dea47 (PR)
1. Check liveness of validators at old version: e8e41d2e33ae0fff6283eaeb37b2d44f898e4404
compatibility::simple-validator-upgrade::liveness-check : committed: 15217.74 txn/s, latency: 2262.64 ms, (p50: 2300 ms, p70: 2500, p90: 3000 ms, p99: 3600 ms), latency samples: 494660
2. Upgrading first Validator to new version: 603158c97ac3d0c336892300c3b151006f3dea47
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 6197.52 txn/s, latency: 5439.46 ms, (p50: 6000 ms, p70: 6100, p90: 6200 ms, p99: 6600 ms), latency samples: 213060
3. Upgrading rest of first batch to new version: 603158c97ac3d0c336892300c3b151006f3dea47
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 6086.35 txn/s, latency: 5429.47 ms, (p50: 6000 ms, p70: 6200, p90: 6700 ms, p99: 6900 ms), latency samples: 209860
4. upgrading second batch to new version: 603158c97ac3d0c336892300c3b151006f3dea47
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 10102.70 txn/s, latency: 3297.37 ms, (p50: 3400 ms, p70: 3700, p90: 4000 ms, p99: 4300 ms), latency samples: 335280
5. check swarm health
Compatibility test for e8e41d2e33ae0fff6283eaeb37b2d44f898e4404 ==> 603158c97ac3d0c336892300c3b151006f3dea47 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 603158c97ac3d0c336892300c3b151006f3dea47

two traffics test: inner traffic : committed: 15643.26 txn/s, latency: 1088.83 ms, (p50: 1000 ms, p70: 1100, p90: 1300 ms, p99: 1500 ms), latency samples: 5843020
two traffics test : committed: 99.99 txn/s, latency: 845.48 ms, (p50: 800 ms, p70: 900, p90: 1000 ms, p99: 1200 ms), latency samples: 1760
Latency breakdown for phase 0: ["MempoolToBlockCreation: max: 0.321, avg: 0.261", "ConsensusProposalToOrdered: max: 0.119, avg: 0.113", "ConsensusOrderedToCommit: max: 0.176, avg: 0.145", "ConsensusProposalToCommit: max: 0.284, avg: 0.258"]
Max non-epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 0.85s no progress at version 68073 (avg 0.06s) [limit 15].
Max epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 0.32s no progress at version 2897131 (avg 0.32s) [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 e8e41d2e33ae0fff6283eaeb37b2d44f898e4404 ==> 603158c97ac3d0c336892300c3b151006f3dea47

Compatibility test results for e8e41d2e33ae0fff6283eaeb37b2d44f898e4404 ==> 603158c97ac3d0c336892300c3b151006f3dea47 (PR)
Upgrade the nodes to version: 603158c97ac3d0c336892300c3b151006f3dea47
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1799.32 txn/s, submitted: 1805.24 txn/s, failed submission: 5.92 txn/s, expired: 5.92 txn/s, latency: 1603.84 ms, (p50: 1200 ms, p70: 1500, p90: 3300 ms, p99: 3900 ms), latency samples: 164140
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1915.94 txn/s, submitted: 1921.47 txn/s, failed submission: 5.53 txn/s, expired: 5.53 txn/s, latency: 1571.08 ms, (p50: 1200 ms, p70: 1500, p90: 3600 ms, p99: 4200 ms), latency samples: 173140
5. check swarm health
Compatibility test for e8e41d2e33ae0fff6283eaeb37b2d44f898e4404 ==> 603158c97ac3d0c336892300c3b151006f3dea47 passed
Upgrade the remaining nodes to version: 603158c97ac3d0c336892300c3b151006f3dea47
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 2260.81 txn/s, submitted: 2268.09 txn/s, failed submission: 7.29 txn/s, expired: 7.29 txn/s, latency: 1263.41 ms, (p50: 1200 ms, p70: 1300, p90: 1900 ms, p99: 2600 ms), latency samples: 204742
Test Ok

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