Providing a Specification by Hand

This tutorial builds on the Getting Started with Scaffold tutorial.

In the previous chapter, we asked scaffold to generate a default specification in order to prove memory safety of a simple swap function. This tutorial builds upon the previous chapter by demonstrating how to manually provide a specification for swap that fully specifies the functions behavior. We assumes that the example/ directory has been initialized with scaffold init and that all the files of the previous chapter are still present.

We start by creating a copy of the swap function in a new cpp file src/stage2.cpp. The code is unchanged from the previous chapter:

#include <cstddef>

void swap(size_t& x, size_t& y) {
    size_t tmp = y;
    y = x;
    x = tmp;
}

To make sure scaffold understands the new file, we re-run our bear and clang combination command and add the newly created file.

$ bear -- clang -c src/stage1.cpp -c src/stage2.cpp

Since we updated compile_commands.json, we need to inform scaffold of the change using

$ scaffold gen

Now that scaffold understands how to build stage2.cpp, we proceed by running scaffold verify. This time, we will pass a --filename argument to ask scaffold to focus on a specific file.

$ scaffold verify --filename src/stage2.cpp

We select the swap function and then choose By hand, and press e to open an editor. scaffold pre-populates the temporary file with specifiers for the function arguments but leaves the rest to us. (\post emp indicates an trivial postcondition.)

\arg{x} "x" (Vref x)
\arg{y} "y" (Vref y)
\post emp

Building on the default specification that we inspected at the end of the previous chapter, we want to extend scaffold's bare-bones specification to properly specify a) the two function arguments of swap and their contents, as well as b) swap's precise postcondition, i.e. the fact it swaps the contents of its arguments. We thus change the provided specification to:

\arg{x_addr} "x" (Vptr x_addr)
\pre{x} x_addr |-> ulongR 1$m x 
\arg{y_addr} "y" (Vptr y_addr)
\pre{y} y_addr |-> ulongR 1$m y 
\post 
  x_addr |-> ulongR 1$m y **
  y_addr |-> ulongR 1$m x

Compared to the default specification from the previous chapter, we have made one important change as well as several small cosmetic changes to make the specification more idiomatic and easier to read.

Most importantly, we removed the existential quantifiers from the postcondition. Instead of merely requiring the references to contain any two numbers, we now specify exactly that the reference x must contain the initial value of y and vice versa.
To make the specification a bit more readable, we omit the types of our verification variables. The syntax \arg{x_addr} is shorthand for \arg{(x_addr : _)} which indicates to Rocq that it should infer the type from the variable's usage.
We introduce the verification variables for the references' contents (x and y) only where we first need them. Similarly to \arg{..}, the syntax \pre{..} generalizes the remaining specification over the variable(s) introduced between the curly braces.

We finish the process of manually providing this specification by saving the file and closing the editor, which brings us back to our interactive scaffold session. As before, select <DONE> to write the changes to disk.

This is all we need to have Rocq check this more precise specification. Given the simplicity of swap's code, BlueRock's proof automation makes short work of proving the function's correctness against the new specification.

$ dune b proof/stage2_cpp/

Having successfully checked our proof, we can now be certain that swap does indeed swap the contents of its two arguments.