Writing Flex Contracts

Flex contracts let you verify properties of your code with an SMT solver. In this tutorial you will write a basic contract, generalize it with parameters, watch the solver find a bug, and then fix it. For background on how SMT-based verification works and why it is more powerful than testing, see SMT-Based Verification in Flex.

Basic Flex Contracts

Here's an example of a basic Flex contract:

contract average_example_1 {
    let x: int32 = 10;
    let y: int32 = 20;
    let average: int32 = (x + y) / 2;
    assert (x <= average && average <= y)
        || (y <= average && average <= x);
}

Contracts begin with the contract keyword followed by a name and contain Flex code in its curly braces. Any code you could expect writing in a Flex function will be valid within a contract. A typical use would involve using the assert keyword to describe desirable properties about your code. This should be familiar to those who have written unit tests before. However, contracts will check more than just assertions.

You can think of a Flex contract as a statement that claims "this code doesn't fail." There are several ways Flex code can fail:

• An assert statement evaluates to false.
• A division by zero occurs.
• The discriminee of a match expression does not have a pattern that matches it.
• A struct or newtype is constructed that violates a field constraint.
• An array is indexed at a position out of bounds.

The contract average_example_1 checks that the average of the numbers 10 and 20 sits between 10 and 20. There are two possible points of failure: the division in the computation of average and the assert statement that follows.

Contracts with Parameters

Contracts can take parameters. The meaning of contracts that take parameters is "this code doesn't fail for any values of the parameters." Let's generalize average_example_1 from above to check that the average of any two numbers must sit between them.

contract average_example_2(x: int32, y: int32) {
    let average: int32 = (x + y) / 2;
    assert (x <= average && average <= y)
        || (y <= average && average <= x);
}

The SMT solver disproves this contract and informs us that when x = -1878786048 and y = -1878781949, the assert statement on line 13 does not hold. It turns out that these two numbers are so negative that their addition overflows the bounds of a 32-bit signed integer and wraps around to a positive number. A positive number certainly does not sit between two negative numbers.

Let's fix the contract to avoid any addition that can overflow:

contract average_example_3(x: int32, y: int32) {
    let average: int32 = x - x/2 + y/2;
    assert (x <= average && average <= y)
        || (y <= average && average <= x);
}

We can see the power of SMT-based verification at work! In a fraction of a second, we verified that this formula x - x/2 + y/2 for computing an average is safe for any pair of numbers x and y. To get that same level of certainty with black-box testing, we would need to manually test the property for all inputs. If testing a single input takes one nanosecond, then testing all 2⁶⁴ possibilities would take over 500 years!