framework spec: first pass at the Move Prover modifies cascade

[booleanfunction]

Summary

This PR tries to get movement move prove --package-dir aptos-move/framework/aptos-framework --dev
working again. On m1 right now the Move Prover fails at the
bytecode-transformation stage before any verification conditions are
generated, so the package can't be checked at all. The fixes here:

1. Unblock the bytecode-transformation cascade.
2. Address four of the regression sites identified in ganymedio's
   commit-blame trace from the PR Chore: clean up Move compiler warnings and Move Prover errors #320 discussion, using
   aborts_if_is_partial + TODO comments rather than blanket
   pragma verify = false.
3. Include a one-line soundness fix in aptos_coin.spec.move that I
   was able to validate empirically once the cascade was unblocked.

Following the direction from the PR #320 discussion ("separate fix PRs
for each module where possible"), this PR is the foundational piece —
the modifies-cascade unblock plus the regression sites that become
locally provable once the cascade clears. Other regression sites that
showed up during shard isolation are out of scope here and enumerated
under "Out of scope" below.

Marking as draft

Marked as draft for a few reasons:

• This is my first PR to aptos-core, and I'm still learning the codebase
  and Move Prover internals. Feedback on whether this is the right shape
  would be really helpful — and please tell me if I've misunderstood
  anything as I work out how to best contribute here.
• The drop-vs-broaden modifies analysis (below) may be new structural
  information about Move Prover's modifies-propagation rule. I'd love
  ganymedio / fEst1ck input on the framing before finalizing.
• The PR bundles five fixes. If reviewers prefer a per-module split per
  the original plan, happy to break this into the foundational
  cascade-unblock + four small PRs.
