**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.

*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.

*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.

`doc/Tutorial.v`in the Bedrock distribution) using

`coqdoc`.

# Three Verified Bedrock Programs

## A Trivial Example: The Addition Function

`-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`.

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
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

*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.*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
It doesn't seem surprising that addM should be a correct implementation of an addition function, but, just to be sure, let's

*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.*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
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.

*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.)## 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
Both precondition and postcondition use notation inspired by
Here is an implementation.

*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.*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.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

*data structures*, formalized in a way similar to

*abstract predicates*in separation logic. As an example, consider the following recursive definition of an abstract predicate for singly linked lists.

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
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.

*disjoint*from each other.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
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.

*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.)
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

**Bedrock IL**), such that the theorem statement only depends on a conventional operational semantics for this language. This means we can apply Coq's normal

*proof checker*to validate our verification results, without trusting anything about the process whereby the proofs were constructed. When the

*trusted code base*of a verification system is so small, we call the system (or the theorems it produces)

*foundational*.

## The Bedrock IL

**A nifty BNF grammar appears here in the PDF version!**

*(omitted in HTML version)*gives the complete syntax of the Bedrock IL, which is meant to be a cross between an assembly language and a compiler intermediate language. Like an assembly language, there are a fixed word size, a small set of registers, and direct access to an array-like finite memory. Like a compiler intermediate language, the Bedrock IL is designed to be compiled to a variety of popular assembly languages, though this compilation process is more straightforward than usual. There is no built-in notion of local variables or calling conventions, but code labels are maintained with special syntactic treatment, to allow compilation to perform certain jump-related optimizations soundly.

*gets stuck*if a program tries to jump to a word not associated with any code label. Further, another piece of global state gives a

*memory access policy*, identifying a set of addresses that the program may read from or write to. Execution gets stuck on any memory access outside this set. One consequence of verifying a whole-program Bedrock module is that we are guaranteed lack of stuckness during execution, starting in states related appropriately to the module's specs.

## The XCAP PropX Assertion Logic

*modular*program verification. That is, we want to verify libraries separately and then compose their correctness theorems to yield a theorem about the final program. We must fix some

*theorem format*that enables easy composition, and a

*program logic*may be thought of as such a format.

*first-class code pointers*in a logic expressive enough to verify

*functional correctness*, not just traditional notions of type safety. However, XCAP's insight is to apply the

*syntactic approach to type soundness*in this richer setting. We no longer think in terms of assigning types to the variables of a program, but we retain the key idea of establishing a global

*invariant*that all reachable program states must satisfy, where the invariant is expressed in terms of a

*syntactic language of assertions*. In Coq, this notion of

*syntactic*means

*deep embedding*of a type of formulas.

**A nifty BNF grammar appears here in the PDF version!**

*(omitted in HTML version)*gives the syntax of , XCAP's language of formulas, otherwise known as an

*assertion logic*when taken together with the associated proof rules. The standard connectives /\, \/, --->, forall, and exists are present, but a few other cases imbue the logic with a richer structure. First, the lifting operator [| _ |] allows injection of

*any Coq proposition*.

*modular theorems about first-class code pointers*without some extra layer of complication, and for XCAP, that layer is associated with formulas Cptr w f. Such a formula asserts that word w points to a valid code block, whose specification is f, a function from machine states to formulas. The idea is that f(s) is true iff it is safe to jump to w in state s.

*safe*to jump to a code block, which does not directly yield the discipline of functions, preconditions, and postconditions. The explanation is that we

*encode*such disciplines using

*higher-order*features. Bedrock IL programs, like assembly programs, are inherently in

*continuation-passing style*, and it is possible to lower

*direct style*programs to this format and reason about them in a logic that only builds in primitives for continuations, not functions. The freedom to work with continuations when needed will be invaluable in implementing and verifying systems components like thread schedulers.

*impredicative quantifiers*, which may range over assertions themselves. With these quantifiers, we can get around an apparent deficiency of Cptr, which is that its arguments must give the

*exact*spec of a code block, whereas we will generally want to require only that the spec of the code block be

*implied*by some other spec. We define an infix operator @@ for this laxer version of Cptr.

