proof functions

Consider the pub closed spec min function from the previous section. This defined an abstract min function without revealing the internal definition of min to other modules. However, an abstract function definition is useless unless we can say something about the function. For this, we can use a proof function. In general, proof functions will reveal or prove properties about specifications. In this example, we’ll define a proof function named lemma_min that reveals properties about min without revealing the exact definition of min. Specifically, lemma_min reveals that min(x, y) equals either x or y and is no larger than x and y:

mod M1 {
    use builtin::*;

    pub closed spec fn min(x: int, y: int) -> int {
        if x <= y {
            x
        } else {
            y
        }
    }

    pub proof fn lemma_min(x: int, y: int)
        ensures
            min(x, y) <= x,
            min(x, y) <= y,
            min(x, y) == x || min(x, y) == y,
    {
    }
}

mod M2 {
    use builtin::*;
    use crate::M1::*;

    proof fn test() {
        lemma_min(10, 20);
        assert(min(10, 20) == 10); // succeeds
        assert(min(100, 200) == 100); // FAILS
    }
}

Like exec functions, proof functions may have requires and ensures clauses. Unlike exec functions, proof functions are ghost and are not compiled to executable code. In the example above, the lemma_min(10, 20) function is used to help the function test in module M2 prove an assertion about min(10, 20), even when M2 cannot see the internal definition of min because min is closed. On the other hand, the assertion about min(100, 200) still fails unless test also calls lemma_min(100, 200).

proof blocks

Ultimately, the purpose of spec functions and proof functions is to help prove properties about executable code in exec functions. In fact, exec functions can contain pieces of proof code in proof blocks, written with proof { ... }. Just like a proof function contains proof code, a proof block in an exec function contains proof code and can use all of the ghost code features that proof functions can use, such as the int and nat types.

Consider an earlier example that introduced variables inside an assertion:

fn test_consts_infer() {
    let u: u8 = 1;
    assert({
        let i: int = 2;
        let n: nat = 3;
        0 <= u < i < n < 4
    });
}

We can write this in a more natural style using a proof block:

fn test_consts_infer() {
    let u: u8 = 1;
    proof {
        let i: int = 2;
        let n: nat = 3;
        assert(0 <= u < i < n < 4);
    }
}

Here, the proof code inside the proof block can create local variables of type int and nat, which can then be used in a subsequent assertion. The entire proof block is ghost code, so all of it, including its local variables, will be erased before compilation to executable code.

Proof blocks can call proof functions. In fact, any calls from an exec function to a proof function must appear inside proof code such as a proof block, rather than being called directly from the exec function’s exec code. This helps clarify which code is executable and which code is ghost, both for the compiler and for programmers reading the code. In the exec function test shown below, a proof block is used to call lemma_min, allowing subsequent assertions about min to succeed.

mod M1 {
    use builtin::*;

    pub closed spec fn min(x: int, y: int) -> int {
        if x <= y {
            x
        } else {
            y
        }
    }

    pub proof fn lemma_min(x: int, y: int)
        ensures
            min(x, y) <= x,
            min(x, y) <= y,
            min(x, y) == x || min(x, y) == y,
    {
    }
}

mod M2 {
    use builtin::*;
    use crate::M1::*;

    fn test() {
        proof {
            lemma_min(10, 20);
            lemma_min(100, 200);
        }
        assert(min(10, 20) == 10);  // succeeds
        assert(min(100, 200) == 100);  // succeeds
    }
}

assert-by

Notice that in the previous example, the information that test gains about min is not confined to the proof block, but instead propagates past the end of the proof block to help prove the subsequent assertions. This is often useful, particularly when the proof block helps prove preconditions to subsequent calls to exec functions, which must appear outside the proof block.

However, sometimes we only need to prove information for a specific purpose, and it clarifies the structure of the code if we limit the scope of the information gained. For this reason, Verus supports assert(...) by { ... } expressions, which allows proof code inside the by { ... } block whose sole purpose is to prove the asserted expression in the assert(...). Any additional information gained in the proof code is limited to the scope of the block and does not propagate outside the assert(...) by { ... } expression.

In the example below, the proof code in the block calls both lemma_min(10, 20) and lemma_min(100, 200). The first call is used to prove min(10, 20) == 10 in the assert(...) by { ... } expression. Once this is proven, the subsequent assertion assert(min(10, 20) == 10); succeeds. However, the assertion assert(min(100, 200) == 100); fails, because the information gained by the lemma_min(100, 200) call does not propagate outside the block that contains the call.

mod M1 {
    use builtin::*;

    pub closed spec fn min(x: int, y: int) -> int {
        if x <= y {
            x
        } else {
            y
        }
    }

    pub proof fn lemma_min(x: int, y: int)
        ensures
            min(x, y) <= x,
            min(x, y) <= y,
            min(x, y) == x || min(x, y) == y,
    {
    }
}

mod M2 {
    use builtin::*;
    use crate::M1::*;

    fn test() {
        assert(min(10, 20) == 10) by {
            lemma_min(10, 20);
            lemma_min(100, 200);
        }
        assert(min(10, 20) == 10); // succeeds
        assert(min(100, 200) == 100); // FAILS
    }
}