aptos prover - improving verification time

[MoonShiesty]

Discord user ID

moonshiesty

Describe your question in detail.

i have a function that im trying to specify, with a struct:

    struct OracleGlobalConfig has key {
        /// Pyth fee store
        pyth_fee_store: Coin<AptosCoin>,
        /// Smart vector holding all oracles
        all_oracles: SmartVector<Object<Oracle>>,
    }

when the function i want to specify borrows this struct, and does nothing else with it, it increases verification time from 14s to ~1000s, ie:

borrow_global_mut<OracleGlobalConfig>(@mirage_oracle);

why would simply borrowing from global stores increase verification time so much?

any tips for how to reduce verification time in cases like these?

[rahxephon89]

One possible reason is encoding of complicated data structure such as SmartVector in your case but sometime butterfly effect may also play a role: https://www.cs.cmu.edu/~csd-phd-blog/2024/mariposa/.
Improving the verification time is one of the most important issues we want to resolve.