is there a support of modifies keyword for framing?

[zpzigi754]

In Dafny, there is a support for frame which denotes a set of objects whose fields may be updated by the method, and is used with the keyword of modifies (https://dafny.org/latest/QuickReference).

I wonder whether there is a similar functionality in Verus which helps to track what has not been changed, what has been changed, etc.

[parno]

Verus takes advantage of Rust's type system, so that there is no need for a modifies clause. If a function takes in a mutable reference, then it can modify the value; if it takes in an immutable reference, then the code can't modify it.