Multiple Levels of Models and Refinement

When doing formal verification, the properties that we want to verify are sometimes very different from the actual implementation of the program. It happens in particular when working on data structures, with the specification being in terms of mathematical structures (sets, sequences…) and the implementations rather containing arrays and/or pointers. This challenge occurred when working on verifying the formal hashed sets library of the SPARKlib. In this post, I am going to explain how to make this kind of proof tractable by using several layers of abstraction to enforce separation of concerns.

As explained in a previous blog post, the bounded hashed sets provided in the SPARKlib are implemented using a linked structure inside an array. Verifying them requires handling different concerns that are more easily dealt with separately (the soundness of the linked structures, the separation of buckets, the unicity of the representative of each equivalence class…). To achieve this, I have introduced several abstraction layers and verified the structure by successive refinement proofs. Said like that, it might seem complicated, but I hope you will find that it is, in fact, rather straightforward. The specification and verification of each layer is similar to the verification of a program against its specification, except that the implementation of a layer is based on the specification of the previous layer. Here is an example of how it can be achieved:

package Lower_Layer is
  procedure P (...) with
    Post => <lower level post>;
end Lower_Layer;

package Higher_Layer is
  procedure P (...) with
    Post => <higher level post>;
end Higher_Layer;

with Lower_Layer;
package body Higher_Layer is
  procedure P (...) is
  begin
    Lower_Layer.P (...);
  end P;
end Higher_Layer;

We introduce a package per abstraction layer. In each package, we define the capabilities that we want to provide at the given layer. The functionalities of the higher layer are implemented by calling those of the lower level.

The fact that each layer is defined in a separate package, with only the body having visibility on the previous layer, enforces proper abstraction, that is to say, that the verification of a layer only depends on the specification of the previous layer and not on potential lower layers. This relies on the fact that the proof tool automatically hides information located in the body of a package from package users, as explained in a previous blog post. Here, for example, to prove the postcondition of Higher_Layer.P, we can only rely on the postcondition of Lower_Layer.P. The potential dependencies on lower layers, which are only visible in the implementation of Lower_Layer.P, are not visible.

This mechanism, generally called refinement proof, is only interesting if the layers are carefully designed so that each layer hides some complexity while retaining sufficient information to prove the upper layers. To exemplify this, let’s look at the proof of the hashed set library. It is made of four layers: the implementation, the top-level models used for the specification of the SPARKlib, and two additional intermediate layers that are here to simplify the proof. The implementation and the specification of the hashed sets library are described in a previous blog post. To recall, the implementation of a hashed set is made of two arrays: the first array, called Nodes, stores the element contained in the set. These elements are linked together in several singly linked lists using a special Next field in each node. The heads of the lists are stored in an array called Buckets, for the allocated nodes, and a free list for the others. Allocated nodes are stored in a given bucket depending on the return value of the hash function:

On the other hand, the specification of the SPARKlib is expressed in terms of three model functions that allow users to choose the level of granularity they need on a case-by-case basis. A ghost function called Model returns a functional set as a high-level view of the data structure. Then, to support iteration over the content of a set, we have two other models: the Elements function returns a sequence of elements representing their order in the container, and the Positions function returns a functional map that associates the valid cursors in a container with an integer representing their position in this sequence:

function Model (Container : Set) return M.Set;
        --  The high-level model of a set is a set of elements. Neither cursors
        --  nor order of elements are represented in this model. Elements are
        --  modeled up to equivalence.

      function Elements (Container : Set) return E.Sequence;
        --  The Elements sequence represents the underlying list structure of
        --  sets that is used for iteration. It stores the actual values of
        --  elements in the set. It does not model cursors.

      function Positions (Container : Set) return P.Map;
        --  The Positions map is used to model cursors. It only contains valid
        --  cursors and maps them to their position in the container.

To reduce the gap between these two representations, we have introduced two intermediate layers. The first one is used to hide the linked structures inside the array. It replaces the two arrays in the implementation by an array of sequences of indexes, for the buckets, and a map from (allocated) indexes to elements:

Because of this first layer of abstraction, inductive proofs over linked structures, that by essence require a lot of manual intervention as explained in a previous blog post, are confined to the lowest layer. The linked structure is no longer visible in upper layers.

The second intermediate layer gets rid of the buckets to only keep a single sequence of allocated indexes in the order of iteration. It is at this level that we prove the absence of duplicated values in the structure. It is more interesting to enforce this property at this layer, as it is independent from the linked structure but benefits from visibility on the buckets:

