Bedrock is a Coq library that supports implementation, specification, and verification of low-level programs. Low-level means roughly "at the level of C or assembly," and the idea of "systems programming" is closely related, as some of the primary target domains for Bedrock are operating systems and runtime systems.
Bedrock is foundational, meaning that one needs to trust very little code to believe that a program has really been verified. Bedrock supports higher-order programs and specifications. That is, programs may pass code pointers around as data, and specifications are allowed to quantify over other specifications. Bedrock supports mostly automated proofs, to save programmers from the tedium of step-by-step formal derivations; and Bedrock is also an extensible low-level programming language, where programmers can add new features by justifying their logical soundness.
This advertising pitch can be a bit of a mouthful. To make things more concrete, we'll start with three small examples. Some knowledge of Coq will be helpful in what follows, but especially our first pass through the examples should be accessible to a broad audience with a basic level of "POPL literacy." Readers interested in applying Bedrock, but who don't have backgrounds in core Coq concepts, should consult some other source. Naturally, the author is partial to his Certified Programming with Dependent Types. Other popular choices are Software Foundations by Pierce et al. and Coq'Art by Bertot and Casteran.
This document is generated from a literate Coq source file (doc/Tutorial.v in the Bedrock distribution) using coqdoc.
To begin, we issue the following magic incantation to turn a normal Coq session into a Bedrock session, where we have run Coq with command-line arguments -R BEDROCK/src Bedrock -I BEDROCK/examples, with BEDROCK replaced by the directory for a Bedrock installation, where we have already run make successfully, at least up through the point where it finishes building AutoSep.vo.
Three Verified Bedrock Programs
A Trivial Example: The Addition Function
Require Import AutoSep.
Importing a library module may not seem like magic, but this module, like any other module in Coq may choose to do, exports syntax extensions and tactics that allow a very different sort of coding than one sees in most Coq developments. We demonstrate by implementing a function for adding together two machine integers. Bedrock is an environment for verified programming, so we should start by writing a specification for our function.
Up through the :=, this is normal Coq syntax for associating an identifier with a definition. Past that point, we use a special Bedrock notation. The SPEC("n", "m") part declares this as a spec for a function of two arguments with the given formal parameter names, and reserving 0 declares that this function will require no more stack space than is needed to store its parameters. (As Bedrock is targeted at operating systems and similar lowest-level code, we opt for static tracking of stack space usage, rather than forcing use of a fixed dynamic regime for avoiding stack overflows. Furthermore, handling of the stack is not built into the underlying program logic, and it is possible to implement alternate regimes without changing the Bedrock library.)
A specification includes a precondition and a postcondition. The notation PRE[V] introduces a precondition, binding a local variable V that can be used to refer to the function argument values. In this example, we impose no conditions on the arguments, so the precondition is merely True. Actually, Bedrock uses a fancier domain of logical assertions than Coq's usual Prop, so we need to use the [| ... |] operator to lift a normal proposition as an assertion. More later on what assertions really are.
A postcondition begins with the notation POST[R], which introduces a local variable R to stand for the function return value. In our postcondition above, we require that the return value equals the sum of the two function arguments, where we write addition with the ^+ operator, which applies to machine words.
Now that we know what our function is meant to do, we can show how to do it with an implementation. This will be a Bedrock module, which in general might contain several functions, but which will only contain one function here.
The syntax should be mostly self-explanatory, for readers familiar with the C programming language. Two points are nonstandard, beyond just the concrete syntax. First, we refer to variable names with string literals. These are not string literals in the Bedrock programming language, but merely a trick to get Coq's lexer to accept C-like programs. Second, the function header ends in a Coq term between square brackets. This is the position where each function must have a specification.
It doesn't seem surprising that addM should be a correct implementation of an addition function, but, just to be sure, let's prove it.
The predicate moduleOk captures the usual notion from Hoare Logic, etc., of when a program satisfies a specification. Here we prove correctness by chaining invocations of two tactics: vcgen, which performs verification condition generation, reducing program correctness to a set of proof obligations that only refer directly to straightline code, not structured code; and sep_auto, a simplification procedure based on separation logic that is quite a bit of overkill for this example, but gets the job done. (There actually is some quite non-trivial reasoning going on behind the scenes here, dealing with complexity hidden by our nice notations; more on that later.)
A crucial component of low-level programming is mutable state, which we introduce with a simple example: a function that takes two pointers as arguments and swaps the values in the memory cells that they point to. Here is its spec.
Pointers and Memory: A Swap Function
Definition swapS := SPEC("x", "y") reserving 2
Al v, Al w,
PRE[V] V "x" =*> v * V "y" =*> w
POST[_] V "x" =*> w * V "y" =*> v.
We see several important changes from the last spec. First, this time we reserve 2 stack slots, to use for local variable temporaries. Second, the spec is universally quantified. The function may be called whenever the precondition can be satisfied for some values of v and w. Note that the same quantified variables appear in precondition and postcondition, giving us a way to connect the initial and final states of a function call.
Both precondition and postcondition use notation inspired by separation logic. The syntax p =*> v indicates that pointer p points to a memory cell holding value v. The * operator combines facts about smaller memories into facts about larger composite memories. The concrete precondition above says that the function will be aware of only two memory cells, whose addresses come from the values of parameters "x" and "y". These cells start out holding v and w, respectively. The postcondition says that the function swaps these values.
Here is an implementation.
Definition swap := bmodule "swap" {{
bfunction "swap"("x", "y", "v", "w") [swapS]
"v" <-* "x";;
"w" <-* "y";;
"x" *<- "w";;
"y" *<- "v";;
Return 0
end
}}.
We write private local variables as extra function formal parameters. The operator ;; sequences commands, the operator <-* is a memory read, and *<- is memory write.
Our function is not very complex, but there are still opportunities for mistakes. A quick verification establishes that we implemented it right after all.
An Abstract Predicate: In-Place List Reverse
Fixpoint sll (ls : list W) (p : W) : HProp :=
match ls with
| nil => [| p = 0 |]
| x :: ls' => [| p <> 0 |] * Ex p', (p ==*> x, p') * sll ls' p'
end%Sep.
The type W is for machine words, and the %Sep at the end of the definition asks to parse the function body using the rules for separation logic-style assertions.
The predicate sll ls p captures the idea that mathematical list ls is encoded in memory, starting from root pointer p. The codomain HProp is the domain of predicates over memories.
We define sll by recursion on the structure of ls. If the list is empty, then we merely assert the lifted fact p = 0, forcing p to be null. Note that a lifted fact takes up no memory, so we implicitly assert emptiness of whatever memory this HProp is later applied to.
If the list is nonempty, we split it into head x and tail ls'. Next, we assert that p is not null, and that there exists some pointer p' such that p points in memory to the two values x and p', such that p' is the root of a list encoding ls'. By using *, we implicitly require that all of the memory regions that we are describing are disjoint from each other.
To avoid depending on Coq's usual axiom of functional extensionality, Bedrock requires that we prove administrative lemmas like the following for each new separation logic-style predicate we define.
Theorem sll_extensional : forall ls (p : W), HProp_extensional (sll ls p).
Proof.
destruct ls; reflexivity.
Qed.
We add the lemma as a hint, so that appropriate machinery within Bedrock knows about it.
We want to treat the predicate sll abstractly, relying only on a set of rules for simplifying its uses. For instance, here is an implication in separation logic, establishing the consequences of a list with a null root pointer.
Theorem nil_fwd : forall ls (p : W), p = 0
-> sll ls p ===> [| ls = nil |].
Proof.
destruct ls; sepLemma.
Qed.
The proof only needs to request a case analysis on ls and then hand off the rest of the work to sepLemma, a relative of sep_auto. Staying at more or less this same level of automation, we also prove 3 more useful facts about sll.
Theorem nil_bwd : forall ls (p : W), p = 0
-> [| ls = nil |] ===> sll ls p.
Proof.
destruct ls; sepLemma.
Qed.
Theorem cons_fwd : forall ls (p : W), p <> 0
-> sll ls p ===> Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p'.
Proof.
destruct ls; sepLemma.
Qed.
Theorem cons_bwd : forall ls (p : W), p <> 0
-> (Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p') ===> sll ls p.
Proof.
destruct ls; sepLemma;
match goal with
| [ H : _ :: _ = _ :: _ |- _ ] => injection H; sepLemma
end.
Qed.
So that Bedrock knows to use these rules where applicable, we combine them into a hint package, using a Bedrock tactic prepare.
Now that we have our general "theory of lists" in place, we can specify and verify in-placed reversal for lists.
Definition revS := SPEC("x") reserving 3
Al ls,
PRE[V] sll ls (V "x")
POST[R] sll (rev ls) R.
Definition revM := bmodule "rev" {{
bfunction "rev"("x", "acc", "tmp1", "tmp2") [revS]
"acc" <- 0;;
[Al ls, Al accLs,
PRE[V] sll ls (V "x") * sll accLs (V "acc")
POST[R] sll (rev_append ls accLs) R ]
While ("x" <> 0) {
"tmp2" <- "x";;
"tmp1" <- "x" + 4;;
"x" <-* "tmp1";;
"tmp1" *<- "acc";;
"acc" <- "tmp2"
};;
Return "acc"
end
}}.
Note that the function implementation contains a While loop with a loop invariant before it. As for all instances of invariants appearing within Bedrock programs, we put the loop invariant within square brackets. We must be slightly clever in stating what is essentially a strengthened induction hypothesis. Where the overall function is specified in terms of the function rev, reasoning about intermediate loop states requires use of the rev_append function. (There is also something else quite interesting going on in our choice of invariant. We reveal exactly what in discussing a simpler example in a later section.)
Tactics like sep_auto take care of most reasoning about programs and memories. A finished Bedrock proof generally consists of little more than the right hints to finish the rest of the process. The hints package we created above supplies rules for reasoning about memories and abstract predicates, and we can use Coq's normal hint mechanism to help with goals that remain, which will generally be about more standard mathematical domains. Our example here uses Coq's list type family, and the only help Bedrock needs to verify "rev" will be a lemma from the standard library that relates rev and rev_append, added to a hint database that Bedrock uses in simplifying separation logic-style formulas.
Now the proof script is almost the same as before, except we call Bedrock tactic sep instead of sep_auto. The former takes a hint package as argument.
Foundational Guarantees
The Bedrock IL
A nifty BNF grammar appears here in the PDF version!
The XCAP PropX Assertion Logic
A nifty BNF grammar appears here in the PDF version!
Notation "w @@ f" := (ExX, Cptr w #0 /\ Al s, f s ---> #0 s)%PropX.
A Note on the Format of Invariants
[Al ls, Al accLs,
PRE[V] sll ls (V "x") * sll accLs (V "acc")
POST[R] sll (rev_append ls accLs) R ]
While ("x" <> 0) {
The XCAP Program Logic
Interactive Program Verification
Ltac sep hints := post; evaluate hints; descend; repeat (step hints; descend).
Definition sillyS := SPEC("p", "q") reserving 5
PRE[V] V "p" =?> 1 * V "q" =?> 1
POST[R] [| R = 3 |] * V "p" =?> 1 * V "q" =?> 1.
Definition sillyM := bimport [[ "swap"!"swap" @ [swapS] ]]
bmodule "silly" {{
bfunction "main"("p", "q") [sillyS]
"p" *<- 3;;
"q" *<- 8;;
Call "swap"!"swap"("p", "q")
[ Al v,
PRE[V] V "q" =*> v
POST[R] [| R = v |] * V "q" =*> v ];;
"q" <-* "q";;
Return "q"
end
}}.
We use the Call notation, which always requires an invariant afterward. That invariant position is often a convenient place to simplify the state that we are tracking. The invariant above is an example: we forget about the pointer p, remembering only q, since the rest of the function only touches q. Bedrock's tactics automatically justify this state reduction, with a reasoning pattern reminiscent of separation logic's frame rule. That pattern and many others are encapsulated in the definition of step.
To demonstrate the recommended interactive verification approach, we will step through a more manual proof of the most challenging verification condition, the one associated with the Call command. Interested readers may step through this proof script in Coq, so we will not dump the gory details of subgoal structure into this tutorial. Instead, we give a high-level account of what each subgoal means and how it is dealt with.
This is the subgoal for the function call. We always begin with post-processing the verification condition.
post.
Next, we need to execute the instructions of the prior basic block symbolically, to reflect their effects in the predicate that characterizes the current machine state.
evaluate auto_ext.
At this point, we are staring at the spec of "swap", which begins with some existential quantifiers and conjunctions. One of the conjuncts comes from a use of the @@ derived PropX operator, to express the postcondition via a fact about the return pointer we pass to "swap". We call descend to peel away the quantifiers and conjunctions, leaving the conjuncts as distinct subgoals.
descend.
This subgoal is the precondition we gave for "swap", with an extra fact added to characterize the stack contents in terms of values of local variables. There are unification variables in positions that were previously existentially quantified. This sort of goal is just what step is designed for.
step auto_ext.
We are thrown back another goal, this time stated as an implication between separation logic assertions. One of the unification variables has been replaced with a known substitution for local variable values, which will enable step to discharge the subgoal completely this time.
step auto_ext.
Here is an easy subgoal. It asks us to find a spec for the return pointer we pass in the function call, and exactly such a fact was given to us by vcgen.
step auto_ext.
We have finished proving the precondition of "swap". Now we must prove that its postcondition implies the invariant we wrote after the function call. The form of the obligation is an implication within PropX, where the antecedent is the postcondition of "swap" and the consequent is the invariant we wrote after the call. Recall that simplifying PropX implications into normal-looking Coq formulas is difficult. However, we can rely on step to simplify the implication into some more basic subgoals, some of which will still be PropX implications.
descend; step auto_ext.
The first resulting subgoal is an implication between the postcondition of "swap" and the PRE clause from the post-call invariant. Again, this is exactly the sort of separation logic simplification that step handles predictably.
step auto_ext.
Now we are asked to find a specification for the original return pointer passed to "main". Again, vcgen left us a matching hypothesis.
step auto_ext.
We are in the home stretch now! The single subgoal asks us to prove an implication P ---> Q ---> R, where P is the POST clause of the post-call invariant, Q is the postcondition of "swap", and R is the literal specification of the original return pointer for "main". In fact, R is an application of a second-order variable to the current machine state. We also have a hypothesis telling us that R is implied by the postcondition we originally ascribed to "main" in its spec.
Our first step is to reduce the implication to just P ---> R, augmented with extra pure (memory-independent) hypotheses that we glean from Q. The intuition behind this step is that we already incorporated in P any facts about memory that we will need.
descend; step auto_ext.
Now we prove P ---> R using the hypothesis mentioned above, which can be thought of as a quantified version of U ---> R. That means step can help us by reducing the subgoal to P ---> U.
step auto_ext.
Here is another PropX implication, which we want to simplify to convert as much structure as possible into normal Coq propositions.
step auto_ext.
The first of two new subgoals is an equality between the current stack pointer and the value that the spec of "main" says it should have. We call a library tactic for proving equalities between bitvector expressions.
words.
The last subgoal is an implication between the POST clause of the post-call invariant and the overall postcondition of "main". This is just a separation logic implication, so we make short work of it.
step auto_ext.
This concludes our proof of the most interesting verification condition. Let's back up to the high level and prove the whole theorem automatically.
Abort.
A manual exploration like the above is about learning which hints will be important in proving the theorem. One might even do this exploration using more usual manual Coq proofs. In the end, we distill what we've learned into hint commands. In the script above, we saw only one place where sep wouldn't be sufficient, and that was an equality between machine words. Therefore, we register a hint for such cases.
Now it is easy to prove the theorem automatically.
We might even make small changes to the program specification or implementation, and often a proof script like the above will continue working.
This tutorial will likely grow some more sections later. One topic worth adding is Bedrock's structured programming system, which includes support for extending the visible programming language with new control flow constructs, when they are accompanied by appropriate proofs.