Specification style: Abstractions with pre- and post-conditions

In POCS you will often write specifications that abstract away the state manipulated by the lower-level code into a higher-level representation of the state, which we will call a "spec state". This style of specification, for a given procedure, consists of two parts: (1) the type of the abstract state, and (2) a description of how this abstract state can change as a result of running a procedure. To prove that an implementation (code) meets its specification (spec), which puts the following obligations on you:

• You need to define an abstraction relation that connects code states and spec states;
• Whenever the code runs from state w to state w' and the abstraction relation holds between w and state, you must show that there exists a spec state state' for which the abstraction relation holds between w' and state', and that the specification allows the procedure to change the abstract state from state to state'.

Here's a picture representing these proof obligations:

                     spec semantics
     forall state ===================> exists state'
              ^                                 ^^
         absR |                            absR ||
              V   semantics of code             VV
       forall w  -----------------------> forall w'

Single lines are what the proof assumes, and double lines are what you must show in your proof. The rest of this file defines what it means to construct an abstraction relation between code states and spec states, what it means to define a specification, and how we can structure these proofs.

Abstraction relation and composition

A LayerAbstraction is a record with one field, abstraction, which relates two states: one of type State1 and another of type State2. Think of State1 as being the type of code states whereas State2 is the type for specification states. The abstraction relation links these two states together. For example, in StatDB lab, the spec state is a list of integers and the implementation state is is a pair of variables. In the StatDB lab, the abstraction function must state what must be true of the relationship between the list of integers and the pair of variables.

The above definition of LayerAbstraction helps us connect two layers, such as the layer of variables and the layer of the StatDB specification. A particular kind of abstraction is one that connects the bottom-most type of state, world, with some abstract state above the world. (Recall that our model of execution is that, at the lowest level, procedures (code) always manipulates the "real world", whose state is of type world.) We define Abstraction to be this particular kind of abstraction: it is a relation between world states and some other type of states, State.

We can compose abstractions, by layering one abstraction on top of another. In our case, since everything is ultimately connected to world states at the bottom, we define a composition of two kinds of abstraction: one that goes from world states to State1, and another that goes from State1 to State2, to produce an abstraction from world to State2. abstraction_compose makes this connection precise, by saying that world and State2 states are connected by the fact that there exists some intermediate State1 state that matches the two abstractions being composed.

In some situations, we will want to keep the same level of abstraction (i.e., have the code and spec states be the same). IdAbstraction defines this "identity" kind of abstraction: it is a relation between states of the same type State, and the relation says that the two states must be equal.

Specification

Our specifications describe how a procedure can change the state of the system, at some level of abstraction. We describe the allowed state changes using pre- and post-conditions, as captured by the following structure, SpecProps. SpecProps is parametrized by three types: T, R, and State. State is the type of states that this specification uses. For instance, in the StatDB example, State would be list nat. T is the type of the return value of the procedure being specified. Note that the post condition is a function of two arguments: one of type T (the returned value), and another of type State (the resulting state). In addition to pre- and post-conditions, our specifications include recovery conditions, which help reason about crashes during the execution of a procedure. After a crash, a recovery procedure will run to recover any state from the crash. The recovery procedure may also return some result; this result's type is R, and the recovery condition, recovered, takes two arguments: the return value from recovery, R, and the state after recovery, State.

One obvious part missing from the SpecProps specification is any reference to the starting state. The reason we didn't pass it as an argument to the precondition, pre, is that it's useful to refer to the starting state inside the post and recovered conditions as well, in order to connect the final state to the starting state. Another part which is not so obviously missing is a way to talk about existential variables in the specification (sometimes called "ghost variables" in the PL literature). This is a bit hard to grasp in an abstract sense; we will use this in lab 4, and it's safe to ignore it until then. We add these two missing parts to a specification by defining the actual type of specifications, Specification, as a function from a ghost variable A and a starting state State to a SpecProps. This allows the pre-, post-, and recovered conditions in SpecProps to refer to the starting state (and the ghost variable).

Correctness of a procedure

proc_spec defines when a specification holds for a procedure p and a recovery procedure rec. (The recovery procedure will become important in labs 3 and 4, when we reason about crashes.) proc_spec formalizes our intuition of what it might mean to satisfy a pre- and post-condition specification. The general shape of what proc_spec says, ignoring recovery for now, is:

            pre                      post
             |                        ||
             V                        VV
           state                    state'
             ^                        ^^
        absR |                   absR ||
             V                        VV
             w ---[procedure p]-----> w'