Notation "w @@ f" := (ExX, Cptr w #0 /\ Al s, f s ---> #0 s)%PropX.

*de Bruijn indices*. Unraveling that detail, we can rephrase the above definition as: program counter w may be treated as having spec f if there exists a such that (1) a is the literal spec of w and (2) any state s satisfying f also satisfies a.

*the impredicative quantifiers have introduction rules but no elimination rules*. As a result, we may really only reason non-trivially about those quantifiers at the level of the meta-logic, which is Coq. One consequence is that we cannot transparently and automatically translate uses of interp into normal-looking Coq propositions. However, this can be done for formulas that do not use implication. A Bedrock tactic propxFo handles that automated simplification, where it applies.

### 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) {

*precondition*and a

*postcondition*. Standard Hoare-logic loop invariants only represent assertions over single program states. How should an invariant like the above be interpreted?

*precondition*describes what the machine state looks like upon entering a loop iteration, and the

*postcondition*describes what the state must be transformed into before it is legal to

*return*from the current function.

*more natural*for assembly language than the more common notation is. It all has to do with the idea that assembly programs are naturally thought of as in

*continuation-passing style*, since call stacks and return pointers are represented explicitly via memory and registers. Thus, the natural idea of specification for a function is just a precondition, not a precondition plus a postcondition.

`forall x. {P} {Q}`

`{exists x. P /\ {Q}Rp}`

*nested Hoare double*, writing {Q}

`Rp`to assert that

*register*. That is, we mention the return pointer explicitly, rather than keeping it as implicit in our use of a postcondition.

`Rp`holds a pointer to a code block whose precondition is compatible with`Q``{exists x, a. P * a /\ {Q * a}Rp}`

*frame rule*into the desugaring scheme. Some piece of memory is described by an unknown predicate

`a`on entry and must still be described by

`a`on exit.

*frame rule*ought to be applied.

## The XCAP Program Logic

*each basic block is annotated with a PropX assertion*. For the program to be truly verified, two conditions must be proved for each block b with spec f. First, a

*progress*condition says: for any initial state satisfying f, if execution starts at the beginning of b, then execution continues safely without getting stuck, at least until after the jump that ends b. Second, a

*preservation*condition says: for any state satisfying f, if execution starts at the beginning of b and makes it safely to another block b', then b' has some spec that is satisfied by the machine state at this point.

*progress*and

*preservation*are chosen to evoke the

*syntactic approach to type soundness*, which is based around a small-step operational semantics and an inductive invariant on reachable states: each state (program term) is well-typed, according to an inductively defined typing judgment. In XCAP, we follow much the same approach, where a single small-step transition is

*one basic block execution*, and the inductive invariant is that

*the current machine state satisfies the spec of the current basic block*.

*execution continues forever without getting stuck*. Second, if execution begins in a block whose spec is satisfied, then

*every basic block's spec is satisfied whenever control enters that block*. The first condition is a sort of

*memory safety*, while the second is a kind of

*functional correctness*.

*structured programs*and what it means for them to be correct. We defer details of structured programs to a later section. For now, what matters is that structured programs can be

*compiled*into verified Bedrock IL programs, at which point their code and the associated guarantees can be understood as in this section.

# Interactive Program Verification

*hints*that can come in many varieties. There are the normal auto and autorewrite hints familiar to most Coq users, but there are also new notions like

*unfolding rules*and

*symbolic evaluators*. Bedrock verifications of serious programs will tend to use all of these notions in concert.

Ltac sep hints := post; evaluate hints; descend; repeat (step hints; descend).

*symbolic execution*, modifying a block's precondition to reflect the effects of a piece of straightline code, possibly including the equivalents of assume statements to record the results of conditionals. The descend tactic is a generic simplifier; among other steps, it descends under existential quantifiers and conjunctions in the conclusion, introducing new unification variables for the quantifiers. The rest of the procedure is a loop over step and descend, where the former implements a variety of basic steps in a Bedrock proof.

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
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.

*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.
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

# More

*structured programming system*, which includes support for extending the visible programming language with new control flow constructs, when they are accompanied by appropriate proofs.