Stack.v

*

A layer implementing a bounded stack using a bounded counter.

Compcert helper lib

Compcert types and semantics

CertiKOS layer library

This file is meant to continue demonstrating how the layer calculus used in CertiKOS works by implementing a new layer on top of an existing one. This layer consists of a global stack variable STACK that can be manipulated with push and pop primitives as well as have its size checked with get_size. The stack is implemented as an array where the index of the next open slot is tracked by the COUNTER variable. This guarantees that one cannot pop from an empty stack or push to a full one. The underlay upon which this layer is built is the counter_L defined in Counter.v. The overlay consists of the primitives described above, and an abstract state containing a stack of type list Z with the invariant that the length of the stack is not greater than MAX_COUNTER.

Abstract Data

We want our layer to abstract a stack of signed integers, so our abstract data will represent this as a list Z. We then provide the initial state and our invariant and wrap it in layerdata as before.

High Level Specifications

get_size returns the current number of items on the stack, which is just the length of the list in the abstract data.

push needs a value to add to the stack, so the spec reflects that by having an additional argument after stack_data. As usual we encode the potential failure by making the return type option stack_data and returning None in case of an error. N.B. The x argument must come before abs because while the type Zsign → stack_data → option stack_data is declared as an instance of SemOf, stack_data → Zsign → option stack_data is not. Also, Zsign is simply a wrapper type around Z in order to allow both signed and unsigned versions of Z → T to be instances of SemOf.

Module Implementation

f_get_size simply returns the current value of COUNTER because that always equals the number of items on the stack.

unsigned int get_size() {
  return get_counter();
}

These identifiers are used as function temporaries and parameters.

f_push queries the current index with get_counter, moves it ahead with incr_counter, and stores x into STACK at the index. It does not have to check whether the index is in range because incr_counter will already fail if it is not.

void push(int x) {
  unsigned int idx = get_counter();
  incr_counter();
  STACK[idx] = x;
}

int pop() {
  unsigned int idx = decr_counter();
  return STACK[idx];
}

Low Level Specifications

Because this layer is built on top of the counter layer, we can write the low level specs in terms of primitives from counter_L instead of dealing with the memory directly. This simplifies both the specification and the refinement proofs.

The STACK global variable is stored at some memory block sb

Because we have access to the counter layer abstract data, we can read the counter value using the get_counter high level spec instead of loading from memory

get_size takes no arguments, returns sz, and does not change memory or abstract state

The STACK global variable is stored at some memory block sb

We again use the high level spec of a counter layer primitive

We can also use the high level spec for incr_counter

Storing x at STACK[idx] returns some new memory m'

push takes one argument, returns nothing and changes both the memory and abstract state

TUTORIAL: Replace the False premises in pop_step_intro with correct premises

We will find out later in this file that the code proof of pop will make use of the invariants of the counter layer. This will require that we show that the low level specs preserve these invariants. More explanation later on.

TUTORIAL: Finish this proof that pop_step preserves its layer invariant

Code Proofs

We will need the function pointer for the following primitive later on. This tactic pulls it out of the layer and into the current context.

so (4 * _) not unfolded

get_counter return value

incr_counter return value

Storing into STACK

In order to prove that f_pop is correct with respect to its low spec, we need to know that the idx returned by get_counter is bounded above by Int.max_unsigned. In the proof of f_push this wasn't a problem because we use incr_counter which gives us the tighter upper bound of idx ≤ MAX_COUNTER, and we also know that 4 × MAX_COUNTER ≤ Int.max_unsigned. With f_pop however, we call decr_counter, which only gives us a lower bound of 0 ≤ idx. Fortunately, the invariant of the counter layer is that counter ≤ MAX_COUNTER. However, in order to use this fact, we have to strengthen our simulation diagram to reflect the fact that if the invariant holds in the initial states, it is preserved in the final state. This means we have to show that the semantics of the Clight function f_pop evaluated on counter_L preserves the invariants of counter_L. As it turns out, it is sufficient to show that all of the primitives in counter_L preserve the invariant due to the monotonicity of the semantics.

counter_L preserves invariants

simulation where invariant holds for the initial state

Layer Relation

We relate the overlay's abstract data and the underlay's concrete memory by requiring that for every item in the abstract stack, the same item can be found at the appropriate place in memory.

This time our relation between the high and low abstract data is not empty. We require that the size of the stack is equal to the value of the counter.

These lemmas about match_stack will be useful later to show that the relation still holds after pushing a new item to the stack. If two memories m1 and m2 have the same values at every offset below some idx, and the match_stack relation holds for stack s on m1 up to idx, then match_stack also holds for s on m2 up to idx.

If match_stack holds for stack s on m1 up to idx, and m2 is the result of storing x at idx in m1, then match_stack holds for x pushed onto s on m2 up to idx + 1.

Refinement Proofs

here again to prevent cbn expanding 4 * _

TUTORIAL: Try to prove this lemma. Something won't be quite right. Fix the lemma statement, then complete your proof.

Linking

TUTORIAL: State and prove the linking theorem for Stack

TUTORIAL: Uncomment this line once you've stated the linking theorem.

The final result we want to prove is that the behaviors allowed by the stack high level primitives are refined by the counter and stack C code evaluated on the base (empty) layer.

TUTORIAL: Change Admitted to Qed. If you've completed the exercises, it will probably just work.