How hard can writing C code actually be?

Well, why don't we have a look.

Let's consider the following snippet — a simple, standard, procedure to copy a linked list:

void listcopy(void **r) {
  void *x2 = *r;
  if (x2 == NULL) {
    return;
  } else {
    int vx22 = *(int *)x2;
    void *nxtx22 = *((void **)x2+1);
    *r = nxtx22;
    listcopy(r);
    void *y12 = *(void **)r;
    void *y2 = (void *) malloc(2 * sizeof(void *));
    *r = y2;
    *((int *)y2) = vx22;
    *((void **)y2+1) = y12;
    return;
  }
}

Surely, that's not too hard to understand? After all, it's just a bit of pointer twiddling, a malloc or two, and a single recursive call - what could be more simple?

Do you understand how this code works?

Are you sure?

Would you have been able to tell if I removed one of the statements? (or have I already removed a statement and just not told you?).

The point I'm trying to make here is that pointer-manipulating code can often be complex and convoluted, even for simple operations such as copying a linked list. These kinds of complexities provide ample opportunity for bugs to sneak in, and can make it difficult to trust code written by C-developers.

As it turns out, this is in fact possible! In our latest research - "Certifying the synthesis of heap-manipulating programs" by Yasunari Watanabe, myself, George Pîrlea, Nadia Polikarpova, and Ilya Sergey, we tentatively answer this question in the affirmative, developing a novel tool (available here) for automatically synthesising completely correct C-code in a mere matter of seconds. Additionally, to provide trust in the generated code, inspired by early work on proof-carrying-code, the tool also outputs independently verifiable proof-certificates for each synthesised program, which then formally guarantee that the generated code must satisfy its functional specifications. These certificates are written in Coq, a well-established formal proof assistant that has been used for several significant developments in mathematics and software engineering (CompCert, CertiKOS etc.), and serves as one of the de-facto means that humanity has to ensure absolute correctness of code.

In fact, the code written above was actually entirely automatically synthesised by our tool, along with a proof certificate, formally guaranteeing its correctness. As end users of the tool, we didn't even have to bother reasoning about how exactly it did its pointer manipulations, and instead could rely on the formal certificate to guarantee that it would indeed correctly copy a linked list.

In other words, given a specification to copy a list, our synthesis tool was able to produce a complete self-contained C program with a separate independent proof certificate, formally guaranteeing, without a shadow of a doubt, that it fully satisfies the specification, thereby removing any need to trust a fallible human developer.

This is the future of coding!

So how on earth does this work? Is it Machine Learning? GPT3? Some advanced form of GOFAI?

As it turns out, this actually all just boils down to a rather clever composition of various aspects of Programming Languages theory - in particular, separation logic, deductive synthesis and constructive proofs.

In the rest of this post, we'll provide a high-level overview of this work, starting with an introduction to theory on which this research builds, the general technique used to construct certified C programs and finally discussing the limitations and potential directions in which this work could be extended.

Warning: What you are about to read is bleeding-edge research. The following is a sneak peak of what the future will look like, but it may be a while before it will reach end users.

Naturally, given our desire to reason about heap-manipulating programs, the core building block of separation logic is this notion of a points-to relation.

We write x :-> y, read as "x points to y", to denote the fact that the memory address x maps to a memory cell containing the value y.

Different variations of separation logic have different choices of specific notation — here, for simplicity, we'll introduce some additional notation to allow explicitly referencing contiguous blocks of memory.

We write [x; n] to denote the fact that the the memory address x maps to the start of a block of n contiguous cells in memory.

We can then specify the individual values of each of these cells by adding an offset index - i.e. (x + i) :-> a.

These are typically referred to as spatial assertions or heap assertions, as they each assert some kind of property on the heap.

All that I've presented so far probably seems pretty straightforward, however there's one additional component that we're still missing - in particular, a mechanism for composing spatial assertions together, and this is exactly where the true novelty of separation logic lies.

When we start trying to compose spatial assertions together, we start to have to reason about how these assertions may influence each other, and this can cause problems.

So far, we've assumed that each spatial assertion, i.e. x :-> y, asserts that some particular property holds over the heap, in this case that the memory address x contains the value y.

The problem with this reasoning is that if each spatial assertion holds over the entire heap, then checking the validity of a arbitrary collection of spatial assertions can become very hairy, as it requires one to reason about all the assertions at once and determine if they hold over the entire heap. In particular, the issue is that this model lacks compositionality.

To fix this problem, separation logic instead proposes that spatial assertions apply over subsets of the entire heap, and introduces a special construct, the separating conjunct, to allow denotating that assertions hold over disjoint subsets of the heap.

The separating conjunct, written P ** Q, is conceptually fairly simple. All it asserts is that there exists some partitioning of the entire heap, such that one can make spatial assertions P and Q both true. This then restores compositionality of analysis, as we can reason about individual assertions independently, as they must, by definition, apply to disjoint subsets of the heap.

