Verifying (simple) C in Isabelle/HOL with AutoCorres
This post details the first steps of verifying a C function in Isabelle/HOL using AutoCorres. It'll go over the basic setup for Isabelle and AutoCorres, what AutoCorres gives you, and how we can verify some basic properties of a function (here, the sum of a list.) I use the latest versions of Isabelle and AutoCorres available at time of writing (24/08/26). This is not official documentation for AutoCorres, nor may it be 100% correct in all places. All the proofs go through, but I do not work on AutoCorres, nor have I used it professionally; most of my experience is hobby verification. However, I have found resources on it are woefully lacking, so I wished to introduce some more. Much of this information has been gleaned from the official documentation (which can be found at the aforementioned,) and this course . When it runs, the slides/similar may be removed for some time - they exist on the internet archive also. This article assumes a little either Isabelle/HOL or general verification knowledge, but I try to explain wherever feasible. A bit of C knowledge is required as well, and so is a little knowledge about program verification - a little Hoare logic, and the like. I'll try to explain as much as I can without being excessively verbose, and much of it is very searchable. You can find Isabelle here . Install as is appropriate for your platform. You can decide whether to put in your path or not. First, pick a directory for your project. It may be feasible to use AutoCorres globally, but I wouldn't recommend it for versioning reasons. Then, AutoCorres can be found by scrolling down here . (It will probably take you here , whereupon you should scroll down to the latest AutoCorres release). You only need the AutoCorres download, as it bundles the C parser. Take that file, and extract it in your directory of choice. Then we need to build AutoCorres. From the directory where you unpacked it, run This'll take a second. Replace paths as appropriate. Note that is not the architecture you are on - it determines how the tool translates various C sizes into Isabelle. This will need to be the same architecture you launch with later. There are some others, and on a related note: It may not all make sense yet, but it may answer some questions. I recommend making a little shell script for this step ( perhaps.) You'll need to invoke Isabelle in a manner similar to the following: Remember that needs to be the same as earlier. Now that we have Isabelle running, we can use AutoCorres to generate Isabelle versions of C files. The manner in which this is performed is long, complex, and interesting - I recommend a rabbit hole evening - but in short, the C parser first translates it to a deep embedding in a language called Simpl, and then AutoCorres takes this Simpl representation and turns it into a monadic shallow embedding best it can. Here's what we'll be verifying today: The use of unsigned will be expanded on later. We'll put it in a C file named . At this point, your directory should look something like or similar. Begin a regular Isabelle theory, importing AutoCorres (and whatever else you want): We then need to let AutoCorres perform its magic. First, we "install" the C file with the C parser: You can use to see what this defines. Of particular interest is . Then, AutoCorres: The idea the C parser and AutoCorres use for verifying C is that it is reasonable to do a very direct translation of C to Simpl, and then a refinement to the monadic representation. The C parser is correct through inspection, and extensive testing. However, the translation of Simpl to the monadic form is verified - there exist Isabelle-checkable proofs that show that the monadic representation, however different it may be, behaves identically to the Simpl equivalent. This makes the monadic form a refinement of Simpl, and is why the things we prove about the monadic forms translate back down to C. This might also take a second. We choose to use . This makes unsigned integers perform modular arithmetic instead of using overflow checks; this has positives and negatives. Read the README for more. Again, you can use to see what this gives you. Of particular interest is . This is the monadic embedding of our function. We then need to enter the locale (think of it as an environment) defined by the C parser and AutoCorres, so your file should look something like: We do our work in this locale. If you haven't already, and . The former is the deep embedding produced by the C parser, and the latter is the result of AutoCorres's shallow embedding. These can be unfolded with and respectively. You can examine the types of things with ctrl-hover (cmd-hover on Macs.) Also examine . The type for the monadic state used by AutoCorres is called (You may see it displayed as in some places.) It's a record containing fields for each type of pointer used; ours only uses , so it only contains information for 32 bit words. We can examine the extract and update functions used in with and . Which monad AutoCorres chooses to embed a function into depends on the function, and can also be configured. This function is simple enough that it can be encoded with purely , but others include , (option with state,) and . Yes, this is a reasonable question to ask. What does it actually mean to verify this function? Generally, there are a few reasons to verify something: We'll look at all three. The not failing example will go into quite a lot of depth, whereas the correctness example will go into much less, only covering broad strokes. This is because the proofs are quite similar, and if you find the former excessively verbose, you might want to skip to the latter. Let's consider what we need for this function to not fail in C. The obvious constraint is that must be defined for all . Using , we can state this as a definition: Now we have our suitable precondition, let's set up our "doesn't fail" lemma. We expect that: We can state this using the combinator . The NF stands for , and it adds the additional condition that our program does not fail in some way during execution. Precisely what we want! It takes three arguments: The arguments are: Here, is used because of the choice of state monad AutoCorres makes. Note that our postcondition takes both the state and the return value . When we use with , will be our state . So, our lemma then becomes: If we have our list defined properly and some property Q, and we run our program, then it does not fail and Q is still true. If you're familiar with Hoare logic, you'll know we probably want to use some sort of weakest precondition reasoning. A weakest precondition is roughly "what is the smallest amount of information we need to know for this to be true", which allows us to simplify our proof obligations. Indeed, AutoCorres provides us with a family of tactics such as and . However, I find it nice to start these proofs by unfolding the function at hand, and applying or similar to get some simplification going. Then we can apply to apply relevant weakest precondition rules automatically. This should leave you with a state something like: I highly recommend using the Query tab of jedit throughout (or equivalents like .) will come in handy, and it's a nice fuzzy search. will do what's on the tin, and will find theorems that could apply. As we have a while-loop, a reasonable step is to add an invariant. An invariant is something that is invariant over the loop - it is always true, at the top of every loop cycle, and right after the loop finishes. This is how we conclude things about what a loop does. Indeed, we can see a theorem of use: Most of the time, the prefixes can be omitted. So first, we add an invariant, and then we can use to transform our into theorems we can work with. The invariants we care about right now are: We also care that this loop terminates, so let's add a suitable measure. is our invariant, and is the termination measure for the loop. Note the type conversion in . Then, again: This'll probably give you a few more normal looking goals. can come in handy again to chunk these down. This leaves me with: The first we talked about earlier - we can solve it by unfolding via , and basic reasoning. For the second, it seems obvious - why hasn't solved it? (If it were on s, it certainly would have.) Alas, it's on s, which as we have chosen to use modular arithmetic, are slightly less nice. It's hard to search for theorems involving as it's so overloaded, but luckily here finds . The final goal is more interesting. The initial intuition might be to use again, but this leaves us with nasty metavariables because of the chaining nature of the binds, and the fact that AutoCorres here is slightly too general. With a little searching we have the following: But we only really need to be identical to . We could instantiate manually each time, or we can make a little helper lemma (which I will do.) Above this lemma, we add Then we can apply twice (There are two binds.) We hence have: It's finally time to start unfolding the definition of so we can crunch down these last few goals. If we hit the first goal with: we're left with which takes out nicely. Tip: I fiddled with this for a bit manually, but if it looks fiddly and obvious, there's a good chance sledgehammer can do it. Finally, the last two are easy: We have a proof of non-failure! This is very exciting. The final proof is as follows: Then, what does it mean for our function to be correct? Well, a reasonable definition is that it produces the output we expect. We then need to figure out what "output we expect" means. We could have also defined the sum of a list as similar to the following recursive function: Note that we explicitly check for 0 to ensure the recursion terminates (We can't pattern match on 0/Suc, as we're working with s.). Unfortunately, this function's termination can't be proven automatically due to the use of a , which Isabelle isn't as good with as its own s. This is why we use a instead of , and we must do the termination proof ourselves: We also delete from the default simp set because it seems to cause some solvers to loop. We can set up our lemma like before, but this time, we use the parameter: We want the result to be equivalent to summing the entire list with our recursive function. We also don't bother to prove that it doesn't fail here. We can begin as before, omitting the step. We then need to annotate with a suitable invariant. A hint: We want the sum at the end to be correct, so a good invariant should capture correctness at every step , which gives us full correctness when the loop finishes. We have to manually a few times as we deleted it from the simp set, but otherwise the proof is very straightforward. Mine came out to be: We could take this one step further if we wanted, and define a bijection between and assuming our precondition, and then also show that our own spec is equivalent to the sum of that list. That'd give us even more confidence our function is correct. I'm personally pretty convinced, but you're welcome to try this yourself! We could then finally prove that if some property is true for the sum of a list, it's true for the result of our program. I won't detail this one; it should follow reasonably easily from the former two. So, what have we (hopefully) learnt? I hope this has been informative! (With less fixing of indentation for the web, sorry): A bit underwhelming for how long it took to explain, perhaps! To prove it never "fails" (what failing means is another question) To prove it produces some desired output To prove it holds some desired property is a , as perhaps expected. has been converted into a . is our state for the function, and carries information as mentioned about the heap. We use the perhaps confusing for pointer addition. You can write this in jedit with . We also need an explicit type conversion , as you can add negatives to a pointer, so the argument is an (this is not unsigned int; that's . here corresponds to Isabelle , which is signed.) If: The list is defined properly Some other property Q is true Then: Our function does return successfully, so That property is still true. A precondition function. A computation function. A postcondition function. (for termination) (for no-failure) (for simplified correctness) How to install and setup Isabelle and AutoCorres What it means to prove things about programs How to set up appropriate proofs How to prove them What tools we have available and how we can search for more
Programming
Tutorial
Shell
Backend
C++
Rust
JavaScript
Security
AI
Career