Goose  Program verification

Goose aims to implement a powerful but practical compilation-time program verification system, inspired by languages such as Dafny and Whiley.

This is implemented on a per function basis, by taking the CFG built by the parsing process and converting it into formulas for the z3 solver, which is used to try and find counter-examples for any requirement or compilation time assertion.

Loops are verified by applying the "combined-case k-induction" algorithm, as described in this paper.

Since verifying programs is undecidable, there will be cases where correct programs will be rejected. Currently, the goose language hopes that offering the two following approaches will be enough to handle these situations:

The first appproach is to move undecidable checks to runtime. In other words, to enclose them in a if statement and handle either outcome at runtime. Within the branches of the if, the condition will be assumed to be either true or false, therefore removing the need for the solver to figure it out during compilation.

The second one, for cases where the above would be an unacceptable waste of performances, is an "assume" statement that allows the programmer to dictate to the solver that a certain condition is to be assumed to be true from that point on, probably at the cost of a runtime assertion check to be inserted in debug builds. This is obviously a trade of of correctness to performance, and as such would be restricted to an "unsafe", optional subset of the language (together with pointers, poiter arithmetics, and such)

Program verification, in practice, takes the form of a few features: assert builtin function, function contracts (pre-conditions and post-conditions), and refinement types. All of these are just different locations where the programmer can add conditions that are to be verified during compilation.

Assert builtin function

The assert builtin function requests a compilation-time check to be performed at any point in the program.

void someFunc( sint(32) a )
{
    if( a > 0 )
    {
        assert( a != 0 ) // Ok: we can only reach this if a > 0
    }

    assert( a != 0 ) // Error: there is nothing that allows us to know that a can't be 0 here
}

Function contracts

Functions and function types can specify pre-conditions and post-conditions. They are checked both inside of the function itself, to verify that its return value upholds the post-conditions, and at function calls, to make sure that the values passed to functions meet their preconditions. In post-conditions, the return value of the function can be refered to as @result.

sint(32) someFunc( sint(32) a, sint(32) b )
    requires // pre-conditions
    [
        a >= b
        a != 0
    ]

    ensures // post-conditions
    [
        @result > 0
        @result < 10
    ]
{
    ...
}

Refinement types

Almost all types can have predicates attached to them by using the where operator. Inside of those predicates, the value can be refered to as @val. The following is equivalent to the above:

sint(32) where [@val>0 @val<10] someFunc( sint(32) where [@val != 0] a, sint(32) b )
    requires // pre-conditions
    [
        a >= b
    ]
{
    ...
}

This is verbose but can easily be shortened by creating type aliases:

using ItemCount = sint(32) where [@val>0 @val<100]

Implementation status

The general architecture and most of the feature is up and running, even though it only has been exercised against small test programs so far.

Many things are also currently missing:

• the "assume" statement is not yet implemented.
• type predicates on local variable types are not checked.
• only booleans, signed integers and unsigned integers are handled so far by the verifier.
• when passing function as values, their contracts are not checked against the the parameter function type's contract.
• special operators for verification conditions need to be implemented, such as "implies" to be able to specify post-conditions that depend on the input values of functions.