Formal Verification

The Move language is designed to support formal verifications against specifications. Currently, there are a number of these written for the liquidswap::math module. We encourage further verification of contract functions as well as some improvements to current specifications. Here are some examples.

liquidswap::math

First, the specification for math::overflow_add could be improved. The purpose of this function is to add u128 integers, but allowing for overflow.

spec overflow_add {
    ensures result <= MAX_U128;
    ensures a + b <= MAX_U128 ==> result == a + b;
    ensures a + b > MAX_U128 ==> result != a + b;
    ensures a + b > MAX_U128 && a < (MAX_U128 - b) ==> result == a - (MAX_U128 - b) - 1;
    ensures a + b > MAX_U128 && b < (MAX_U128 - a) ==> result == b - (MAX_U128 - a) - 1;
    ensures a + b <= MAX_U128 ==> result == a + b;
}

However, this does not reflect how the function should work conceptually. Instead, consider the following specification:

spec overflow_add {
    /// The function should never abort.
    aborts_if false;

    /// Addition should overflow if the sum exceeds `MAX_U128`
    ensures result == (a + b) % (MAX_U128 + 1);
}

This checks that the function cannot abort and makes the desired functionality more clear.

liquidswap::emergency

Another strong application for the prover is in liquidswap::emergency. This module provides a way to pause and resume operations as well as a way to disable itself. The emergency::disable_forever function is intended to be permanent, and that can actually be proven:

spec liquidswap::emergency {
    invariant update old(is_disabled()) ==> is_disabled();
}

Essentially, this claims that across updates to storage, the emergency module cannot change from disabled to enabled.