The single arrows indicate the assumptions (that there exists some starting abstract state state, corresponding to a world state w, where the precondition pre holds, and that running the procedure p gives us state w'.) The double arrows indicate what proc_spec concludes: that there is an abstract state state' corresponding to w', and that the postcondition holds in that resulting state state'. This picture should look familiar; it is quite similar to the proof obligations described at the top of this file, with the extra detail of how we describe the allowed transitions (namely, using pre- and post-conditions). In more detail, proc_spec states that for all ghost variables a, starting states w, and spec states state:

• assume that the abstraction relation holds between w and state
• assume that the precondition holds for a and state
• if the procedure p starts from code state w, then one of the following must be true:
  • (1) if execution finishes without crashes in code state w' and returns v, then there exists a spec state state' in which the abstraction relation holds between w' and state' and the postcondition holds in state' with return value v, OR
  • (2) if execution finishes in code state w' and returns v (after perhaps several crashes and running the recovery procedure r on each crash), then there exists a spec state state' and some return value v from the recovery procedure, in which the abstraction relation holds between w' and state' and the recovered condition holds in state' with return value v.

The rexec relation describes how procedures execute, and is defined in Spec.Proc.

Proving correctness

To help us construct proofs about procedures satisfying a specification, it helps to have a notion of when one specification implies another specification. Here, we define what it means for spec1 to imply spec2 (the two specifications must be at the same level of abstraction and must talk about the same types of return values):

• for all ghost variables and all states state for which spec2's precondition holds,
• there exists a ghost variable for which spec1's precondition holds in state
• for all states state' in which the postcondition of spec1 holds, then the post condition of spec2 also holds
• for all states state' in which the recovered condition of spec1 holds, then the recovered condition of spec2 also holds.

We now prove that the above definition of what it means for one specification to imply another one is actually correct. This means that, if a procedure satisfies spec1, and spec1 implies spec2, then the same procedure must also satisfy spec2.

This is a crucial step for constructing proofs of correctness. We will decompose proofs about a Bind operation (i.e., combining two procedures, p and rx, with a semicolon) into smaller proofs about the individual procedures p and rx. Specifically, in order to prove that p; rx satisfies spec', it suffices to have some specification spec for p, and to prove that the precondition of spec' implies the precondition of spec, and that rx meets a specification that, informally, fixes up the postcondition of spec to match the postcondition of spec'. More precisely:

In some situations, the precondition of a specification may define variables or facts that you want to intros. Here we define several helper theorems and an Ltac tactic, spec_intros, that does so. This is done by changing the specification's precondition from an arbitrary Prop (i.e., pre) into a statement that there's some state state0 such that state = state0, and introsing the arbitrary Prop in question as a hypothesis about state0.

Finally, we prove that our notion of equivalent procedures, exec_equiv, is actually correct: if p and p' are equivalent, then they meet the same specifications. We will use this next to reason about procedure transformations that shouldn't change the behavior of a procedure.

Reasoning about the Ret return operation.

The simplest procedure we can construct in our model is the return operation, Ret. Writing a specification for Ret should be intuitively straightforward, but turns out to be slightly complicated by the possibility of crashes. The rec_noop definition below captures this notion: a Ret v procedure has no precondition, and has a simple postcondition (the state does not change and the return value is v), but in case of a crash, the state is wiped according to some wipe relation. rec_noop is a theorem that states that Ret v actually meets this specification. Proving rec_noop will be a proof obligation, and boils down to showing that the recovery procedure rec corresponds to the wipe relation wipe.

A more general theorem about specifications for Ret, which we will use as part of our proof automation, says that Ret v meets a specification spec if the rec_noop theorem holds (i.e., the recovery procedure is correctly described by a wipe relation wipe), and the specification spec matches the wipe relation:

Proof automation

We will now define some Ltac tactics to help us prove the correctness of procedures. We start with a simple tactic that will eliminate unnecessary Ret return statements and will re-order semicolons into a consistent order. This tactic, monad_simpl, makes use of the monad_left_id and monad_assoc theorems to manipulate procedures, simplifying their return statements and semicolons, together with the theorem we proved above, spec_exec_equiv, about specifications of equivalent procedures.

step_proc

To simplify proofs, we automate reasoning about proc_spec. Consider a proof for a proc_spec about "a ; b". What do we need to prove?

      pre                             post
       |                               |
       V                               V
     state0 --[a]--> state1 --[b]--> state2

We need to find a proc_spec for a and line up our precondition with that spec's, then reduce to proving a proc_spec for b, with a's post as the new pre. Keep doing this repeatedly. There are two requirements to make this plan work:

• a proc_spec for the a procedure
• a way to line up our current state's precondition with a's proc_spec precondition

The following Ltac, step_proc, implements this plan. It compares Coq's current goal to:

• a proc_spec with a procedure that invokes a Ret operation: if so, apply the ret_spec theorem to consume the Ret. This will generate some proof obligations, corresponding to the premises of the ret_spec theorem.
• a proc_spec with a procedure that sequences two operations a and b (with Bind): if so, apply the proc_spec_rx theorem to consume the Bind. This will generate some proof obligations, corresponding to the premises of the proc_spec_rx theorem.
  A common pattern is that we have already proven that a already meets some specification. To automate this case, step_proc calls eauto to find such a theorem. We tell Coq about these theorems using Hint Resolve statements that you will see throughout our lab code.
  Proving the correctness of the b procedure will remain as a proof obligation.
• a proc_spec that is implied by a proc_spec that is already in context: if so, apply the proc_spec_weaken theorem and try to prove that one spec implies the other.

Initialization

Initialization is special because, when the initialization procedure starts running, the system may be in a state that does not correspond to ANY abstract state yet. This means that we will need to write a stylized kind of specification about initialization procedures. As a common pattern, initialization can succeed or fail. If it fails, we typically do not promise anything.

When we compose multiple layers together, a common pattern that emerges is trying to initialize the lower level first, and then initializing the higher level. The reason we don't just combine the procedures using semicolon (i.e., Bind) is that if the lower-level initialization fails, we should return failure right away, instead of continuing to run the higher-level initialization.

Initialization specs

To specify what it means for the initialization procedure to be correct, it suffices to simply write a predicate describing the initialized states that will be produced by the initialization procedure. A common description of these states is "any state that satisfies the abstraction relation", which we can define using inited_any:

We define this shorthand for the specification of an initialization procedure. Given a description of the states that initialization should produce (e.g., inited_any above), init_abstraction produces a full-fledged pre- and post-condition-style specification, which says that, if initialization returns success, the resulting state is one of the allowed states:

Since the init_abstraction specification above does not place any requirements in case we crash during initialization, the specific recovery procedure doesn't matter:

Finally, we prove a specialized theorem about how to compose two initialization procedures using the then_init composition operator defined above: