more nla spec

[rahxephon89]

Description

Loosely-coupled improvements to the formal-verification surface, all on top of teng/handle-intrinsics-for-spec-infer.

1. BigOrderedMap specs

New spec blocks (callers gain abstract postconditions enabling existence / FIFO-progress / frame-condition reasoning):

• front_key, back_key, remove_or_none
• pop_back (was previously empty), full ensures mirroring pop_front
• iter_modify, iter_remove — declare the value-mutation / removal frame condition through the closure / iterator interface
• internal_find_with_path, iter_with_path_get_iter
• internal_leaf_new_begin_iter, internal_leaf_iter_is_end, internal_leaf_borrow_value, internal_leaf_iter_borrow_entries_and_next_leaf_index

New / expanded ensures on previously-empty specs:

• iter_is_end, iter_borrow, iter_borrow_mut, iter_borrow_key, iter_is_begin, iter_next, iter_prev
• pop_front, pop_back
• internal_find, internal_lower_bound, internal_new_begin_iter, internal_new_end_iter
• new_with_config, new_with_reusable, new_with_type_size_hints — gain aborts_if on inner/leaf max-degree bounds plus empty-result ensures.

Shared spec_unchanged_except_at(self, key) predicate — captures the frame condition "for all keys other than key, containment and value are unchanged between old(self) and self." Used in remove, remove_or_none, upsert, pop_front, pop_back, iter_modify, iter_remove. Collapses verbose forall k where k != key clauses into a single named predicate, applied uniformly across single-key mutating operations.

Drops the [abstract] modifier from existing ensures / aborts_if clauses across remove, keys, new_from, upsert, borrow_front, borrow_back, prev_key, next_key, compute_length. Each of these specs still carries pragma verify = false, so the contracts remain trusted; removing [abstract] enforces the convention "one trust lever per spec block."

2. Move-Prover prelude fix

Adds the missing $1_vector_move_range{{S}} procedure. Before this fix, any verification path that lowered to vector::move_range failed Boogie with:

call to undeclared procedure: $1_vector_move_range'u64'

This forced pragma verify = false on every function that transitively called vector::move_range. The stub models the operation via existing SliceVec / ConcatVec primitives and relies on Move's guarantee that the two &mut vector<T> arguments cannot alias. Defensive < 0 bounds checks (against possibly-negative Boogie ints) follow the convention used in $1_vector_insert.

3. NLA-adjacent stdlib fixes

• math64::floor_log2: added two loop invariants ((res as u64) + 2*(n as u64) <= 64 and n == 0 ==> (res as u64) <= 63) so the loop discharges.
• math_fixed::sqrt: added ensures x.get_raw_value() == 0 ==> result.get_raw_value() == 0; so callers can rule out zero outputs without descending into non-linear arithmetic.
• string::utf8: tightened from previous trusted aborts_if [abstract] false to honest aborts_if !spec_internal_check_utf8(bytes). Callers using static ASCII literals must discharge UTF-8 validity (typically via a module-level axiom std::string::spec_internal_check_utf8(b"...")).

4. transaction_context.spec.move

Marks monotonically_increasing_counter_internal, monotonically_increasing_counter_internal_for_test_only, and monotonically_increasing_counter as aborts_if [abstract] false so callers can treat the counter as total.

Note: per the source comment, monotonically_increasing_counter can abort if the local counter overflows after 65535 calls in a single session. The [abstract] false claim is a deliberate trust assumption — no realistic single-tx workload reaches this bound — but worth documenting for future tightening.

How Has This Been Tested?

aptos move prove --package-dir aptos-move/framework/aptos-framework --filter big_ordered_map passes. All BOM spec changes are pragma verify = false (trusted contracts on top of the intrinsic / opaque body), so they impose no verification load themselves while exposing stronger postconditions to downstream callers.

Key Areas to Review

