Counter.v

*

A single layer implementing a bounded counter.

Compcert helper lib

Compcert types and semantics

CertiKOS layer library

This file makes use of some tactics and lemmas defined in a library created for this tutorial. It is not necessary for you to read this file in order to follow the tutorial.

This file is meant to demonstrate how the layer calculus used in CertiKOS works by implementing a simple layer consisting of a global counter variable COUNTER that can be accessed and manipulated by the primitives get_counter, incr_counter, and decr_counter. The counter variable is bounded within in the range 0 to MAX_COUNTER and the semantics are such that calling incr_counter (or decr_counter) when COUNTER is at its high (or low) bound results in an error. The underlay upon which this layer is built contains no abstract data or primitives. The overlay consists of the primitives described above and a counter of type nat as abstract data with the invariant that counter ≤ MAX_COUNTER.

The only constraint on the value of MAX_COUNTER is that it is less than the maximum unsigned integer divided by 4 since it will be used as an array index later on. We mark it Opaque to ensure that later proofs do not depend directly on its value.

TUTORIAL: complete proof. Possible in 1 tactic.

These are the identifiers for the primitives and the global counter variable.

Abstract Data

Underlay

The underlay has no abstract data, we model this as unit and declare unit as layer data through the two typeclasses AbstractDataOps and AbstractData. AbstractDataOps requires several fields. First, an initial element of the desired type (unit in our case). The other fields are predicates and invariants that we can simply instantiate with True predicates for the moment. The field data_inv specifies an invariant of the abstract data that must be preserved by all operations on abstract data. The field data_inject specifies how data is injected, i.e. how injections relate these abstract data, in a manner close to CompCert's val_inject. The only time this begins to get interesting is when you are dealing with pointers.

Now, we prove some properties of the aforementioned predicates. This is trivial in our case since we chose True.

We now pack those into a layerdata record.

We can now define the underlay, base_L, as the empty layer interface.

Overlay

We want our overlay to abstract a counter, hence our abstract data will consist of a record counter_data that encapsulates this counter as a natural number. Then, we declare this abstract data as appropriate layer data, as before.

We initialize counter to 0 and require that it is never greater than MAX_COUNTER.

This time we must prove that the initial abstract state (counter = 0) satisfies the invariants (0 ≤ MAX_COUNTER).

High Level Specifications

We now specify the behaviour of the primitives we will expose through our new layer. These are expressed as functions from counter_data to some other type. get_counter simply returns the current value of the counter.

We prove that our high level specs preserve the invariant (counter ≤ MAX_COUNTER) by declaring them as instances of GenSemPreservesInvariant. This is important so we can make use of the invariant later on in the code or refinement proofs. In particular, the code proof of the pop primitive in the Stack layer relies on this fact.

To incorporate this specification in a layer interface, we must wrap it as a cprimitive. A cprimitive is merely a relation between inputs (list of arguments and starting memory state) and outputs (return value and resulting memory state), along with some properties. The cgensem function automatically discharges some proof obligations for us, provided that the specification is of a certain form (SemOf).

We can then define a layer consisting of just the get_counter primitive.

Because incr_counter can fail, it returns a value of type option (counter_data × nat). In the case where the counter is not already at its maximum value it returns a new abstract data with the incremented counter, along with the value of the incremented counter. Otherwise it returns None, representing an error.

decr_counter is defined similarly to incr_counter.

TUTORIAL: Prove that decr_counter preserves the layer invariant

Module Implementation

We now provide implementations of our primitives as Clight functions. Functions are encoded in records with their return type in field fn_return, the types of their parameters, local variables and temporary variables in fn_params, fn_vars and fn_temps respectively, and the function body in fn_body. The difference between local and temporaries variables is that the former are stored inside the memory while the latter are part of an abstract semantic environment which is not part of the memory. We omit a description of the field fn_callconv here, as it is not relevant to this tutorial. The corresponding C code for each function is also provided. f_get_counter is implemented as expected.

int get_counter() {
  return COUNTER;
}

f_incr_counter handles the case where counter < MAX_COUNTER as expected. It handles the failure case by not incrementing COUNTER and returning an error code represented by MAX_COUNTER + 1.

int incr_counter() {
  if (counter < MAX_COUNTER) {
    COUNTER = COUNTER + 1;
    return COUNTER;
  } else {
    return MAX_COUNTER + 1;
  }
}

f_decr_counter handles failure in the same way as f_incr_counter.

int decr_counter() {
  if (0 < counter) {
    COUNTER = COUNTER - 1;
    return COUNTER;
  } else {
    return MAX_COUNTER + 1;
  }
}

Similar to the layers we defined for each of the primitive high specs, we can also define modules consisting of the Clight implementations of the primitives.

Low Level Specifications

Next we define a low-level specification of each primitive, i.e. a specification with respect to the underlay. We define those as transition relations step of type list val → mem → val → mem → Prop. The meaning of step args (m, d) res (m', d') is the following: given arguments args and starting from a memory state m with abstract data d, the primitive returns a value res, the memory state is updated to m' and the abstract data is now d'.

The COUNTER global variable is stored at some memory block sb

The value at block cb is an integer i

get_counter takes no arguments, returns i, and makes no changes to abstract state or memory

TUTORIAL: Replace the four Falses in this inductive definition with appropriate hypotheses

The COUNTER global variable is stored at some memory block cb

The value at block cb is an integer i

i is less than MAX_COUNTER

A new integer j is defined as i + 1

Storing j at block cb results in a new memory m'

incr_counter takes no arguments, returns j, changes m to m', and makes no change to abstract state

The COUNTER global variable is stored at some memory block cb

The value at block cb is an integer i

i is greater than 0

A new integer j is defined as i - 1

