---

By changing code but must preserve storage invariants (no data loss, no invariant breaks). Move modules are usually immutable after publishing; upgrades are typically implemented by proxy patterns, limited-versioned storage, or migration scripts that carefully transform on-chain state.

Strategy

1. Use a proxy module that holds canonical data (resources) and delegates logic calls to an implementation module address/version.
2. Store an explicit version and migration_state resource to coordinate safe migrations.
3. Provide migrate_vN_to_vN+1 functions in the new implementation that the proxy calls; make migration functions idempotent and proof-checked via spec invariants.
4. Use capability checks so only a governance/admin address can upgrade or run migrations.
5. Write spec lemmas in the new module that prove the migration preserves invariants (e.g., balances sum, non-negativity).

Working-style code (proxy + implementation + migration)

// Proxy module at 0xA::proxy_token — storage is here and persistent across upgrades.
module 0xA::proxy_token {
    use std::signer;
    use std::vector;
    use std::option;

    // Admin who can upgrade / trigger migrations
    struct Admin has key { addr: address }

    // Persistent storage
    struct TokenStore has key {
        balances: vector<(address, u128)>, // simple illustrative mapping
        total_supply: u128,
    }

    // Which implementation to delegate to (module id + version marker)
    struct ImplRef has key {
        impl_addr: address, // address of implementation module
        version: u64,
    }

    public fun init(admin: &signer, impl_addr: address) {
        move_to(admin, Admin { addr: signer::address_of(admin) });
        move_to(admin, TokenStore { balances: vector::empty(), total_supply: 0u128 });
        move_to(admin, ImplRef { impl_addr, version: 1u64 });
    }

    /////////////////////////////////////
    // Delegation entrypoints (very thin)
    /////////////////////////////////////
    public fun mint(admin: &signer, to: address, amt: u128) acquires ImplRef, TokenStore {
        // authorization
        let impl = borrow_global<ImplRef>(signer::address_of(admin));
        // delegate: call implementation's mint function by using a known interface.
        // In Move you call by module path; proxy knows the impl address.
        // Example: call 0xB::impl_v1::mint_impl(...) — but proxy must import the impl module at compile time.
        // To support multiple impls you'd switch on impl.impl_addr and call the correct function.
        // Here we show the pattern for a single friend impl at 0xB.
        0xB::impl_v1::mint_impl(signer::address_of(admin), to, amt);
    }

    public fun set_impl(admin: &signer, new_impl_addr: address, new_version: u64) acquires ImplRef, Admin {
        let a = borrow_global<Admin>(signer::address_of(admin));
        assert!(a.addr == signer::address_of(admin), 1);
        let r = borrow_global_mut<ImplRef>(signer::address_of(admin));
        r.impl_addr = new_impl_addr;
        r.version = new_version;
    }

    /////////////////////////////////////
    // Storage access helpers (implementation calls these)
    /////////////////////////////////////
    public friend 0xB::impl_v1;
    public fun get_store(addr: address): &mut TokenStore acquires TokenStore {
        borrow_global_mut<TokenStore>(addr)
    }
}

// Implementation v1 (0xB::impl_v1) — contains logic and migration entrypoints
module 0xB::impl_v1 {
    use std::signer;
    use std::vector;

    // Mint implementation will directly update storage owned by proxy (friend).
    public fun mint_impl(proxy_admin: address, to: address, amt: u128) {
        // Here we assume proxy exposes friend accessors and the storage is stored under admin address
        let store = 0xA::proxy_token::get_store(proxy_admin);
        // very naive balance update for demo; use map in prod.
        vector::push_back(&mut store.balances, (to, amt));
        store.total_supply = store.total_supply + amt;
    }

    ////////////////////////////
    // Migration entrypoint for v1 -> v2
    ////////////////////////////
    // Suppose v2 changes representation: we need an idempotent migration function.
    public fun migrate_v1_to_v2(proxy_admin: address) {
        // 1) Read old store
        let store = 0xA::proxy_token::get_store(proxy_admin);
        // 2) Create any auxiliary storage needed by v2, copy state carefully.
        // For safety: make the migration idempotent by checking a migration marker in proxy storage
        // (not shown) or by designing migration to be a no-op if already applied.
        // Example check (pseudo):
        // if (!migrated) { perform migration; mark migrated; }
    }
}

How this preserves invariants

• Storage never moves addresses — data stays under proxy_token::TokenStore so external references to that resource remain valid after upgrade.
• New implementation provides migrate_* functions that are explicit and idempotent; the proxy admin triggers them and can verify results.
• spec blocks in impl_v2 should assert total_supply equals sum(balances) before and after migration — this is how the Move Prover can be used to check migration correctness.

Practical recommendations

• Keep storage layout stable where possible. If layout must change, migrate piecewise and leave a rollback or checkpoint.
• Use small, well-tested migration scripts and unit tests (#[test]) that run init → prepopulate → migrate → assert invariants.
• Limit upgrade privileges to a multisig/governance contract to reduce centralized risk.

---