• native.bpl move_range procedure: confirm the abort conditions (removal_position + length > LenVec(from_v), insert_position > LenVec(to_v)) exactly match Move-runtime semantics, and that the no-aliasing assumption is safe at every current and plausibly-future call site.
• math64::floor_log2 loop invariants: confirm the invariants are strong enough to discharge whatever downstream proof obligations motivated adding them.
• spec_unchanged_except_at predicate — the centerpiece refactor. Confirm semantics by inspection of remove, pop_front / pop_back, iter_modify / iter_remove.
• monotonically_increasing_counter trust: confirm the over-claim against the documented overflow abort path is acceptable for current callers.

---

Note

Medium Risk
Changes are spec/prelude-only (no on-chain runtime logic), but trusted contracts and the move_range Boogie model must match Move semantics; the counter’s aborts_if false over-claims vs documented overflow.

Overview
Strengthens Move Prover contracts across BigOrderedMap, stdlib math/string helpers, transaction context, and the Boogie vector prelude so downstream proofs can rely on richer postconditions without re-proving bodies.

BigOrderedMap gains trusted (pragma verify = false) specs for iterators, bounds search, front_key / back_key, remove_or_none, pop_*, path-based find/remove, and leaf helpers. A shared spec_unchanged_except_at frame predicate replaces repeated forall k != key clauses on single-key mutators. Many specs drop the [abstract] modifier on ensures / aborts_if while staying trusted via verify = false. Constructors document degree bounds and empty-map results; remove postconditions are tightened (including length on delete).

The prover prelude adds $1_vector_move_range, fixing undeclared-procedure failures when verification lowers vector::move_range.

math64::floor_log2 gets loop invariants; math_fixed::sqrt documents zero-in/zero-out; string::utf8 aborts on invalid UTF-8 instead of a blanket non-abort. monotonically_increasing_counter (and internal variants) are marked non-aborting under an abstract trust assumption (documented overflow caveat).

^{Reviewed by Cursor Bugbot for commit b47a790. 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 👈 (View in Graphite)
• [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
• 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.

All prior threads have been resolved. The changes remain confined to Move Prover formal-verification artifacts (specs, Boogie prelude) with no impact on on-chain runtime behavior.

  

_{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]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, have a team admin enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit ca6638c. Configure here.}

[cursor]

Stale comment

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

  

_{Sent by Cursor Automation: Security Review Bot}

[wrwg]

Why do we still have abstract here? (In contrast to PR description) Here and elsewhere

[rahxephon89]

Removed all [abstract] in the spec.

[wrwg]

Maybe can pull this here and below into a helper function?

FWIW we can now use old in spec functions: spec fun f(a: address) { R[a] == old(R[a]) } should be possible, and f can then be used only in ensures (two-state predicates). Not sure how well tested.

[rahxephon89]

Added a spec function. However, old only works for global resources (at least for now) so the added spec function still requires passing both old and new value to it.

[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]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, have a team admin enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit 5d9b2d6. Configure here.}

