Jianan Yao

The [verify_sort.move](https://github.com/move-language/move/blob/main/language/move-prover/tests/sources/functional/verify_sort.move) test program implements a vector sorting algorithm. Currently the vector length is set to 45 and the program is successfully verified by Move. When we change the length...

[move-prover] Ghost parameter for verification

1

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,...

Consider the following protocol. ``` type node relation active(N:node) type int_t interpret int_t -> int individual num_active : int_t after init { active(N) := false; num_active := 0; } action...