The handling of the equivalence relation and hash function is entirely done at this layer. The abstraction ensures that references to the hash function and the buckets are no longer visible in upper layers. Due to this organization of the proofs, the top-level contracts from the SPARKlib with the three models have been proved really quickly, in a few days, and nearly without any user input or guidance - except for refined contracts for model functions, linking them to the middle model.

As another example, I had already used the refinement approach to verify insertion in an ordered set implemented as a red-black tree a few years ago. Above the implementation in an array, I had a layer defining binary trees, then used inside search trees (ordered binary trees) and finally red-black trees (balanced search trees).

Without going into the details, I will give a few tips that may be of interest if you want to try your hand at refinement proof with SPARK. At each layer, the key properties used in the specification of the functionalities, like the models described above, for example, need to be declared in the package specification. However, as they are defined in terms of the lower layer’s properties, they are necessarily defined in the body. The easiest is generally to define them directly as expression functions. As an alternative, the refined postcondition can be used. As an example, the model function used for the second intermediate layer of the hashed set implementation is declared in the specification but completed as an expression function in the body of Data_Structures. Operations (see the full example in the testsuite):

  package Advanced_Model is

      --  High level model of a set:
      --    * An association from memory indexes to values,
      --    * A sequence of allocated memory indexes in the iteration order

      type Set_HL_Model is record
         Values            : Values_Type;
         Allocated_Indexes : Sequence;
      end record;

      --  Extracts the high-level model (values map and allocated-index
      --  sequence) from a set.
      function HL_Model (S : Set) return Set_HL_Model
      with
        Post =>
          (for all I of HL_Model'Result.Allocated_Indexes =>
             Has_Key (HL_Model'Result.Values, I));

   end Advanced_Model;

   package body Advanced_Model is

      function HL_Model (S : Set) return Set_HL_Model
      is ((Values            => LL_Model (S).Values,
           Allocated_Indexes => …));
       --  Definition in terms of the model from the lower layer

   end Advanced_Model;

At the simplest, all layers provide the same functionalities (like for Lower_Layer.P and Higher_Layer.P) and the implementation at upper layers consists of a single call to the same operation from the lower layer. In practice, it can make more sense to combine several functionalities of a lower layer into a single one at the higher level, particularly if additional invariants are enforced at this layer. You could, for example, provide simple insertion in a search tree, and then call it along with rotation primitives to rebalance the tree for red-black trees. Another reason to not provide the same primitives at all layers is to take advantage of sharing to reduce the number of refinement proofs needed at each layer. In this way, I have chosen to only provide a small number of functionalities in the lower layers of my hashed sets, and then to combine them at top-level. As an example, the only way to insert an element in a set in intermediate layers is through Conditional_Insert, that inserts an element if no equivalent element is already present in the tree and returns whether it was inserted and the position of the element after insertion. At top level, it is used to implement several other flavors of insertions that either fail if an equivalent element is present or replace it with the new value.

If the refinement is well designed, we may be proving properties at a given layer that are then hidden in upper layers as they are no longer a concern. This can lead to the apparition of invariants over global state or data types, that is, properties that always hold above a given layer. There are several ways to express such invariants. The easiest is through a ghost function that is called explicitly in the preconditions and postconditions of all the functionalities. Invariant functions of upper layers simply call the invariant functions of lower levels. It is what I have done for hashed sets. As an example, here is how the invariant function of the upper intermediate level is defined, LL_Invariant being the function of the lower intermediate level:

  --  High level invariant, there are no duplicated element in the set

      function No_Duplicated_Elements
        (B : Sequence; Values : Values_Type) return Boolean
      is (for all P1 in Interval'(1, Last (B)) =>
            (for all P2 in Interval'(1, Last (B)) =>
               (if P1 /= P2
                then
                  not Equivalent_Elements
                        (Get (Values, Get (B, P1)),
                         Get (Values, Get (B, P2))))))
      with Pre => (for all I of B => Has_Key (Values, I));

      function HL_No_Duplicated_Elements (S : Set) return Boolean
      is (No_Duplicated_Elements
            (HL_Model (S).Allocated_Indexes, HL_Model (S).Values))
      with Pre => LL_Invariant (S);

      function HL_Invariant (S : Set) return Boolean
      is (LL_Invariant (S) and then HL_No_Duplicated_Elements (S));

In general, the invariant function is declared in the package specification and then defined in its body like other property functions. As an alternative, if the invariant is on a data type and not on global data, then it is possible to directly use a type invariant instead. It requires redefining the data type in each layer as a private type. Its full view is generally a wrapper over the previous data type, though it can also add new fields, like I did in my implementation of red-black trees - the search trees have an additional array of values and the red-black trees of colors. It has the disadvantage of requiring the with clause for the lower layer to be supplied in the specification of the upper layer and not in its body, at least as a private with. It is then the responsibility of the developer to make sure that the definitions of their properties are kept in the body to enforce abstraction.  If some property over the data-structure is never broken even in the implementation of its functionalities, it might be possible to use a subtype predicate instead of or in addition to an invariant. If it is the case, it is in general easier.

Note that choosing to go for an invariant function in intermediate layers does not preclude turning them into an invariant at top-level - to avoid the residual calls to the invariant function in the top-level specification, for example. This is what I have done for hashed sets. It requires some manual handling to carry the proof of the invariant on the default value of the type from lower levels. Here is the full type definition I have used for sets. Note that it has a predicate for all the - simple - invariants that are never broken in the implementation:

 type Set
     (Capacity : Count_Type;
      Modulus  : Positive_Hash_Type)
   is record
      Length  : Count_Type := 0;
      Free    : Count_Type'Base := -1;
      Nodes   : Nodes_Type (1 .. Capacity);
      Buckets : Buckets_Type (1 .. Modulus) := (others => 0);
   end record
   with
     Predicate      =>
       Length in 0 .. Capacity
       and then
         (if Capacity = 0 then Free = -1 else Free in -Capacity .. Capacity)
       and then (for all B of Set.Buckets => B <= Capacity),
     Type_Invariant => Invariant (Set);

   --  Full structural invariant of the set representation; used in the
   --  type invariant.
   function Invariant (S : Set) return Boolean
   with Ghost;

   --  Predicate that holds when a set is initialized by default
   function Default_Init (S : Set) return Boolean
   is ((for all B of S.Buckets => B = 0)
       and S.Free = -1
       and S.Length = 0
       and (for all I in 1 .. S.Capacity => not S.Nodes (I).Has_Element));

In the definition of the invariant function, we call the invariant function of the lower layer, as usual, but we also use a lemma that proves that this invariant holds on objects initialized by default:

function Invariant (S : Set) return Boolean
   with
     Refined_Post =>
       Invariant'Result = Operations.Advanced_Model.HL_Invariant (S)
       and then (if Default_Init (S) then Invariant'Result)
   is
   begin
      Operations.Advanced_Model.Prove_Invariant_On_Default (S);
      return Operations.Advanced_Model.HL_Invariant (S);
   end Invariant;

Where the lemma Operations.Advanced_Model.Prove_Invariant_On_Default is defined as a functionality in the lower level as follows:

     --  Proves the high-level invariant holds on a default-initialized set
      procedure Prove_Invariant_On_Default (S : Set)
      with Ghost, Post => (if Default_Init (S) then HL_Invariant (S));

Conclusion

As demonstrated in this post, when the proof is complex, it can gain from being separated into simpler proofs by introducing increasingly abstract versions of the contracts. Refinement between the various layers can then be verified, like any SPARK program. As parting words, I would like to encourage you into taking a step back and to think about what it means for a program to be formally verified. Every user of SPARK already knows that there are several ways to prove a program, depending on the level of assurance we are aiming for. In this article, a notion of levels is defined for proof, that has been largely reused afterwards. They range from level silver, absence of runtime errors, to level platinum, full functional correctness.

What we are presenting here is orthogonal, as arguably, even the lower layers are already proved at level platinum - their contracts are enough to prove the upper layers after all. This means that there are different kinds of platinum, and all models are not necessarily equivalent. In general, it might be worth reflecting on the model that a library should provide to make the proof of the rest of the code easier. It might not be the one that makes the proof of the library itself easier. Food for thought for when you will be designing the contracts for your next program.

This post is the last of a series explaining how we applied proof on a relatively complex and interesting example, the hashed sets package of the SPARKlib. For reference, earlier posts in this series are:

• Formally Verified Hashed Sets in Ada SPARK
• Reasoning about Linked Structures in an Array
• Information Hiding and Context Management in SPARK

The intent of this series of posts was to give you more food for thought to chart your own proof journey. As with any topic in software engineering, there are many ways to approach proof. Our support engineers are always available to help you lay out your approach. Feel free to reach out if you would like to discuss how the topics here apply to your design.