Summary
The Move Prover does not currently support verifying code that stores function values (closures) in resources and later calls them. The Boogie backend fails to generate correct memory label declarations when specs reference stored function values via behavioral predicates (result_of, aborts_of, ensures_of).
Example
See third_party/move/move-prover/tests/inference/calculator.exp.move — a calculator that stores operations as |u64|u64 closures in a State::Continuation variant. Spec inference produces correct-looking specs, but verification fails with Boogie compilation errors (undeclared memory label identifiers) because the backend doesn't handle the intermediate states needed for stored function value invocation.
Expected behavior
Verification should succeed for code that stores and invokes function values in resources, provided specs are correct.
Summary
The Move Prover does not currently support verifying code that stores function values (closures) in resources and later calls them. The Boogie backend fails to generate correct memory label declarations when specs reference stored function values via behavioral predicates (
result_of,aborts_of,ensures_of).Example
See
third_party/move/move-prover/tests/inference/calculator.exp.move— a calculator that stores operations as|u64|u64closures in aState::Continuationvariant. Spec inference produces correct-looking specs, but verification fails with Boogie compilation errors (undeclared memory label identifiers) because the backend doesn't handle the intermediate states needed for stored function value invocation.Expected behavior
Verification should succeed for code that stores and invokes function values in resources, provided specs are correct.