The final relevant part of separation logic for this work is a notion of spatial predicates which build on top of the basic foundations we've covered so far to allow logicians to encode more complex heap-based data structures.

As an example, consider the implementation of a spatial predicate linked_list for encoding linked lists:

linked_list(x,S) = 
  | x == NULL -> emp; S = {}
  | x != NULL -> 
      [x;2] ** x :-> v ** (x + 1) :-> y 
        ** linked_list(y, S'); S = {v} ++ S'

Our predicate linked_list(x,S) asserts that the memory address x denotes the start of a linked-list with contents denoted by the set S.

To do this, it considers two separate cases:

• Case 1: x == NULL, the base case, the empty list, which contains no elements, so set S must be empty.
• Case 2: x != NULL, the inductive case, where x is not NULL, and so:
  • x maps to a 2-element block of memory, where the first element is some value v from the set, and the second element contains a memory location y
  • y itself is the head of another linked list linked_list(y, S') which contains the remaining elements of the list S'.

As we can see, this simple spatial predicate is thereby able to capture any and all possible linked lists that could be constructed, by simply choosing the correct parameters and cases for each element of the list:

Putting all these components together, we now have a fairly expressive logic, which we can use to completely specify the behaviours of many standard C programs.

Now we have a better understanding of separation logic, we can try and formulate some kind of specification for list copy, to construct the synthesis task from the introduction.

// r :-> x ** linked_list(x,S)
void listcopy(void **r)
// r :-> y ** linked_list(y,S) ** linked_list(x,S)

In the above specification the comment before the function declaration specifies the pre-condition, the spatial assertions that are required to be true in order to call the operation, and the comment after represents the post-condition, the spatial assertion guaranteed to hold after executing the method.

Using the notations and definitions we covered earlier, we can now decipher each of these annotations fairly easily back into natural language:

Precondition

asserts that the argument r must map to a cell containing a memory location x, and that location must denote the start of a linked list linked_list(x,S).

Postcondition

then asserts that after execution, r should now map to a cell containing a memory location y, and that location must denote the start of a new linked list linked_list(y,S), with the original linked list linked_list(x,S) still present on the heap.

In summary, listcopy, given a pointer to a linked list, must ensure that after executing the heap must contain two copies of the original list — i.e. listcopy must copy a list.

The core idea with deductive synthesis is to use specifications in separation logic to act as a guide during the synthesis process. This approach turns out to be quite efficient, because often the specifications found during synthesis can uniquely determine the program statements that are required to satisfy them.

As an example, let's work through the example of synthesising a swap function:

// x :-> a ** y :-> b
void swap(int *x, int *y)  { ??? }
// x :-> b ** y :-> a

The goal for the synthesizer during the synthesis is to iteratively emit program statements that gradually change the pre and post-conditions, until they are eventually equal, at which point the synthesis is complete.

At the start, as the variables a and b are not accessible by the program (as they are stored within the cells denoted by both pointers), the only operation that the synthesis procedure can do is to emit read operations to load their values:

void swap(int *x, int *y)  {
    int a = *x;
    int b = *y;
// x :-> a ** y :-> b
    ???
}
// x :-> b ** y :-> a

Now that a and b are accessible, the synthesizer can try to unify individual spatial assertions in the pre and post-conditions by using their values.

For example, we can unify the assertions x :-> a in the pre-condition and x :-> b in the post-condition by simply emitting a write to x:

void swap(int *x, int *y)  {
    int a = *x;
    int b = *y;
    *x = b;
// x :-> b ** y :-> b
    ???
}
// x :-> b ** y :-> a

From here, if we repeat the same analysis for y :-> a, the synthesizer emits a write to y, and we are left with:

void swap(int *x, int *y)  {
    int a = *x;
    int b = *y;
    *x = b;
    *y = a;
// x :-> b ** y :-> a
    ???
}
// x :-> b ** y :-> a

At this point, the pre and post-condition are now equal, and so the synthesis is complete, leaving us with a complete standalone program:

void swap(int *x, int *y)  {
    int a = *x;
    int b = *y;
    *x = b;
    *y = a;
    return;
}

It just so happens that this same reasoning procedure presented above for synthesising swap actually scales quite well, and can be directly used to verify more complex programs like list copy.

To illustrate how well this works let's have a look at the process of synthesising the base case of list copy from before:

// r :-> x ** linked_list(x,S)
void listcopy(void **r) {
  ???
}
// r :-> y ** linked_list(y,S) ** linked_list(x,S)

Following the same reasoning as before, the synthesis starts by emitting a read operation:

void listcopy(void **r) {
  void *x2 = *r;
// r :-> x2 ** linked_list(x2,S)
  ???
}
// r :-> y ** linked_list(y,S) ** linked_list(x2,S)

In order to proceed further, the synthesis must unfold the definition of the heap predicate for linked lists, and this naturally translates into an if-else-statement for each case of the predicate:

void listcopy(void **r) {
  void *x2 = *r;
  if (x2 == NULL) {
    // r :-> x2 ** emp; x2 == NULL && S = {}
    ???
    // r :-> y ** linked_list(y,S) ** linked_list(x2,S)
  } ...
}

For the base-case, the synthesis procedure can propagate the equalities, x2 == NULL and S = {}, that the constructor exposes across both the pre and post-condition without having to emit any new statements:

void listcopy(void **r) {
  void *x2 = *r;
  if (x2 == NULL) {
    // r :-> NULL ** emp
    ???
    // r :-> y ** linked_list(y,{}) ** linked_list(NULL,{})
  } ...
}

At this point, the synthesis procedure notices that the linked_list(y,{}) predicate can be satisfied by instantiating y with NULL:

void listcopy(void **r) {
  void *x2 = *r;
  if (x2 == NULL) {
    // r :-> NULL ** emp
    ???
    // r :-> NULL ** emp
  } ...
}

At this point, the pre and post-conditions are equal, and so the synthesis procedure knows that it has successfully synthesised the base case of the function:

// r :-> x ** linked_list(x,S)
void listcopy(void **r) {
  void *x2 = *r;
  if (x2 == NULL) {
    return;
  } ...
}
// r :-> y ** linked_list(y,S) ** linked_list(x,S)

A similar search procedure can be done on the inductive case as well, and eventually leads to the original code presented in the introduction. The SuSLik paper also demonstrates this technique can be used to synthesise a variety of other complex algorithms, such as tree flattening, sorting, binary search trees etc.

Broadly speaking, there are two possible approaches one could take to certified synthesis – either that of certifying the synthesizer, or producing proof certificates.

Certified Synthesizer

The core idea with this approach is to encode the source code of the synthesizer itself with an formal setting and then prove additional properties about the validity of its synthesis procedure, such as ensuring that the programs it outputs will always satisfy the specifications that they are generated from.

Proof Certificates

An alternative approach to certified synthesis, first developed by early research work on proof-carrying code, is extend the synthesis procedure to also produce proofs of correctness for the synthesised programs. This way, users of the synthesised program can verify its correctness without having to trust the synthesizer by simply verifying the associated proof.

For our work, certifying the synthesis procedure was certainly a wildly impractical approach to the problem. The SuSLik project, while being relatively young, is a fairly mature software project, with the main branch having over 1000 commits, and it's source code collectively comprising over 10,000 lines of complex Scala code. Needless to say, even just the process of encoding SuSLik in a format amenable to verification would likely be an insurmountable task. Luckily, as it turns out, as the SuSLik synthesis procedure is based around deductive reasoning, it is far more tractable to extend SuSLik to produce proof certificates for its synthesised programs.

How can we leverage SuSLik's synthesis procedure to produce proof certificates?

Well the key idea here is that as SuSLik bases its synthesis procedure around the formalisms and logical rules of separation logic, the implicit reasoning that it performs during its search process is actually inherently quite close to the steps that a human might take while proving the correctness of a program in a separation logic-based verification framework.

Using this observation, we can then come up with a generic methodology for extending SuSLik to produce proof certificates for different verification backends: for each kind of synthesis rule that SuSLik uses during its search process to generate code, we can then map it to a corresponding proof rule that implements the corresponding operation in terms of the verification backend. Using this perspective, the entire certification process can be uniformly implemented in terms of a kind of specialised traversal over the synthesis tree, where a so-called "proof-interpreter" steps over each synthesis rule and maps it to a corresponding operation in the verification framework. There is some additional complexity in this approach that we won't cover here in that often the order in which proof rules are applied in a verification framework doesn't exactly align with the order in which they occur during synthesis, but it turns out that we are able to handle this quite elegantly using a kind of deferred evaluation.

Using this methodology, we then are able to extend the existing SuSLik to produce fully certified programs, with associated Coq proof-scripts verified in 3 different separation logic frameworks:

• The Hoare Type Theory Coq Framework
• The Iris Coq Framework
• The Verified Software Toolchain (VST) Framework

Notably of which, the last one (VST), allows us to produce fully verified executable C code as an output from SuSLik.

• Project Repository
• "Structuring the Synthesis of Heap-Manipulating Programs" (POPL'19)
• "Certifying the Synthesis of Heap Manipulating Programs" (ICFP'21)
• Coq Proof Assistant
• Iris Coq Framework
• Verified Software Toolchain (VST) Framework
• Hoare Type Theory Coq Framework
• Separation logic
• Proof Carrying Code