Prophecy Variables and Invariants in the Move Prover

Abstract

In this paper, 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(BL) to O(BL), where B is the number of possible parent nodes and L is the length of the borrow chain. In our benchmark tests evaluating conditional borrow and update operations within the Move Prover (L = 2, B = 8), the original model required 42 seconds to complete verification, whereas our proposed model finished in under 2 seconds. The Move Prover models these borrows through mutations, which represent copies of values and record borrowing relationships. This representation faces the challenge of strictly identifying the exact parent node at each level of a sub-borrow, which significantly increases the complexity of direct write-back operations. We resolve this through the adoption of the prophecy variable model: a representation that constrains parent node 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.