move-language / move

Apache License 2.0
2.26k stars 689 forks source link

[move-prover] check data invariants for a &mut param ... #820

Closed meng-xu-cs closed 1 year ago

meng-xu-cs commented 1 year ago

... when and only when the param goes out of scope.

Previously, the approach is to check data invariants on every write-back to a &mut param. This is by definition more restrictive as this is essentially saying that data invariants are not allowed to be violated even temporarily in funciton body, which might not be a practical assumption (as shown in the newly added test case.)

Resolves https://github.com/move-language/move/issues/819

Motivation

Intuitive data invariant checking

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

CI, test cases updated