[move-prover] Ghost parameter for verification

[jyao15]

The Move prover now supports ghost variables in function specification. In some cases, we further need ghost variables that can be assigned in the function body, or in other words, ghost parameters. For example, the following program proves that after swapping the first and last element of a vector, the resulting vector is a permutation of the original vector.

fun swap_first_with_last(v : &mut vector<u64>, iperm : &mut vector<u64>) {
    let vlen = vector::length(v);
    spec {
        assume len(iperm) == vlen && (forall k in 0..vlen : iperm[k] == k);
        assume vlen >= 2;
    };
    vector::swap(v, 0, vlen - 1);
    vector::swap(iperm, 0, vlen - 1);
    spec {
        assert exists perm : vector<u64> : (len(perm) == vlen &&
            (forall k in 0..vlen : 0 <= perm[k] && perm[k] < vlen && v[perm[k]] == old(v)[k]) &&
            (forall k in 0..vlen, l in 0..vlen : k != l ==> perm[k] != perm[l]));
    }
}

Here, iperm acts as a trigger to instantiate exists perm .... It is introduced for verification only so it is natural to make iperm a ghost variable. However, a ghost variable currently cannot be updated in the function body (Line 8). Therefore, we have to declare iperm as a regular function parameter, which changes the function signature undesirably.

[rahxephon89]

#830 partially solves the issue by allowing updating global spec variables in the function body. However, local ghost variables are not supported yet.