[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.

All changed files are Move Prover formal specification artifacts (big_ordered_map.spec.move, transaction_context.spec.move, math64.move loop invariants, math_fixed.spec.move, string.spec.move, native.bpl Boogie prelude, and the auto-generated head.mrb). No on-chain execution semantics are altered.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Stale comment

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

All changes are Move Prover formal specification additions (spec blocks, loop invariants, Boogie prelude stubs) with no runtime behavior changes. All prior automation findings have been addressed.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

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

All changed files are Move Prover formal specifications (big_ordered_map.spec.move, transaction_context.spec.move, math64.move, math_fixed.spec.move, string.spec.move, native.bpl) and the cached-packages binary. These changes carry no runtime impact and introduce no security-relevant logic.

  

_{Sent by Cursor Automation: Security Review Bot}

[github-actions]

✅ Forge suite compat success on 7d4aeb52496187f2ae9494d2ef82e9360931fc9f ==> b47a790878985d7c707ee7027e2cc9f635fde11d

Compatibility test results for 7d4aeb52496187f2ae9494d2ef82e9360931fc9f ==> b47a790878985d7c707ee7027e2cc9f635fde11d (PR)
1. Check liveness of validators at old version: 7d4aeb52496187f2ae9494d2ef82e9360931fc9f
compatibility::simple-validator-upgrade::liveness-check : committed: 14967.51 txn/s, latency: 2303.04 ms, (p50: 2200 ms, p70: 2700, p90: 3100 ms, p99: 3800 ms), latency samples: 487720
2. Upgrading first Validator to new version: b47a790878985d7c707ee7027e2cc9f635fde11d
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 6096.75 txn/s, latency: 5537.61 ms, (p50: 6100 ms, p70: 6200, p90: 6300 ms, p99: 6400 ms), latency samples: 213100
3. Upgrading rest of first batch to new version: b47a790878985d7c707ee7027e2cc9f635fde11d
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 6000.83 txn/s, latency: 5585.23 ms, (p50: 6200 ms, p70: 6300, p90: 6400 ms, p99: 6700 ms), latency samples: 208020
4. upgrading second batch to new version: b47a790878985d7c707ee7027e2cc9f635fde11d
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 9971.64 txn/s, latency: 3382.95 ms, (p50: 3600 ms, p70: 3800, p90: 3900 ms, p99: 4000 ms), latency samples: 328560
5. check swarm health
Compatibility test for 7d4aeb52496187f2ae9494d2ef82e9360931fc9f ==> b47a790878985d7c707ee7027e2cc9f635fde11d 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 b47a790878985d7c707ee7027e2cc9f635fde11d

two traffics test: inner traffic : committed: 13405.60 txn/s, latency: 1373.59 ms, (p50: 1300 ms, p70: 1500, p90: 1800 ms, p99: 2100 ms), latency samples: 5007120
two traffics test : committed: 100.02 txn/s, latency: 833.06 ms, (p50: 800 ms, p70: 1000, p90: 1100 ms, p99: 1200 ms), latency samples: 1740
Latency breakdown for phase 0: ["MempoolToBlockCreation: max: 0.408, avg: 0.374", "ConsensusProposalToOrdered: max: 0.112, avg: 0.107", "ConsensusOrderedToCommit: max: 0.149, avg: 0.140", "ConsensusProposalToCommit: max: 0.255, avg: 0.246"]
Max non-epoch-change gap was: 1 rounds at version 88884 (avg 0.00) [limit 4], 0.59s no progress at version 88884 (avg 0.06s) [limit 15].
Max epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 0.29s no progress at version 2571697 (avg 0.29s) [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 7d4aeb52496187f2ae9494d2ef82e9360931fc9f ==> b47a790878985d7c707ee7027e2cc9f635fde11d

Compatibility test results for 7d4aeb52496187f2ae9494d2ef82e9360931fc9f ==> b47a790878985d7c707ee7027e2cc9f635fde11d (PR)
Upgrade the nodes to version: b47a790878985d7c707ee7027e2cc9f635fde11d
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 2260.12 txn/s, submitted: 2267.62 txn/s, failed submission: 7.50 txn/s, expired: 7.50 txn/s, latency: 1239.69 ms, (p50: 1200 ms, p70: 1400, p90: 1800 ms, p99: 2400 ms), latency samples: 205021
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 2350.63 txn/s, submitted: 2360.03 txn/s, failed submission: 9.40 txn/s, expired: 9.40 txn/s, latency: 1201.77 ms, (p50: 1200 ms, p70: 1200, p90: 1700 ms, p99: 2400 ms), latency samples: 210042
5. check swarm health
Compatibility test for 7d4aeb52496187f2ae9494d2ef82e9360931fc9f ==> b47a790878985d7c707ee7027e2cc9f635fde11d passed
Upgrade the remaining nodes to version: b47a790878985d7c707ee7027e2cc9f635fde11d
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1905.60 txn/s, submitted: 1911.33 txn/s, failed submission: 5.73 txn/s, expired: 5.73 txn/s, latency: 1631.27 ms, (p50: 1200 ms, p70: 1500, p90: 2700 ms, p99: 11400 ms), latency samples: 172881
Test Ok

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