• Per-module .fv.md companion docs (à la timelock.fv.md from PR get timelock module spec green, write full verification plan #334)
  aren't written yet — happy to add them based on review preference.

Why drop the modifies clause (rather than broaden it)

As far as I can tell, the cascade is a spec bug, not a prover
limitation. The depleted-staking-rewards-treasury feature work (merged
into m1 via the "movement thursday" merge on 2025-11-13) added a
treasury-branch path to stake::distribute_rewards that calls
governed_gas_pool::withdraw_staking_reward → coin::withdraw.
That widened the function's actual modification set from
{coin::CoinInfo<AptosCoin>} to
{coin::CoinInfo<AptosCoin>, coin::CoinStore<AptosCoin> at gov-gas-signer}.
The DistributeRewardsAbortsIf schema still claimed
modifies global<coin::CoinInfo<AptosCoin>>(addr) — strictly tighter
than what the implementation now does. Move Prover's caller ⊇ callee
modifies check picks up the mismatch, which is what's producing the
cascade.

For context, the relevant passages from the MSL docs
(third_party/move/move-prover/doc/user/spec-lang.md):

The modifies condition is used to provide permissions to a function
to modify global storage. The annotation itself comprises a list of
global access expressions. It is specifically used together with
[opaque function specifications].

— spec-lang.md:756-758

If the modifies annotation is omitted on a function, then that
function is deemed to have all possible permissions for those
resources it may modify during its execution. The set of all
resources that may be modified by a function is obtained via an
interprocedural analysis of the code. […] if the programmer adds
modifies global<S>(addr1) to the specification […], then the call
to mutate_at is checked to make sure that modify permissions
granted to mutate_S_test cover the permissions it grants to
mutate_at.

— spec-lang.md:800-807

With those in mind, two approaches considered:

• Drop the inaccurate modifies clause. Per the second passage
  above, a function with no modifies annotation has "all possible
  permissions for those resources it may modify during its execution".
  That's now an accurate description of distribute_rewards after the
  treasury-branch path was added.
• Broaden the modifies set. Cover both CoinInfo and the
  gov-gas-pool CoinStore. I tried this — added the second modifies
  clause and re-ran prove. The prover then cascaded the requirement
  through every callee in the chain: withdraw_staking_reward had to
  declare both, coin::withdraw had to declare both (it currently only
  declares CoinStore), and the requirements propagated outward across
  the framework.

From this one experiment, my reading of how Move Prover handles
modifies in practice is: once a caller declares any explicit
modifies, every callee in the chain must declare matching modifies
for every resource the caller names, even resources the callee
doesn't actually touch. If that's right, adding more resources to the
caller multiplies the propagation requirements downstream — which
would make dropping the inaccurate clause the better fix here.

But this is one negative result from one experiment, and I'm new to
Move Prover internals — I'd really appreciate a sanity check on this
interpretation. Am I reading the modifies semantics correctly? Is
there an MSL construct I missed (abstract modifies, schema parameters,
something else) that would let me declare modifies without the
downstream cascade? If this matches what the prover team has already
seen, great; if not, please let me know what I'm misreading.

Commits

This branch has two commits (could be split per reviewer preference):

• 363ab14742 — framework prover restoration (cascade unblock + 4 spec fixes)
• 538cd2249d — aptos_coin::find_delegation address fix (@core_resources → @aptos_framework)

Per-fix breakdown

1. stake.spec.move — drop inaccurate modifies CoinInfo

Removed one line from DistributeRewardsAbortsIf:

- modifies global<coin::CoinInfo<AptosCoin>>(addr);

See "Why this approach" above. This is the unblocker; the four other fixes
target VC errors that the cascade was masking.

2. aptos_coin.spec.move::initialize — partial mode with TODO

Switched to pragma aborts_if_is_partial = true. Inline TODO covers two
viable paths back to strict mode:

• (a) Add requires !permissioned_signer::spec_is_permissioned_signer(aptos_framework)
  and propagate through genesis::create_initialize_validators_with_commission.
  Principled for public(friend) functions called only from genesis.
• (b) Model fungible_asset::withdraw_permission_check_by_address's abort
  condition precisely. Heavier but closes the gap framework-wide.

Tried (a) standalone in development; the requires propagation hits genesis,
which lacks a matching requires, producing "precondition does not hold"
failures. Both paths are noted in the TODO; (b) is likely the long-term
right call.

3. aptos_coin.spec.move::destroy_mint_capability_from — new spec

Three-line spec mirroring the existing destroy_mint_cap pattern. The
function was added in commit f23bc892bd ("move2 upgrade") without a
companion spec; this restores that pairing.

4. aptos_account.spec.move::register_fa_and_apt — new partial-mode spec

Added a real spec block (vs. the sibling register_apt's pragma verify = false
stub at line 272). Partial mode + TODO documenting the same chain through
coin::register → assert_signer_has_permission that initialize hits.

Sibling register_apt left as-is to keep this PR scoped.

5. governed_gas_pool.spec.move::initialize — requires → aborts_if

This is one of the items called out in ganymedio's commit-blame trace
for commit 5256a49f4a ("feat: add spec invariants and unit tests",
2025-12-08):

Three issues in governed_gas_pool.spec.move: malformed aborts_with
clause, withdraw_staking_reward non-terminating, initialize uses
requires instead of aborts_if.

This PR addresses the third (the requires/aborts_if issue). The
malformed aborts_with on withdraw and the withdraw_staking_reward
non-termination are tracked under "Out of scope" below.

Converted the requires system_addresses::is_aptos_framework_address(...)
precondition into aborts_if !system_addresses::is_aptos_framework_address(...)
plus pragma aborts_if_is_partial = true. The original requires form
propagated unprovable preconditions through governed_gas_pool::init_module
and genesis::initialize_aptos_coin; converting shifts the verification
obligation here.

This surfaced naturally as part of the cascade-unblock work — once the
bytecode-transformation failure was cleared, the prover started
reaching the genesis-side calls and the precondition failures showed up.

6. aptos_coin.spec.move::find_delegation — soundness fix (one line)

-    aborts_if !exists<Delegations>(@core_resources);
+    aborts_if !exists<Delegations>(@aptos_framework);

The implementation in aptos_coin.move:147 reads
borrow_global<Delegations>(@aptos_framework).inner, but the spec was left
referencing @core_resources after commit f23bc892bd swapped the
implementation's address. The drift produces a counterexample whenever
Delegations is present at @core_resources but absent at @aptos_framework:
spec says "no abort", runtime aborts on borrow_global.

I was able to confirm this with the prover: running
movement move prove --only-shard 5 on the prior checkpoint surfaces
the bug with a concrete counterexample (addr = 0x3d6c), and applying
the fix clears both find_delegation errors. The bug was previously
masked by the bytecode-transformation cascade.

Honest pragmas inventory

Each new pragma aborts_if_is_partial = true introduced by this PR has a
specific named gap and follow-up path in an inline TODO:

Function	Module	Gap
initialize	aptos_coin.spec.move	assert_signer_has_permission's conditional permissioned-signer abort path; coin_address equality not linked
register_fa_and_apt	aptos_account.spec.move	Same chain via coin::register; also ensure_primary_fungible_store_exists has no spec
initialize	governed_gas_pool.spec.move	Multiple abort paths beyond framework-address check (resource-account creation, event-handle creation, transitive register_fa_and_apt call, move_to)

The TODOs cite this PR's investigation doc for further context.

Testing

movement 7.4.0 (Homebrew), Z3 4.11.2 (required — newer Z3 versions
trigger spurious failures in this codebase), Boogie via .dotnet/tools.

Before this PR (on m1):

error: caller `stake::distribute_rewards` specifies modify targets for
       `coin::CoinInfo` but callee `governed_gas_pool::withdraw_staking_reward`
       does not
{"Error": "Move Prover failed: exiting with bytecode transformation errors"}

After this PR, per shard:

Shard	Result
1	✓ Success (130 VCs)
2	⏱ Timeout — distribute_rewards (out of scope; see below)
3	✓ Success (119 VCs)
4	✗ 3 errors — reconfiguration::update_configuration ×2 + governed_gas_pool::fund (out of scope; see below)
5	✗ 1 error — system_addresses::is_core_resource_address (bv8/int8; out of scope)

The full-package run exits at the shard 2 timeout; per-shard reveals the
complete picture. The shard 2 timeout has the additional effect of
masking the shards 4 and 5 errors when the full prove runs. This is the
same dynamic PR #320 attempted to work around with
pragma verify_duration_estimate = 120; that workaround is intentionally
not included here — running it locally during development surfaced the
shards 4/5 errors as actual VC failures, confirming they exist and are
exactly the regression sites scoped as separate plan PRs.

Out of scope (separate follow-up PRs)

Each of the remaining failures has its own root cause and is worth a
dedicated PR. Brief enumeration:

• reconfiguration::update_configuration admin-override modeling.
  Two of the shard-4 errors (abort not covered, plus global invariant
  now_microseconds() >= last_reconfiguration_time broken by the admin
  override). Originating commit 12ff3b92dd ("fix epoch duration",
  2025-09-29) added the admin function without paired spec, and the
  function can violate the invariant by construction. Requires a real
  decision about what should be invariant under the admin bypass.
• governed_gas_pool::fund aborts_with completion. One shard-4
  error. primary_fungible_store::create_user_derived_object_address
  can abort with code 0x0 (counterexample uses an arithmetic-overflow
  amount); not currently in the aborts_with list. Likely a small fix.
• stake::distribute_rewards structural timeout. Shard 2. From
  what I've been able to work out, the timeout reflects genuine work
  the prover has to do: withdraw_staking_reward's transitive
  modify-surface is 10+ resource types via the FA-migration call chain.
  Viable fix paths (surgical opaque + curated modifies, abstract spec
  function modeling, upstream coordination) all look like "days of
  work" range to me. Happy to share more detailed analysis of what I
  tried in this branch (the pragma opaque experiment, schema
  simplification consideration) on request.
• system_addresses::is_core_resource_address bv8/int8.
  One shard-5 error. Post-condition result == (addr == @core_resources)
  is violated under the decommission_core_resources_enabled feature
  flag. Root cause is the bv8/int8 mismatch in
  features::contains's Boogie translation. Likely a prover-internals
  fix or a spec restructuring to avoid the broken codepath.

Visual: relationships between fixes, errors, and plan PRs

graph TD
    M1[m1 baseline] --> Cascade["Bytecode-transformation cascade<br/>(blocks all VC generation)"]

    Cascade -->|"<b>Drop</b><br/>(remove inaccurate<br/>modifies CoinInfo)"| BState["Cascade cleared<br/>3 VC errors visible"]
    Cascade -->|"<b>Broaden</b><br/>(add CoinStore modifies)<br/><i>REJECTED</i>"| BPrime["Dead end:<br/>wider cascade through<br/>coin::withdraw"]

    BState -->|"aptos_coin::initialize<br/>partial mode + TODO"| Step2[2 errors]
    Step2 -->|"aptos_coin::destroy_mint_capability_from<br/>new spec"| Step3[1 error]
    Step3 -->|"aptos_account::register_fa_and_apt<br/>partial mode + TODO"| Step4["surfaces gov_gas_pool::initialize<br/>precondition issue"]
    Step4 -->|"gov_gas_pool::initialize<br/>requires → aborts_if"| Checkpoint["This PR<br/>1 visible error: timeout"]

    Checkpoint -->|"Shard isolation"| Discovery{"Timeout masks 6<br/>more errors"}

    Discovery --> Shard2["Shard 2 timeout<br/>(distribute_rewards)"]
    Discovery --> Shard4["Shard 4<br/>3 errors"]
    Discovery --> Shard5["Shard 5<br/>3 errors"]

    Shard4 --> S4A["gov_gas_pool::fund<br/>abort code mismatch"]
    Shard4 --> S4B["reconfiguration::update_configuration<br/>abort not covered"]
    Shard4 --> S4C["reconfiguration global invariant<br/>now_us ≥ last_reconfig_time"]

    Shard5 --> S5A["find_delegation<br/>function does not abort"]
    Shard5 --> S5B["find_delegation<br/>abort not covered"]
    Shard5 --> S5C["is_core_resource_address<br/>post-condition fail"]

    Shard2 -.->|"out of scope"| FollowupTimeout["Structural timeout fix<br/>(separate PR)"]
    S4A -.->|"out of scope"| FollowupFund["gov_gas_pool::fund<br/>aborts_with completion"]
    S4B -.->|"out of scope"| FollowupReconfig["reconfiguration admin<br/>modeling"]
    S4C -.->|"out of scope"| FollowupReconfig
    S5A -.->|"<b>this PR</b>"| PR1Fix["@core_resources → @aptos_framework"]
    S5B -.->|"<b>this PR</b>"| PR1Fix
    S5C -.->|"out of scope"| FollowupG003["bv8/int8 in features::contains<br/>Boogie translation"]

    classDef done fill:#7c9c7c,stroke:#365636,color:#fff
    classDef checkpoint fill:#5e7a9b,stroke:#2c4a6e,color:#fff
    classDef pending fill:#c9a96e,stroke:#7a5f30,color:#000
    classDef dead fill:#9c7c7c,stroke:#5a3838,color:#fff

    class BState,Step2,Step3,Step4,PR1Fix done
    class Checkpoint checkpoint
    class BPrime dead
    class FollowupTimeout,FollowupFund,FollowupReconfig,FollowupG003 pending

Loading

Reviewers I'd suggest

• @ganymedio — original commit-blame trace; deepest context on the PR Chore: clean up Move compiler warnings and Move Prover errors #320 regressions
• @fEst1ck — was in the PR Chore: clean up Move compiler warnings and Move Prover errors #320 redirect discussion; decision-maker on prover-direction questions
• (cc as discussion grows)

Test plan

• movement move prove --package-dir aptos-move/framework/aptos-framework --dev per-shard (1, 3 succeed; 2 timeout; 4, 5 contain only out-of-scope regression-site errors)
• CI runs whatever validation the Movement aptos-core CI does on PRs (haven't checked which workflows trigger for spec-only changes)
• Reviewer confirmation of PR shape (this PR vs. split into per-module PRs)

[ganymedio]

@booleanfunction, this seems like a good improvement from #320, with the structural fixes and todos. What do you think is a good plan for the remaining failures? Maybe stacked PRs against this branch? Not sure that we should merge anything into m1 that has failures... so maybe we should PR against this branch with fixes until there's a solution that makes verification pass, and include a CI job for movement move prove that runs whenever the Move code is changed?

[booleanfunction]

Thanks @ganymedio — that's exactly the shape I was hoping for. To be explicit about intent: I opened this as a draft mainly to sanity-check the approach and share what I'd worked out, not to push toward an m1 merge. I'm definitely on the side of keeping this off m1 for now and continuing to explore on this branch (or stacked branches off it) before any merge decision.

A few of the remaining failures — the reconfiguration admin-override one especially — feel like they want a real design discussion before code, and the distribute_rewards timeout has several viable approaches with quite different trade-offs. I'd rather not commit to one of those in isolation; better to work through them here in the open.

Happy to defer the CI question to whoever has more context on the existing setup, but in principle a movement move prove job on Move-code changes seems like a clear win.

Will keep iterating here and ping when there's something new worth a look.