[framework] BigOrderedMap iterator validity specs

[rahxephon89]

Description

Activate iterator-validity checking for BigOrderedMap using the hidden-slot machinery from #20310: iterator staleness becomes a machine-checked precondition instead of a documented presumption, per map object.

The spec binds the three validity roles and declares their native predicates — no ghost state, no new fields, nothing nameable beyond the predicates themselves:

spec BigOrderedMap {
    pragma intrinsic = map, ...,
        map_spec_iter_valid = spec_iter_current,          // keyed IteratorPtr<K>
        map_spec_leaf_iter_valid = spec_leaf_iter_valid,  // key-agnostic LeafNodeIteratorPtr
        map_spec_iter_preserved = spec_iter_preserved;    // frame predicate
}
spec native fun spec_iter_current<K, V>(it: IteratorPtr<K>, map: BigOrderedMap<K, V>): bool;

Binding the roles gives the map and both iterator types hidden version slots (fresh at creation, havocked by every structural mutation, preserved by value writes); the natives are defined by the prover as slot equality. The contracts then say the obvious things:

• create (internal_lower_bound, internal_find, internal_new_begin_iter, internal_find_with_path, internal_leaf_new_begin_iter): ensures spec_iter_current(result, self) — a fresh iterator is valid for its map.
• use (iter_borrow, iter_borrow_mut, iter_next, iter_prev, iter_is_begin, iter_modify, iter_remove): requires spec_iter_valid(self, map). Advancing (iter_next/iter_prev) re-ensures validity of the result.
• preserve (iter_modify, allocate_spare_slots): ensures spec_iter_preserved(map, old(map)) — modifying a value through an iterator, or preallocating storage slots, is not a structural mutation.

spec_iter_valid is a thin public wrapper adding the End disjunct: End iterators carry no position, so they are valid regardless of mutation (iter_prev from End legitimately finds the largest key of the current map). The leaf walker has no End variant distinct from its NULL_INDEX sentinel and binds its native directly.

Structural mutations havoc the map's slot, so they invalidate outstanding iterators of that map object only — same-type sibling maps, other elements of a vector<BigOrderedMap>, and copies that have since diverged are unaffected, while stale or cross-map iterator use fails verification. One refinement lives in the intrinsic model itself: an existing-key upsert replaces the value in place (add_at overwrites before ever splitting), so the upsert/add_override_if_exists templates preserve the slot on that branch — iterators survive value-only upserts with no annotation.

Supporting changes:

• iter_with_path_get_iter becomes transparent (it is a plain projection): an opaque ensures result == self.iterator would not carry the projected iterator's hidden slot (equality excludes it), while inlined value flow does.
• fat_loop.rs: loop-invariant and unrolling-mark placement validation now ignores declarations in unreachable code — inline expansion (e.g. of for_each_mut) leaves dead copies of the spec block behind, which are never verified and must not be flagged as misplaced. The reachability check is a single pass collecting reachable Prop attr ids, so validation stays linear in function size.
• The module's iterator loops (for_each_mut, for_each_leaf_node_children_ref, intersection_zip_for_each_ref) carry spec_iter_valid / spec_leaf_iter_valid invariants so advanced iterators survive the loop-head havoc; the intersection walk needs them for both maps' leaf iterators.

How Has This Been Tested?

• aptos-move-cli prove -f big_ordered_map: the module verifies, including the transparent projection, the three invariant-carrying loops, and the new witness test_verify_iter_across_upsert (an iterator survives an existing-key upsert and reads through afterwards).
• Full framework prover battery (move_stdlib, aptos_stdlib, framework, token) green — all existing framework specs verify unchanged with validity active.
• The acceptance matrix for the model itself (stale use, cross-map, vector elements, copy divergence, opaque &mut, loops, wrappers) is pinned in [move prover] ghost carrier and iterator validity for intrinsic maps #20310's verify_iterator_validity.move against a mock map.

Type of Change

• New feature

Which Components or Systems Does This Change Impact?

• Other (specify): Move Prover, framework specs

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

🤖 Generated with Claude Code

---

Note

Medium Risk
Touches Move prover map intrinsics, Boogie mutation semantics, and framework verification contracts; runtime map behavior is unchanged but proof obligations and prover diagnostics shift.

Overview
Turns BigOrderedMap iterator staleness from a documented presumption into prover-enforced preconditions via intrinsic map roles (map_spec_iter_valid, map_spec_leaf_iter_valid, map_spec_iter_preserved) and native predicates tied to hidden validity slots.

Iterator create/use/advance specs now require or ensure validity; value-only paths (iter_modify, allocate_spare_slots) ensure spec_iter_preserved. iter_with_path_get_iter is no longer opaque so projected iterators keep validity through equality. for_each_mut, leaf walks, and intersection_zip_for_each_ref add loop **invariant**s for iterator validity.

Boogie map templates treat existing-key upsert / add_override_if_exists as in-place value updates ($UpdateMutation without ghost havoc) so iterators can survive those updates; test_verify_iter_across_upsert witnesses that behavior.

fat_loop.rs skips “misplaced” loop invariant / unrolling diagnostics when the spec Prop lives only in unreachable bytecode (e.g. dead copies after inline expansion).

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

[rahxephon89]

Warning

This pull request is not mergeable via GitHub because a downstack PR is open. Once all requirements are satisfied, merge this PR as a stack on Graphite.
Learn more

• [framework] BigOrderedMap iterator validity specs #20311 👈 (View in Graphite)
• [move prover] ghost carrier and iterator validity for intrinsic maps #20310
• [framework] BigOrderedMap iterator contracts #20303 : 1 other dependent PR (#20307 )
• [prover] implement ghost field for structs/enums #20272
• [move prover] havoc loop-modified global memory at loop headers #20258
• main

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

[cursor]

Aptos Security Bugbot has reviewed your changes and found 1 potential issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 1 issues that need to be addressed from previous scan.

Open findings:

• Iterator-advancing loops cannot satisfy the new contract

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 1 issues that need to be addressed from previous scan.

Open findings:

• Iterator-advancing loops cannot satisfy the new contract

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 1 issues that need to be addressed from previous scan.

Open findings:

• Iterator-advancing loops cannot satisfy the new contract

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 1 issues that need to be addressed from previous scan.

Open findings:

• Iterator-advancing loops cannot satisfy the new contract

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 1 issues that need to be addressed from previous scan.

Open findings:

• Iterator-advancing loops cannot satisfy the new contract

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes and found 1 potential issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 2 issues that need to be addressed from previous scan.

Open findings:

• Iterator-advancing loops cannot satisfy the new contract
• Preallocation invalidates valid iterators in the model

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 1 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes and found 1 potential issue.

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 2 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 2 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 2 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 5 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 5 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 5 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes and found 1 potential issue.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes and found 1 potential issue.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 5 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 5 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 5 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

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

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 5 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 5 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}

[cursor]

Aptos Security Bugbot has reviewed your changes, there are still 5 issues that need to be addressed from previous scan.

Open findings:

• Preallocation invalidates valid iterators in the model
• Conditional non-structural updates discard iterator validity
• Misplaced-invariant validation is quadratic in function size
• Iterator validity is not preserved across the intersection leaf loop
• Unreachable loop-unrolling marks still fail validation

  

_{Sent by Cursor Automation: Security Review Bot}