Module 0x1::mem

Module with methods for safe memory manipulation.

• Function swap
• Function replace
• Specification
  • Function swap
  • Function replace

Function swap

Swap contents of two passed mutable references.

Move prevents from having two mutable references to the same value, so left and right references are always distinct.

public fun swap<T>(left: &mut T, right: &mut T)

public native fun swap<T>(left: &mut T, right: &mut T);

Function replace

Replace the value reference points to with the given new value, and return the value it had before.

public fun replace<T>(ref: &mut T, new: T): T

public fun replace<T>(ref: &mut T, new: T): T {
    swap(ref, &mut new);
    new
}

Specification

Function swap

public fun swap<T>(left: &mut T, right: &mut T)

pragma opaque;
aborts_if false;
ensures right == old(left);
ensures left == old(right);

Function replace

public fun replace<T>(ref: &mut T, new: T): T

pragma opaque;
aborts_if false;
ensures result == old(ref);
ensures ref == new;