Storing j at block cb results in a new memory m'

decr_counter takes no arguments, returns j, changes m to m', and makes no change to abstract state

As with the high-level specifications, to use the low-level specs in a layer definition, we must wrap it in a cprimitive using the mkcprimitive function. This generates a proof obligation that says the return value has the appropriate type. Since this obligation is fairly trivial we use a custom tactic to discharge it for all but the first primitive.

Code Proofs

Now we want to show that these implementations are correct with respect to the underlay and overlay. We will do that in two steps for each primitive. First, we prove that the module implementation together with the underlay refines the low-level specification. Later, we will prove that the low-level specification refines the high-level specification.

We state our theorems in the form underlay ⊢ (R, module) : overlay which says that the code in the module executed on the underlay refines the overlay with respect to some relation R. What we actually want to prove, however, is a simulation diagram like the following: (hargs, hstate) high_spec_step (hresult, hstate') || ---------------> || R || || R || || \/ ---------------> \/ (largs, lstate) low_spec_step (lresult, lstate') In the code proofs, the overlay is the low level spec of some C primitive, and R is typically id. In this case we can simplify the diagram into: high_spec_step (args, state) ---------------> (result, state') low_spec_step The tactic code_proof_tac will automatically convert the goal into the appropriate simulation diagram. You will then have to prove that the cprimitive_step relation holds between the initial and final states. cprim_step will convert this goal into one that states that the final state is reachable in a sequence of Clight steps. The step_tac tactic will try to prove all of the Clight smallstep semantics details and just leave you with a few remaining goals.

TUTORIAL: Replace invalid contradiction with an actual proof.

0 < i

Storing i - 1 gives m'

Loading m' gives i - 1

Return value is i - 1

0 >= i

Layer Relation

Finally, we want to match the high-level specifications of our primitives to the low-level specifications. To achieve this, we need to build an abstraction relation (abrel), which requires two components:

• match_data: a matching relation between the abstract data in the overlay and the memory state in the underlay
• relate_data: a relation between high and low abstract data

In our case, the match_data predicate states that the memory associated with the COUNTER variable must match counter in the high abstract data.

The COUNTER global variable is stored at some memory block b

The value at block b is an integer i

The value of counter in the abstract data equals i

Since the abstract data of the underlay is just unit, relate_data is trivial.

In a more complicated example we might have relations like: var1 hadt = var1 ladt or var1 hadt = var2 ladt + var3 ladt

We now wrap our relations and a list of the global variables' initialization information intro an abrel_components record and declare it an instance of AbstractionRelation. We must now prove the following properties:

• The init_data of the high and low abstract data types must be related by abrel_relate.
• Given information about the newly-introduced globals, we must show that the initial abstract data matches the initial low memory state.
• abrel_match should be preserved by Mem.unchanged_on in the part of memory where the global variables are stored. In other words, the match relation should only depend on the memory used by the global variables.

• The newly-introduced global variables must have identifiers lower than the global threshold.

Initial abs data matches

Initial high abs data matches initial low memory

If global variable memory is unchanged, abrel_match is preserved

Global variable identifiers are lower than glob_threshold

Finally we wrap everything into an abrel record, which just contains the abrel_components plus the proof that they are an instance of AbstractionRelation.

TODO: explain simrel vs abrel? Try to hide it somehow? It will be convenient to wrap this into a simrel with abrel_simrel.

Refinement Proofs

We can finally prove a simulation between the overlay (with the high-level specification of our primitive) and the low-level specification of the primitive. In these proofs, the module is empty (∅) because it is purely an abstraction; no additional code is needed. The refine_proof_tac tactic is similar to code_proof_tac and will also convert your goal into a simulation diagram.

TUTORIAL: Prove that incr_counter_layer simulates the C implementation of incr_counter

Abs data relate

High abs data matches low memory

Global variable permissions

Global variable memory blocks are valid

Linking

We can now define the complete Counter layer by composing the high level specs.

The low level specs (often represented as σ, hence Σ for their composition) also form an intermediate layer between base_L and counter_L.

As a last step, we must horizontally and vertically compose the code and refinement proofs we have done so far for individual primitives. The result is a statement that the C code in counter_M evaluated on top of base_L refines the behaviours specified by the specs in counter_L. This means that other layers that build on this one can write primitives in terms of the high level specs in counter_L and be sure that any properties proved will still hold in the C implementation. This linking step is usually fairly mechanical and can be largely automated using custom tactics and hint databases. Here we show the proof both with and without automation.

We want to prove the linking in two steps:

• base_L ⊢ (id, counter_M) : counter_Σ
• counter_Σ ⊢ (counter_R, ∅) : counter_L

So first we must rewrite counter_R so it is composed with id on the left, and counter_M so it is composed with the empty module on the right.

Now we can use the vertical composition rule to split our goal.

Then we want to split the modules and low level specs into the individual primitives so we can apply the code proofs we did before.

For the refinement portion we have the empty module because no extra code is needed to abstract from the low to the high level specs. pjr is a reflection tactic that can solve goals involving ⊕ and ≤.

The tactic link_tac essentially repeats the steps seen in the manual proof as many times as necessary and uses the linking Hint database to figure out which code and refinement proofs to use.

ForallPrimitive allows us to state properties that hold for every primitive in a layer. We want to use it here to check that everything in the layer preserves its invariants. This can be solved automatically with typeclasses eauto (assuming of course that an instance of CPrimitivePreservesInvariant actually exists for each primitive. A little unfolding might be necessary to help the proof search recognize the structure of the layer.

Although we did not need to make use of the layer invariant in order to complete our simulation proofs, because we know that each of our primitives preserves the invariants, we can prove that the linking still holds when we require that the invariants of the under- and overlay are preserved.