Please note: This master’s thesis presentation will take place in DC 2310 and online.
Dao Bo Yang, Master’s candidate
David R. Cheriton School of Computer Science
Supervisors: Professors Arie Gurfinkel, Richard Trefler
In this thesis, we demonstrate a significant empirical performance gain in the Move Prover, particularly in scenarios with highly branched borrowing structures, by reducing the verification complexity of ownership borrows from O(B^L) to O(BL), where B is the number of possible parent nodes and L is the length of the borrow chain. Traditionally, the Move Prover models these borrows through mutations, which represent copies of values and record borrowing relationships. This traditional representation faces the challenge of strictly identifying the exact parent node at each level of a subborrow, which significantly increases the complexity of write-back operations.
To resolve this, we adopt the prophecy variable model: a representation that constrains parent nodes’ values instead of using direct write-backs. All operations are resolved within the active scope, avoiding complex parent tracking and yielding the aforementioned complexity reduction. During our experiments, we also observed that the current implementation of global and update invariants in the Move Prover operates with limited regard for Move’s strict ownership rules, making the adoption of the prophecy variable model more complex. Consequently, we analyze how existing invariant architectures affect the adoption of this model.
To attend this master’s thesis presentation in person, please go to DC 2310. You can also attend virtually on MS Teams.