Goose: Contracts

Contracts are pre-conditions and post-conditions attached to functions, which are checked during compilation. This is inspired by the dafny and the whiley languages.

The preconditions and post conditions are checked using the z3 smt solver.

This is currently where the implementation work is focused. The current state is that it can successfully verify contracts for functions that don't contain loops or bitwise operations, only on integer and bool types.

Each function can define any number of pre conditions with the "requires" keyword, and post conditions with the "ensures" keyword. The later can refer to the function's returned value as '@'.

At the points where a function returns, we check that we can't satisfy that its precondition is false. If we can, it means there exists a counter example where the precondition will be violated.

For example, if we comment out the if that reorders a and b in the following function:

sint(32) testFunc( sint(32) a, sint(32) b )
    requires [ a != b ]
    ensures [ @ > 0 ]
{
    var ta, var tb = a,b

    //if ta < tb
    //    ta,tb = tb,ta

    return ta - tb
}

We obtain the following error:

tests/noprelude/diagnostics/compile-verif-test-2.g:
    3 |     ensures [ @ > 0 ]
      |               ^~~~~
      |     Error: assertion failure.
     ...
   12 |     return ta - tb
      |            ~~~~~~~
      |      When returning this.

When a function is called, we likewise verify that we are honoring its preconditions.

If we comment the requirement that a is non 0 in the following function:

sint(32) testFunc2( sint(32) a )
    requires [ a != 0 ]
    //ensures [ @ != 0 ]
{
    return testFunc( a, 2*a )
}

We obtain the following error:

tests/noprelude/diagnostics/compile-verif-test-3.g:
    2 |     requires [ a != b ]
      |                ^~~~~~
      |       Error: assertion failure.
     ...
   20 |     return testFunc( a, 2*a )
      |            ~~~~~~~~~~~~~~~~~~
      |              At this call.

It is also possible to check for some condition anywhere in a function by calling the assert builtin function. It is named this way to be consistent with how it is named in other languages with similar features, however it is different from the classic C/C++ assert function: it only requests a static check of the condition and doesn't result in any code to be emitted.

Since verifying programs in undecidable, there are many cases where this will fail to reach a decision. Therefore, the system requires an escape hatch. The current idea is to have an "assume" statement which instructs the solver to accept a specified condition as true, and in addition emits a runtime check and error message (like C/C++ assert), probably only in debug builds.

This way, even in cases where the system can't prove things at compilation time, it will degrade into an assistant pointing out where a run time assert check is necessary, which is also useful.

The next step will be to handle loops. k-induction seems like a good and relatively simple method.

Further steps will be to flesh out type handling, among other things by using bitvecs where necessary to work with bitwise operations.

Also, this will require lots and lots and lots of tests.

An interesting future extension would be to attach requirements to types, to implement refinement types.

Some interesting applications of this are non-null constraints checks on pointers and checking object lifetime constraints.

Goose Contracts