How to use update in the contract specifications?

[0x-j]

Asked by .ansonpro on discord in move-language, I only found very little doc about update

---

Hi, I am trying to use move prover like stake.move in aptos-core repo line 442.
My code is :

let (shareholders_address, vesting_records) = simple_map::to_vec_pair(vesting_contract.shareholders);
spec {
    update ghost_address_num = len(shareholders_address);
    update ghost_records_num = len(vesting_records);
};

And the prover gives me the following error:

error: target of update restricted to specification variables
  ┌─ <internal>:1:1
  │
1 │ <internal>
  │ ^^^^^^^^^^

Can anyone share some insight on how to use update keyword in move source code to define ghost variable for loop invariant?

[rahxephon89]

Thanks for the question. The ghost variables are defined at the spec of the module. For instance, ghost variables for the spec of the stake module is defined in stake.spec.move:

    spec module {
        pragma verify = true;
        // ...
        // ghost variable
        global ghost_valid_perf: ValidatorPerformance;
        global ghost_proposer_idx: Option<u64>;
        global ghost_active_num: u64;
        global ghost_pending_inactive_num: u64;
    }