---

Different modules perform work (calls, storage writes) and should pay fees that (a) can be split across modules, (b) are provably conserved (no hidden minting), and (c) are deterministic even across cross-module calls and reentrancy. On many chains gas is external, but for internal “service fees” you must manage accounting yourself.

Strategy

1. Implement a single canonical FeeSink resource that lives at a known address; only this module can mint/burn the fee token.
2. Use a linear FeeTicket created at entrypoint that threads through subcalls (or is passed explicitly) so every module that does fee-earning must consume/return the ticket — prevents duplication.
3. Make all fee operations atomic and update FeeSink via a single settle call at transaction end (or whenever you want to finalize), and store preconditions in spec to prove conservation.
4. Use sequence numbers / nonce to make fee payments replay-safe.

Why this works

• Linearity of FeeTicket ensures fee cannot be duplicated.
• Centralized sink with controlled mint/burn preserves conservation.
• Passing the ticket explicitly avoids hidden side-effects across modules.

Working-style Move package (conceptual)

module 0xA::fee {
    use std::signer;

    /// The canonical fee token (linear).
    struct FeeToken has store, drop { amount: u128 }

    /// FeeSink keeps accumulated fees under admin account
    struct FeeSink has key { collected: u128, admin: address, nonce: u64 }

    /// A FeeTicket must be obtained by a top-level caller and passed down to submodules
    /// to register earned fees. FeeTicket holds the remaining budget for the call.
    struct FeeTicket has key {
        remaining: u128,
        tx_nonce: u64
    }

    /// Initialize sink under admin
    public fun init(admin: &signer, start_collected: u128) {
        move_to(admin, FeeSink { collected: start_collected, admin: signer::address_of(admin), nonce: 0 });
    }

    /// Create a FeeTicket for a top-level transaction. This consumes no sink funds yet,
    /// but records a nonce for replay protection.
    public fun issue_ticket(caller: &signer, budget: u128) acquires FeeSink {
        assert!(budget > 0, 1);
        let sink_addr = 0xA; // admin stored here; adapt as needed
        let s = borrow_global_mut<FeeSink>(sink_addr);
        s.nonce = s.nonce + 1;
        FeeTicket { remaining: budget, tx_nonce: s.nonce }
    }

    /// Submodules call this to claim part of the ticket. This consumes from the ticket and
    /// returns a small FeeToken to the module to prove claim handling. The FeeToken is linear.
    public fun claim(ticket: &mut FeeTicket, claim_amt: u128): FeeToken {
        assert!(claim_amt > 0 && ticket.remaining >= claim_amt, 2);
        ticket.remaining = ticket.remaining - claim_amt;
        FeeToken { amount: claim_amt }
    }

    /// Module that earned fees returns FeeToken to the sink (settle).
    public fun settle_to_sink(admin: &signer, t: FeeToken) acquires FeeSink {
        let s = borrow_global_mut<FeeSink>(signer::address_of(admin));
        s.collected = s.collected + t.amount;
        // t consumed by function arguments (linear)
    }

    /// Finalize: any unused ticket budget can be optionally returned or burned.
    public fun finalize_ticket(admin: &signer, ticket: FeeTicket) acquires FeeSink {
        // Ticket being moved here consumes it; unused portion is burned or credited per policy.
        let s = borrow_global_mut<FeeSink>(signer::address_of(admin));
        s.collected = s.collected + ticket.remaining;
        // ticket consumed
    }

    /////////////////////////////
    // Example usage flow (conceptual)
    /////////////////////////////
    // 1. Top-level caller obtains ticket = issue_ticket(caller, 100)
    // 2. call module A: feeA = claim(&mut ticket, 30); module A does work
    //    module A returns feeA: settle_to_sink(admin, feeA)
    // 3. call module B: feeB = claim(&mut ticket, 20); module B returns feeB
    // 4. finalize_ticket(admin, ticket) => leftover 50 credited to sink
}

Spec & proofs (advice)

• Add spec invariants that collected equals sum of all settled amounts + burned leftovers and is non-negative.
• Prove no ticket duplication by showing FeeTicket is linear and claim only reduces remaining.
• Prove replay-safety: each issued ticket carries a unique tx_nonce from the sink that you verify in any API requiring the ticket; if a client attempts to reuse a ticket nonce, the sink’s nonce will have moved forward.

---